This repository brings together a set of examples for the formal analysis of cryptographic primitives and protocols. Our goal is to provide here a set of cryptographic problems, presented in pdf notes in a way accessible to both cryptographers or formal methods people, as well as a set of solutions for those problems, using distinct tools from the computer-aided cryptography domain.

If:

• you are a formal method curious cryptographer, you should be able to understand all the problems, and then use the multiple solutions to discover the multiple tools, what kind of guarantees we can obtain with them, see which tools is best suited for which kind of analysis, ...;
• if you are cryptography curious formal verification researcher, you should be able to get a feel for the kind of guarantees cryptographers expects, and the variety of techniques that are currently used to get them;
• if you are a tool developper, you can use this opportunity to showcase your tool and understand how it compares with others, on a set of clearly defined examples.

We consider three separates set of problems, focusing on

• symmetric primitives;
• asymmetric primitves;
• protocols.

The following sections provide the details for each of those sets. To contribute to the repository, see the Contributing section below.

The problem sets and possible modeling options are detailed in the pdf notes, which should be read first. Then it is possible to explore the solutions, summarized below. For people hoping to get familiar with cryptographic definitions and proofs of key-exchanges, a pen-and-paper solution is available here for problem 2 (the signed DH protocol) and 4 (the simplified NTOR).

The directory structure for problems is as follows: there are top-level directories for each problem. Within these problem directories, there are tool-named subdirectories that contain solutions for that problem with the named tool.

We encourage tool developers to -- in addition to the solution files -- provide additional repositories with more detailed versions of the solutions, partial solutions with corrections, or additional incremental tutorials and materials. The corresponding repositories are listed as:

• Tamarin: https://github.com/tamarin-prover/teaching

Model features:
 * attacker: active/passive    // whether the attacker is active or passive
 * sessions: n/∞ // whether there is a bounded (precise number n) or unbounded number (∞) of possible session
 * agents: n/∞ //  there is a bounded or unbounded number of agents
 * compromises: none/LTK/EK/EK+LTK
  // LTK means that there is only long term key compromise
  // EK means that there is only only ephemeral key compromise
  // EK+LTK enables both
 * Attacker class: computational/symbolic
 * Primitives: IND-CCA/UF-CMA/.../signature/signature with DEO/...
   // if approach is computational, this contains the list of assumptions
   // if it is symbolic, it contains the list of primitives with eventual advanced capabilities
 * Properties: Prop1, ..., ⚡Propi, ..., Propn
  // provide here the properties or class of attacks covered by the tool.
  // by default, giving a property means it is proved.
  // for tools that enable attack finding, a found attack on a property is given by prefixing the property with the  ⚡ emoji.


Analysis features:
  * difficulty ratings:	easy/medium/hard/possible/impossible (X), easy/medium/hard/possible/impossible (Y), ...
    // relative difficulty of the analysis (in case of WIP, this is of course an expected difficulty rating)
	// possible means that it is theoretically possible, but would require for the moment unreasonable effort
	// if relevant, several distinct ratings may be given, for example X might be a set of easy properties to prove
	// and Y a set of hard properties
  * status: ✅/WIP/❎
    // status of the solution, if the model and proofs are fully complete (✅), do not exist at all (❎), or is partially completed (WIP)

subfolder: basic-hash

subfolder: signedDH

subfolder: signedKEM

subfolder: signedDH+KEM

subfolder: ntor

spec: https://spec.torproject.org/proposals/216-ntor-handshake.html

subfolder: acme

• Case Study: Kyber
• Description: formosa-ML-KEM is a formalisation of security for a high-performance implementation of ML-KEM, connecting a machine-checked security proof in EasyCrypt with a verifiably-correct and verifiably speculative-constant-time implementation in Jasmin.

• Case Study: SPDM
• Description: SPDM is a protocol that aims to provide platform security, for example for communicating hardware components or cloud computing scenarios. The standard is under development by the DMTF consortium, and supported by major industry players including Broadcom, Cisco, Dell, Google, HP, IBM, Intel, and NVIDIA. Paper, Model

• Case Study: MLS (TreeKEM)
• Description: MLS is a secure group messaging protocol standardized at the IETF (RFC 9420). It includes a continuous group key agreement protocol, TreeKEM, where each session features an unbounded number of key derivations, unbounded number of public-key encryption, and a tree data-structure baked-in the protocol, making it difficult to analyze automatically. Paper, Model

Current primitive examples:

• Encrypt-Then-Mac is IND-CPA + INT-CTXT
• KEM+DEM is semantically secure as a PKE
• CCA KEM + CCA DEM is CCA secure as a PKE

Possible ideas:

• IND-CPA KEM from DH + ROM
• play around DDH/CDH/gapDH
• biKEM from dualPRF + two IND-CPA KEM

Basic primitives are OOS for symbolic tools.

All primitives models in Squirrel will have a weaker attacker model (only asymptotic security, limitation being lifted in WIP)

subfolder: EtM-IND-CPA+CTXT

subfolder: kemdem

We are open to outside contributions for the problems, which should follow a few guidelines:

• the protocol/construction and security models must be explained in terms that clearly relate them to the problem sets or other notes provided in the repository;
• the file contains the header defined above;
• the code is commented and executable;
• the "code quality" is up to par with existing proofs of the same tool;
• the README tables are updated.

If an example corresponds to a new tool, it should be an open source tool from the research community with at least one bibliographical reference specifying its formal guarantees.

Note that we highlight some models in the "how to start with the ladder" tutorials we are developing on the homepage of the project. While we do not for the moment welcome contributions for the tutorial we are developing ourselves, we will however be maintaining a list of additional and different tutorials.

This work was initiated by the HACS workshop. The main contributors for the design of the problems set are: Manuel Barbosa (primitives), Cas Cremers (protocols), François Dupressoir (primitives and protocols), Charlie Jacomme (protocols), Aurora Naska (protocols), Trevor Perrin (main coordinator), Mike Rosulek (primitives). Doreen Riepel and Paul Rösler contributed computational models and detailed proofs for two of the proposed protocols. We additionally thank the following for their valuable feedback: Karthikeyan Bhargavan, Jonathan Katz, Devon Tuma, Bas Spitters, and Théophile Wallez. Further authorship attributions can be found in specific solutions.