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.
Step 6: Write Participant Processes
Write one
let
process per participant. Structure each process to mirror the
Mermaid diagram step-by-step, in order.
Template for a two-party protocol:
let Initiator(sk_I: skey, pk_R: pkey) =
( Step: generate ephemeral key )
new ek_I: skey;
let epk_I = dhpk(ek_I) in
( Step: sign and send msg1 — pkey2bs casts pkey to bitstring )
let sig_I = sign(concat(msg1_label, pkey2bs(epk_I)), sk_I) in
event beginI(pk(sk_I), pk_R);
out(c, (epk_I, sig_I));
( Step: receive msg2 )
in(c, (epk_R: pkey, sig_R: bitstring));
( Step: verify responder signature — destructor aborts on failure )
let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in
let _ = verify(sig_R, concat(msg2_label, transcript), pk_R) in
( Step: derive session key )
let dh_val = dh(ek_I, epk_R) in
let sk_session = hkdf(dh_val, concat(info_session_key, transcript)) in
event endI(pk(sk_I), pk_R, sk_session);
( Secrecy witness: encrypt private_I under the session key.
* Declared as: free private_I: bitstring [private].
* The query attacker(private_I) checks the attacker cannot derive it. )
out(c, aead_enc(private_I, sk_session)).
Rules for writing processes:
Each
A ->> B: msg_contents
in the diagram becomes:
out(c, msg_contents)
in A's process
in(c, x)
(with matching destructuring) in B's process
Each
Note over A: op → result
becomes a
let result = op in
binding
Each
Note over A: Verify(...)
becomes a
let _ = verify(...) in
binding (the destructor aborts on failure — no explicit else needed,
modeling abort)
Use
alt
blocks in the diagram as
if/then/else
in the process
Long-term keys are process parameters; ephemeral values use
new
N-party or MPC protocols:
write one process per distinct role. For
threshold protocols, write a single role process and replicate it
!N
times
in the main process.
Step 7: Write Main Process and Finalize
The main process:
Generates long-term keys with
new
Publishes public keys to the attacker via
out(c, pk(sk))
Runs participant processes in parallel under replication (
!
) to allow
multiple sessions
Optionally leaks long-term keys for forward-secrecy analysis
process
new sk_I: skey; let pk_I = pk(sk_I) in out(c, pk_I);
new sk_R: skey; let pk_R = pk(sk_R) in out(c, pk_R);
(
!Initiator(sk_I, pk_R)
| !Responder(sk_R, pk_I)
)
Place the full file in this order:
( 1. Channel declarations (free c: channel. / free ch: channel [private].) )
( 2. noselect directives (if needed for termination) )
( 3. Type declarations )
( 4. Constants )
( 5. Function declarations )
( 6. Equations (algebraic identities on constructors only) )
( 7. Table declarations )
( 8. Events )
( 9. Queries )
( 10. Let processes )
( 11. Main process )
Step 8: Verify and Deliver
Before writing the file:
Every participant in the diagram has a matching
let
process
Every
out(c, ...)
has a matching
in(c, ...)
on the other side with
compatible types
Every function used in a process is declared in the preamble
Every destructor uses inline
reduc
(not a separate
equation
block)
Every event in a query is declared and triggered in a process
Long-term public keys are output to channel
c
in the main process
(attacker can see them — that is the Dolev-Yao model)
No unused declarations (clean up anything added speculatively)
If
table
declarations are present: every
insert T(...)
has a
corresponding
get T(...)
with compatible column types and matching
pattern constraints (
=key
vs bare name)
If
noselect
is used: its tuple structure matches the actual message
shapes sent on
c
(e.g., pairs →
mess(c, (x, y))
)
If the Key Exposure Oracle pattern is used:
event key_exposed(sk_type)
is 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
secret, 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,
e.g.
noise-xx-handshake.pv
or
x3dh-key-agreement.pv
.
After writing, print a brief summary:
Protocol:
Output:
Queries:
Assumptions:
Decision Tree
├─ No Mermaid diagram provided?
│ └─ Ask the user: "Please provide the Mermaid sequenceDiagram,
│ or run the crypto-protocol-diagram skill first."
│
├─ Diagram uses DH (not just symmetric crypto)?
│ └─ Use dh/dhpk with commutativity equation
│ See references/crypto-to-proverif-mapping.md → DH section
│
├─ Diagram uses asymmetric signatures (Sign/Verify)?
│ └─ Use sign/verify with inline reduc (not equation)
│ verify returns the message on success; let _ = verify(...) in to abort on failure
│ Distinguish signing key (skey) from verification key (pkey)
│
├─ Diagram has an "alt" block (abort path)?
│ └─ Model as if/then only — the else branch aborts (process terminates)
│ Do NOT add out(c, error_message) unless the diagram shows it
│
├─ Protocol has N > 2 parties?
│ └─ Write one process per role, use ! for replication
│ Pass participant index as a parameter if roles differ by index only
│
├─ Forward secrecy requested?
│ └─ Add a ForwardSecrecy variant in the main process that leaks
│ long-term sk after session; add secrecy query for past session_key
│ See references/security-properties.md → Forward Secrecy
│
├─ Type-checker rejects the model?
│ └─ ProVerif is typed: check every function arg type matches declaration.
│ bitstring is the catch-all; key/pkey/skey/nonce are stricter.
│ Cast with explicit constructors when needed.
│
├─ Protocol has cross-process state coordination (e.g., one process must wait
│ for another to record acceptance before proceeding)?
│ └─ Use ProVerif tables (table/insert/get)
│ See references/proverif-syntax.md → Tables
│
├─ Verification does not terminate after several minutes?
│ └─ Add noselect directive matching the message tuple structure on c
│ See references/proverif-syntax.md → noselect
│
├─ Protocol generates a private-type key (type sk [private]) that is never
│ output directly but whose secrecy should be verified?
│ └─ Use the Key Exposure Oracle pattern instead of query attacker(sk)
│ See references/security-properties.md → Key Exposure Oracle
│
└─ Unsure which security properties to verify?
└─ Default set: secrecy of session key + injective authentication
(both directions). Add forward secrecy if diagram shows ephemeral keys.
Example
examples/simple-handshake/
contains a worked example:
diagram.md
— Mermaid sequenceDiagram for a two-party authenticated key
exchange (X25519 DH + Ed25519 signing + HKDF)
sample-output.pv
— exact ProVerif model the skill should produce,
with secrecy and injective authentication queries
Study this before working on an unfamiliar protocol.
Supporting Documentation
references/crypto-to-proverif-mapping.md
—
Mapping table from Mermaid cryptographic annotations to ProVerif function
declarations, equations, and process patterns
references/proverif-syntax.md
—
ProVerif language reference: types, functions, equations, processes, events,
queries, and common pitfalls
references/security-properties.md
—
Decision guide for choosing the right queries: secrecy, authentication
(weak vs injective), forward secrecy, unlinkability, and how to model them