Searching for Shapes in Cryptographic Protocols

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 informationpreserving map. We describe a procedure that searches through skeletons using homomorphisms. The search procedure has been implemented in a Cryptographic Protocol Shape Analyzer (CPSA).