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
Installs just this skill. Get the whole plugin for auto-invocation.
โก How it fires
How this skill gets triggered: by you, by Claude, or both.
Fires itselfClaude auto-loads it when your prompt matches the work.
You can call itInvoke it directly when you want it.
Slash command/mermaid-to-proverif
๐๏ธ Context preview
The summary Claude sees to decide when to auto-load this skill.
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
๐ Stats
Stars6,227
Forks540
LanguagePython
LicenseCC-BY-SA-4.0
๐ฆ Ships with trailofbits-skills
</> SKILL.md
mermaid-to-proverif.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
| "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 |
