Using Checkable Types in Automatic Protocol Analysis

The Automatic Authentication Protocol Analyzer, 2nd Version AAPA2 is a fast, completely automatic tool for formally analyzing cryptographic protocols. It correctly identi es vulnerabilities or their absence in 43 of 51 protocols studied in the literature, and it nds errors in previously asserted authentication properties of two large commercial protocols. This paper describes the AAPA2 and its modeling of type, equality, and inequality tests performed by protocol participants. This description includes de ning the AAPA2's Interface Speci cation Language, 2nd Version ISL2, which expresses user assumptions about identi ably distinct plaintext types.

• Type: Conference
• Year: 1999
• Where: ACSAC
• Authors: Stephen H. Brackin
• Keywords: ACSAC 1999, Automatic Authentication Protocol, Identi Es Vulnerabilities, Large Commercial Protocols, Security Privacy