Mermaid to ProVerif Model

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

Workflow

ProVerif Model Progress:
- [ ] 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

Step 1: Parse Participants and Channels

From the Mermaid diagram:

1. Extract every participant or actor declaration. Each becomes a ProVerif process.
2. Count message arrows (->>, -->>, -x, --x). Each distinct A ->> B: label creates a communication step on a channel.
3. Decide channel model:
   • Public channel for any message sent over the network before a secure channel is established (e.g., ClientHello, ephemeral keys, ciphertext to be decrypted by the peer).
   • Private channel only for internal state threading within a single party process (not for cross-party messages).
   • Default: declare one shared public channel c for all cross-party messages. Add per-flow channels only when two distinct parallel sessions must be independent.

free c: channel.

Step 2: Inventory Cryptographic Operations

Walk through every Note over annotation and message label. Build a list of all distinct operations used. Map each to a ProVerif declaration category:

Consult references/crypto-to-proverif-mapping.md for exact ProVerif syntax for each.

Step 3: Declare Types, Functions, and Equations

Build the cryptographic preamble in this order:

1. Types — declare custom types used to distinguish key material:

type key.
type pkey.   (* public key *)
type skey.   (* secret key *)
type nonce.

2. Constants — for fixed strings used as domain separators or labels:

const msg1_label: bitstring.
const msg2_label: bitstring.
const info_session_key: bitstring.

3. Functions — constructors and destructors. Destructors use inline reduc so that the process aborts on verification or decryption failure:

(* Asymmetric encryption *)
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring
    reduc forall m: bitstring, k: skey;
        adec(aenc(m, pk(k)), k) = m.
fun pk(skey): pkey.

(* Symmetric encryption / AEAD *)
fun aead_enc(bitstring, key): bitstring.
fun aead_dec(bitstring, key): bitstring
    reduc forall m: bitstring, k: key;
        aead_dec(aead_enc(m, k), k) = m.

(* Digital signatures — verify returns the message on success, aborts on failure *)
fun sign(bitstring, skey): bitstring.
fun verify(bitstring, bitstring, pkey): bitstring
    reduc forall m: bitstring, k: skey;
        verify(sign(m, k), m, pk(k)) = m.

(* KDF — first arg is key (from DH), second is bitstring (info/context) *)
fun hkdf(key, bitstring): key.

(* MAC *)
fun mac(bitstring, key): bitstring.

(* Hash *)
fun hash(bitstring): bitstring.

(* DH *)
fun dh(skey, pkey): key.
fun dhpk(skey): pkey.

(* Serialization — ProVerif is strongly typed: pkey cannot appear
 * where bitstring is expected. Use these to build signed payloads. *)
fun pkey2bs(pkey): bitstring.
fun concat(bitstring, bitstring): bitstring.

4. Equations — algebraic identities on constructors only (not on destructors, which already have their rewrite rules inline):

equation forall sk_a: skey, sk_b: skey;
    dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a)).

Only declare what the diagram actually uses. Do not add functions for operations not present.

Step 4: Identify and Declare Events

Events mark security-relevant moments in the protocol execution. Extract them by identifying:

• Begin events (event beginRole(params)): triggered immediately before a party sends a message that depends on a long-term identity commitment (e.g., right before sending a signed message or a MAC'd message).
• End events (event endRole(params)): triggered immediately after a party successfully verifies the peer's identity (e.g., after Verify(...) or MAC check passes, session key confirmed).
• Secrecy markers: any key or nonce that should remain unknown to the attacker after the handshake.

event beginI(pkey, pkey).     (* pk_I, pk_R — fired before sending the signed message *)
event endI(pkey, pkey, key).  (* pk_I, pk_R, session_key — fired after accepting *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).

Parameters should uniquely identify the session: the parties' public keys, plus the session key or a transcript hash.

Step 5: Formulate Security Queries

Write one query per security property. Choose from:

Reachability (always add first — structural sanity check):

Verify that the success events are actually reachable. If ProVerif reports any of these as false, the model has a structural bug (dead receive, type mismatch, impossible guard) and no other query result should be trusted. Once the model is validated, comment them out if they slow down the main property checks:

(* Sanity: both endpoints must be reachable — comment out once validated. *)
(*
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
*)

Secrecy (key not derivable by attacker):

Declare a private free name and encrypt it under the session key. The attacker knowing private_I is equivalent to breaking the session key:

free private_I: bitstring [private].

(* In process, after deriving sk_session: *)
out(c, aead_enc(private_I, sk_session));

(* Query: *)
query attacker(private_I).

Weak authentication (if B accepted, A ran at some point with matching params — does not prevent replay):

query pk_i: pkey, pk_r: pkey, k: key;
    event(endR(pk_i, pk_r, k)) ==> event(beginI(pk_i, pk_r)).

Injective authentication (prevents replay — each B-accept corresponds to a distinct A-run):

query pk_i: pkey, pk_r: pkey, k: key;
    inj-event(endR(pk_i, pk_r, k)) ==>
    inj-event(beginI(pk_i, pk_r)).

Forward secrecy: add a ForwardSecrecyTest process to the main process that leaks both long-term secret keys to the attacker, then check that a past session key remains secret. Pair it with a free fs_witness: key [private] declaration and query attacker(fs_witness). See references/security-properties.md → Forward Secrecy, and the worked example in examples/simple-handshake/sample-output.pv.

Choose the strongest applicable query for each property. See references/security-properties.md for the full decision tree.