A bound on attacks on authentication protocols

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 verication 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.