Mermaid To Proverif
Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif...
Install
npx skills add trailofbits/skills --skill mermaid-to-proverif -g -a claude-code -y- Repository
- trailofbits/skills7.9k
- Category
- Security
- Updated
- 7d ago
- License
- CC-BY-SA-4.0
- Context cost
- Mediumabout 3,000 tokens
- Runs scripts
- Yes, review before use
What it does
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-diagramskill
When NOT to Use
- No Mermaid sequenceDiagram exists yet, use
crypto-protocol-diagramfirst 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.pvdirectly
