# Fast, Automatic Checking of Security Protocols

**Authors**:
Darrell Kindred and
Jeannette M. Wing

Appears in the Second USENIX Workshop on Electronic Commerce,
November 1996, pp. 41-52.

The full text of this paper is available in postscript
and HTML formats.

## 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 [4, 6, 8].
For each we verified the
desired properties using specialized theory checkers; most checks
took less than two minutes, and all less than fifteen.