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. Keywords: protocol analysis tools, stateful protocols, TPM, PKCS#11.
@article{arxiv.1509.07552,
title = {Formal Support for Standardizing Protocols with State},
author = {Joshua D. Guttman and Moses D. Liskov and John D. Ramsdell and Paul D. Rowe},
journal= {arXiv preprint arXiv:1509.07552},
year = {2018}
}