Cryptographic Protocols

Publications

Dean Rosenzweig, Davor Runje: "The Cryptographic Abstract Machine", Abstract State Machines - Advances in Theory and Applications: 11th International Workshop, ASM 2004, volume 3065 of LNCS, Springer-Verlag.
[ PostScript, PDF ]
Full version with reasonably expanded proofs is also available:
[ PostScript, PDF ]

Dean Rosenzweig, Davor Runje and Neva Slani. Privacy, Abstract Encryption and Protocols: an ASM Model - Part I, Abstract State Machines - Advances in Theory and Applications: 10th International Workshop, ASM 2003, volume 2589 of LNCS, Springer-Verlag.
[ PostScript, PDF]

AsmL Models

Vocabulary and Assumptions. Declaration of functionality shared among same classes of cryptographic primitives is shared among all models in the sequel. It is modeled here with interfaces for classes representing objects and appropriate variables.
[ HTML, DOC ]

Abstract Cryptography. We provide an AsmL model of abstract cryptographic primitives, implementing above mentioned interfaces.
[ HTML, DOC ]

Message Patterns. The language of message pattern is universal wtr creation and analysis of abstract cryptographic messages by an AsmL program.
[ HTML, DOC ]

Protocol Roles. A protocol role is a sequence of mesage patterns sharing a common storage. Agents are factories of roles with equivalent initial storage.
[ HTML, DOC ]

The Cryptographic Abstract Machine (CrAM). The cryptographic abstract machine is a simple machine designed for analysis and creation of cryptographic messages.
[ HTML, DOC ]

Compiling Message Patterns to CrAM. Message patterns can be compiled to CrAM programs in a provably correct way.
[ HTML, DOC ]

Protocol Examples. We provide examples of Needham-Schroeder and Perrig-Song protocols.
[ HTML, DOC ]

prospec

http://prospec.sourceforge.net/ - Protocol Specification Tool.