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.

A cryptographic protocol is a short series of message exchanges, usually involving encryption, intended to establish secure communication over an insecure network. A protocol fails if an active wiretapper can obtain confidential information or impersonate a legitimate user, without performing cryptanalysis, by blocking, replaying, relabeling or otherwise modifying messages. Since the number of possible wiretapper-induced distortions of a protocol grows exponentially with the size of the protocol, most tools for detecting protocol failure require extended, expert user guidance. The Automatic Authentication Protocol Analyzer, 2nd Version (AAPA2), in contrast, automatically correctly identifies 88% of the protocols in an independently selected collection of protocols as failed or not failed, on a modest computer, in an average of only 2.6 minutes per protocol. This paper summarizes the AAPA2's results, sketches how it produces them and gives references providing more information.

The paper summarizes the results of Automatic Authentication Protocol Analyzer (AAPA) analyses of 52 protocols from A Survey of Authentication Protocol Literature: Version 1.0 by Clark and Jacob, a continually updated library of protocols analyzed in the protocol-failure literature. The AAPA found no problems in 27 that Clark and Jacob did not identify as having problems, but also found no problems in 16 that Clark and Jacob did identify as having problems, though the attacks on 8 of these would be prevented by type checks that the AAPA assumes are always made. It found problems in 6 that Clark and Jacob also identified as having problems, and found problems in 3 that Clark anal Jacob did not identify as having problems. The paper defines a semantics for the AAPA's specification language, defines valid inference and protocol failure with respect to this semantics, identifies reasons for each of the AAPA's "misses", and sketches ongoing work that should correct all, or all except one, of these "misses".

This paper describes a simple interface specification language (ISL) for cryptographic protocols and their desired properties, and an automatic authentication protocol analyzer (AAPA) that automatically either proves-using an extension of the Gong, Needham, Yahalom (1990) belief logic-that specified protocols have their desired properties, or identifies precisely where these proof attempts fail. The ISL and the AAPA make it easy for protocol designers to incorporate formal analysis into the protocol design process, where they clarify designs and reveals a large class of common errors. The ISL and the AAPA have already shown potential deficiencies in published protocols and been useful in designing new protocols.

The paper describes Convince, a tool being developed to facilitate the modeling and analysis of cryptographic protocols, particularly those supporting authentication. Convince uses a belief logic to facilitate the analysis and proof of desired properties of these protocols. Convince incorporates in its front-end a commercial computer aided software engineering tool, StP/OMT, so that an analyst can model a protocol using a combination of familiar graphical and textual notations. Convince uses a Higher Order Logic theorem prover with automated support, so as to minimize the need for specialized theorem proving knowledge. The paper describes how an analyst can use Convince to rapidly construct models of authentication protocols, and outlines a strategy for verifying their correctness. It discusses the integration of StP/OMT with the theorem proving component and practical analysis techniques based on experience acquired through analyzing several published protocols.

This paper describes a Higher Order Logic (HOL) theory formalizing an extended version of the Gong, Needham, Yahalom (GNY) belief logic, a theory used by software that automatically proves authentication properties of cryptographic protocols. The theory's extensions to the GNY logic include being able to specify protocol properties at intermediate stages and being able to specify protocols that use multiple encryption and hash operations, message authentication codes, computed values (e.g., hash codes) as keys, and key-exchange algorithms.