|
Second USENIX Workshop on Electronic Commerce
Fast, Automatic Checking of Security Protocols
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.
|
Need help? Use our Contacts page.
Conference Index