Implementing effective automatic cryptographic protocol analysis

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