Abstract or Summary:
Protocol failure, which occurs when an active wiretapper can obtain confidential information or impersonate a legitimate user, without performing cryptanalysis, by blocking, replaying, or modifying messages, is a surprisingly difficult, and surprisingly common, problem. This paper describes how the Automatic Authentication Protocol Analyzer, 2nd Version (AAPA2), a fast and completely automatic tool for finding the vulnerabilities that give rise to protocol failure, reveals errors in assumptions about the authentication capabilities of two large commercial protocols.