Computer Science Department
School of Computer Science, Carnegie Mellon University
Theory Generation for Security Protocols
Darrell Scott Kindred
Security-sensitive protocols are widely used today, and the growing popularity of electronic commerce is leading to increasing reliance on them. Though simple in structure, these protocols are notoriously difficult to design properly. Since specifications of these protocols typically involve a small number of principals, keys, nonces, and messages, and since many properties of interest can be expressed in "little logics" such as the Burrows-Abadi-Needham (BAN) logic of authentication, this domain is amenable to theory generation.
Theory generation enables fast, automated analysis of these security protocols. Given the theory representation generated from a protocol specification, one can quickly test for specific desired properties, as well as directly manipulate the representation to perform other kinds of analysis, such as protocol comparison. This thesis describes applications of theory generation to more than a dozen security protocols using three existing logics of belief; these examples confirm, or in some cases expose flaws in earlier analyses.
This thesis introduces a new logic, RV, for security protocol analysis. While drawing on the BAN heritage, RV addresses a common criticism of BAN-like logics: that the idealization step can mask vulnerabilities present in the concrete protocol. By formalizing message interpretation, RV allows the verification of honesty and secrecy properties, in addition to the traditional belief properties. The final contribution of this thesis, the REVERE protocol analysis tool, has a theory generation core with plug-in modules for RV and other logics. Its performance is suitable for interactive use; verification times are under a minute for all examples.