Title :
Using checkable types in automatic protocol analysis
Author :
Brackin, Stephen H.
Author_Institution :
Exodus Commun., Arca Syst., Ithaca, NY, USA
Abstract :
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. The 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
Keywords :
cryptography; message authentication; network analysers; protocols; type theory; AAPA2 Interface Specification Language; Automatic Authentication Protocol Analyzer; authentication properties; automatic protocol analysis; checkable types; completely automatic tool; cryptographic protocols; formal analysis; identifiably distinct plaintext types; inequality tests; large commercial protocols; protocol participants; user assumptions; vulnerabilities; Authentication; Communication system control; Contracts; Cryptographic protocols; Cryptography; Error correction; Laboratories; Performance evaluation; Public key; Testing;
Conference_Titel :
Computer Security Applications Conference, 1999. (ACSAC '99) Proceedings. 15th Annual
Conference_Location :
Phoenix, AZ
Print_ISBN :
0-7695-0346-2
DOI :
10.1109/CSAC.1999.816017
