Check out the new USENIX Web site.

Home About USENIX Events Membership Publications Students
Second USENIX Workshop on Electronic Commerce

Fast, Automatic Checking of Security Protocols

Darrell Kindred and Jeannette Wing
Carnegie Mellon University


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.

?Need help? Use our Contacts page.

Last changed: 15 April 2002 aw
Conference Index