Paper 2006/435
Searching for Shapes in Cryptographic Protocols (extended version)
Shaddin F. Doghmi, Joshua D. Guttman, and F. Javier Thayer
Abstract
We describe a method for enumerating all essentially different executions possible for a cryptographic protocol. We call them the shapes of the protocol. Naturally occurring protocols have only finitely many, indeed very few shapes. Authentication and secrecy properties are easy to determine from them, as are attacks and anomalies. CPSA, our Cryptographic Protocol Shape Analyzer, implements the method. 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.
Note: Improved exposition and corrected various errors.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Short version in TACAS 2007, LNCS 4424
- Keywords
- authentication protocolsDolev-Yao modelstrand spacesmechanized protocol analysis
- Contact author(s)
- guttman @ mitre org
- History
- 2007-02-02: revised
- 2006-11-21: received
- See all versions
- Short URL
- https://ia.cr/2006/435
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2006/435,
author = {Shaddin F. Doghmi and Joshua D. Guttman and F. Javier Thayer},
title = {Searching for Shapes in Cryptographic Protocols (extended version)},
howpublished = {Cryptology ePrint Archive, Paper 2006/435},
year = {2006},
note = {\url{https://eprint.iacr.org/2006/435}},
url = {https://eprint.iacr.org/2006/435}
}
