A Bound on Attacks on Authentication Protocols
Abstract:
Authentication protocols are designed to work correctly in the presence
of an adversary that can prompt honest principals to engage in an
unbounded number of concurrent executions of the protocol. The amount
of local state used in a single execution of a typical authentication
protocol is bounded. This suggests that there is a bound on the number
of protocol executions that could be useful in attacks. Such bounds
clarify the nature of attacks on and provide a rigorous basis for
automated verification of authentication protocols. This paper
establishes such a bound for a large class of protocols, which contains
versions of some well-known authentication protocols, including the
Yahalom, Otway-Rees, and Needham-Schroeder-Lowe protocols.
BiBTeX
PDF
Scott Stoller's Home Page