Searching for Shapes in Cryptographic Protocols

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. 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.

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Shaddin F. Doghmi, Joshua D. Guttman, F. Javier Thayer
• Keywords: Algorithms, Cryptographic Protocol, Cryptographic Protocol Shape, Initial Behavior, TACAS 2007