Reads a Mermaid sequenceDiagram describing a cryptographic protocol and\nproduces a ProVerif model (.pv file) that can be passed directly to the\nProVerif verifier.
Tools used: Read, Write, Grep, Glob.
\nThe typical input is the output of the crypto-protocol-diagram skill — a\nMermaid sequenceDiagram annotated with cryptographic operations (Sign,\nVerify, DH, HKDF, Enc, Dec, etc.) and message arrows.
crypto-protocol-diagram skillcrypto-protocol-diagram first to generate oneproverif model.pv directly| Rationalization | \nWhy It's Wrong | \nRequired Action | \n
|---|---|---|
| \"Reachability queries are just busywork\" | \nIf events aren't reachable, all other query results are meaningless | \nAlways add reachability queries first as a sanity check | \n
| \"Public channels are fine for all messages\" | \nPrivate channels for internal state prevent false attacks | \nUse private channels for intra-process state threading | \n
| \"I'll skip the forward secrecy test\" | \nEphemeral keys demand forward secrecy verification | \nAdd the ForwardSecrecyTest process whenever the diagram shows ephemeral keys | \n
| \"Unused declarations are harmless\" | \nProVerif may report spurious results from orphan declarations | \nClean up all unused types, functions, and events | \n
| \"The model compiles, so it's correct\" | \nA compiling model can have dead receives, type mismatches, or impossible guards that make queries vacuously true | \nValidate reachability before trusting any security query | \n
| \"I don't need to check the example first\" | \nThe example defines the expected output quality bar | \nStudy examples/simple-handshake/ before working on unfamiliar protocols | \n
ProVerif Model Progress:\n- [ ] Step 1: Parse participants and channels\n- [ ] Step 2: Inventory cryptographic operations\n- [ ] Step 3: Declare types, functions, and equations\n- [ ] Step 4: Identify and declare events\n- [ ] Step 5: Formulate security queries\n- [ ] Step 6: Write participant processes\n- [ ] Step 7: Write main process and finalize\n- [ ] Step 8: Verify and deliver\nFrom the Mermaid diagram:
\nparticipant or actor declaration. Each becomes a\nProVerif process.->>, -->>, -x, --x). Each distinct\nA ->> B: label creates a communication step on a channel.c for all cross-party\nmessages. Add per-flow channels only when two distinct parallel sessions\nmust be independent.free c: channel.\nWalk through every Note over annotation and message label. Build a list of\nall distinct operations used. Map each to a ProVerif declaration category:
| Mermaid annotation | \nProVerif category | \n
|---|---|
keygen() → sk, pk | \nNew name (new sk), public key derived via function | \n
DH(sk_A, pk_B) | \nDH function or exp with group | \n
Sign(sk, msg) → σ | \nSignature function | \n
Verify(pk, msg, σ) | \nEquation or destructor | \n
Enc(key, msg) → ct | \nSymmetric or asymmetric encryption function | \n
Dec(key, ct) → msg | \nDestructor (equation) | \n
HKDF(ikm, info) → k | \nPRF/KDF function | \n
HMAC(key, msg) → tag | \nMAC function | \n
H(msg) → digest | \nHash function | \n
Commit(v, r) → C | \nCommitment function | \n
Open(C, v, r) | \nCommitment equation | \n
Consult references/crypto-to-proverif-mapping.md\nfor exact ProVerif syntax for each.
\nBuild the cryptographic preamble in this order:
\ntype key.\ntype pkey. (* public key *)\ntype skey. (* secret key *)\ntype nonce.\nconst msg1_label: bitstring.\nconst msg2_label: bitstring.\nconst info_session_key: bitstring.\nreduc\nso that the process aborts on verification or decryption failure:(* Asymmetric encryption *)\nfun aenc(bitstring, pkey): bitstring.\nfun adec(bitstring, skey): bitstring\n reduc forall m: bitstring, k: skey;\n adec(aenc(m, pk(k)), k) = m.\nfun pk(skey): pkey.\n\n(* Symmetric encryption / AEAD *)\nfun aead_enc(bitstring, key): bitstring.\nfun aead_dec(bitstring, key): bitstring\n reduc forall m: bitstring, k: key;\n aead_dec(aead_enc(m, k), k) = m.\n\n(* Digital signatures — verify returns the message on success, aborts on failure *)\nfun sign(bitstring, skey): bitstring.\nfun verify(bitstring, bitstring, pkey): bitstring\n reduc forall m: bitstring, k: skey;\n verify(sign(m, k), m, pk(k)) = m.\n\n(* KDF — first arg is key (from DH), second is bitstring (info/context) *)\nfun hkdf(key, bitstring): key.\n\n(* MAC *)\nfun mac(bitstring, key): bitstring.\n\n(* Hash *)\nfun hash(bitstring): bitstring.\n\n(* DH *)\nfun dh(skey, pkey): key.\nfun dhpk(skey): pkey.\n\n(* Serialization — ProVerif is strongly typed: pkey cannot appear\n * where bitstring is expected. Use these to build signed payloads. *)\nfun pkey2bs(pkey): bitstring.\nfun concat(bitstring, bitstring): bitstring.\nequation forall sk_a: skey, sk_b: skey;\n dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a)).\nOnly declare what the diagram actually uses. Do not add functions for\noperations not present.
\nEvents mark security-relevant moments in the protocol execution. Extract them\nby identifying:
\nevent beginRole(params)): triggered immediately before a\nparty sends a message that depends on a long-term identity commitment (e.g.,\nright before sending a signed message or a MAC'd message).event endRole(params)): triggered immediately after a party\nsuccessfully verifies the peer's identity (e.g., after Verify(...) or MAC\ncheck passes, session key confirmed).event beginI(pkey, pkey). (* pk_I, pk_R — fired before sending the signed message *)\nevent endI(pkey, pkey, key). (* pk_I, pk_R, session_key — fired after accepting *)\nevent beginR(pkey, pkey).\nevent endR(pkey, pkey, key).\nParameters should uniquely identify the session: the parties' public keys,\nplus the session key or a transcript hash.
\nWrite one query per security property. Choose from:
\nReachability (always add first — structural sanity check):
\nVerify that the success events are actually reachable. If ProVerif reports any\nof these as false, the model has a structural bug (dead receive, type mismatch,\nimpossible guard) and no other query result should be trusted. Once the model\nis validated, comment them out if they slow down the main property checks:
(* Sanity: both endpoints must be reachable — comment out once validated. *)\n(*\nquery pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).\nquery pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).\n*)\nSecrecy (key not derivable by attacker):
\nDeclare a private free name and encrypt it under the session key. The attacker\nknowing private_I is equivalent to breaking the session key:
free private_I: bitstring [private].\n\n(* In process, after deriving sk_session: *)\nout(c, aead_enc(private_I, sk_session));\n\n(* Query: *)\nquery attacker(private_I).\nWeak authentication (if B accepted, A ran at some point with matching\nparams — does not prevent replay):
\nquery pk_i: pkey, pk_r: pkey, k: key;\n event(endR(pk_i, pk_r, k)) ==> event(beginI(pk_i, pk_r)).\nInjective authentication (prevents replay — each B-accept corresponds to\na distinct A-run):
\nquery pk_i: pkey, pk_r: pkey, k: key;\n inj-event(endR(pk_i, pk_r, k)) ==>\n inj-event(beginI(pk_i, pk_r)).\nForward secrecy: add a ForwardSecrecyTest process to the main process\nthat leaks both long-term secret keys to the attacker, then check that a past\nsession key remains secret. Pair it with a free fs_witness: key [private]\ndeclaration and query attacker(fs_witness). See\nreferences/security-properties.md →\nForward Secrecy, and the worked example in\nexamples/simple-handshake/sample-output.pv.
Choose the strongest applicable query for each property. See\nreferences/security-properties.md for\nthe full decision tree.
\nWrite one let process per participant. Structure each process to mirror the\nMermaid diagram step-by-step, in order.
Template for a two-party protocol:
\nlet Initiator(sk_I: skey, pk_R: pkey) =\n (* Step: generate ephemeral key *)\n new ek_I: skey;\n let epk_I = dhpk(ek_I) in\n (* Step: sign and send msg1 — pkey2bs casts pkey to bitstring *)\n let sig_I = sign(concat(msg1_label, pkey2bs(epk_I)), sk_I) in\n event beginI(pk(sk_I), pk_R);\n out(c, (epk_I, sig_I));\n (* Step: receive msg2 *)\n in(c, (epk_R: pkey, sig_R: bitstring));\n (* Step: verify responder signature — destructor aborts on failure *)\n let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in\n let _ = verify(sig_R, concat(msg2_label, transcript), pk_R) in\n (* Step: derive session key *)\n let dh_val = dh(ek_I, epk_R) in\n let sk_session = hkdf(dh_val, concat(info_session_key, transcript)) in\n event endI(pk(sk_I), pk_R, sk_session);\n (* Secrecy witness: encrypt private_I under the session key.\n * Declared as: free private_I: bitstring [private].\n * The query attacker(private_I) checks the attacker cannot derive it. *)\n out(c, aead_enc(private_I, sk_session)).\nRules for writing processes:
\nA ->> B: msg_contents in the diagram becomes:\nout(c, msg_contents) in A's processin(c, x) (with matching destructuring) in B's processNote over A: op → result becomes a let result = op in bindingNote over A: Verify(...) becomes a let _ = verify(...) in\nbinding (the destructor aborts on failure — no explicit else needed,\nmodeling abort)alt blocks in the diagram as if/then/else in the processnewN-party or MPC protocols: write one process per distinct role. For\nthreshold protocols, write a single role process and replicate it !N times\nin the main process.
The main process:
\nnewout(c, pk(sk))!) to allow\nmultiple sessionsprocess\n new sk_I: skey; let pk_I = pk(sk_I) in out(c, pk_I);\n new sk_R: skey; let pk_R = pk(sk_R) in out(c, pk_R);\n (\n !Initiator(sk_I, pk_R)\n | !Responder(sk_R, pk_I)\n )\nPlace the full file in this order:
\n(* 1. Channel declarations (free c: channel. / free ch: channel [private].) *)\n(* 2. noselect directives (if needed for termination) *)\n(* 3. Type declarations *)\n(* 4. Constants *)\n(* 5. Function declarations *)\n(* 6. Equations (algebraic identities on constructors only) *)\n(* 7. Table declarations *)\n(* 8. Events *)\n(* 9. Queries *)\n(* 10. Let processes *)\n(* 11. Main process *)\nBefore writing the file:
\nlet processout(c, ...) has a matching in(c, ...) on the other side with\ncompatible typesreduc (not a separate equation block)c in the main process\n(attacker can see them — that is the Dolev-Yao model)table declarations are present: every insert T(...) has a\ncorresponding get T(...) with compatible column types and matching\npattern constraints (=key vs bare name)noselect is used: its tuple structure matches the actual message\nshapes sent on c (e.g., pairs → mess(c, (x, y)))event key_exposed(sk_type)\nis declared, the oracle in(c, guess: sk_type); if pk(guess) = pk_new then event key_exposed(guess) appears at the end of the process that holds the\nsecret, and the query is query x: sk_type; event(key_exposed(x))Write the model to a .pv file. Choose a filename from the protocol name,\ne.g. noise-xx-handshake.pv or x3dh-key-agreement.pv.
After writing, print a brief summary:
\nProtocol: <Name>\nOutput: <filename>\nQueries: <list each query and what property it tests>\nAssumptions: <list modeling decisions and simplifications>\n├─ No Mermaid diagram provided?\n│ └─ Ask the user: \"Please provide the Mermaid sequenceDiagram,\n│ or run the crypto-protocol-diagram skill first.\"\n│\n├─ Diagram uses DH (not just symmetric crypto)?\n│ └─ Use dh/dhpk with commutativity equation\n│ See references/crypto-to-proverif-mapping.md → DH section\n│\n├─ Diagram uses asymmetric signatures (Sign/Verify)?\n│ └─ Use sign/verify with inline reduc (not equation)\n│ verify returns the message on success; let _ = verify(...) in to abort on failure\n│ Distinguish signing key (skey) from verification key (pkey)\n│\n├─ Diagram has an \"alt\" block (abort path)?\n│ └─ Model as if/then only — the else branch aborts (process terminates)\n│ Do NOT add out(c, error_message) unless the diagram shows it\n│\n├─ Protocol has N > 2 parties?\n│ └─ Write one process per role, use ! for replication\n│ Pass participant index as a parameter if roles differ by index only\n│\n├─ Forward secrecy requested?\n│ └─ Add a ForwardSecrecy variant in the main process that leaks\n│ long-term sk after session; add secrecy query for past session_key\n│ See references/security-properties.md → Forward Secrecy\n│\n├─ Type-checker rejects the model?\n│ └─ ProVerif is typed: check every function arg type matches declaration.\n│ bitstring is the catch-all; key/pkey/skey/nonce are stricter.\n│ Cast with explicit constructors when needed.\n│\n├─ Protocol has cross-process state coordination (e.g., one process must wait\n│ for another to record acceptance before proceeding)?\n│ └─ Use ProVerif tables (table/insert/get)\n│ See references/proverif-syntax.md → Tables\n│\n├─ Verification does not terminate after several minutes?\n│ └─ Add noselect directive matching the message tuple structure on c\n│ See references/proverif-syntax.md → noselect\n│\n├─ Protocol generates a private-type key (type sk [private]) that is never\n│ output directly but whose secrecy should be verified?\n│ └─ Use the Key Exposure Oracle pattern instead of query attacker(sk)\n│ See references/security-properties.md → Key Exposure Oracle\n│\n└─ Unsure which security properties to verify?\n └─ Default set: secrecy of session key + injective authentication\n (both directions). Add forward secrecy if diagram shows ephemeral keys.\nexamples/simple-handshake/ contains a worked example:
diagram.md — Mermaid sequenceDiagram for a two-party authenticated key\nexchange (X25519 DH + Ed25519 signing + HKDF)sample-output.pv — exact ProVerif model the skill should produce,\nwith secrecy and injective authentication queriesStudy this before working on an unfamiliar protocol.
\n