Searching for Shapes in Cryptographic Protocols
Abstract
A shape describes the behavior of the honest participants in some minimal protocol execution. These shapes are informative, because typically protocols have very few of them. Authentication and secrecy properties are easy to determine from the set of shapes, as are attacks, and other protocol characteristics. A skeleton gives partial information about some possible executions, and a homomorphism from one skeleton to another is an information-preserving map. We describe a procedure that searches through skeletons using homomorphisms. The search procedure has been implemented in a Cryptographic Protocol Shape Analyzer CPSA.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 22, 2006
- Accession Number
- AD1107091
Entities
People
- F. J. Thayer
- Joshua D. Guttman
- Shaddin F. Doghmi
Organizations
- MITRE Corporation