A Reduction for Automated Verification of Authentication Protocols


Authentication protocols (including protocols that provide key establishment) are designed to work correctly in the presence of an adversary that can prompt honest principals to engage in an unbounded number of concurrent runs of the protocol. The amount of local state maintained by a single run of an authentication protocol is bounded. Intuitively, this suggests that there is a bound on the resources needed to attack the protocol. Such bounds clarify the nature of attacks on and provide a rigorous basis for automated verification of authentication protocols. However, few such bounds are known. This paper defines a domain-specific language for authentication protocols and establishes an upper bound on the resources needed to attack a large subset of the protocols expressible in that language, including versions of the Yahalom, Otway-Rees, and Needham-Schroeder public-key protocols.


This result was subsequently re-formulated in the strand space model, leading to a considerable simplification. That version is available here.

Scott Stoller's Home Page