Formal Support for Standardizing Protocols with State

June 2015
Topics: Cybersecurity, Data Encryption, Network Protocols, Computer Security
Joshua D. Guttman, The MITRE Corporation
Moses D. Liskov, The MITRE Corporation
Dr. John D. Ramsdell, The MITRE Corporation
Paul D. Rowe, The MITRE Corporation
Download PDF (214.18 KB)

Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions. We adapt one of these tools, cpsa, to provide automated support for reasoning about state. We use Ryan’s Envelope Protocol as an example to demonstrate how the message-passing reasoning can be integrated with state reasoning to yield interesting and powerful results.​


Publication Search