15th Annual Computer Security Applications Conference
December 6-10, 1999
Phoenix, Arizona

Using Checkable Types in Automatic Protocol Analysis

Stephen H. Brackin, brackin@arca.com
Arca Systems / Exodus Communications
303 E. Yates St.
Ithaca, NY 14850

Keywords: Cryptographic Protocols, Formal Methods, Automatic Analysis

The Automatic Authentication Protocol Analyzer, 2nd Version (AAPA2) is a fast, completely automatic tool for formally analyzing cryptographic protocols. It correctly identifies vulnerabilities or their absence in 43 of 51 protocols studied in the literature, and it finds 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 defining the AAPA2's Interface Specification Language, 2nd Version (ISL2), which expresses user assumptions about identifiably distinct plaintext types.