Justifying Finite Resources for Adversaries in Automated Analysis 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 (1) perform
an unbounded number of encryptions (and other operations) while
fabricating messages, and (2) 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 these
protocols. They also provide a rigorous basis for automated
verification of authentication protocols. However, few such
bounds are known. This paper defines a language for
authentication protocols and establishes two bounds on the
resources needed to attack protocols expressible in that language:
an upper bound on the worst-case number of encryptions by the
adversary, and an exponential lower bound on the worst-case number
of concurrent runs of the protocol. The upper bound on
encryptions is relative to an upper bound on the number of runs;
on-going work on proving such a bound is briefly described.
BiBTeX
PDF
Scott Stoller's Home Page