Loading skill
Install any skill in seconds. Free to start, no credit card required.
Get Started Free →trailofbits/mermaid-to-proverif
Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif formal verification models (.pv files).
Passed 13 of 18 test cases with the skill, and 11 of 18 without it.
3 fixed13 passed either way5 still failing1 broke
Tokens, turns and time describe resource use, not a dollar price.
One of 3 test cases the skill fixed. Same model, same prompt, with and without the skill.
Write a ProVerif model for an ECDH key agreement step where key exchange relies on Diffie-Hellman exponentiation.
| Checked | Without skill | With skill |
|---|---|---|
| The DH operation is modeled using constructor functions with an equation defining dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a)). | Missed | Passed |
The instructions your model reads when the skill loads.
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.
crypto-protocol-diagram skillcrypto-protocol-diagram first to generate oneproverif model.pv directly| 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 |
test cases passed, vs 11 / 18 without
More skills from the same source and nearby in the registry, with their headline benchmark lift.