crypto-protocol-diagram

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Crypto Protocol Diagram

密码协议示意图

Produces a Mermaid

sequenceDiagram

(written to file) and an ASCII sequence diagram (printed inline) from either:

Source code implementing a cryptographic protocol, or
A specification — RFC, academic paper, pseudocode, informal prose, ProVerif (
```
.pv
```
), or Tamarin (
```
.spthy
```
) model.

Tools used: Read, Write, Grep, Glob, Bash, WebFetch (for URL specs).

Unlike the

diagramming-code

skill (which visualizes code structure), this skill extracts protocol semantics: who sends what to whom, what cryptographic transformations occur at each step, and what protocol phases exist.

For call graphs, class hierarchies, or module dependency maps, use the

diagramming-code

skill instead.

可基于以下任意一种输入生成Mermaid

sequenceDiagram

（写入文件）和ASCII时序图（在响应中直接输出）：

实现密码协议的源代码，或
规范文档——RFC、学术论文、伪代码、非正式文本、ProVerif（
```
.pv
```
）或Tamarin（
```
.spthy
```
）模型。

使用工具： Read、Write、Grep、Glob、Bash、WebFetch（用于处理URL形式的规范）。

和用于可视化代码结构的

diagramming-code

技能不同，本技能提取的是协议语义：谁向谁发送了什么内容、每个步骤执行了哪些密码学转换，以及包含哪些协议阶段。

如果需要生成调用图、类层次结构或模块依赖映射，请使用

diagramming-code

技能。

When to Use

适用场景

User asks to diagram, visualize, or extract a cryptographic protocol
Input is source code implementing a handshake, key exchange, or multi-party protocol
Input is an RFC, academic paper, pseudocode, or formal model (ProVerif/Tamarin)
User names a specific protocol (TLS, Noise, Signal, X3DH, FROST)

用户要求绘制、可视化或提取密码协议信息
输入内容为实现握手、密钥交换或多方协议的源代码
输入内容为RFC、学术论文、伪代码或形式化模型（ProVerif/Tamarin）
用户指定了具体协议（TLS、Noise、Signal、X3DH、FROST）

When NOT to Use

不适用场景

User wants a call graph, class hierarchy, or module dependency map — use
```
diagramming-code
```
User wants to formally verify a protocol — use
```
mermaid-to-proverif
```
(after generating the diagram)
Input has no cryptographic protocol semantics (no parties, no message exchange)

用户需要调用图、类层次结构或模块依赖映射——请使用
```
diagramming-code
```
用户需要对协议进行形式化验证——请先生成示意图，再使用
```
mermaid-to-proverif
```
输入内容不包含密码协议语义（无参与方、无消息交换）

Rationalizations to Reject

拒绝理由说明

Rationalization	Why It's Wrong	Required Action
"The protocol is simple, I can diagram from memory"	Memory-based diagrams miss steps and invert arrows	Read the source or spec systematically
"I'll skip the spec path since code exists"	Code may diverge from the spec — both paths catch different bugs	When both exist, run spec workflow first, then annotate code divergences
"Crypto annotations are optional decoration"	Without crypto annotations, the diagram is just a message flow — useless for security review	Annotate every cryptographic operation
"The abort path is obvious, no need for alt blocks"	Implicit abort handling hides missing error checks	Show every abort/error path with `alt` blocks
"I don't need to check the examples first"	The examples define the expected output quality bar	Study the relevant example before working on unfamiliar input
"ProVerif/Tamarin models are code, not specs"	Formal models are specifications — they describe intended behavior, not implementation	Use the spec workflow (S1–S5) for `.pv` and `.spthy` files

拒绝理由	错误原因	所需操作
"这个协议很简单，我凭记忆就能画出来"	基于记忆绘制的示意图会遗漏步骤、箭头方向倒置	系统地阅读源代码或规范文档
"既然有代码，我就不看规范了"	代码可能与规范存在差异——两种路径能发现不同的问题	如果两者都存在，先运行规范工作流，再标注代码与规范的差异
"密码学注解是可选的装饰内容"	没有密码学注解的示意图只是单纯的消息流，对安全审查毫无用处	为每一个密码学操作添加注解
"中止路径很明显，不需要用alt块标注"	隐式的中止处理会隐藏缺失的错误检查	使用 `alt` 块展示所有中止/错误路径
"我不需要先看示例"	示例定义了预期的输出质量标准	处理不熟悉的输入前，先学习相关示例
"ProVerif/Tamarin模型是代码，不是规范"	形式化模型属于规范——它们描述的是预期行为，而非实现	对 `.pv` 和 `.spthy` 文件使用规范工作流（S1–S5）

Workflow

工作流

Protocol Diagram Progress:
- [ ] Step 0: Determine input type (code / spec / both)
- [ ] Step 1 (code) or S1–S5 (spec): Extract protocol structure
- [ ] Step 6: Generate sequenceDiagram
- [ ] Step 7: Verify and deliver

协议示意图绘制进度：
- [ ] 步骤0：确定输入类型（代码/规范/两者都有）
- [ ] 步骤1（代码）或S1–S5（规范）：提取协议结构
- [ ] 步骤6：生成sequenceDiagram
- [ ] 步骤7：验证并交付

Step 0: Determine Input Type

步骤0：确定输入类型

Before doing anything else, classify the input:

Signal	Input type
Source file extensions ( `.py` , `.rs` , `.go` , `.ts` , `.js` , `.cpp` , `.c` )	Code
Function/class definitions, import statements	Code
RFC-style section headers ( `§` , `Section X.Y` , `MUST` / `SHALL` keywords)	Spec
`Algorithm` / `Protocol` / `Figure` labels, mathematical notation	Spec
ProVerif file ( `.pv` ) with `process` , `let` , `in` / `out`	Spec
Tamarin file ( `.spthy` ) with `rule` , `--[...]->`	Spec
Plain prose or numbered steps describing a protocol	Spec
Both source files and a spec document	Both (annotate divergences with `⚠️` )

Code only → skip to Step 1 below
Spec only → skip to Spec Workflow (S1–S5) below
Both → run Spec Workflow first, then use the code-reading steps to verify the implementation against the spec diagram and annotate any divergences with
```
⚠️
```
Ambiguous → ask the user: "Is this a source code file, a specification document, or both?"

在执行任何操作前，先对输入进行分类：

特征	输入类型
源文件扩展名（ `.py` 、 `.rs` 、 `.go` 、 `.ts` 、 `.js` 、 `.cpp` 、 `.c` ）	代码
函数/类定义、import语句	代码
RFC风格的章节标题（ `§` 、 `Section X.Y` 、 `MUST` / `SHALL` 关键词）	规范
`Algorithm` / `Protocol` / `Figure` 标签、数学符号	规范
包含 `process` 、 `let` 、 `in` / `out` 的ProVerif文件（ `.pv` ）	规范
包含 `rule` 、 `--[...]->` 的Tamarin文件（ `.spthy` ）	规范
描述协议的纯文本或编号步骤	规范
同时提供源文件和规范文档	两者都有（用 `⚠️` 标注差异）

仅代码 → 直接跳转到下方步骤1
仅规范 → 直接跳转到下方规范工作流（S1–S5）
两者都有 → 先运行规范工作流，再使用代码读取步骤对照规范示意图验证实现，并用
```
⚠️
```
标注所有差异
类型不明确 → 询问用户："这是源代码文件、规范文档，还是两者都有？"

Step 1: Locate Protocol Entry Points

步骤1：定位协议入口点

Grep for function names, type names, and comments that reveal the protocol:

bash

undefined

使用Grep查找能体现协议特征的函数名、类型名和注释：

bash

undefined

Find handshake, session, round, phase entry points

查找握手、会话、轮次、阶段入口点

rg -l "handshake|session_init|round[_0-9]|setup|keygen|send_msg|recv_msg" {targetDir}

Find crypto primitives in use

查找使用的密码学原语

rg "sign|verify|encrypt|decrypt|dh|ecdh|kdf|hkdf|hmac|hash|commit|reveal|share"
{targetDir} --type-add 'src:*.{py,rs,go,ts,js,cpp,c}' -t src -l


Start reading from the highest-level orchestration function — the one that calls
into handshake phases or the main protocol loop.

rg "sign|verify|encrypt|decrypt|dh|ecdh|kdf|hkdf|hmac|hash|commit|reveal|share"
{targetDir} --type-add 'src:*.{py,rs,go,ts,js,cpp,c}' -t src -l


从最高层的编排函数开始阅读——也就是调用握手阶段或主协议循环的函数。

Step 2: Identify Parties and Roles

步骤2：识别参与方和角色

Extract participant names from:

Struct/class names:

Client

Server

Initiator

Responder

Prover

Verifier

Dealer

Party

Coordinator

Function parameter names that carry state for a role
Comments declaring the protocol role
Test fixtures that set up two-party or N-party scenarios

Map these to Mermaid

participant

declarations. Use short, readable aliases:

participant I as Initiator
participant R as Responder

从以下位置提取参与者名称：

结构体/类名：

Client

、

Server

、

Initiator

、

Responder

、

Prover

、

Verifier

、

Dealer

、

Party

、

Coordinator

承载角色状态的函数参数名
声明协议角色的注释
配置两方或多方场景的测试用例

将这些映射为Mermaid的

participant

声明，使用简短易读的别名：

participant I as Initiator
participant R as Responder

Step 3: Trace Message Flow

步骤3：追踪消息流

Follow state transitions and network sends/receives. Look for patterns like:

Pattern	Meaning
`send(msg)` / `recv()`	Direct message exchange
`serialize` + `transmit`	Structured message sent
Return value passed to other party's function	Logical message (in-process)
`round1_output` → `round2_input`	Round-based MPC step
Struct fields named `ephemeral_key` , `ciphertext` , `mac` , `tag`	Message contents

For in-process protocol implementations (where both parties run in the same process), treat function call boundaries as logical message sends when they represent what would be a network boundary in deployment.

跟踪状态转换和网络收发操作，查找以下模式：

模式	含义
`send(msg)` / `recv()`	直接消息交换
`serialize` + `transmit`	发送结构化消息
传递给另一方函数的返回值	逻辑消息（进程内）
`round1_output` → `round2_input`	基于轮次的MPC步骤
名为 `ephemeral_key` 、 `ciphertext` 、 `mac` 、 `tag` 的结构体字段	消息内容

对于进程内的协议实现（双方运行在同一进程中），如果函数调用边界对应部署时的网络边界，将其视为逻辑消息发送。

Step 4: Annotate Cryptographic Operations

步骤4：标注密码学操作

At each protocol step, identify and label:

Operation	Diagram annotation
Key generation	`Note over A: keygen(params) → pk, sk`
DH / ECDH	`Note over A,B: DH(sk_A, pk_B)`
KDF / HKDF	`Note over A: HKDF(ikm, salt, info)`
Signing	`Note over A: Sign(sk, msg) → σ`
Verification	`Note over B: Verify(pk, msg, σ)`
Encryption	`Note over A: Enc(key, plaintext) → ct`
Decryption	`Note over B: Dec(key, ct) → plaintext`
Commitment	`Note over A: Commit(value, rand) → C`
Hash	`Note over A: H(data) → digest`
Secret sharing	`Note over D: Share(secret, t, n) → {s_i}`
Threshold combine	`Note over C: Combine({s_i}) → secret`

Keep annotations concise — use mathematical shorthand, not code.

在每个协议步骤中，识别并标记以下操作：

操作	示意图注解
密钥生成	`Note over A: keygen(params) → pk, sk`
DH / ECDH	`Note over A,B: DH(sk_A, pk_B)`
KDF / HKDF	`Note over A: HKDF(ikm, salt, info)`
签名	`Note over A: Sign(sk, msg) → σ`
验签	`Note over B: Verify(pk, msg, σ)`
加密	`Note over A: Enc(key, plaintext) → ct`
解密	`Note over B: Dec(key, ct) → plaintext`
承诺	`Note over A: Commit(value, rand) → C`
哈希	`Note over A: H(data) → digest`
秘密共享	`Note over D: Share(secret, t, n) → {s_i}`
阈值合并	`Note over C: Combine({s_i}) → secret`

保持注解简洁——使用数学简写，而非代码。

Step 5: Identify Protocol Phases

步骤5：识别协议阶段

Group message steps into named phases using

rect

Note

blocks:

Common phases to detect:

Setup / Key Generation: party key creation, trusted setup, parameter gen
Handshake / Init: ephemeral key exchange, nonce exchange, version negotiation
Authentication: identity proof, certificate exchange, signature verification
Key Derivation: session key derivation from shared secrets
Data Transfer / Main Protocol: encrypted application data exchange
Finalization / Teardown: session close, MAC verification, abort handling

Detect abort/error paths and show them with

alt

blocks.

使用

rect

或

Note

块将消息步骤分组为命名阶段：

常见可识别的阶段：

设置/密钥生成：参与方密钥创建、可信设置、参数生成
握手/初始化：临时密钥交换、随机数交换、版本协商
认证：身份证明、证书交换、签名验证
密钥派生：从共享秘密派生会话密钥
数据传输/主协议：加密应用数据交换
收尾/销毁：会话关闭、MAC验证、中止处理

识别中止/错误路径，使用

alt

块展示。

Spec Workflow (S1–S5)

规范工作流（S1–S5）

Use this path when the input is a specification document rather than source code. After completing S1–S5, continue with Step 6 (Generate sequenceDiagram) and Step 7 (Verify and deliver) from the code workflow above.

当输入是规范文档而非源代码时使用此路径。完成S1–S5后，继续执行上述代码工作流中的步骤6（生成sequenceDiagram）和步骤7（验证并交付）。

Step S1: Ingest the Spec

步骤S1：读取规范

Obtain the full spec text:

File path provided → read with the Read tool
URL provided → fetch with WebFetch
Pasted inline → work directly from conversation context

Then identify the spec format and read references/spec-parsing-patterns.md for format-specific extraction guidance:

Format	Signals
RFC	`RFC XXXX` , `MUST` / `SHALL` / `SHOULD` , ABNF grammars, section-numbered prose
Academic paper / pseudocode	`Algorithm X` , `Protocol X` , `Figure X` , numbered steps, `←` / `→` in math mode
Informal prose	Numbered lists, "A sends B ...", plain English descriptions
ProVerif ( `.pv` )	`process` , `let` , `in(ch, x)` , `out(ch, msg)` , `!` (replication)
Tamarin ( `.spthy` )	`rule` , `--[ ]->` , `Fr(~x)` , `!Pk(A, pk)` , `In(m)` , `Out(m)`

If the spec references a known named protocol (TLS, Noise, Signal, X3DH, Double Ratchet, FROST), also read references/protocol-patterns.md to use its canonical flow as a skeleton and fill in spec-specific details.

获取完整的规范文本：

提供了文件路径 → 使用Read工具读取
提供了URL → 使用WebFetch获取
直接粘贴在对话中 → 直接使用对话上下文内容

然后识别规范格式，阅读references/spec-parsing-patterns.md获取对应格式的提取指南：

格式	特征
RFC	`RFC XXXX` 、 `MUST` / `SHALL` / `SHOULD` 、ABNF语法、带章节编号的文本
学术论文/伪代码	`Algorithm X` 、 `Protocol X` 、 `Figure X` 、编号步骤、数学模式下的 `←` / `→`
非正式文本	编号列表、"A sends B ..."、纯英文描述
ProVerif（ `.pv` ）	`process` 、 `let` 、 `in(ch, x)` 、 `out(ch, msg)` 、 `!` （复制）
Tamarin（ `.spthy` ）	`rule` 、 `--[ ]->` 、 `Fr(~x)` 、 `!Pk(A, pk)` 、 `In(m)` 、 `Out(m)`

如果规范引用了已知的命名协议（TLS、Noise、Signal、X3DH、Double Ratchet、FROST），还需要阅读references/protocol-patterns.md，将其标准流程作为骨架，填充规范特有的细节。

Step S2: Extract Parties and Roles

步骤S2：提取参与方和角色

Identify all protocol participants. Look for:

Named roles in prose or pseudocode:

Alice

Bob

Client

Server

Initiator

Responder

Prover

Verifier

Dealer

Party_i

Coordinator

Signer

Section headers: "Parties", "Roles", "Participants", "Setup", "Notation"
ProVerif: process names at top level (
```
let ClientProc(...)
```
,
```
let ServerProc(...)
```
)
Tamarin: rule names and fact arguments (e.g.
```
!Pk($A, pk)
```
—
```
$A
```
is a party)

Map each role to a Mermaid

participant

declaration. Use short IDs with descriptive aliases (see naming conventions in references/mermaid-sequence-syntax.md).

识别所有协议参与者，查找以下内容：

文本或伪代码中的命名角色：

Alice

、

Bob

、

Client

、

Server

、

Initiator

、

Responder

、

Prover

、

Verifier

、

Dealer

、

Party_i

、

Coordinator

、

Signer

章节标题："Parties"、"Roles"、"Participants"、"Setup"、"Notation"
ProVerif：顶层进程名（
```
let ClientProc(...)
```
、
```
let ServerProc(...)
```
）
Tamarin：规则名和事实参数（例如
```
!Pk($A, pk)
```
——
```
$A
```
是参与方）

将每个角色映射为Mermaid的

participant

声明，使用带描述性别名的短ID（参考references/mermaid-sequence-syntax.md中的命名规范）。

Step S3: Extract Message Flow

步骤S3：提取消息流

Trace what each party sends to whom and in what order. Extraction patterns by format:

RFC / informal prose:

Arrow notation:
```
A → B: msg
```
,
```
A -> B
```
Sentence patterns: "A sends B ...", "B responds with ...", "A transmits ...", "upon receiving X, B sends Y"
Numbered steps: extract in order, inferring sender/receiver from context

Pseudocode:

Function signatures with explicit
```
sender
```
/
```
receiver
```
parameters
```
send(party, msg)
```
/
```
receive(party)
```
calls
Return values passed as inputs to the other party's function in the next step

ProVerif (
.pv
):

```
out(ch, msg)
```
— send on channel
```
ch
```
```
in(ch, x)
```
— receive on channel
```
ch
```
, bind to
```
x
```
Match
```
out
```
/
```
in
```
pairs on the same channel to identify message flows
```
!
```
(replication) signals a role that handles multiple sessions

Tamarin (
.spthy
):

```
In(m)
```
premise — receive message
```
m
```
```
Out(m)
```
conclusion — send message
```
m
```
Rule name and ordering of rules reveal protocol rounds
```
Fr(~x)
```
— fresh random value generated by a party
```
--[ Label ]->
```
facts — security annotations, not messages

Preserve the ordering and round structure. Group concurrent sends (broadcast) using

par

blocks in the final diagram.

追踪每个参与方向谁发送了什么内容，以及发送顺序。不同格式的提取模式：

RFC/非正式文本：

箭头表示：
```
A → B: msg
```
、
```
A -> B
```
句式："A sends B ..."、"B responds with ..."、"A transmits ..."、"upon receiving X, B sends Y"
编号步骤：按顺序提取，根据上下文推断发送方/接收方

伪代码：

带有显式
```
sender
```
/
```
receiver
```
参数的函数签名
```
send(party, msg)
```
/
```
receive(party)
```
调用
下一步中作为另一方函数输入的返回值

ProVerif（
.pv
）：

```
out(ch, msg)
```
——在通道
```
ch
```
上发送消息
```
in(ch, x)
```
——在通道
```
ch
```
上接收消息，绑定到
```
x
```
匹配同一通道上的
```
out
```
/
```
in
```
对来识别消息流
```
!
```
（复制）表示处理多个会话的角色

Tamarin（
.spthy
）：

```
In(m)
```
前提——接收消息
```
m
```
```
Out(m)
```
结论——发送消息
```
m
```
规则名和规则顺序体现协议轮次
```
Fr(~x)
```
——参与方生成的新鲜随机值
```
--[ Label ]->
```
事实——安全注解，不是消息

保留顺序和轮次结构，在最终示意图中使用

par

块对并发发送（广播）进行分组。

Step S4: Extract Cryptographic Operations

步骤S4：提取密码学操作

For each protocol step, identify the cryptographic operations performed and which party performs them:

Spec notation	Operation	Diagram annotation
`keygen()` , `Gen(1^λ)`	Key generation	`Note over A: keygen() → pk, sk`
`DH(a, B)` , `g^ab`	DH / ECDH	`Note over A,B: DH(sk_A, pk_B)`
`KDF(ikm)` , `HKDF(...)`	Key derivation	`Note over A: HKDF(ikm, salt, info) → k`
`Sign(sk, m)` , `σ ← Sign`	Signing	`Note over A: Sign(sk, msg) → σ`
`Verify(pk, m, σ)`	Verification	`Note over B: Verify(pk, msg, σ)`
`Enc(k, m)` , `{m}_k`	Encryption	`Note over A: Enc(k, plaintext) → ct`
`Dec(k, c)`	Decryption	`Note over B: Dec(k, ct) → plaintext`
`H(m)` , `hash(m)`	Hash	`Note over A: H(data) → digest`
`Commit(v, r)` , `com`	Commitment	`Note over A: Commit(value, rand) → C`
ProVerif `senc(m, k)`	Symmetric encryption	`Note over A: Enc(k, m) → ct`
ProVerif `pk(sk)`	Public key derivation	`Note over A: pk = pk(sk)`
ProVerif `sign(m, sk)`	Signing	`Note over A: Sign(sk, m) → σ`

Identify security conditions and abort paths:

Prose: "if verification fails, abort", "only if ...", "reject if ..."
Pseudocode:
```
assert
```
,
```
require
```
,
```
if ... abort
```
ProVerif:
```
if m = expected then ... else 0
```
Tamarin: contradicting facts or restriction lemmas

These become

alt

blocks in the final diagram.

针对每个协议步骤，识别执行的密码学操作以及执行方：

规范符号	操作	示意图注解
`keygen()` 、 `Gen(1^λ)`	密钥生成	`Note over A: keygen() → pk, sk`
`DH(a, B)` 、 `g^ab`	DH / ECDH	`Note over A,B: DH(sk_A, pk_B)`
`KDF(ikm)` 、 `HKDF(...)`	密钥派生	`Note over A: HKDF(ikm, salt, info) → k`
`Sign(sk, m)` 、 `σ ← Sign`	签名	`Note over A: Sign(sk, msg) → σ`
`Verify(pk, m, σ)`	验签	`Note over B: Verify(pk, msg, σ)`
`Enc(k, m)` 、 `{m}_k`	加密	`Note over A: Enc(k, plaintext) → ct`
`Dec(k, c)`	解密	`Note over B: Dec(k, ct) → plaintext`
`H(m)` 、 `hash(m)`	哈希	`Note over A: H(data) → digest`
`Commit(v, r)` 、 `com`	承诺	`Note over A: Commit(value, rand) → C`
ProVerif `senc(m, k)`	对称加密	`Note over A: Enc(k, m) → ct`
ProVerif `pk(sk)`	公钥派生	`Note over A: pk = pk(sk)`
ProVerif `sign(m, sk)`	签名	`Note over A: Sign(sk, m) → σ`

识别安全条件和中止路径：

文本："if verification fails, abort"、"only if ..."、"reject if ..."
伪代码：
```
assert
```
、
```
require
```
、
```
if ... abort
```
ProVerif：
```
if m = expected then ... else 0
```
Tamarin：矛盾的事实或约束引理

这些内容在最终示意图中会成为

alt

块。

Step S5: Flag Spec Ambiguities

步骤S5：标记规范歧义

Before moving to Step 6, check for gaps:

Unclear message ordering: infer from round structure or section order; annotate with
```
⚠️ ordering inferred from spec structure
```
Implied parties: if a party's role is implied but unnamed, give it a descriptive name and note the inference
Missing steps: if the spec omits a step that the canonical pattern for this protocol requires, annotate:
```
⚠️ spec omits [step] — canonical protocol requires it
```
Underspecified crypto: if the spec says "encrypt" without specifying the scheme, annotate:
```
⚠️ encryption scheme not specified
```
ProVerif/Tamarin: private channels (
```
c
```
declared with
```
new c
```
or as a private free name) represent out-of-band channels — note them

进入步骤6前，检查是否存在信息缺口：

消息顺序不明确：根据轮次结构或章节顺序推断，标注
```
⚠️ ordering inferred from spec structure
```
隐含参与方：如果某个参与方的角色是隐含的但未命名，为其赋予描述性名称并标注推断说明
步骤缺失：如果规范省略了该协议标准模式要求的步骤，标注：
```
⚠️ spec omits [step] — canonical protocol requires it
```

Step 6: Generate sequenceDiagram

步骤6：生成sequenceDiagram

Produce Mermaid syntax following the rules in references/mermaid-sequence-syntax.md.

Completeness over brevity. Show every distinct message type. Omit repeated loop iterations (use

loop

blocks instead), but never omit a distinct protocol step.

Correctness over aesthetics. The diagram must match what the code actually does. If the code diverges from a known spec, annotate the divergence:

Note over A,B: ⚠️ spec requires MAC here — implementation omits it

遵循references/mermaid-sequence-syntax.md中的规则编写Mermaid语法。

完整性优先于简洁性：展示所有不同的消息类型。可省略重复的循环迭代（改用

loop

块），但绝对不能省略不同的协议步骤。

正确性优先于美观性：示意图必须与代码实际行为完全匹配。如果代码与已知规范存在差异，标注差异：

Note over A,B: ⚠️ spec requires MAC here — implementation omits it

Step 7: Verify and Deliver

步骤7：验证并交付

Before delivering:

Every participant declared actually sends or receives at least one message
Arrows point in the correct direction (sender → receiver)
Cryptographic operations are on the correct party (the one computing them)
If protocol phases are used, no arrows appear outside a phase block
```
alt
```
blocks cover known abort/error paths
Diagram renders without syntax errors (check references/mermaid-sequence-syntax.md for common pitfalls)
If spec divergence found, annotated with
```
⚠️
```

Write the diagram to a file. Choose a filename derived from the protocol name, e.g.

noise-xx-handshake.md

x3dh-key-agreement.md

. Write a Markdown file with this structure:

markdown

undefined

交付前检查：

所有声明的参与者都至少发送或接收过一条消息
箭头方向正确（发送方→接收方）
密码学操作标注在正确的参与方（执行操作的一方）上
如果使用了协议阶段，没有箭头出现在阶段块之外
```
alt
```
块覆盖了所有已知的中止/错误路径
示意图可正常渲染，无语法错误（参考references/mermaid-sequence-syntax.md中的常见问题）
如果发现与规范的差异，已用
```
⚠️
```
标注

将示意图写入文件：文件名从协议名称派生，例如

noise-xx-handshake.md

或

x3dh-key-agreement.md

。编写的Markdown文件结构如下：

markdown

undefined

<Protocol Name> Sequence Diagram

<协议名称> 时序图

```mermaid sequenceDiagram ... ```

Protocol Summary

协议摘要

Parties: ...
Round complexity: ...
Key primitives: ...
Authentication: ...
Forward secrecy: ...
Notable: [spec deviations or security observations, or "none"]


After writing the file, print an **ASCII sequence diagram** inline in the
response, followed by the Protocol Summary. State the output filename so the
user knows where to find the Mermaid source.

Follow all drawing conventions in
[references/ascii-sequence-diagram.md](references/ascii-sequence-diagram.md),
including the inline output format.

---

参与方： ...
轮次复杂度： ...
核心原语： ...
认证方式： ...
前向保密性： ...
注意事项： [规范偏差或安全观察，无则填"none"]


写入文件后，在响应中直接输出**ASCII时序图**，随后附上协议摘要。说明输出文件名，方便用户找到Mermaid源文件。

遵循[references/ascii-sequence-diagram.md](references/ascii-sequence-diagram.md)中的所有绘制规范，包括内联输出格式。

---

Decision Tree

决策树

── Input is a spec document (not code)?
│  └─ Step S1: identify format, read references/spec-parsing-patterns.md
│
── Input is source code (not a spec)?
│  └─ Step 1: grep for handshake/round/send/recv entry points
│
── Both spec and code provided?
│  └─ Run Spec Workflow (S1–S5) first to build canonical diagram,
│     then read code and annotate divergences with ⚠️
│
── Spec is a known protocol (TLS, Noise, Signal, X3DH, FROST)?
│  └─ Read references/protocol-patterns.md and use canonical flow as skeleton
│
── Spec is ProVerif (.pv) or Tamarin (.spthy)?
│  └─ Read references/spec-parsing-patterns.md → Formal Models section
│
── Spec message ordering is ambiguous?
│  └─ Infer from round/section structure, annotate with ⚠️
│
── Can't identify parties from spec?
│  └─ Check "Parties"/"Notation" sections; for ProVerif read process names;
│     for Tamarin read rule names and fact arguments
│
── Don't know which code files implement the protocol?
│  └─ Step 1: grep for handshake/round/send/recv entry points
│
── Can't identify parties from struct names?
│  └─ Read test files — test setup reveals roles
│
── Protocol runs in-process (no network calls)?
│  └─ Treat function argument passing at role boundaries as messages
│
── MPC / threshold protocol with N parties?
│  └─ Read references/protocol-patterns.md → MPC section
│
── Mermaid syntax error?
│  └─ Read references/mermaid-sequence-syntax.md → Common Pitfalls
│
└─ ASCII drawing conventions?
   └─ Read references/ascii-sequence-diagram.md

── 输入是规范文档（非代码）？
│  └─ 步骤S1：识别格式，阅读references/spec-parsing-patterns.md
│
── 输入是源代码（非规范）？
│  └─ 步骤1：grep查找handshake/round/send/recv入口点
│
── 同时提供了规范和代码？
│  └─ 先运行规范工作流（S1–S5）构建标准示意图，再阅读代码并用⚠️标注差异
│
── 规范是已知协议（TLS、Noise、Signal、X3DH、FROST）？
│  └─ 阅读references/protocol-patterns.md，使用标准流程作为骨架
│
── 规范是ProVerif（.pv）或Tamarin（.spthy）？
│  └─ 阅读references/spec-parsing-patterns.md → 形式化模型章节
│
── 规范的消息顺序不明确？
│  └─ 从轮次/章节结构推断，用⚠️标注
│
── 无法从规范中识别参与方？
│  └─ 检查"Parties"/"Notation"章节；ProVerif读取进程名；Tamarin读取规则名和事实参数
│
── 不知道哪些代码文件实现了协议？
│  └─ 步骤1：grep查找handshake/round/send/recv入口点
│
── 无法从结构体名识别参与方？
│  └─ 阅读测试文件——测试设置会体现角色
│
── 协议在进程内运行（无网络调用）？
│  └─ 将角色边界处的函数参数传递视为消息
│
── 多方计算/阈值协议，包含N个参与方？
│  └─ 阅读references/protocol-patterns.md → MPC章节
│
── Mermaid语法错误？
│  └─ 阅读references/mermaid-sequence-syntax.md → 常见问题
│
└─ ASCII绘制规范？
   └─ 阅读references/ascii-sequence-diagram.md

Examples

示例

Code path —

examples/simple-handshake/

protocol.py
— two-party authenticated key exchange (X25519 DH + Ed25519 signing + HKDF + ChaCha20-Poly1305)
expected-output.md
— exact ASCII diagram and Mermaid file the skill should produce for that protocol

Spec path (ProVerif) —

examples/simple-proverif/

model.pv
— HMAC challenge-response authentication modeled in ProVerif
expected-output.md
— step-by-step extraction walkthrough (parties, message flow, crypto ops) and the exact ASCII diagram and Mermaid file the skill should produce

Study the relevant example before working on an unfamiliar input.

代码路径 —

examples/simple-handshake/

：

protocol.py
— 两方认证密钥交换（X25519 DH + Ed25519签名 + HKDF + ChaCha20-Poly1305）
expected-output.md
— 本技能应为该协议生成的标准ASCII示意图和Mermaid文件

规范路径（ProVerif） —

examples/simple-proverif/

：

model.pv
— 用ProVerif建模的HMAC挑战响应认证
expected-output.md
— 分步提取流程（参与方、消息流、密码学操作），以及本技能应生成的标准ASCII示意图和Mermaid文件

处理不熟悉的输入前，请先学习相关示例。

Supporting Documentation

支持文档

references/spec-parsing-patterns.md — Extraction rules for RFC, academic paper/pseudocode, informal prose, ProVerif, and Tamarin input formats; read during Step S1
references/mermaid-sequence-syntax.md — Participant syntax, arrow types, activations, grouping blocks, escaping rules, and common rendering pitfalls
references/protocol-patterns.md — Canonical message flows for TLS 1.3, Noise, X3DH, Double Ratchet, Shamir secret sharing, commit-reveal, and generic MPC rounds; use as a reference when comparing implementation against spec
references/ascii-sequence-diagram.md — Column layout, arrow conventions, self-loops, phase labels, and inline output format for the ASCII diagram

references/spec-parsing-patterns.md — 适用于RFC、学术论文/伪代码、非正式文本、ProVerif和Tamarin输入格式的提取规则；步骤S1期间阅读
references/mermaid-sequence-syntax.md — 参与者语法、箭头类型、激活、分组块、转义规则和常见渲染问题
references/protocol-patterns.md — TLS 1.3、Noise、X3DH、Double Ratchet、Shamir秘密共享、承诺-揭示和通用MPC轮次的标准消息流；对照规范验证实现时作为参考
references/ascii-sequence-diagram.md — ASCII示意图的列布局、箭头规范、自循环、阶段标签和内联输出格式