Darrell Kindred and Jeannette Wing

Carnegie Mellon University

#### Abstract

Protocols in electronic commerce and other security-sensitive
applications require careful reasoning to demonstrate their robustness
against attacks. Several logics have been developed for doing this
reasoning formally, but protocol designers usually do the proofs by
hand, a process which is time-consuming and error-prone.
We present a new approach, *theory checking*, to analyzing and
verifying properties of security protocols. In this approach we
generate the entire finite theory, *Th*, of a logic for reasoning
about a security protocol; determining whether it satisfies a
property, *phi*, is thus a simple membership test: *phi in
Th*. Our approach relies on (1) modeling a finite instance of a
protocol in the way that the security community naturally, though
informally, presents a security protocol, and (2) placing restrictions
on a logic's rules of inference to guarantee that our algorithm
terminates, generating a finite theory. A novel benefit to our
approach is that because of these restrictions we can provide an
automatic *theory-checker generator*. We applied our approach
and our theory-checker generator to three different logics for
reasoning about authentication and electronic commerce protocols: the
Burrows-Abadi-Needham logic of authentication, AUTLOG, and Kailar's
accountability logic.
For each we verified the desired properties using specialized theory
checkers; most checks took less than two minutes, and all less than
fifteen.

View the full text of this paper in
HTML and
POSTSCRIPT (155,102 Bytes) form.

To Become a USENIX Member, please see our
Membership Information.