interface:
  display_name: "Mermaid to ProVerif"
  short_description: "Translate protocol diagrams into formal verification models"
  icon_small: "assets/trail-of-bits-mark.svg"
  icon_large: "assets/trail-of-bits-mark.svg"
  brand_color: "#D83A34"

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

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

# 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