mermaid-to-proverif

Mermaid 转 ProVerif

读取描述加密协议的 Mermaid sequenceDiagram，并生成 ProVerif 模型（.pv 文件），可直接交由 ProVerif 验证器处理。

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

典型输入是 crypto-protocol-diagram 技能的输出——一个带有加密操作（Sign、Verify、DH、HKDF、Enc、Dec 等）和消息箭头注释的 Mermaid sequenceDiagram。

适用场景

• 用户要求对以 Mermaid sequenceDiagram 描述的加密协议进行形式化验证
• 用户想根据协议图生成 ProVerif 模型（.pv 文件）
• 用户想证明保密性、认证或前向保密属性
• 输入是 crypto-protocol-diagram 技能的输出

不适用场景

• 尚无 Mermaid sequenceDiagram——请先使用 crypto-protocol-diagram 生成一个
• 用户想验证非加密系统（状态机、访问控制）的属性
• 用户想对现有 .pv 文件运行 ProVerif——直接运行 proverif model.pv 即可

应拒绝的错误理由

错误理由	错在哪里	必须采取的操作
“可达性查询只是无用功”	如果事件不可达，其他所有查询结果都没有意义	始终先添加可达性查询，作为合理性检查
“所有消息都使用公共信道也没问题”	使用私有信道传递内部状态可以避免虚假攻击	使用私有信道传递进程内状态
“我会跳过前向保密测试”	临时密钥需要进行前向保密验证	只要图中显示了临时密钥，就添加 ForwardSecrecyTest 进程
“未使用的声明没有危害”	ProVerif 可能会因孤立声明报告虚假结果	清理所有未使用的类型、函数和事件
“模型能编译就说明没问题”	能编译的模型仍可能存在无效接收、类型不匹配或不可能满足的守卫条件，导致查询平凡地为真	在相信任何安全性查询之前，先验证可达性
“我不需要先检查示例”	示例定义了预期输出的质量标准	在处理不熟悉的协议前，先研究 examples/simple-handshake/

---

工作流

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

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

根据 Mermaid 图：

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

free c: channel.

步骤 2：盘点密码学操作

逐一检查每条 Note over 注释和消息标签，列出所有不同的操作。将每项操作映射到 ProVerif 声明类别：

Mermaid 注释	ProVerif 类别
keygen() → sk, pk	新名称（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 语法。

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

按以下顺序构建密码学前置声明：

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

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

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

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

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

(* 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. 等式 — 仅针对构造函数的代数恒等式（析构函数已有内联重写规则，因此不需要为其声明等式）：

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

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

步骤 4：识别并声明事件

事件标记协议执行中与安全相关的时刻。通过识别以下内容提取事件：

• 开始事件（event beginRole(params)）：在一方发送依赖于长期身份承诺的消息之前立即触发（例如，在发送已签名消息或带 MAC 的消息之前）。
• 结束事件（event endRole(params)）：在一方成功验证对等方身份后立即触发（例如，在 Verify(...) 或 MAC 检查通过、会话密钥得到确认后）。
• 保密性标记：握手结束后仍应对攻击者保密的任何密钥或随机数。

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

参数应能唯一标识会话：双方的公钥，以及会话密钥或转录哈希。

第 5 步：编写安全查询

针对每项安全属性编写一个查询。可从以下选项中选择：

可达性（始终首先添加——结构健全性检查）：

验证成功事件是否确实可达。当事件可达时，ProVerif 会输出 RESULT not event(endR(...)) is false，这正是你想要的结果。如果输出 is true，则表示事件从未触发：模型存在结构性错误（死接收、类型不匹配、不可能的守卫条件），不能信任其他查询结果。模型 验证通过后，如果这些检查拖慢了主要属性检查，可将它们注释掉：

(* 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 等同于破解了会话密钥：

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 曾在某个时刻使用匹配的 参数运行——无法防止重放）：

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

注入式认证（防止重放——每次 B 接受都对应一次不同的 A 运行）：

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 进程，在会话结束后（在 phase 1 中）将两个长期密钥泄露给攻击者，然后检查过去的会话密钥是否仍然保密。配合 free fs_witness: key [private] 声明和 query attacker(fs_witness) 一起使用。参见 references/security-properties.md → 前向保密性。

针对每项属性，选择适用的最强查询。完整的决策树请参见 references/security-properties.md。

第 6 步：编写参与方进程

为每个参与方编写一个 let 进程。每个进程都应按顺序逐步对应 Mermaid 图。

双方协议模板：

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 次。

第 7 步：编写主进程并完成

主进程：

1. 使用 new 生成长期密钥
2. 通过 out(c, pk(sk)) 向攻击者公开公钥
3. 在复制（!）下并行运行参与方进程，以允许多个会话
4. 可选地泄露长期密钥以分析前向保密性

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

步骤 8：验证并交付

写入文件前：

• 图中的每个参与方都有对应的 let 进程
• 每个 out(c, ...) 在另一侧都有类型兼容的 in(c, ...)
• 进程中使用的每个函数都在前言中声明
• 每个析构函数都使用内联 reduc（而非单独的 equation 块）
• 查询中的每个事件都已声明，并在进程中触发
• 主进程会将长期公钥输出到通道 c（攻击者可以看到它们——这就是 Dolev-Yao 模型）
• 没有未使用的声明（清理任何推测性添加的内容）
• 如果存在 table 声明：每个 insert T(...) 都有对应的 get T(...)，且列类型兼容、模式约束相匹配（=key 与裸名称）
• 如果使用了 noselect：其元组结构与通过 c 发送的实际消息形状相符（例如，成对数据 → mess(c, (x, y))）
• 如果使用了 Key Exposure Oracle 模式：已声明 event key_exposed(sk_type)，持有机密的进程末尾包含 oracle 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>

---

决策树

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

---

示例

examples/simple-handshake/ 包含一个完整示例：

• diagram.md — Mermaid sequenceDiagram，展示双方认证的密钥交换（X25519 DH + Ed25519 签名 + HKDF）
• sample-output.pv — 该技能应生成的确切 ProVerif 模型，包含保密性和注入式认证查询。其 Q3（从 R 的视角进行注入式认证）报告 false：图示协议没有响应方质询，因此重放的 msg1 会完成另一次 R 运行。这是对协议的真实发现，而不是建模错误。

在着手处理不熟悉的协议前，请先研读此示例。

---

支持文档

• references/crypto-to-proverif-mapping.md — Mermaid 加密注释到 ProVerif 函数声明、方程和进程模式的映射表
• references/proverif-syntax.md — ProVerif 语言参考：类型、函数、方程、进程、事件、查询和常见陷阱
• references/security-properties.md — 用于选择合适查询的决策指南：保密性、认证（弱认证与注入式认证）、前向保密性及其建模方式