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.
npx skills add trailofbits/skills --skill mermaid-to-proverif --agent claude-code
Same command for any agent — swap --agent for codex, cursor, copilot.
Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.
# 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 | |-----------------|----------------|--------
- When to Use
- When NOT to Use
- Rationalizations to Reject
- Workflow
- 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
- Decision Tree
- Example
What does the mermaid-to-proverif skill do?
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.
How do I install it?
Run `npx skills add trailofbits/skills --skill mermaid-to-proverif --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.
Where does this skill come from?
From trailofbits/skills, a repository with 6,426 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.
Is a popular skill a good skill?
Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.