mermaid-to-proverif

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Mermaid to ProVerif

Mermaid 转 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.

读取描述密码协议的Mermaid

sequenceDiagram

，生成可直接传入ProVerif验证器的ProVerif模型（

.pv

文件）。

使用的工具： Read、Write、Grep、Glob。

典型输入是

crypto-protocol-diagram

skill的输出——标注了密码学操作（

Sign

、

Verify

、

DH

、

HKDF

、

Enc

、

Dec

等）和消息箭头的Mermaid

sequenceDiagram

。

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

用户要求对以Mermaid sequenceDiagram描述的密码协议进行形式化验证
用户希望从协议图生成ProVerif模型（.pv文件）
用户想要证明保密性、认证性或前向保密性属性
输入是
```
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

尚未生成Mermaid sequenceDiagram——先使用
```
crypto-protocol-diagram
```
生成
用户想要验证非密码学系统的属性（状态机、访问控制）
用户想要对已有的.pv文件运行ProVerif——直接运行
```
proverif model.pv
```
即可

Rationalizations to Reject

拒绝理由的错误说明

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

理由	错误原因	所需操作
"可达性查询只是无用功"	如果事件不可达，所有其他查询结果都没有意义	始终优先添加可达性查询作为合理性检查
"所有消息都使用公共信道就可以"	内部状态使用私有信道可避免误报攻击	进程内部状态传递使用私有信道
"我可以跳过前向保密性测试"	临时密钥要求进行前向保密性验证	当图中出现临时密钥时，始终添加ForwardSecrecyTest进程
"未使用的声明没有危害"	孤立声明可能导致ProVerif返回虚假结果	清理所有未使用的类型、函数和事件
"模型能编译就说明是正确的"	可编译的模型也可能存在死接收、类型不匹配或不可能的守卫条件，导致查询结果空真	信任任何安全查询结果前先验证可达性
"我不需要先查看示例"	示例定义了预期的输出质量标准	处理不熟悉的协议前先学习 `examples/simple-handshake/` 目录的内容

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

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

步骤1：解析参与者和信道

From the Mermaid diagram:

Extract every
```
participant
```
or
```
actor
```
declaration. Each becomes a ProVerif process.
Count message arrows (
```
->>
```
,
```
-->>
```
,
```
-x
```
,
```
--x
```
). Each distinct
```
A ->> B: label
```
creates a communication step on a channel.
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.

proverif

free c: channel.

从Mermaid图中：

提取所有
```
participant
```
或
```
actor
```
声明，每个都对应一个ProVerif进程。
统计消息箭头（
```
->>
```
、
```
-->>
```
、
```
-x
```
、
```
--x
```
），每个不同的
```
A ->> B: label
```
都会在信道上创建一个通信步骤。
确定信道模型：
- 公共信道：用于在安全信道建立前通过网络发送的所有消息（例如ClientHello、临时密钥、待对端解密的密文）。
- 私有信道：仅用于单个参与方进程内部的状态传递（不用于跨参与方消息）。
- 默认：声明一个共享公共信道
```
c
```
  用于所有跨参与方消息。仅当两个不同的并行会话必须相互独立时，才添加逐流信道。

proverif

free c: channel.

Step 2: Inventory Cryptographic Operations

步骤2：清点密码学操作

Walk through every

Note over

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

Mermaid annotation	ProVerif category
`keygen() → sk, pk`	New name ( `new sk` ), public key derived via function
`DH(sk_A, pk_B)`	DH function or `exp` with group
`Sign(sk, msg) → σ`	Signature function
`Verify(pk, msg, σ)`	Equation or destructor
`Enc(key, msg) → ct`	Symmetric or asymmetric encryption function
`Dec(key, ct) → msg`	Destructor (equation)
`HKDF(ikm, info) → k`	PRF/KDF function
`HMAC(key, msg) → tag`	MAC function
`H(msg) → digest`	Hash function
`Commit(v, r) → C`	Commitment function
`Open(C, v, r)`	Commitment equation

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

遍历所有

Note over

标注和消息标签，构建所有使用的不同操作的列表，将每个操作映射到对应的ProVerif声明类别：

Mermaid annotation	ProVerif category
`keygen() → sk, pk`	New name ( `new sk` )，公钥通过函数派生
`DH(sk_A, pk_B)`	DH函数或带群参数的 `exp`
`Sign(sk, msg) → σ`	签名函数
`Verify(pk, msg, σ)`	等式或析构函数
`Enc(key, msg) → ct`	对称或非对称加密函数
`Dec(key, ct) → msg`	析构函数（等式）
`HKDF(ikm, info) → k`	PRF/KDF函数
`HMAC(key, msg) → tag`	MAC函数
`H(msg) → digest`	哈希函数
`Commit(v, r) → C`	承诺函数
`Open(C, v, r)`	承诺等式

参考references/crypto-to-proverif-mapping.md获取每个操作对应的准确ProVerif语法。

Step 3: Declare Types, Functions, and Equations

步骤3：声明类型、函数和等式

Build the cryptographic preamble in this order:

Types — declare custom types used to distinguish key material:

proverif

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

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

proverif

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

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

proverif

(* 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.

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

proverif

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.

按以下顺序构建密码学前言部分：

类型——声明用于区分密钥材料的自定义类型：

proverif

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

常量——用于作为域分隔符或标签的固定字符串：

proverif

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

函数——构造函数和析构函数。析构函数使用内联
```
reduc
```
，以便验证或解密失败时进程中止：

proverif

(* 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.

等式——仅针对构造函数的代数恒等式（不适用于析构函数，析构函数已经有内联的重写规则）：

proverif

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

仅声明图中实际使用的内容，不要为不存在的操作添加函数。

Step 4: Identify and Declare Events

步骤4：识别并声明事件

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.

proverif

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.

事件标记协议执行中与安全相关的时刻，通过以下方式提取：

开始事件（
```
event beginRole(params)
```
）：在参与方发送依赖于长期身份承诺的消息前立即触发（例如，在发送签名消息或MAC消息之前）。
结束事件（
```
event endRole(params)
```
）：在参与方成功验证对端身份后立即触发（例如，
```
Verify(...)
```
或MAC检查通过、会话密钥确认之后）。
保密性标记：握手后应该对攻击者保密的所有密钥或临时值。

proverif

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).

参数应能唯一标识会话：参与方的公钥，加上会话密钥或转录哈希。

Step 5: Formulate Security Queries

步骤5：制定安全查询

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:

proverif

(* 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:

proverif

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):

proverif

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):

proverif

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.

每个安全属性对应一个查询，可从以下类型中选择：

可达性（始终优先添加——结构合理性检查）：

验证成功事件实际可达。如果ProVerif报告其中任何一个为

false

，说明模型存在结构错误（死接收、类型不匹配、不可能的守卫条件），其他查询结果都不可信。模型验证通过后，如果这些查询拖慢了主属性检查的速度，可以将其注释掉：

proverif

(* 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)).
*)

保密性（攻击者无法推导密钥）：

声明一个私有自由名称，并使用会话密钥加密。攻击者获取到

private_I

等价于破解了会话密钥：

proverif

free private_I: bitstring [private].

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

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

弱认证（如果B接受了会话，说明A在某个时刻使用匹配参数运行了协议——无法防止重放）：

proverif

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

单射认证（防止重放——每个B的接受对应一次唯一的A运行）：

proverif

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

前向保密性：在主进程中添加

ForwardSecrecyTest

进程，将两个长期私钥泄露给攻击者，然后检查过往会话密钥是否仍然保密。配合

free fs_witness: key [private]

声明和

query attacker(fs_witness)

使用。参考references/security-properties.md → 前向保密性部分，以及

examples/simple-handshake/sample-output.pv

中的示例。

为每个属性选择适用的最强查询。参考references/security-properties.md获取完整的决策树。

Step 6: Write Participant Processes

步骤6：编写参与方进程

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:

proverif

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.

每个参与方对应一个

let

进程，每个进程的结构要逐步骤对应Mermaid图的顺序。

两方协议模板：

proverif

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)).

编写进程的规则：

图中每个
```
A ->> B: msg_contents
```
对应：
- A进程中的
```
out(c, msg_contents)
```
- B进程中的
```
in(c, x)
```
  （带有匹配的解构）

每个

Note over A: op → result

对应一个

let result = op in

绑定

每个
```
Note over A: Verify(...)
```
对应一个
```
let _ = verify(...) in
```
绑定（析构函数在失败时中止——不需要显式的else分支，对应中止逻辑）
图中的
```
alt
```
块对应进程中的
```
if/then/else
```
长期密钥是进程参数；临时值使用
```
new
```
声明

**N方或MPC协议：**每个不同角色对应一个进程。对于门限协议，编写单个角色进程，然后在主进程中复制

!N

次。

Step 7: Write Main Process and Finalize

步骤7：编写主进程并完成收尾

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

proverif

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 *)

主进程：

使用
```
new
```
生成长期密钥
通过
```
out(c, pk(sk))
```
将公钥发布给攻击者
在复制（
```
!
```
）下并行运行参与方进程，以支持多会话
可选地泄露长期密钥用于前向保密性分析

proverif

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)
    )

完整文件的内容顺序：

(* 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

步骤8：验证并交付

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

x3dh-key-agreement.pv

After writing, print a brief summary:

Protocol:   <Name>
Output:     <filename>
Queries:    <list each query and what property it tests>
Assumptions: <list modeling decisions and simplifications>

编写文件前：

图中的每个参与方都有对应的
```
let
```
进程
每个
```
out(c, ...)
```
在对端都有匹配的、类型兼容的
```
in(c, ...)
```
进程中使用的每个函数都在前言部分声明
每个析构函数都使用内联
```
reduc
```
（不是单独的
```
equation
```
块）
查询中的每个事件都已声明并在进程中触发
长期公钥在主进程中输出到信道
```
c
```
（攻击者可以看到它们——这是Dolev-Yao模型）
没有未使用的声明（清理所有试探性添加的内容）
如果存在
```
table
```
声明：每个
```
insert T(...)
```
都有对应的
```
get T(...)
```
，列类型兼容，模式约束匹配（
```
=key
```
vs 裸名称）
如果使用了
```
noselect
```
：它的元组结构与信道
```
c
```
上发送的实际消息形状匹配（例如，成对消息 →
```
mess(c, (x, y))
```
）

如果使用了密钥泄露预言机模式：已声明

event key_exposed(sk_type)

，持有密钥的进程末尾有预言机

in(c, guess: sk_type); if pk(guess) = pk_new then event key_exposed(guess)

，且查询为

query x: sk_type; event(key_exposed(x))

将模型写入
.pv
文件。文件名使用协议名称，例如

noise-xx-handshake.pv

或

x3dh-key-agreement.pv

。

编写完成后，打印简短摘要：

Protocol:   <Name>
Output:     <filename>
Queries:    <list each query and what property it tests>
Assumptions: <list modeling decisions and simplifications>

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.

├─ 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.

examples/simple-handshake/

目录包含完整示例：

diagram.md
——两方认证密钥交换的Mermaid sequenceDiagram（X25519 DH + Ed25519签名 + HKDF）
sample-output.pv
——本skill应该生成的准确ProVerif模型，包含保密性和单射认证查询

处理不熟悉的协议前先学习该示例。

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

references/crypto-to-proverif-mapping.md——Mermaid密码标注到ProVerif函数声明、等式和进程模式的映射表
references/proverif-syntax.md——ProVerif语言参考：类型、函数、等式、进程、事件、查询和常见陷阱
references/security-properties.md——查询选择决策指南：保密性、认证性（弱 vs 单射）、前向保密性、不可链接性以及建模方法