mermaid-to-proverif

What this skill does

# 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.

```proverif
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:

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

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

```proverif
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:

```proverif
(* 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 returns the message on success, aborts on failure *)
fun sign(bitstring, skey): bitstring.
fun verify(bitstring, bitstring, pkey): bitstring
    reduc forall m: bitstring, k: skey;
        verify(sign(m, k), m, pk(k)) = m.

(* KDF — first arg is key (from DH), second is bitstring (info/context) *)
fun hkdf(key, bitstring): key.

(* MAC *)
fun mac(bitstring, key): bitstring.

(* Hash *)
fun hash(bitstring): bitstring.

(* DH *)
fun dh(skey, pkey): key.
fun dhpk(skey): pkey.

(* Serialization — ProVerif is strongly typed: pkey cannot appear
 * where bitstring is expected. Use these to build signed payloads. *)
fun pkey2bs(pkey): bitstring.
fun concat(bitstring, bitstring): bitstring.
```

4. **Equations** — algebraic identities on constructors only (not on destructors,
   which already have their rewrite rules inline):

```proverif
equation forall sk_a: skey, sk_b: skey;
    dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a)).
```

Only declare what the diagram actually uses. Do not add functions for
operations not present.

### Step 4: Identify and Declare Events

Events mark security-relevant moments in the protocol execution. Extract them
by identifying:

- **Begin events** (`event beginRole(params)`): triggered immediately before a
  party sends a message that depends on a long-term identity commitment (e.g.,
  right before sending a signed message or a MAC'd message).
- **End events** (`event endRole(params)`): triggered immediately after a party
  successfully verifies the peer's identity (e.g., after `Verify(...)` or MAC
  check passes, session key confirmed).
- **Secrecy markers**: any key or nonce that should remain unknown to the
  attacker after the handshake.

```proverif
event beginI(pkey, pkey).     (* pk_I, pk_R — fired before sending the signed message *)
event endI(pkey, pkey, key).  (* pk_I, pk_R, session_key — fired after accepting *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).
```

Parameters should uniquely identify the session: the parties' public keys,
plus the session key or a transcript hash.

### Step 5: Formulate Security Queries

Write one query per security property. Choose from:

**Reachability (always add first — structural sanity check):**

Verify that the success events are actually reachable. If ProVerif reports any
of these as `false`, the model has a structural bug (dead receive, type mismatch,
impossible guard) and no other query result should be trusted. Once the m