Partial order semantics and operational semantics for strand spaces, via Rocq

Strand spaces are a special-purpose theory for security protocols, i.e. tiny distributed programs that use cryptography for authentication, confidentiality, and related goals. Strand spaces yield compact and understandable proofs that security protocols meet their goals—and counterexamples when they do not—as well as supporting an automated search tool that can compute the security goals a protocol satisfies. The strand space notion of execution, the bundle, is partially ordered, where the causal dependence of receptions on transmissions generates the ordering. In this paper, we examine how this partially ordered semantics relates to sequential, trace-oriented notions of execution. We provide a Structured Operational Semantics for protocols in strand spaces. We prove that every SOS history yields a bundle that respects its causal relations, and that—given a bundle—there is an ordering of its events that yields an SOS history. Our results are formalized in Rocq using the StrandsRocq framework.