Automatically detecting most vulnerabilities in cryptographic protocols

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 how the AAPA2 finds vulnerabilities in 13 of 16 vulnerable protocols, protocols for which the earlier Automatic Authentication Protocol Analyzer (AAPA) finds vulnerabilities in only 6 of these protocols.