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
CMU-CS-00-107.ps
CMU-CS-00-107.pdf
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 This page maintained by reports@cs.cmu.edu
School of Computer Science homepage