📣 September 2026 Release: the partial order semantics of the JLAMP paper, unique origination relative to a bundle, and a witness for every guarantee. See the release notes.

This repository contains a Rocq mechanization of strand spaces. It includes the full mechanization of the strand framework, new general results about strands, and case studies with a number of variants. StrandsRocq originally appeared in:

"Strands Rocq: Why is a Security Protocol Correct, Mechanically?" by Matteo Busi, Riccardo Focardi, and Flaminia Luccio (arXiv version)

and is extended in:

"Partial Order Semantics and Operational Semantics for Strand Spaces, via Rocq" by Matteo Busi, Riccardo Focardi, Joshua Guttman, and Flaminia Luccio (to appear in the Journal of Logical and Algebraic Methods in Programming, JLAMP)

with an inductive characterization of bundles, a CPSA-style protocol syntax embedded in Rocq, a structured operational semantics for protocol execution, and correspondence theorems proving that reachable thread pools and bundles carry exactly the same information.

The code that accompanies each paper is tagged: csf25 for the CSF 2025 paper and sep-2026-release for the JLAMP one, archived on Zenodo with DOI 10.5281/zenodo.22939512. The version first submitted to JLAMP is tagged partial-order-semantics. This README describes the current version, and Changes since the CSF 2025 paper lists where it departs from the first.

You can download StrandsRocq locally and use your favorite editor to check the proofs interactively. For a complete build of StrandsRocq, you can simply run:

$ dune clean
$ dune build

A successful build requires dune>=3.21 and Rocq 9.1.0. The process requires about 15 seconds on a machine with an Apple M4 Pro processor.

• Our CSF 2025 paper explains the ideas and design principles behind StrandsRocq, and includes some examples;
• The online documentation covers every module of the current version, without proofs, and links each identifier to its definition;
  • A good walkthrough is its page on SimpleAuth, the protocol of Section IV of the CSF 2025 paper, commented step by step;
• An online tutorial walks through the SimpleAuth protocol of the CSF 2025 paper in the browser, running the code of the csf25 version.

To generate HTML documentation, run the following script, which builds the project first and also needs python3:

$ bash scripts/generate-docs.sh

The generated pages are written to docs/coqdoc-noproofs/. Open docs/coqdoc-noproofs/index.html in a browser to browse them. The documentation covers all the modules in Common/, CPSA/, and Original/, rendered without proof bodies and with identifiers linked to their definitions. Maintainers publish it online with bash scripts/publish-docs.sh --push, which commits the pages to the gh-pages branch served by GitHub Pages.

If you plan citing our work, you can use the following bib entry:

@inproceedings{strandsrocq,
  author       = {Matteo Busi and
                  Riccardo Focardi and
                  Flaminia L. Luccio},
  title        = {Strands Rocq: Why is a Security Protocol Correct, Mechanically?},
  booktitle    = {38th {IEEE} Computer Security Foundations Symposium, {CSF} 2025, Santa
                  Cruz, CA, USA, June 16-20, 2025},
  pages        = {33--48},
  publisher    = {{IEEE}},
  year         = {2025},
  doi          = {10.1109/CSF64896.2025.00022}
}

We will add an entry for the JLAMP paper once it is published.

Thanks for your interest in contributing, you can get started here.

The project is structured as follows:

• Common/ contains the Rocq mechanization of the common abstract structures of strand spaces:

  • Strands.v is the entry point of the strands formalization, with all the basic definitions;
  • StrandsTacticsFunctor.v includes the tactics that help in automating the proofs (functor-based);
  • Universe.v and UniverseNat.v introduce a UniverseSig module type for the term universe with a concrete nat-indexed instantiation;
  • Bundles.v and BundleRelations.v include definitions and facts about bundles, using a bundle_type record with separate nodes, intra (strand-succession), and inter (communication) edge lists; Bundles.v also defines origination relative to a bundle (originates_at_most_once_in and uniquely_originates_in);
  • BundleInductive.v contains the inductive characterization of bundles (IndBundle) with five constructors (Empty, Send0, Send, Recv0, Recv), together with soundness (IndBundle_sound) and completeness (IndBundle_complete) theorems;
  • Enumerate.v develops finite enumerations compatible with a causal ordering;
  • BundleSizeInduction.v provides bundle-size and sink-removal induction principles;
  • DefaultInstanceFunctor.v and EmbeddedTraceStrandsFunctor.v are functors that assemble tactics, bundle definitions, and MPT into concrete instances;
  • SanityTactics.v contains the tactics that build witness bundles: well-formedness through IndBundle, membership in a role and in a strand space, origination, and uniqueness of strands;
  • MinimalMPT.v generalizes concepts from the paper about minimal elements of sets of terms;
  • RelMinimal.v is a small helper library with facts about minimal elements of sets;
  • LogicalFacts.v is a subset of FSetLogicalFacts from FSetDecide.v in the standard Rocq library.

• CPSA/ contains the CPSA-style protocol syntax and operational semantics (new in the JLAMP paper):

  • RoleSyntax.v defines an intrinsically sorted term language for CPSA messages (sorts: Name, Text, Data, Tag, Skey, Akey, Mesg) and role/protocol records with valuation-based instantiation into the concrete message algebra;
  • ChoiceRoles.v implements the desugaring of CPSA choice constructs into flat role lists with shared prefixes;
  • PenetratorProtocol.v defines the standard Dolev-Yao adversary as a CPSA protocol (atom, pair, sep, enc, dec, hash roles);
  • Semantics.v defines the reachable_pool operational semantics (P ⊨ T) with five rules (Base, SpawnSend, ExtendSend, SpawnRecv, ExtendRecv), and proves bundle_of_reachable (soundness) and reachable_of_wf_bundle (completeness);
  • ComputableSemantics.v refines the Prop-level semantics to Type, recording indexed communication witnesses to enable computation over derivations and bundle extraction;
  • LabelledSemantics.v defines a labeled transition system over thread pools where each label carries the destination node, the event, and the communication source;
  • EnumerationSemantics.v proves that every compatible enumeration of a well-formed protocol bundle is realized by a labelled execution;
  • ProtocolExamples.v contains worked examples: a simple initiator/responder, choice roles (yes-or-no protocol), and the Concurrent Yahalom protocol;
  • PaperExamples.v is a proof index collecting the Rocq developments referenced directly by the JLAMP paper;
  • examples/ contains the CPSA sources of the yes-or-no, Yahalom, and Concurrent Yahalom protocols, and the CPSA output for yes-or-no;
  • Instances/ concretely instantiates UTerms, Penetrator, UTermsTactics, and DefaultInstances for use in the CPSA development.

• Original/ contains the development of the CSF 2025 paper, with the changes described in Changes since the CSF 2025 paper:

  • Instances/ instantiates strands as pairs (nat, list sT) and provides UTerms.v, Penetrator.v, UTermsTactics.v, UTermTacticsTests.v, and DefaultInstances.v;
  • Examples/ includes the protocol case studies:
    • simple_auth/ is the full development of Section IV of the CSF 2025 paper;
    • nsl/ and ns_original/ cover the Needham-Schroeder-Lowe and original Needham-Schroeder protocols, and nsl/NSL_sanity.v holds the NSL witnesses;
    • kmp/ is the key management policies case study: KMP_policy_examples.v and KMP_policy_examples_improved.v exhibit policies and their closures, KMP_runs.v the witness bundles, and KMP_sanity.v and KMP_sanity_improved.v what the two closure definitions prove about them.

• scripts/ contains generate-docs.sh and publish-docs.sh, described above.

• docs/coqdoc-assets/ contains the style of the generated documentation.

Here we reconstruct the correspondence between the concepts presented in the papers and those mechanized here. The mechanization includes many details omitted from the papers; we encourage the interested reader to inspect the proofs with their favorite editor.

The tables refer to the current code; Changes since the CSF 2025 paper lists where it departs from the paper.

Every security guarantee in Original/Examples/ is now paired with witness bundles. Building them showed that two hypotheses could never hold, so the guarantees that assumed them were vacuously true; fixing them changed a few definitions.

In the CSF version, uniquely_originates t asked for a unique node originating t among all the nodes of the strand space. Strands such as (0, [⊕ t]) and (1, [⊕ t]) always exist there, so the hypothesis was false for every term. It is replaced by originates_at_most_once_in C t in Common/Bundles.v, which only constrains the nodes of the bundle C; uniquely_originates_in C t adds existence for the statements that need it. In KMP, freshness is a premise of the key creation role, and fresh_sound_for in Original/Examples/kmp/KMP_protocol.v states that it agrees with the bundle.

• The closure asked the reachability relation to be reflexive on every key type, which a finite list cannot be, so no policy had a closure. Reflexivity is now required only on the types that the policy mentions (policy_types in Original/Examples/kmp/KMP_policies.v), and the key creation role only creates keys of those types. KMP_policy_examples.v and KMP_policy_examples_improved.v exhibit closures, and a policy on which the two closure definitions differ.
• Encryption and decryption carry a key rather than a text, so that wrap-then-decrypt can be expressed.
• The usage rules no longer assume that the keys they are given are device keys, so that an attacker's key can be injected.

An honest run is a bundle that satisfies all the hypotheses of a guarantee at once, so the guarantee is not vacuous. A counterexample shows that a hypothesis is needed, or that a flawed protocol is indeed flawed. The tactics that build them are in Common/SanityTactics.v.

The witnesses also led to two corrections:

• the injective agreement of ns_original was Proposition 4.8 of the original strand spaces paper, with uniqueness on the initiator; it is now stated on the responder, as for NSL, and the original is kept as injective_agreement_orig;
• the NSL secrecy corollaries no longer carry a premise that their conclusion already implied.