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

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

📣 You can run StrandsRocq directly in your browser, without installing anything!

📄 If you wish, 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.20, Rocq 9.1.0, and the compatibility package coq-core that can be installed with opam install coq-core. The process requires about 20 seconds on a machine with an Apple M2 processor.

• Our paper explains the ideas and design principles behind StrandsRocq, and includes some examples;
• For a more hands-on introduction you may also want to consider our online tutorial;
• If you are interested in StrandsRocq's internals there's an AI-generated wiki (⚠️ May include errors! ⚠️)

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}
}

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

The project is structured as follows:

• Common this folder 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;
  • StrandTactics.v include the tactics that help in automating the proofs;
  • Bundles.v and BundleRelations.v include definitions and facts about bundles;
  • MinimalMPT.v generalization of concepts ideas from the paper about minimal elements of sets of terms;
  • RelMinimal.v small helper library with facts about minimal elements of sets
  • LogicalFacts.v subset of FSetLogicalFacs module from FSetDecide.v in the standard Rocq library.
• Instances this folder includes the part of the development that concretely instantiates various modules from the Commonfolder:
  • StrandList.v instantiates strands as pairs (nat * list sT). The first element serves as a strand identifies, the second represents the actual trace of the strand.
  • UTerms.v and Penetrator.v actual instances of Strand's terms and Dolev-Yao intruder, building on top of StrandsList;
  • UTermsTactics.v and UTermTacticsTests.v tactics (and corresponding test suite) for terms on Universes described within StrandsList;
  • DefaultInstances.v is a file with default implementation of the module types as used in the case studies.
• Examples includes our case studies:
  • simple_auth is the full development of Section III of the paper
  • nsl and ns_original correspond to the development of Needham-Schroeder and Needham-Schroeder-Lowe protocols;
  • kmp is for the key management policies case study.

Here we reconstruct the correspondence between the concepts presented in the paper and those mechanized here. Notice that the mechanization includes a lot of details that are omitted in the paper, hence we encourage the interested reader to inspect the proof with their favorite editor.