Speaker:  Jeanette Wing
Affiliation:  Computer Science Department, Carnegie Mellon University
Date:  11/11/99 - Thursday
Time & Location:  4:15PM, 101 Phillips
Title:  Reasoning About Security Protocols

Security protocols 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. 

I will present a new approach, theory generation, for analyzing and verifying properties of authentication protocols. In this approach, we automatically generate a finite representation, Th, of the entire theory associated with a given security protocol; determining whether it satisfies a property, P, is thus a simple membership test: P in Th? We applied this approach to a classic set of authentication protocols for different well-known logics including the Burrows-Abadi-Needham logic of authentication, AUTLOG, and Kailar's accountability logic. We also invented a new RV logic that enables checks for honesty, secrecy, and feasibility properties, thus addressing some of the criticisms against the original BAN logic. Theory generation for each protocol we analyzed takes less than one minute.

Theory generation draws inspiration from, and complements, both theorem proving and model checking. This work was developed in detail by my former student, Darrell Kindred, a newly minted Ph.D.

I will conclude my talk with some general remarks about where the formal methods community should focus their energy if they want to make a difference in security.