mermaid-to-proverif

Files (9)

• SKILL.md
• openai.yaml · agents/
• trail-of-bits-mark.svg · assets/
• diagram.md · examples/simple-handshake/
• sample-output.pv · examples/simple-handshake/
• crypto-to-proverif-mapping.md · references/
• proverif-syntax.md · references/
• security-properties.md · references/
• test_guidance.py · tests/

SKILL.md (first lines)

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

From trailofbits/skills, CC-BY-SA-4.0.

More from trailofbits/skills