mermaid-to-proverif

Mermaid 转 ProVerif

读取描述加密协议的 Mermaid sequenceDiagram，生成可直接传递给 ProVerif 验证器的 ProVerif 模型（.pv 文件）。

使用的工具： 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 model.pv

拒绝理由

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

工作流程

ProVerif 模型进度：
- [ ] 步骤 1：解析参与者和通道
- [ ] 步骤 2：盘点加密操作
- [ ] 步骤 3：声明类型、函数和方程
- [ ] 步骤 4：识别并声明事件
- [ ] 步骤 5：制定安全查询
- [ ] 步骤 6：编写参与者进程
- [ ] 步骤 7：编写主进程并最终确定
- [ ] 步骤 8：验证并交付

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

从 Mermaid 图中：

提取每个 participant 或 actor 声明。每个对应一个 ProVerif 进程。
统计消息箭头（->>、-->>、-x、--x）。每个不同的 A ->> B: label 在通道上创建一个通信步骤。
决定通道模型：
- 公共通道 用于在安全通道建立之前通过网络发送的任何消息（例如 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：声明类型、函数和方程

按以下顺序构建加密前导：

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

type key.
type pkey.   (* 公钥 *)
type skey.   (* 私钥 *)
type nonce.

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

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

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

(* 非对称加密 *)
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.

(* 对称加密 / 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.

(* 数字签名——验证成功时返回消息，失败时中止 *)
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——第一个参数是密钥（来自 DH），第二个是 bitstring（信息/上下文） *)
fun hkdf(key, bitstring): key.

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

(* 哈希 *)
fun hash(bitstring): bitstring.

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

(* 序列化——ProVerif 是强类型的：pkey 不能出现在需要 bitstring 的地方。使用这些来构建签名负载。 *)
fun pkey2bs(pkey): bitstring.
fun concat(bitstring, bitstring): bitstring.

方程——仅针对构造器的代数恒等式（析构器已有内联重写规则）：

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 检查通过后，会话密钥确认）。
机密性标记：握手后应保持对攻击者未知的任何密钥或 nonce。

event beginI(pkey, pkey).     (* pk_I, pk_R——在发送签名消息前触发 *)
event endI(pkey, pkey, key).  (* pk_I, pk_R, session_key——在接受后触发 *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).

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

步骤 5：制定安全查询

每个安全属性编写一个查询。从以下选择：

可达性（始终先添加——结构完整性检查）：

验证成功事件是否实际可达。如果 ProVerif 报告其中任何一个为 false，则模型存在结构错误（死接收、类型不匹配、不可能守卫），不应信任任何其他查询结果。一旦模型验证通过，如果它们减慢主要属性检查的速度，可以将其注释掉：

(* 完整性检查：两个端点必须可达——验证后注释掉。 *)
(*
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].

(* 在进程中，推导出 sk_session 后： *)
out(c, aead_enc(private_I, sk_session));

(* 查询： *)
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 进程，将两个长期私钥泄露给攻击者，然后检查过去的会话密钥是否仍然保密。配合声明 free fs_witness: key [private] 和 query attacker(fs_witness)。参见 references/security-properties.md → 前向安全性，以及 examples/simple-handshake/sample-output.pv 中的工作示例。

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

步骤 6：编写参与者进程

每个参与者编写一个 let 进程。将每个进程结构化为逐步镜像 Mermaid 图，按顺序。

两方协议模板：

let Initiator(sk_I: skey, pk_R: pkey) =
    (* 步骤：生成临时密钥 *)
    new ek_I: skey;
    let epk_I = dhpk(ek_I) in
    (* 步骤：签名并发送 msg1——pkey2bs 将 pkey 转换为 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));
    (* 步骤：接收 msg2 *)
    in(c, (epk_R: pkey, sig_R: bitstring));
    (* 步骤：验证响应者签名——析构器在失败时中止 *)
    let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in
    let _ = verify(sig_R, concat(msg2_label, transcript), pk_R) in
    (* 步骤：派生会话密钥 *)
    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);
    (* 机密性见证：在会话密钥下加密 private_I。
     * 声明为：free private_I: bitstring [private]。
     * 查询 attacker(private_I) 检查攻击者无法推导出它。 *)
    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：编写主进程并最终确定

主进程：

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

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. 通道声明（free c: channel. / free ch: channel [private].） *)
(* 2. noselect 指令（如果需要终止） *)
(* 3. 类型声明 *)
(* 4. 常量 *)
(* 5. 函数声明 *)
(* 6. 方程（仅构造器的代数恒等式） *)
(* 7. 表声明 *)
(* 8. 事件 *)
(* 9. 查询 *)
(* 10. Let 进程 *)
(* 11. 主进程 *)

步骤 8：验证并交付

在写入文件之前：

[ ] 图中的每个参与者都有一个匹配的 let 进程
[ ] 每个 out(c, ...) 在另一侧都有一个匹配的 in(c, ...)，类型兼容
[ ] 进程中使用的每个函数都在前导中声明
[ ] 每个析构器使用内联 reduc（而不是单独的 equation 块）
[ ] 查询中的每个事件都已声明并在进程中触发
[ ] 长期公钥在主进程中输出到通道 c（攻击者可以看到它们——这是 Dolev-Yao 模型）
[ ] 没有未使用的声明（清理任何推测性添加的内容）
[ ] 如果存在 table 声明：每个 insert T(...) 都有对应的 get T(...)，列类型兼容且模式约束匹配（=key 与裸名称）
[ ] 如果使用了 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。

写入后，打印简要摘要：

协议：   <名称>
输出：     <文件名>
查询：    <列出每个查询及其测试的属性>
假设：    <列出建模决策和简化>

决策树

├─ 没有提供 Mermaid 图？
│  └─ 询问用户：“请提供 Mermaid sequenceDiagram，
│     或先运行 crypto-protocol-diagram 技能。”
│
├─ 图使用 DH（不仅仅是对称加密）？
│  └─ 使用带交换律方程的 dh/dhpk
│     参见 references/crypto-to-proverif-mapping.md → DH 部分
│
├─ 图使用非对称签名（Sign/Verify）？
│  └─ 使用带内联 reduc 的 sign/verify（不是 equation）
│     verify 在成功时返回消息；let _ = verify(...) in 在失败时中止
│     区分签名密钥（skey）和验证密钥（pkey）
│
├─ 图有 "alt" 块（中止路径）？
│  └─ 仅建模为 if/then——else 分支中止（进程终止）
│     除非图中显示，否则不要添加 out(c, error_message)
│
├─ 协议有 N > 2 方？
│  └─ 每个角色编写一个进程，使用 ! 进行复制
│     如果角色仅按索引区分，则将参与者索引作为参数传递
│
├─ 请求前向安全性？
│  └─ 在主进程中添加 ForwardSecrecy 变体，在会话后泄露
│     长期 sk；为过去的 session_key 添加机密性查询
│     参见 references/security-properties.md → 前向安全性
│
├─ 类型检查器拒绝模型？
│  └─ ProVerif 是类型化的：检查每个函数参数类型是否与声明匹配。
│     bitstring 是通用类型；key/pkey/skey/nonce 更严格。
│     必要时使用显式构造器进行转换。
│
├─ 协议有跨进程状态协调（例如，一个进程必须等待
│  另一个记录接受才能继续）？
│  └─ 使用 ProVerif 表（table/insert/get）
│     参见 references/proverif-syntax.md → 表
│
├─ 验证几分钟后不终止？
│  └─ 添加与 c 上消息元组结构匹配的 noselect 指令
│     参见 references/proverif-syntax.md → noselect
│
├─ 协议生成一个私有类型密钥（type sk [private]），该密钥从未
│  直接输出，但其机密性应被验证？
│  └─ 使用密钥暴露预言机模式而不是 query attacker(sk)
│     参见 references/security-properties.md → 密钥暴露预言机
│
└─ 不确定要验证哪些安全属性？
   └─ 默认集合：会话密钥机密性 + 单射认证
      （双向）。如果图显示临时密钥，则添加前向安全性。

示例

examples/simple-handshake/ 包含一个工作示例：

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

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

支持文档

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

你可能还喜欢

security-and-hardening

77Ksecurity

强化代码以抵御漏洞。适用于处理用户输入、身份验证、数据存储或外部集成时。适用于构建任何接受不可信数据、管理用户会话或与第三方服务交互的功能。

addyosmani

获取

api-security-best-practices

43Ksecurity

实现安全的API设计模式，包括身份验证、授权、输入验证、速率限制以及防范常见API漏洞

sickn33

获取

security-review

37Ksecurity

AI驱动的代码库安全扫描器，像安全研究员一样推理代码——追踪数据流、理解组件交互、捕捉模式匹配工具遗漏的漏洞。当被要求扫描代码安全漏洞、查找错误、检查SQL注入、XSS、命令注入、暴露的API密钥、硬编码密钥、不安全的依赖、访问控制问题，或任何类似“我的代码安全吗？”、“审查安全问题”、“审计此代码库”或“检查漏洞”的请求时，使用此技能。涵盖JavaScript、TypeScript、Python、Java、PHP、Go、Ruby和Rust中的注入缺陷、身份验证和访问控制错误、密钥暴露、弱加密、不安全的依赖以及业务逻辑问题。

github

获取

继续探索

浏览 security 热门 Skills 最近更新