# mermaid-to-proverif

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.

- **Kind:** skill
- **Source:** https://github.com/trailofbits/skills
- **Page:** https://forefy.com/skills/88e8dd7f-b7c2-4283-a9bb-a8ec2e4312aa
- **API (JSON + files):** https://forefy.com/api/asr/88e8dd7f-b7c2-4283-a9bb-a8ec2e4312aa

---

## SKILL.md

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

```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 model
is validated, comment them out if they slow down the main property checks:

```proverif
(* Sanity: both endpoints must be reachable — comment out once validated. *)
(*
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
*)
```

**Secrecy** (key not derivable by attacker):

Declare a private free name and encrypt it under the session key. The attacker
knowing `private_I` is equivalent to breaking the session key:

```proverif
free private_I: bitstring [private].

(* In process, after deriving sk_session: *)
out(c, aead_enc(private_I, sk_session));

(* Query: *)
query attacker(private_I).
```

**Weak authentication** (if B accepted, A ran at some point with matching
params — does not prevent replay):

```proverif
query pk_i: pkey, pk_r: pkey, k: key;
    event(endR(pk_i, pk_r, k)) ==> event(beginI(pk_i, pk_r)).
```

**Injective authentication** (prevents replay — each B-accept corresponds to
a distinct A-run):

```proverif
query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endR(pk_i, pk_r, k)) ==>
    inj-event(beginI(pk_i, pk_r)).
```

**Forward secrecy**: add a `ForwardSecrecyTest` process to the main process
that leaks both long-term secret keys to the attacker, then check that a past
session key remains secret. Pair it with a `free fs_witness: key [private]`
declaration and `query attacker(fs_witness)`. See
[references/security-properties.md](references/security-properties.md) →
Forward Secrecy, and the worked example in
`examples/simple-handshake/sample-output.pv`.

Choose the strongest applicable query for each property. See
[references/security-properties.md](references/security-properties.md) for
the full decision tree.

### Step 6: Write Participant Processes

Write one `let` process per participant. Structure each process to mirror the
Mermaid diagram step-by-step, in order.

**Template for a two-party protocol:**

```proverif
let Initiator(sk_I: skey, pk_R: pkey) =
    (* Step: generate ephemeral key *)
    new ek_I: skey;
    let epk_I = dhpk(ek_I) in
    (* Step: sign and send msg1 — pkey2bs casts pkey to bitstring *)
    let sig_I = sign(concat(msg1_label, pkey2bs(epk_I)), sk_I) in
    event beginI(pk(sk_I), pk_R);
    out(c, (epk_I, sig_I));
    (* Step: receive msg2 *)
    in(c, (epk_R: pkey, sig_R: bitstring));
    (* Step: verify responder signature — destructor aborts on failure *)
    let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in
    let _ = verify(sig_R, concat(msg2_label, transcript), pk_R) in
    (* Step: derive session key *)
    let dh_val = dh(ek_I, epk_R) in
    let sk_session = hkdf(dh_val, concat(info_session_key, transcript)) in
    event endI(pk(sk_I), pk_R, sk_session);
    (* Secrecy witness: encrypt private_I under the session key.
     * Declared as: free private_I: bitstring [private].
     * The query attacker(private_I) checks the attacker cannot derive it. *)
    out(c, aead_enc(private_I, sk_session)).
```

**Rules for writing processes:**

- Each `A ->> B: msg_contents` in the diagram becomes:
  - `out(c, msg_contents)` in A's process
  - `in(c, x)` (with matching destructuring) in B's process
- Each `Note over A: op → result` becomes a `let result = op in` binding
- Each `Note over A: Verify(...)` becomes a `let _ = verify(...) in`
  binding (the destructor aborts on failure — no explicit else needed,
  modeling abort)
- Use `alt` blocks in the diagram as `if/then/else` in the process
- Long-term keys are process parameters; ephemeral values use `new`

**N-party or MPC protocols:** write one process per distinct role. For
threshold protocols, write a single role process and replicate it `!N` times
in the main process.

### Step 7: Write Main Process and Finalize

The main process:

1. Generates long-term keys with `new`
2. Publishes public keys to the attacker via `out(c, pk(sk))`
3. Runs participant processes in parallel under replication (`!`) to allow
   multiple sessions
4. Optionally leaks long-term keys for forward-secrecy analysis

```proverif
process
    new sk_I: skey; let pk_I = pk(sk_I) in out(c, pk_I);
    new sk_R: skey; let pk_R = pk(sk_R) in out(c, pk_R);
    (
        !Initiator(sk_I, pk_R)
      | !Responder(sk_R, pk_I)
    )
```

Place the full file in this order:

```
(* 1. Channel declarations (free c: channel. / free ch: channel [private].) *)
(* 2. noselect directives (if needed for termination) *)
(* 3. Type declarations *)
(* 4. Constants *)
(* 5. Function declarations *)
(* 6. Equations (algebraic identities on constructors only) *)
(* 7. Table declarations *)
(* 8. Events *)
(* 9. Queries *)
(* 10. Let processes *)
(* 11. Main process *)
```

### Step 8: Verify and Deliver

Before writing the file:

- [ ] Every participant in the diagram has a matching `let` process
- [ ] Every `out(c, ...)` has a matching `in(c, ...)` on the other side with
      compatible types
- [ ] Every function used in a process is declared in the preamble
- [ ] Every destructor uses inline `reduc` (not a separate `equation` block)
- [ ] Every event in a query is declared and triggered in a process
- [ ] Long-term public keys are output to channel `c` in the main process
      (attacker can see them — that is the Dolev-Yao model)
- [ ] No unused declarations (clean up anything added speculatively)
- [ ] If `table` declarations are present: every `insert T(...)` has a
      corresponding `get T(...)` with compatible column types and matching
      pattern constraints (`=key` vs bare name)
- [ ] If `noselect` is used: its tuple structure matches the actual message
      shapes sent on `c` (e.g., pairs → `mess(c, (x, y))`)
- [ ] If the Key Exposure Oracle pattern is used: `event key_exposed(sk_type)`
      is declared, the oracle `in(c, guess: sk_type); if pk(guess) = pk_new then
      event key_exposed(guess)` appears at the end of the process that holds the
      secret, and the query is `query x: sk_type; event(key_exposed(x))`

**Write the model to a `.pv` file.** Choose a filename from the protocol name,
e.g. `noise-xx-handshake.pv` or `x3dh-key-agreement.pv`.

After writing, print a brief summary:

```
Protocol:   <Name>
Output:     <filename>
Queries:    <list each query and what property it tests>
Assumptions: <list modeling decisions and simplifications>
```

---

## Decision Tree

```
├─ No Mermaid diagram provided?
│  └─ Ask the user: "Please provide the Mermaid sequenceDiagram,
│     or run the crypto-protocol-diagram skill first."
│
├─ Diagram uses DH (not just symmetric crypto)?
│  └─ Use dh/dhpk with commutativity equation
│     See references/crypto-to-proverif-mapping.md → DH section
│
├─ Diagram uses asymmetric signatures (Sign/Verify)?
│  └─ Use sign/verify with inline reduc (not equation)
│     verify returns the message on success; let _ = verify(...) in to abort on failure
│     Distinguish signing key (skey) from verification key (pkey)
│
├─ Diagram has an "alt" block (abort path)?
│  └─ Model as if/then only — the else branch aborts (process terminates)
│     Do NOT add out(c, error_message) unless the diagram shows it
│
├─ Protocol has N > 2 parties?
│  └─ Write one process per role, use ! for replication
│     Pass participant index as a parameter if roles differ by index only
│
├─ Forward secrecy requested?
│  └─ Add a ForwardSecrecy variant in the main process that leaks
│     long-term sk after session; add secrecy query for past session_key
│     See references/security-properties.md → Forward Secrecy
│
├─ Type-checker rejects the model?
│  └─ ProVerif is typed: check every function arg type matches declaration.
│     bitstring is the catch-all; key/pkey/skey/nonce are stricter.
│     Cast with explicit constructors when needed.
│
├─ Protocol has cross-process state coordination (e.g., one process must wait
│  for another to record acceptance before proceeding)?
│  └─ Use ProVerif tables (table/insert/get)
│     See references/proverif-syntax.md → Tables
│
├─ Verification does not terminate after several minutes?
│  └─ Add noselect directive matching the message tuple structure on c
│     See references/proverif-syntax.md → noselect
│
├─ Protocol generates a private-type key (type sk [private]) that is never
│  output directly but whose secrecy should be verified?
│  └─ Use the Key Exposure Oracle pattern instead of query attacker(sk)
│     See references/security-properties.md → Key Exposure Oracle
│
└─ Unsure which security properties to verify?
   └─ Default set: secrecy of session key + injective authentication
      (both directions). Add forward secrecy if diagram shows ephemeral keys.
```

---

## Example

`examples/simple-handshake/` contains a worked example:

- **`diagram.md`** — Mermaid sequenceDiagram for a two-party authenticated key
  exchange (X25519 DH + Ed25519 signing + HKDF)
- **`sample-output.pv`** — exact ProVerif model the skill should produce,
  with secrecy and injective authentication queries

Study this before working on an unfamiliar protocol.

---

## Supporting Documentation

- **[references/crypto-to-proverif-mapping.md](references/crypto-to-proverif-mapping.md)** —
  Mapping table from Mermaid cryptographic annotations to ProVerif function
  declarations, equations, and process patterns
- **[references/proverif-syntax.md](references/proverif-syntax.md)** —
  ProVerif language reference: types, functions, equations, processes, events,
  queries, and common pitfalls
- **[references/security-properties.md](references/security-properties.md)** —
  Decision guide for choosing the right queries: secrecy, authentication
  (weak vs injective), forward secrecy, unlinkability, and how to model them

## agents

```

```

## agents/openai.yaml

```yaml
interface:
  icon_small: "assets/trail-of-bits-mark.svg"
  icon_large: "assets/trail-of-bits-mark.svg"
  brand_color: "#D83A34"
```

## assets

```

```

## assets/trail-of-bits-mark.svg

```

```

## examples

```

```

## examples/simple-handshake

```

```

## examples/simple-handshake/diagram.md

# Simple Authenticated Key Exchange Sequence Diagram

```mermaid
sequenceDiagram
    participant I as Initiator
    participant R as Responder

    rect rgb(230, 240, 255)
        Note over I,R: Setup (out-of-band key registration)
        Note over I: keygen() → sk_I, pk_I
        Note over R: keygen() → sk_R, pk_R
    end

    rect rgb(230, 255, 230)
        Note over I,R: Handshake
        Note over I: keygen() → ek_I, epk_I
        Note over I: sig_I = Sign(sk_I, "msg1" || epk_I)
        I->>R: epk_I || sig_I
        Note over R: Verify(pk_I, "msg1" || epk_I, sig_I)
        Note over R: keygen() → ek_R, epk_R
        Note over R: transcript = epk_I || epk_R
        Note over R: sig_R = Sign(sk_R, "msg2" || transcript)
        Note over R: dh = DH(ek_R, epk_I)
        Note over R: sk_R = HKDF(dh || transcript, info="session-key-v1")
        R-->>I: epk_R || sig_R
        Note over I: Verify(pk_R, "msg2" || epk_I || epk_R, sig_R)
        Note over I: dh = DH(ek_I, epk_R)
        Note over I: sk_I = HKDF(dh || transcript, info="session-key-v1")
    end

    rect rgb(255, 240, 200)
        Note over I,R: Application Data
        I->>R: ChaCha20Poly1305(sk, nonce, plaintext)
    end

    alt signature verification failure
        R-->>I: abort(INVALID_SIGNATURE)
    end
```

## Protocol Summary

- **Parties:** Initiator (I), Responder (R)
- **Round complexity:** 2 messages (1 round-trip)
- **Key primitives:** X25519 (DH), Ed25519 (Sign/Verify), HKDF-SHA256, ChaCha20-Poly1305
- **Authentication:** Mutual — both parties sign their ephemeral key; both verify the peer's signature
- **Forward secrecy:** Yes — session key derived exclusively from ephemeral DH; long-term keys only used for authentication
- **Notable:** Long-term keys registered out-of-band; no PKI or certificate exchange in-protocol

## examples/simple-handshake/sample-output.pv

```

```

## references

```

```

## references/crypto-to-proverif-mapping.md

# Cryptographic Operation to ProVerif Mapping

Maps every Mermaid annotation produced by the `crypto-protocol-diagram` skill
to the corresponding ProVerif declarations and process patterns.

Use this table to build the preamble (types, functions, equations) and the
per-step process code for each participant.

---

## Key Generation

### Long-term asymmetric keypair

**Mermaid:** `Note over A: keygen() → sk_A, pk_A`

**Meaning:** Party A has a long-term signing or asymmetric encryption keypair.

**ProVerif:**
- Long-term keys are inputs to the participant process (not `new` inside).
- The secret key is a process parameter; the public key is derived.
- The main process generates the keypair and publishes the public key.

```proverif
(* Function declaration *)
fun pk(skey): pkey.

(* In main process *)
new sk_A: skey; let pk_A = pk(sk_A) in out(c, pk_A);

(* In participant process signature *)
let PartyA(sk_A: skey, pk_B: pkey) = ...
```

### Ephemeral keypair

**Mermaid:** `Note over A: keygen() → ek_A, epk_A`

**Meaning:** Party A generates a fresh single-use keypair for this session.

**ProVerif:**
- Generate with `new` inside the participant process.
- Derive the public ephemeral key from the secret ephemeral key.

```proverif
(* Function declaration *)
fun dhpk(skey): pkey.

(* In participant process *)
new ek_A: skey;
let epk_A = dhpk(ek_A) in
```

---

## Diffie-Hellman

### Two-party DH

**Mermaid:** `Note over A: dh = DH(ek_A, epk_B)`

**Meaning:** Party A computes the DH shared secret using their ephemeral
secret key and the peer's ephemeral public key.

**ProVerif:**

```proverif
(* Function declarations *)
fun dhpk(skey): pkey.
fun dh(skey, pkey): key.

(* Equation — DH commutativity *)
equation forall a: skey, b: skey;
    dh(a, dhpk(b)) = dh(b, dhpk(a)).

(* In process *)
let dh_val = dh(ek_A, epk_B) in
```

**Note:** ProVerif's equation engine handles the commutativity — you only
write `dh(ek_A, epk_B)` in A's process and `dh(ek_B, epk_A)` in B's process;
the equation unifies them.

### Static-ephemeral DH (e.g., for authentication)

**Mermaid:** `Note over A: dh_se = DH(sk_A, epk_B)`

Same declaration — `dh` accepts any `skey` regardless of whether it is
long-term or ephemeral. The typing is structural.

---

## Key Derivation (KDF / HKDF / PRF)

**Mermaid:** `Note over A: sk = HKDF(dh || transcript, info="...")`

**Meaning:** Party A derives a session key from keying material and
domain-separation info.

**ProVerif:**

```proverif
(* Function declaration *)
fun hkdf(key, bitstring): key.

(* Constants for domain separation labels *)
const info_session_key: bitstring.
const info_handshake: bitstring.

(* In process — concatenate IKM and call hkdf *)
let sk_session = hkdf(dh_val, concat(info_session_key, concat(pkey2bs(epk_A), pkey2bs(epk_B)))) in
```

**Tuple vs concatenation:** Use tuples `(a, b, c)` rather than a `concat`
function when the protocol only extracts keys from HKDF (not when it computes
a MAC over the same bytes). Tuples are simpler and keep the model readable.

If the protocol chains two HKDF calls (e.g., TLS 1.3's `HKDF-Extract` +
`HKDF-Expand`), model them as two separate function applications:

```proverif
let prk = hkdf_extract(salt, ikm) in
let okm = hkdf_expand(prk, info, length_tag) in
```

---

## Digital Signatures

### Signing

**Mermaid:** `Note over A: σ = Sign(sk_A, msg)`

**ProVerif:**

```proverif
(* Function declarations *)
fun sign(bitstring, skey): bitstring.
fun pk(skey): pkey.    (* verification key derived from signing key *)

(* In process *)
let sig = sign(msg, sk_A) in
```

### Verification

**Mermaid:** `Note over B: Verify(pk_A, msg, σ)`

**ProVerif:**

```proverif
(* Function declaration — returns the message on success, aborts on failure *)
fun verify(bitstring, bitstring, pkey): bitstring
    reduc forall m: bitstring, k: skey;
        verify(sign(m, k), m, pk(k)) = m.

(* In process — let _ = ... in aborts the branch if the signature is invalid *)
let _ = verify(sig, msg, pk_A) in
```

**Signing key vs verification key:** In ProVerif it is idiomatic to use a
single `skey` as the signing key and derive the verification key with `pk`.
Do not create a separate `vk` type unless the diagram explicitly uses
different keys for signing and verification (rare).

---

## Symmetric Encryption / AEAD

### Encryption

**Mermaid:** `Note over A: ct = Enc(key, plaintext)` or
`A ->> B: AEAD(sk, nonce, plaintext)`

**ProVerif:**

```proverif
(* Function declarations *)
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.

(* In process *)
let ct = aead_enc(plaintext, sk_session) in
out(c, ct);
```

### Decryption

**Mermaid:** `Note over B: plaintext = Dec(key, ct)`

```proverif
(* In process *)
in(c, ct: bitstring);
let plaintext = aead_dec(ct, sk_session) in
```

**AEAD vs unauthenticated encryption:** ProVerif does not distinguish AEAD
from unauthenticated encryption at the equational level — both use `aead_enc`/`aead_dec`.
Authentication is modeled implicitly: if decryption succeeds (the equation
fires), the ciphertext was produced with the correct key. This is a standard
simplification in symbolic models.

---

## Message Authentication Codes (MAC)

**Mermaid:** `Note over A: tag = MAC(key, msg)` /
`Note over B: VerifyMAC(key, msg, tag)`

**ProVerif:**

```proverif
(* Function declaration *)
fun mac(bitstring, key): bitstring.

(* Verification: check tag equals recomputed mac *)
if mac(msg, key) = received_tag then
```

**Note:** Unlike signatures, MACs do not have a dedicated verify function.
Verification is equality-checking the recomputed value. This means:
- Both parties must hold the key (symmetric — no public-key exposure).
- Do not output the MAC key to channel `c` in the main process.

---

## Asymmetric Encryption

**Mermaid:** `Note over A: ct = AEnc(pk_B, msg)` /
`Note over B: plaintext = ADec(sk_B, ct)`

**ProVerif:**

```proverif
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring
    reduc forall m: bitstring, k: skey;
        adec(aenc(m, pk(k)), k) = m.

(* Encrypt *)
let ct = aenc(msg, pk_B) in out(c, ct);

(* Decrypt *)
in(c, ct: bitstring);
let msg = adec(ct, sk_B) in
```

---

## Hash Functions

**Mermaid:** `Note over A: h = H(data)` or `h = SHA256(data)`

**ProVerif:**

```proverif
fun hash(bitstring): bitstring.

(* In process *)
let h = hash(data) in
```

Hash functions are modeled as free constructors — the attacker can compute
them on any input. This is the standard symbolic model (random oracle is not
needed for most authentication properties).

---

## Commitments

**Mermaid:** `Note over A: C = Commit(value, rand)` /
`Note over B: Open(C, value, rand)` or `Verify(C, value, rand)`

**ProVerif:**

```proverif
fun commit(bitstring, bitstring): bitstring.

(* Binding: equational model — no equation needed;
   opening is modeled by sending value and rand and letting
   the verifier recompute the commitment *)

(* Committer *)
new r: bitstring;
let com = commit(value, r) in
out(c, com);           (* send commitment *)
...
out(c, (value, r));    (* reveal *)

(* Verifier *)
in(c, (v: bitstring, r2: bitstring));
if commit(v, r2) = received_com then
```

**Hiding:** This symbolic model does not prove computational hiding. For
formal hiding proofs, use a computational tool (CryptoVerif, EasyCrypt).

---

## Nonces

**Mermaid:** `Note over A: nonce_A = random()` or `A ->> B: nonce_A`

**ProVerif:**

```proverif
new nonce_A: bitstring.   (* type can also be nonce *)
out(c, nonce_A);
```

Nonces are just fresh bitstrings. Use `type nonce.` if you want to prevent
accidental type confusion, but `bitstring` is fine for simple protocols.

---

## Message Concatenation and Transcripts

**Mermaid:** `transcript = epk_I || epk_R` or `msg = A || B || C`

**ProVerif approach:**

Prefer **tuples** over a concat function:

```proverif
(* Send: pack into tuple *)
out(c, (epk_I, epk_R));

(* Receive: destructure tuple *)
in(c, (epk_I: pkey, epk_R: pkey));
```

Use a `concat` function only when the protocol computes over the raw
concatenated bytes in a way that matters (e.g., the transcript is fed to a
MAC or HKDF as a single blob, and the parts are also available separately).
In that case:

```proverif
fun concat2(bitstring, bitstring): bitstring.
fun concat3(bitstring, bitstring, bitstring): bitstring.
```

There are no equations on `concat` — it is a free constructor, which is
correct: the attacker cannot split a concatenation unless they know the
length boundaries (length-prefix models are usually out of scope for symbolic
proofs).

---

## Key Agreement Summary Table

| Mermaid annotation | ProVerif function | Equation needed? |
|-------------------|-------------------|------------------|
| `keygen() → sk, pk` | `pk(skey): pkey` | No |
| `keygen() → ek, epk` | `dhpk(skey): pkey` | No |
| `DH(ek, epk)` | `dh(skey, pkey): key` | Yes — commutativity |
| `HKDF(ikm, info)` | `hkdf(key, bitstring): key` | No |
| `Sign(sk, msg)` | `sign(bitstring, skey): bitstring` | No |
| `Verify(pk, msg, σ)` | `verify(bitstring, bitstring, pkey): bitstring` | Yes — inline `reduc` |
| `Enc(k, m)` / `Dec(k, ct)` | `aead_enc` / `aead_dec` | Yes — correctness |
| `AEnc(pk, m)` / `ADec(sk, ct)` | `aenc` / `adec` | Yes — correctness |
| `MAC(k, m)` | `mac(bitstring, key): bitstring` | No |
| `H(data)` | `hash(bitstring): bitstring` | No |
| `Commit(v, r)` | `commit(bitstring, bitstring): bitstring` | No |
| `nonce = random()` | `new nonce: bitstring` | No |

---

## Modeling Notes

### What the symbolic model captures

- Perfect correctness of cryptographic functions (equations hold exactly)
- Dolev-Yao attacker: controls the network, can read/write all public channel
  messages, knows all published public keys
- Unbounded sessions via replication `!`

### What the symbolic model does NOT capture

- Computational hardness (e.g., discrete log, AES key recovery)
- Timing side-channels
- Nonce/IV reuse in AEAD (model assumes nonces are always fresh)
- Key material leakage through implementation bugs
- Computational binding/hiding of commitment schemes

For these properties, use CryptoVerif (computational) or EasyCrypt (proofs).

## references/proverif-syntax.md

# ProVerif Syntax Reference

ProVerif models cryptographic protocols in the applied pi-calculus. This
reference covers the constructs needed to translate a Mermaid sequence diagram
into a verifiable `.pv` file.

---

## File Structure

A `.pv` file must follow this order:

```
1. Channel declarations (free c: channel. / free ch: channel [private].)
2. noselect directives (if needed for termination)
3. Type declarations
4. Constants
5. Function declarations
6. Equations / Reduction rules
7. Table declarations
8. Event declarations
9. Query declarations
10. Let process definitions
11. Main process (process ...)
```

Comments: `(* this is a comment *)` — no inline `//`.

---

## Types

ProVerif is strongly typed. The base type for any untyped byte sequence is
`bitstring`. Declare custom types to prevent confusing distinct key roles:

```proverif
type key.       (* symmetric key *)
type pkey.      (* public key (for enc or verify) *)
type skey.      (* secret key (for dec or sign) *)
type nonce.     (* random nonce *)
type tag.       (* MAC tag or signature *)
```

Types are structural — ProVerif does not enforce physical separation, but
type mismatches cause type errors that prevent verification.

---

## Constants

Declare fixed domain-separation labels or protocol identifiers:

```proverif
const msg1: bitstring.
const msg2: bitstring.
const info_session: bitstring.
const info_handshake: bitstring.
const info_app: bitstring.
```

---

## Functions

### Declaring Functions

```proverif
fun name(arg_type1, arg_type2, ...): return_type.
```

Functions are **constructors** by default — the attacker can apply them freely.

```proverif
fun pk(skey): pkey.          (* derive public key *)
fun sign(bitstring, skey): bitstring.
fun aenc(bitstring, pkey): bitstring.
fun aead_enc(bitstring, key): bitstring.
fun mac(bitstring, key): bitstring.
fun hash(bitstring): bitstring.
fun hkdf(key, bitstring): key.
fun pkey2bs(pkey): bitstring.    (* cast pkey to bitstring *)
fun concat2(bitstring, bitstring): bitstring.
fun concat3(bitstring, bitstring, bitstring): bitstring.
```

For DH:

```proverif
fun dhpk(skey): pkey.           (* g^x given x *)
fun dh(skey, pkey): key.        (* g^(xy) given x and g^y *)
```

### Destructors

Destructors **can fail** — they extract values only when the rewrite rule
matches. Declare them with an inline `reduc` block:

```proverif
fun adec(bitstring, skey): bitstring
    reduc forall m: bitstring, k: skey;
        adec(aenc(m, pk(k)), k) = m.

fun aead_dec(bitstring, key): bitstring
    reduc forall m: bitstring, k: key;
        aead_dec(aead_enc(m, k), k) = m.

fun verify(bitstring, bitstring, pkey): bitstring
    reduc forall m: bitstring, k: skey;
        verify(sign(m, k), m, pk(k)) = m.
```

`verify` returns the verified message on success; the process **aborts** (that
branch is pruned) on failure. Use it as an abort-on-failure guard:

```proverif
let _ = verify(sig_R, msg, pk_R) in
(* reaches here only if sig_R is a valid signature under pk_R *)
```

**`equation` vs `reduc` — critical distinction:**

- A standalone `equation` block applies to **constructors** — functions
  declared with `fun` that the attacker can apply freely. Adding an equation
  does not make the function fail on mismatch; it only enables rewriting.
- An inline `reduc` block declares the function as a **destructor** that
  fails when no rewrite rule matches. This is what you want for `verify`,
  `adec`, `sdec`, and any check that must abort the process on failure.

Use `equation` only for algebraic identities on constructors (e.g., DH
commutativity). Use `reduc` for all cryptographic verification and decryption.

```proverif
(* Constructor + algebraic identity — equation is correct here *)
fun dh(skey, pkey): key.
equation forall a: skey, b: skey;
    dh(a, dhpk(b)) = dh(b, dhpk(a)).
```

**Note:** `bool` is not a valid return type for `fun` declarations in ProVerif.
Use `bitstring` (and return the message on success) or a custom type.

---

## Channels

All cross-party communication happens on channels:

```proverif
free c: channel.                    (* public channel — attacker can read and write *)
free priv_c: channel [private].     (* private channel — only declared code can use *)
```

The `free name: channel.` form declares `name` as a globally accessible
channel name. The `[private]` attribute prevents the attacker from learning
or using the channel.

For most protocol models, one public channel `c` is sufficient.

---

## Events

Events mark security-relevant points for use in authentication queries.

**Declaration:**

```proverif
event beginI(pkey, pkey).          (* pk_I, pk_R — before session key is known *)
event endI(pkey, pkey, key).       (* pk_I, pk_R, session_key *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).
```

**Use in process:**

```proverif
event beginI(pk(sk_I), pk_R);           (* fired before sending authenticated msg *)
event endI(pk(sk_I), pk_R, sk_session); (* fired after deriving session key *)
```

---

## Queries

### Secrecy

```proverif
query attacker(session_key).
```

Succeeds (i.e., ProVerif proves the protocol secure) if the attacker cannot
derive `session_key` in any execution.

For named secrets inside a process, use `query secret session_key.` inside the
process — but `query attacker(x)` at top level is cleaner for most use cases.

### Authentication (Correspondence)

**Weak**: A ran ==> B ran (allows replay):

```proverif
query x: pkey, y: pkey, k: key;
    event(endR(x, y, k)) ==> event(beginI(x, y)).
```

**Injective**: each B-accept corresponds to a unique A-run (prevents replay):

```proverif
query x: pkey, y: pkey, k: key;
    inj-event(endR(x, y, k)) ==> inj-event(beginI(x, y)).
```

### Reachability (sanity check)

Verify that the "success" point of the protocol is actually reachable (rules out
vacuously true results from trivially blocked processes):

```proverif
query x: pkey, y: pkey, k: key; event(endR(x, y, k)).
```

If this query returns `false` (unreachable), the protocol model is broken —
the endpoint never executes. Note: ProVerif does not support `_` wildcards in
`query` declarations; all parameters must be bound to typed variables.

---

## Processes

### Basic Syntax

```proverif
let ProcessName(param1: type1, param2: type2) =
    (* body *).
```

### Core Constructs

| Construct | Meaning |
|-----------|---------|
| `new x: T` | Generate fresh random value of type T |
| `out(c, term)` | Send term on channel c |
| `in(c, x: T)` | Receive a term of type T from channel c |
| `in(c, (x: T, y: U))` | Receive and destructure a tuple |
| `let x = term in P` | Bind term to x, continue with P |
| `let (x, y) = term in P` | Destructure tuple |
| `if t = u then P else Q` | Conditional |
| `if f(t) = true then P` | Destructor check |
| `event e(args)` | Trigger event |
| `P \| Q` | Parallel composition |
| `!P` | Replicate P (unbounded concurrent sessions) |
| `0` | Terminated process |

### Receiving and Destructuring

When a message contains multiple components separated by a comma in the
Mermaid diagram, receive as a tuple:

```proverif
in(c, (epk_R: pkey, sig_R: bitstring));
```

For concatenated values (e.g., `A || B`), model as a tuple `(a, b)` unless the
protocol computes over the concatenated bytes specifically:

```proverif
(* sender *)
out(c, (epk_R_bytes, sig_R));

(* receiver *)
in(c, (epk_R_bytes: pkey, sig_R: bitstring));
```

If the protocol requires an explicit concat (e.g., hashing a concatenation),
declare a constructor:

```proverif
fun concat(bitstring, bitstring): bitstring.
out(c, concat(epk_R_bytes, sig_R));
```

### Verification Checks

Map each `Verify(pk, msg, sig)` annotation to a `let _ = ... in` destructor
call. The destructor fails and aborts the branch when the signature is invalid:

```proverif
let _ = verify(sig_R, concat2(msg2, concat2(pkey2bs(epk_I), pkey2bs(epk_R))), pk_R) in
(* reaches here only if sig_R is a valid signature under pk_R *)
(* else: branch is pruned — models abort on invalid signature *)
```

The `else` branch is implicit; ProVerif prunes the branch on destructor failure.

### Example: Two-Party Process

```proverif
let Initiator(sk_I: skey, pk_R: pkey) =
    new ek_I: skey;
    let epk_I = dhpk(ek_I) in
    let sig_I = sign(concat2(msg1, pkey2bs(epk_I)), sk_I) in
    event beginI(pk(sk_I), pk_R);    (* session key not yet known *)
    out(c, (epk_I, sig_I));

    in(c, (epk_R: pkey, sig_R: bitstring));
    let transcript = concat2(pkey2bs(epk_I), pkey2bs(epk_R)) in
    let _ = verify(sig_R, concat2(msg2, transcript), pk_R) in
    let dh_val = dh(ek_I, epk_R) in
    let sk_session = hkdf(dh_val, concat2(info_session, transcript)) in
    event endI(pk(sk_I), pk_R, sk_session).
```

---

## Main Process

```proverif
process
    new sk_I: skey; let pk_I = pk(sk_I) in out(c, pk_I);
    new sk_R: skey; let pk_R = pk(sk_R) in out(c, pk_R);
    (
        !Initiator(sk_I, pk_R)
      | !Responder(sk_R, pk_I)
    )
```

**Replication `!`** allows arbitrarily many concurrent sessions — essential
for ProVerif to detect replay and man-in-the-middle attacks.

**Long-term key publication** (`out(c, pk_I)`) is mandatory: the Dolev-Yao
attacker must know public keys to attempt attacks.

---

## Tables

ProVerif tables provide shared mutable state across parallel processes — the
only built-in mechanism for synchronizing information between two `let`
processes that run concurrently.

### Declaration

```proverif
table myTable(bitstring, bitstring).   (* two bitstring columns *)
table accepted(bitstring, bitstring).  (* e.g. (session_id, sas) *)
table sessionKeys(bitstring, key).     (* (nonce, derived_key) *)
```

### Insert a row

```proverif
insert myTable(key1, value1);
```

### Read a row

```proverif
get myTable(=key1, x: bitstring) in
    (* x is bound to value1 when the first column equals key1 *)
    ...
```

`=key1` is a pattern-match constraint (first column must equal `key1`).
Bare names like `x: bitstring` capture the column value for use in the body.

**Semantics:** `get T(...) in P` succeeds for every matching row. If no row
matches, the process terminates (that branch is pruned). If multiple rows
match, ProVerif considers all branches.

### When to use tables

| Use tables | Use private channels |
|------------|----------------------|
| Reader determines the lookup key | Writer pushes to a known recipient |
| Fan-in: wait for multiple writers | Point-to-point signal |
| Cross-check: two processes verify agreement on a value | Callback: one-shot reply |

**Typical pattern — coordination between parallel processes:**

```proverif
table accepted(bitstring, bitstring).    (* (nonce, sas) *)

(* Party A: records user acceptance *)
insert accepted(nonce_new, sas);

(* Party B: checks that A recorded acceptance before proceeding *)
get accepted(=nonce_new, =sas) in
    event partyB_accept(...);
    ...
```

---

## `noselect` — Termination Hints

ProVerif's Horn clause solver may not terminate on models with complex tuple
patterns on the public channel. The `noselect` directive restricts which
clauses the solver selects during proof search. It is a **performance hint
only** — it does not restrict what the attacker can send or receive.

### Syntax

```proverif
noselect x: bitstring, y: bitstring; mess(c, (x, y)).
```

This tells ProVerif: "do not select clauses that derive a pair `(x, y)` from
channel `c`." The `mess(c, t)` predicate means "term `t` is on channel `c`."

### When to add

If ProVerif runs for several minutes without terminating on a model with:
- Many concurrent sessions (`!` replication on multiple processes)
- Pair-typed messages on the public channel (tuples sent over `c`)

Then add a `noselect` hint matching the tuple structure of messages on `c`.
For a protocol where all messages are pairs, use:

```proverif
noselect x: bitstring, y: bitstring; mess(c, (x, y)).
```

For triple-element messages:

```proverif
noselect x: bitstring, y: bitstring, z: bitstring; mess(c, (x, y, z)).
```

### Placement

Add immediately after channel declarations, before type and function
declarations. `noselect` is parsed as a query-level directive and must appear
before the `process` block. Placing it early (after channels) keeps it
visible alongside the declarations it constrains.

---

## Common Pitfalls

### Pitfall 1: Type Mismatch

`dh(ek_I, epk_R)` requires `ek_I: skey` and `epk_R: pkey`. If you declared
both as `bitstring`, the equation `dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a))`
cannot fire. Keep types strict.

### Pitfall 2: Missing Replication

Without `!` in the main process, ProVerif only checks single-session security.
Always use `!Initiator(...)` and `!Responder(...)` to allow multiple sessions.

### Pitfall 3: Attacker Cannot Reach End Event

If the reachability query `query event(endR(...))` returns false, the protocol
process is stuck — usually due to a type error in `in(c, ...)` destructuring
or an `if` condition that never holds. Debug by simplifying the process to just
the `out`/`in` steps without guards, confirm reachability, then add guards
back one at a time.

### Pitfall 4: Equations Cause Non-Termination

The DH commutativity equation `dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a))`
is convergent. Arbitrary equations with cycles (e.g., `f(f(x)) = x`) can
cause ProVerif to loop. Stick to the standard primitives in the mapping table.

### Pitfall 5: Secrets Must Be `new` Inside Process

Do not use `new` in the main process for values that should be per-session
secrets — they would be shared across all replications. Generate per-session
secrets inside the participant `let` process.

```proverif
(* WRONG — shared across all sessions *)
new sk_session: key;
!Initiator(sk_session, ...)

(* RIGHT — fresh per session *)
let Initiator(...) =
    ...
    let sk_session = hkdf(...) in   (* derived, not new *)
    ...
```

### Pitfall 6: Queries Reference Undeclared Events

Every event name used in a `query` must be declared with `event name(types).`.
Missing declarations cause a parse error.

## references/security-properties.md

# Security Properties in ProVerif

A guide to choosing and expressing the right security queries for a given
Mermaid sequence diagram.

---

## Decision Tree: Which Queries to Include

```
Start here for every protocol
│
├─ Does the protocol establish a shared key?
│  └─ YES → Add secrecy query for that key
│
├─ Does a party verify the peer's identity (Verify/MAC check)?
│  └─ YES → Add authentication queries (both directions if mutual auth)
│     ├─ Does the verification cover a fresh session value (nonce, epk)?
│     │  └─ YES → Use injective authentication (prevents replay)
│     └─ NO (only verifies static identity, no freshness) → Use weak auth
│
├─ Does the protocol use ephemeral keys (keygen inside the session)?
│  └─ YES → Add forward secrecy query (compromise long-term key after session)
│
├─ Does the protocol have a "challenge-response" nonce exchange?
│  └─ YES → Add injective authentication to capture that freshness
│
└─ Always add: reachability sanity check query
```

---

## 1. Secrecy

### Goal

The session key (or any sensitive value) is not learnable by the attacker,
even after observing all network traffic.

### When to add

Add whenever the Mermaid diagram contains a derived session key label (e.g.,
`sk_session`, `sk_I`, `key_data`) that should remain private.

### Query

The canonical pattern: declare a private free name and encrypt it under the
session key. The attacker learning `private_I` is equivalent to breaking the
session key, because decrypting the ciphertext requires it.

```proverif
(* Top-level declarations *)
free private_I: bitstring [private].
free private_R: bitstring [private].

(* In the Initiator process, after deriving sk_session: *)
out(c, aead_enc(private_I, sk_session));

(* In the Responder process, after deriving sk_session: *)
out(c, aead_enc(private_R, sk_session));

(* Queries *)
query attacker(private_I).
query attacker(private_R).
```

ProVerif proves `attacker(private_I)` by verifying that no derivation path
for `private_I` exists. Since `private_I` is encrypted and decryption requires
`sk_session`, this is equivalent to session key secrecy.

**Important:** `attacker(k)` cannot appear as the consequent of a
correspondence query (`event(...) ==> attacker(k)` is not valid ProVerif
syntax). Use the witness pattern above instead.

---

## 2. Authentication

### Weak Authentication

**Goal:** If B completed accepting a session with A, then A ran at some point.
Does NOT prevent replay (attacker can replay A's messages to create a second
session where B accepts).

**When to use:** Protocol has identity verification but no per-session
freshness binding (e.g., only verifies a static certificate, no nonce or
ephemeral key in the signature).

```proverif
query pk_i: pkey, pk_r: pkey, k: key;
    event(endR(pk_i, pk_r, k)) ==> event(beginI(pk_i, pk_r)).
```

Note: `beginI` fires before the session key is known, so it typically
has fewer parameters than `endR`. Match the parameter list to what the
`begin` event actually receives when it fires.

### Injective Authentication

**Goal:** Each B-accept corresponds to a distinct, unique A-run. Prevents
replay attacks.

**When to use:** The signature (or MAC) covers a fresh value unique to this
session — an ephemeral key, a nonce, or a transcript hash. This is the
default for most modern protocols.

```proverif
query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endR(pk_i, pk_r, k)) ==>
    inj-event(beginI(pk_i, pk_r)).
```

**Note on `inj-event`:** ProVerif will report this as `true` if there is a
one-to-one correspondence. If it reports `false`, the protocol is vulnerable
to replay — investigate whether nonces or ephemeral keys are correctly bound
in the signatures.

### Mutual Authentication

For protocols where both parties authenticate each other, add queries in both
directions:

```proverif
(* Responder accepts => Initiator ran *)
query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endR(pk_i, pk_r, k)) ==>
    inj-event(beginI(pk_i, pk_r)).

(* Initiator accepts => Responder ran *)
query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endI(pk_i, pk_r, k)) ==>
    inj-event(beginR(pk_i, pk_r)).
```

### Placing Events in the Process

| Event | Where to trigger |
|-------|-----------------|
| `beginI(pk_I, pk_R)` | Just before Initiator sends the first authenticated message (the one signed with sk_I) |
| `endI(pk_I, pk_R, sk)` | Just after Initiator successfully verifies Responder's identity AND derives session key |
| `beginR(pk_I, pk_R)` | Just before Responder sends its signed reply |
| `endR(pk_I, pk_R, sk)` | Just after Responder successfully verifies Initiator's identity AND derives session key |

The session key `sk` in the event parameters binds authentication to the
specific key material established — preventing cross-session confusion attacks.

---

## 3. Forward Secrecy

### Goal

Compromise of a long-term key AFTER a session completes does not allow the
attacker to decrypt past session traffic.

### When to add

Add when:
- The Mermaid diagram shows ephemeral key generation inside the session
  (e.g., `keygen() → ek_I, epk_I`)
- The session key derivation uses DH over ephemeral keys (not just static ones)

### Modeling Pattern

Leak long-term keys to the attacker and check that session key secrecy
still holds. If it does, forward secrecy is achieved because the session
key depends only on ephemeral material.

```proverif
(* In main process — leak long-term keys immediately *)
new sk_I: skey; out(c, pk(sk_I)); out(c, sk_I);  (* attacker knows sk_I *)
new sk_R: skey; out(c, pk(sk_R)); out(c, sk_R);  (* attacker knows sk_R *)
(!Initiator(sk_I, pk(sk_R)) | !Responder(sk_R, pk(sk_I)))
```

The existing session key secrecy query (`query attacker(private_I).`) now
tests forward secrecy: if the attacker knows both long-term keys but still
cannot derive the session key, the protocol has forward secrecy. If the
query fails, the session key depended on a long-term key.

---

## 4. Reachability (Sanity Check)

### Goal

Confirm that the success path of the protocol actually executes. A ProVerif
model with a bug (e.g., a type error causing a dead receive) may trivially
prove all security properties because the end event is never reached.

### Always add

```proverif
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
```

Note: ProVerif does not support `_` wildcards in `query` declarations; every
parameter must be bound to a typed variable.

If ProVerif reports these as `false` (unreachable), the model has a structural
bug. Fix it before trusting any other query result.

---

## 5. Key Exposure Oracle (for `[private]` type secrets)

### Goal

Prove that the attacker cannot learn a secret key `sk` that is declared with a
private type (`type sk [private]`) and never directly output on the public
channel.

### Why `query attacker(sk)` doesn't work here

`query attacker(sk)` checks whether the attacker can derive the term `sk` from
public channel traffic. A value of a private type is never synthesised by the
attacker (the type prevents it), and if `sk` is never output, ProVerif cannot
prove the query — it would return `cannot be proved`, not `true`. The property
needs a different formulation.

### The oracle pattern

Give the attacker an explicit "guess oracle": receive an arbitrary value of
type `sk` from the public channel, then fire a `key_exposed` event if that
guess matches the known public key:

```proverif
(* Declare the sentinel event — use whatever secret key type the protocol uses *)
event key_exposed(skey).

(* Secrecy query: key_exposed must be unreachable *)
query x: skey; event(key_exposed(x)).

(* At the end of the process that generated sk_new — place after all other
 * protocol steps so the oracle is only reachable on a complete run: *)
in(c, guess: skey);
if pk(guess) = pk_new then event key_exposed(guess)
else 0.
```

**How it works:**

1. The attacker submits its best guess for `sk_new` via `c`.
2. The process checks whether `pk(guess)` matches the known `pk_new`.
3. If the check succeeds, `key_exposed` fires.
4. ProVerif proves `event(key_exposed(x))` unreachable → no guess can match
   the public key → `sk_new` is secret.

### When to use

Use the oracle pattern when all of these hold:

- The secret key is of a `[private]` type (e.g., `type skey [private]`) and
  never output directly.
- The corresponding public key IS observable on `c` (e.g., sent in a signed
  message or after key exchange).
- `query attacker(sk_new)` would return `cannot be proved` (not meaningful).

### Placement in process

Put the oracle at the very end of the process that generated `sk_new`,
**after** all other steps that depend on the secret are complete (typically
after the signature is sent). This ensures `key_exposed` is only reachable
upon protocol completion, not on every intermediate step.

---

## 6. Query Checklist by Protocol Type

### Two-party key exchange (e.g., DH-based handshake)

```proverif
(* Sanity — all parameters must be bound to typed variables *)
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).

(* Session key secrecy — use the witness pattern, not correspondence *)
query attacker(private_I).
query attacker(private_R).

(* Mutual injective authentication *)
query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endR(pk_i, pk_r, k)) ==> inj-event(beginI(pk_i, pk_r)).
query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endI(pk_i, pk_r, k)) ==> inj-event(beginR(pk_i, pk_r)).
```

### Unilateral authentication (server authenticates, client does not)

```proverif
(* Sanity *)
query pk_s: pkey, k: key; event(endC(pk_s, k)).

(* Session key secrecy — use the witness pattern *)
query attacker(private_C).

(* Server authentication only — client to server direction *)
query pk_s: pkey, k: key;
    inj-event(endC(pk_s, k)) ==> inj-event(beginS(pk_s, k)).
```

### Commit-reveal protocol

```proverif
(* Binding: verifier accepts only the committed value *)
query v: bitstring, r: bitstring;
    event(accepted(v)) ==> event(committed(v, r)).

(* Hiding: attacker cannot learn committed value before reveal *)
query attacker(committed_value).
```

### Challenge-response authentication

```proverif
(* Freshness: each successful auth used a distinct challenge *)
query id: pkey, ch: bitstring;
    inj-event(authSuccess(id, ch)) ==> inj-event(challengeSent(id, ch)).
```

---

## 7. Interpreting ProVerif Output

| ProVerif result | Meaning |
|----------------|---------|
| `RESULT ... is true.` | Property holds for all executions (proof found) |
| `RESULT ... is false.` | Attack found — ProVerif prints a trace |
| `RESULT ... cannot be proved.` | Proof search timed out or approximation too coarse; does not mean the property is false |

When a result is `false`, read the attack trace carefully:
1. Identify the event sequence ProVerif found
2. Map it back to the Mermaid diagram steps
3. Determine if the attack is a real flaw or a modeling artifact

Common false attacks from modeling artifacts:
- **Type confusion**: Two bitstrings with compatible types where the model
  should use distinct types
- **Missing replication**: Single-session model allows trivial "man-in-middle"
  because the attacker is the only other party
- **Missing freshness binding**: Signature does not include the nonce/epk,
  so replay is possible at the model level even if the spec would bind it

When a result is `cannot be proved`, consider:
- Adding more specific type annotations
- Splitting the `!` replication into bounded sessions
- Switching to a weaker query first to establish partial results