crypto-protocol-diagram

暗号プロトコル図

次のいずれかを入力として、Mermaid の sequenceDiagram（ファイルに書き出し）と ASCII のシーケンス図（インラインで出力）を生成します。

• 暗号プロトコルを実装したソースコード
• 仕様書 — RFC、学術論文、擬似コード、非形式的な文章、ProVerif（.pv）、Tamarin（.spthy）のモデル

使用するツール： Read、Write、Grep、Glob、Bash、WebFetch（URL の仕様書用）。

コードの構造を可視化する diagramming-code スキルとは異なり、このスキルではプロトコルの意味、つまり、誰が誰に何を送るのか、各ステップでどのような暗号変換が行われるのか、どのようなプロトコルフェーズがあるのかを抽出します。

呼び出しグラフ、クラス階層、モジュール依存関係図には、代わりに diagramming-code スキルを使用してください。

使用するタイミング

• ユーザーが暗号プロトコルの図示、可視化、抽出を求めている
• 入力がハンドシェイク、鍵交換、またはマルチパーティプロトコルを実装したソースコードである
• 入力が RFC、学術論文、擬似コード、または形式モデル（ProVerif/Tamarin）である
• ユーザーが特定のプロトコル（TLS、Noise、Signal、X3DH、FROST）を指定している

使用しないタイミング

• ユーザーが呼び出しグラフ、クラス階層、またはモジュール依存関係図を求めている — diagramming-code を使用してください
• ユーザーがプロトコルの形式検証を求めている — 図の生成後に mermaid-to-proverif を使用してください
• 入力に暗号プロトコルの意味（当事者やメッセージ交換）がない

退けるべき合理化

合理化	誤りである理由	必須の対応
「プロトコルは単純だから、記憶を頼りに図示できます」	記憶に基づく図では、ステップが抜けたり、矢印の向きが逆になったりします	ソースまたは仕様書を体系的に読みます
「コードがあるので、仕様書の手順は省略します」	コードが仕様書から逸脱している場合があります。両方の手順で異なるバグを見つけられます	両方ある場合は、まず仕様書のワークフローを実行し、その後でコードの相違点を注記します
「暗号に関する注記は任意の装飾です」	暗号に関する注記がなければ、図はメッセージフローにすぎず、セキュリティレビューには役立ちません	すべての暗号操作に注記を付けます
「中断する経路は明らかなので、alt ブロックは不要です」	中断処理を暗黙にすると、エラーチェックの欠落が見えにくくなります	すべての中断／エラー経路を alt ブロックで示します
「先に例を確認する必要はありません」	例は求められる出力品質の基準を示しています	見慣れない入力に取り組む前に、該当する例を確認します
「ProVerif/Tamarin のモデルは仕様書ではなくコードです」	形式モデルは仕様書です。実装ではなく、意図された動作を記述します	.pv および .spthy ファイルには仕様書のワークフロー（S1–S5）を使用します

---

ワークフロー

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：入力タイプを判定する

ほかの作業を始める前に、入力を分類します。

手がかり	入力タイプ
ソースファイルの拡張子（.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）に進みます
• 両方 → まず仕様書ワークフローを実行し、次にコードの読み取り手順で実装と仕様書の図を照合して、相違点があれば ⚠️ を付けて注記します
• 判別できない → ユーザーに「これはソースコードファイル、仕様書、またはその両方ですか？」と尋ねます

---

ステップ 1：プロトコルのエントリーポイントを見つける

プロトコルを示す関数名、型名、コメントを Grep で検索します。

# 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

ハンドシェイクの各フェーズやメインのプロトコルループを呼び出す、最上位のオーケストレーション関数から読み始めます。

ステップ 2：当事者と役割を特定する

以下から参加者名を抽出します。

• 構造体／クラス名：Client、Server、Initiator、Responder、Prover、 Verifier、Dealer、Party、Coordinator
• 役割の状態を受け取る関数パラメーター名
• プロトコル上の役割を宣言するコメント
• 2者間またはN者間のシナリオを設定するテストフィクスチャ

これらを Mermaid の participant 宣言に対応付けます。短く読みやすいエイリアスを使用します。

participant I as Initiator
participant R as Responder

ステップ 3：メッセージの流れを追跡する

状態遷移と、ネットワーク上の送受信を追います。次のようなパターンを探します。

パターン	意味
send(msg) / recv()	直接的なメッセージ交換
serialize + transmit	構造化メッセージの送信
戻り値を他方の関数に渡す	論理メッセージ（インプロセス）
round1_output → round2_input	ラウンドベースの MPC ステップ
ephemeral_key、ciphertext、mac、tag という名前の構造体フィールド	メッセージの内容

インプロセスのプロトコル実装（両方の当事者が同じプロセス内で実行される場合）では、デプロイ時にネットワーク境界となる箇所を表している関数呼び出しの境界を、論理的なメッセージ送信として扱います。

ステップ 4：暗号操作に注釈を付ける

プロトコルの各ステップで、操作を特定してラベルを付けます。

操作	図の注釈
鍵生成	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

注釈は簡潔にし、コードではなく数学的な略記を使用します。

ステップ 5：プロトコルのフェーズを特定する

rect または Note ブロックを使って、メッセージのステップを名前付きのフェーズにまとめます。

検出対象となる一般的なフェーズ：

• セットアップ／鍵生成：当事者の鍵生成、信頼されたセットアップ、パラメーター生成
• ハンドシェイク／初期化：一時鍵交換、ノンス交換、バージョンネゴシエーション
• 認証：本人性の証明、証明書の交換、署名の検証
• 鍵導出：共有秘密からのセッション鍵導出
• データ転送／メインプロトコル：暗号化されたアプリケーションデータの交換
• 終了処理／ティアダウン：セッションの終了、MAC 検証、中断処理

中断／エラーパスを検出し、alt ブロックで示します。

---

仕様書のワークフロー（S1–S5）

入力がソースコードではなく仕様書の場合は、この手順を使用します。 S1–S5 の完了後、上記のコードワークフローにあるステップ 6（sequenceDiagram の生成）と ステップ 7（検証と提出）に進みます。

ステップ S1：仕様書を取り込む

仕様書の全文を取得します。

• ファイルパスが指定されている → 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も読み、 標準的なフローをひな型として使用し、仕様書固有の詳細を補います。

ステップ S2：当事者と役割の抽出

プロトコルに参加するすべての要素を特定します。以下を探してください。

• 文章または擬似コードに記載された役割名：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を参照してください）。

ステップ S3：メッセージフローの抽出

各当事者が、誰に、どの順番で何を送信するかを追跡します。形式ごとの抽出パターンは次のとおりです。

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 ブロックを使用してまとめます。

ステップ S4：暗号操作の抽出

プロトコルの各ステップについて、実行される暗号操作と、それを実行する当事者を特定します。

仕様の表記	操作	図の注釈
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) → σ

セキュリティ条件と中止経路を特定します。

• 文章：「検証に失敗した場合は中止する」、「...の場合に限り」、「...の場合は拒否する」
• 擬似コード：assert、require、if ... abort
• ProVerif：if m = expected then ... else 0
• Tamarin：矛盾するファクトまたは制約補題

これらは最終図で alt ブロックになります。

ステップ S5: 仕様の曖昧さにフラグを立てる

ステップ 6 に進む前に、不足がないか確認します:

• メッセージの順序が不明確: ラウンド構造またはセクションの順序から推測します; ⚠️ ordering inferred from spec structure と注記します
• 暗示された当事者: ある当事者の役割が暗示されているが名前が付いていない場合は、 説明的な名前を付けて、その推測を注記します
• 欠落しているステップ: このプロトコルの正規パターンが要求するステップを仕様が 省略している場合は、次のように注記します: ⚠️ spec omits [step] — canonical protocol requires it
• 不十分な暗号仕様: 仕様が方式を指定せずに「暗号化」と言っている場合は、 次のように注記します: ⚠️ encryption scheme not specified
• ProVerif/Tamarin: プライベートチャネル（new c で宣言された、または プライベートな自由名として宣言された c）は帯域外チャネルを表します — それらを注記します

---

ステップ 6: sequenceDiagram を生成する

references/mermaid-sequence-syntax.md の ルールに従って Mermaid 構文を生成します。

簡潔さよりも完全性を優先します。 すべての異なるメッセージタイプを表示します。 繰り返されるループの各反復は省略します（代わりに loop ブロックを使用します）が、 異なるプロトコルステップを決して省略しないでください。

見た目よりも正確性を優先します。 図はコードが実際に行うことと一致していなければなりません。 コードが既知の仕様から逸脱している場合は、その逸脱を注記します:

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

ステップ 7: 検証して納品する

納品する前に:

• 宣言された各参加者が実際に少なくとも 1 つのメッセージを送信または受信している
• 矢印が正しい方向を指している（送信者 → 受信者）
• 暗号操作が正しい当事者（それを計算する側）に割り当てられている
• プロトコルフェーズを使用している場合、フェーズブロックの外に矢印が現れない
• alt ブロックが既知の中止/エラーパスを網羅している
• 図が構文エラーなくレンダリングされる（よくある落とし穴については references/mermaid-sequence-syntax.md を確認してください）
• 仕様からの逸脱が見つかった場合、⚠️ で注記されている

図をファイルに書き込みます。 プロトコル名から導出したファイル名を選びます。 例: noise-xx-handshake.md や x3dh-key-agreement.md。次の構造で Markdown ファイルを 書き込みます:

# <Protocol Name> Sequence Diagram

\`\`\`mermaid
sequenceDiagram
    ...
\`\`\`

## Protocol Summary

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

ファイルを書き込んだ後、ASCII シーケンス図をレスポンス内にインラインで出力し、 続けてプロトコル概要を出力します。ユーザーが Mermaid ソースをどこで見つけられるか わかるように、出力ファイル名を明記します。

インライン出力形式を含め、 references/ascii-sequence-diagram.md の すべての描画規約に従います。

---

決定木

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

---

例

コードパス — 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 ファイル

慣れない入力に取り組む前に、関連する例をよく確認してください。

---

関連ドキュメント

• 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 図の列の配置、矢印の規則、自己ループ、フェーズラベル、 インライン出力形式について説明します