Computer Science Department
School of Computer Science, Carnegie Mellon University


Combining Theory Generation and Model Checking for
Security Protocol Analysis

Nicholas J. Hopper, Sanjit A. Seshia, Jeannette M. Wing

January 2000

Keywords: Formal methods, security, authentication protocols, model checking, belief logics, theory generation, Brutus, Revere

This paper reviews two relatively new tools for automated formal analysis of security protocols. One applies the formal methods technique of model checking to the task of protocol anaylsis, while the other utilizes the method of theory generation, which borrows from both model checking and automated theorem proving. For purposes of comparison, the tools are both applied to a suite of sample protocols with known flaws, including the protocol used in an earlier study to provide a baseline. We then suggest a heuristic for combining the two approaches to provide a more complex analysis than either approach can provide alone.

23 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by