Formal Support for Standardizing Protocols with State

TL;DR

This paper extends existing protocol analysis tools to support reasoning about protocols that involve non-local, mutable state, demonstrated through the Envelope Protocol example.

Contribution

It adapts the { extcpsa} tool to automate reasoning about stateful cryptographic protocols, integrating message-passing with state reasoning.

Findings

Successfully integrated state reasoning into message-passing analysis.

Analyzed Ryan's Envelope Protocol to demonstrate the approach.

Produced powerful results in protocol verification with state.

Abstract

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.