Using checkable types in automatic protocol analysis

Author

Brackin, Stephen H.

Author_Institution

Exodus Commun., Arca Syst., Ithaca, NY, USA

fYear

1999

fDate

1999

Firstpage

99

Lastpage

108

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Applications Conference, 1999. (ACSAC '99) Proceedings. 15th Annual

Conference_Location

Phoenix, AZ

ISSN

1063-9527

Print_ISBN

0-7695-0346-2

Type

conf

DOI

10.1109/CSAC.1999.816017

Filename

816017