mermaid-to-proverif — Claude Code skill: what it does, how to install
Turns a Mermaid sequence diagram of a crypto protocol into a ProVerif model — a .pv file you can check for secrecy, authentication and forward secrecy.
npx skills add trailofbits/skills --skill mermaid-to-proverif -a claude-codeWhat mermaid-to-proverif does
Give it a Mermaid sequenceDiagram that spells out a cryptographic exchange and it writes the matching ProVerif model. The output is a .pv file you pass straight to the verifier. It does not draw diagrams: the input is usually what the crypto-protocol-diagram skill produces, with message arrows and notes for Sign, Verify, DH, HKDF, Enc, Dec.
The run goes in order — participants and channels, an inventory of crypto operations, type and function declarations, events, security queries, per-party processes, the main process, then delivery. A worked examples/simple-handshake/ ships with it; look at that before taking on an unfamiliar protocol. Everything is done with Read, Write, Grep and Glob.
One habit it insists on: add reachability queries for events before anything else. If an event never fires, the answers to your other queries prove nothing. The verifier itself is not run for you, so proverif model.pv stays your job — worth having ProVerif installed before you start.
What it helps with
- turn a protocol sketch into a
.pvmodel ProVerif can check - prove secrecy for the session key of a hand-rolled handshake
- test forward secrecy when ephemeral keys show up in the diagram
- hunt for replay attacks before the code ships
- audit which crypto primitives a diagram actually uses
Example prompts for the agent
- Turn this Mermaid handshake diagram into a ProVerif model and query session key secrecy.
- Convert the diagram in `examples/simple-handshake/` to `.pv` and add reachability queries for every event.
- Check forward secrecy for this exchange with ephemeral keys.
How to install mermaid-to-proverif
1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a claude-code2Manually: put the files in place
~/.claude/skills/mermaid-to-proverif/SKILL.mdCopy the whole skill folder; for one project use .claude/skills/mermaid-to-proverif/
1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a codex2Manually: put the files in place
.agents/skills/mermaid-to-proverif/SKILL.mdFor all projects use ~/.agents/skills/
1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a cursor2Manually: put the files in place
.cursor/skills/mermaid-to-proverif/SKILL.mdCursor also reads .agents/skills/ and .claude/skills/
1GitHub CLI
gh skill install trailofbits/skills mermaid-to-proverif2Manually: put the files in place
.github/skills/mermaid-to-proverif/SKILL.md1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a gemini-cli2Platform CLI
gemini skills install https://github.com/trailofbits/skills --path plugins/trailmark/skills/mermaid-to-proverifManually: put the files in place
.devin/skills/mermaid-to-proverif/SKILL.mdThe legacy .windsurf/skills/ path still works
Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a opencodeClaude.ai
Zip the folder and upload it in Settings → Capabilities → Skills
From the same set35
The whole set →Similar
Questions about mermaid-to-proverif
How do I install mermaid-to-proverif in Claude Code?
Run npx skills add trailofbits/skills --skill mermaid-to-proverif -a claude-code. The skill lands at ~/.claude/skills/mermaid-to-proverif/SKILL.md.
What does mermaid-to-proverif do?
It translates a Mermaid sequenceDiagram of a cryptographic protocol into a ProVerif model as a .pv file, with queries for secrecy, authentication and forward secrecy.
How is it different from crypto-protocol-diagram?
crypto-protocol-diagram builds the diagram; this skill reads one. With no sequenceDiagram on hand yet, start with the first one.
