/mermaid-to-proverif

name: mermaid-to-proverif
description: "Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif formal verification models (.pv files). Use when generating a ProVerif model, formally verifying a protocol, converting a Mermaid diagram to ProVerif, verifying protocol security properties (secrecy, authentication, forward secrecy), checking for replay attacks, or producing a .pv file from a sequence diagram."

Mermaid to ProVerif

Reads a Mermaid `sequenceDiagram` describing a cryptographic protocol and produces a ProVerif model (`.pv` file) that can be passed directly to the ProVerif verifier.

**Tools used:** Read, Write, Grep, Glob.

The typical input is the output of the `crypto-protocol-diagram` skill — a Mermaid `sequenceDiagram` annotated with cryptographic operations (`Sign`, `Verify`, `DH`, `HKDF`, `Enc`, `Dec`, etc.) and message arrows.

When to Use

• User asks to formally verify a cryptographic protocol described as a Mermaid sequenceDiagram
• User wants to generate a ProVerif model (.pv file) from a protocol diagram
• User wants to prove secrecy, authentication, or forward secrecy properties
• Input is the output of the `crypto-protocol-diagram` skill

When NOT to Use

• No Mermaid sequenceDiagram exists yet — use `crypto-protocol-diagram` first to generate one
• User wants to verify properties of non-cryptographic systems (state machines, access control)
• User wants to run ProVerif on an existing .pv file — just run `proverif model.pv` directly

Rationalizations to Reject

| Rationalization | Why It's Wrong | Required Action | |-----------------|----------------|-----------------| | "Reachability queries are just busywork" | If events aren't reachable, all other query results are meaningless | Always add reachability queries first as a sanity check | | "Public channels are fine for all messages" | Private channels for internal state prevent false attacks | Use private channels for intra-process state threading | | "I'll skip the forward secrecy test" | Ephemeral keys demand forward secrecy verification | Add the ForwardSecrecyTest process whenever the diagram shows ephemeral keys | | "Unused declarations are harmless" | ProVerif may report spurious results from orphan declarations | Clean up all unused types, functions, and events | | "The model compiles, so it's correct" | A compiling model can have dead receives, type mismatches, or impossible guards that make queries vacuously true | Validate reachability before trusting any security query | | "I don't need to check the example first" | The example defines the expected output quality bar | Study `examples/simple-handshake/` before working on unfamiliar protocols |

---

Workflow

ProVerif Model Progress:
- [ ] Step 1: Parse participants and channels
- [ ] Step 2: Inventory cryptographic operations
- [ ] Step 3: Declare types, functions, and equations
- [ ] Step 4: Identify and declare events
- [ ] Step 5: Formulate security queries
- [ ] Step 6: Write participant processes
- [ ] Step 7: Write main process and finalize
- [ ] Step 8: Verify and deliver

Step 1: Parse Participants and Channels

From the Mermaid diagram:

1. Extract every `participant` or `actor` declaration. Each becomes a ProVerif process. 2. Count message arrows (`->>`, `-->>`, `-x`, `--x`). Each distinct `A ->> B: label` creates a communication step on a channel. 3. Decide channel model:

• **Public channel** for any message sent over the network before a

secure channel is established (e.g., ClientHello, ephemeral keys, ciphertext to be decrypted by the peer).

• **Private channel** only for internal state threading within a single

party process (not for cross-party messages).

• Default: declare one shared public channel `c` for all cross-party

messages. Add per-flow channels only when two distinct parallel sessions must be independent.

free c: channel.

Step 2: Inventory Cryptographic Operations

Walk through every `Note over` annotation and message label. Build a list of all distinct operations used. Map each to a ProVerif declaration category:

| Mermaid annotation | ProVerif category | |--------------------|-------------------| | `keygen() → sk, pk` | New name (`new sk`), public key derived via function | | `DH(sk_A, pk_B)` | DH function or `exp` with group | | `Sign(sk, msg) → σ` | Signature function | | `Verify(pk, msg, σ)` | Equation or destructor | | `Enc(key, msg) → ct` | Symmetric or asymmetric encryption function | | `Dec(key, ct) → msg` | Destructor (equation) | | `HKDF(ikm, info) → k` | PRF/KDF function | | `HMAC(key, msg) → tag` | MAC function | | `H(msg) → digest` | Hash function | | `Commit(v, r) → C` | Commitment function | | `Open(C, v, r)` | Commitment equation |

Consult [references/crypto-to-proverif-mapping.md](references/crypto-to-proverif-mapping.md) for exact ProVerif syntax for each.

Step 3: Declare Types, Functions, and Equations

Build the cryptographic preamble in this order:

1. **Types** — declare custom types used to distinguish key material:

type key.
type pkey.   (* public key *)
type skey.   (* secret key *)
type nonce.

2. **Constants** — for fixed strings used as domain separators or labels:

const msg1_label: bitstring.
const msg2_label: bitstring.
const info_session_key: bitstring.

3. **Functions** — constructors and destructors. Destructors use inline `reduc` so that the process aborts on verification or decryption failure:

(* Asymmetric encryption *)
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring
    reduc forall m: bitstring, k: skey;
        adec(aenc(m, pk(k)), k) = m.
fun pk(skey): pkey.

(* Symmetric encryption / AEAD *)
fun aead_enc(bitstring, key): bitstring.
fun aead_dec(bitstring, key): bitstring
    reduc forall m: bitstring, k: key;
        aead_dec(aead_enc(m, k), k) = m.

(* Digital signatures — verify