Theory generation for security protocols

Abstract

Abstract This thesis introduces theory generation, a new general-purpose technique forperforming automated verification. Theory generation draws inspiration from, and complements, both automated theorem proving and symbolic model checking, thetwo approaches that currently dominate mechanical reasoning. At the core of this approach is the notion of producing a finite representation of a theory--all thefacts derivable from a set of assumptions. An algorithm is presented for producing compact theory representations for an expressive class of simple logics. Security-sensitive protocols are widely used today, and the growing popularity ofelectronic commerce is leading to increasing reliance on them. Though simple in