Accession Number:

ADA465044

Title:

Using Temporal Logic to Specify and Verify Cryptographic Protocols (Progress Report)

Descriptive Note:

Progress rept.

Corporate Author:

HONG KONG UNIV OF SCIENCE AND TECHNOLOGY KOWLOON

Personal Author(s):

• Gray, III, James W.
• McLean, John

Report Date:

1995-01-01

Pagination or Media Count:

18.0

Abstract:

We use standard linear-time temporal logic to specify cryptographic protocols, model the system penetrator, and specify correctness requirements. The requirements are specified as standard safety properties, for which standard proof techniques apply. In particular, we are able to prove that the system penetrator cannot obtain a session key by any logical or algebraic techniques. We compare our work to Meadows method. We argue that using standard temporal logic provides greater flexibility and generality, firmer foundations, easier integration with other formal methods, and greater confidence in the verification results.

Descriptors:

• *CRYPTOGRAPHY
• REQUIREMENTS
• VERIFICATION
• REASONING
• SECURITY
• ALGEBRA
• LINEARITY
• SAFETY
• LOGIC
• HONG KONG

Subject Categories:

• Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE