A Reduction for Automated Verification of Authentication Protocols
Abstract:
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.
BiBTeX
PDF
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