In searching for shapes, CPSA starts with some initial behavior, and discovers what shapes are compatible with it. Normally, the initial behavior is the point of view of one participant. The analysis reveals what the other principals must have done, given this participant's view.
The search is complete, i.e. every shape can in fact be found in a finite number of steps. The steps in question are applications of two authentication tests, fundamental patterns for protocol analysis and heuristics for protocol design. We have formulated the authentication tests in a new, stronger form, and proved completeness for a search algorithm based on them.
Category / Keywords: cryptographic protocols / authentication protocols, Dolev-Yao model, strand spaces, mechanized protocol analysis Publication Info: Short version in TACAS 2007, LNCS 4424 Date: received 20 Nov 2006, last revised 2 Feb 2007 Contact author: guttman at mitre org Available formats: PDF | BibTeX Citation Note: Improved exposition and corrected various errors.
Version: 20070202:133207 (All versions of this report) Discussion forum: Show discussion | Start new discussion