Theory generation for security protocols

We introduce theory generation, a new general-purpose technique for performing automated verifi- cation. Theory generation draws inspiration from, and complements, both automated theorem proving and symbolic model checking, the two approaches that currently dominate mechanical reasoning. At the core of this approach is the notion of producing a finite representation of a theory—all the facts derivable from a set of assumptions. We present an algorithm for producing compact theory representations for an expressive class of simple logics. Security-sensitive protocols are widely used today, and the growing popularity of electronic com- merce is leading to increasing reliance on them. Though simple in structure, these protocols are notori- ously difficult to design properly. Since specifications of these protocols typically involve only 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, and 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 rep- resentation 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 paper describes applications of theory generation to more than a dozen security pro- tocols using four different logics of belief; these examples confirm, or in some cases expose fla ws in earlier analyses.