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 を実行したい場合 — 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 を 1 つ宣言します。2 つの異なる並列セッションを独立させる必要がある場合にのみ、フローごとのチャネルを追加します。

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)	コミットメント方程式

各操作の正確な ProVerif 構文については、 references/crypto-to-proverif-mapping.md を参照してください。

ステップ 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：イベントを特定して宣言する

イベントは、プロトコルの実行におけるセキュリティ上重要な時点を示します。次を特定して抽出します。

• Begin イベント（event beginRole(params)）：当事者が長期的なアイデンティティのコミットメントに依存するメッセージを送信する直前に発生します（例：署名付きメッセージまたは MAC 付きメッセージの送信直前）。
• End イベント（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：セキュリティクエリを定式化する

セキュリティ特性ごとに 1 つのクエリを記述します。次から選択してください。

到達可能性（構造上の健全性チェックとして必ず最初に追加します）：

成功イベントが実際に到達可能であることを確認します。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)).

前方秘匿性：セッションの後に（phase 1 で）長期秘密鍵の両方を攻撃者に漏えいする ForwardSecrecyTest プロセスをメインプロセスに追加し、そのうえで過去のセッションキーが引き続き秘匿されることを確認します。これに、free fs_witness: key [private] 宣言と query attacker(fs_witness) を組み合わせます。references/security-properties.md → 前方秘匿性を参照してください。

各特性に適用可能な、最も強いクエリを選択してください。判断の全手順については、references/security-properties.md を参照してください。

ステップ 6：参加者プロセスを記述する

参加者ごとに 1 つの let プロセスを記述します。各プロセスは、Mermaid 図の各ステップを順番どおりに反映する構成にします。

2 者間プロトコルのテンプレート：

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 プロトコル：**役割ごとに 1 つのプロセスを記述します。しきい値プロトコルでは、役割プロセスを 1 つ記述し、メインプロセスで !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, ...) がある
• プロセス内で使用されているすべての関数が、前文で宣言されている
• すべてのデストラクターで、別個の equation ブロックではなくインラインの reduc を使用している
• クエリ内のすべてのイベントが宣言され、プロセス内でトリガーされている
• 長期公開鍵がメインプロセス内でチャネル c に出力されている（攻撃者から見える状態にします。これが Dolev-Yao モデルです）
• 未使用の宣言がない（試しに追加したものはすべて削除する）
• table 宣言がある場合、すべての insert T(...) に、互換性のある列型と一致するパターン制約（=key と単独の名前）を持つ対応する get T(...) がある
• noselect を使用する場合、そのタプル構造が c で送信される実際のメッセージ形式と一致している（例：ペア → mess(c, (x, y))）
• Key Exposure Oracle パターンを使用する場合、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>

---

意思決定ツリー

├─ 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 — 2 者間の認証付き鍵交換（X25519 DH + Ed25519 署名 + HKDF）を表す Mermaid sequenceDiagram
• 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 — 適切なクエリ（機密性、認証（弱認証か単射認証か）、前方秘匿性）を選択し、モデル化する方法を示すガイド