Mermaid to ProVerif

暗号プロトコルを説明するMermaid sequenceDiagram を読み取り、ProVerif検証器に直接渡すことができるProVerifモデル(.pvファイル)を生成します。

使用ツール: Read、Write、Grep、Glob。

典型的な入力は crypto-protocol-diagram スキルの出力です。暗号操作(Sign、Verify、DH、HKDF、Enc、Decなど)とメッセージ矢印で注釈が付けられたMermaid sequenceDiagram です。

使用時期

• ユーザーがMermaidシーケンス図として説明された暗号プロトコルを形式検証するよう求めている場合
• ユーザーがプロトコル図からProVerifモデル(.pvファイル)を生成したい場合
• ユーザーが機密性、認証、または前方秘匿性プロパティを証明したい場合
• 入力が crypto-protocol-diagram スキルの出力である場合

使用しない場合

• Mermaidシーケンス図がまだ存在しない場合 — 最初に crypto-protocol-diagram を使用して生成してください
• ユーザーが非暗号システム(ステートマシン、アクセス制御)のプロパティを検証したい場合
• ユーザーが既存の.pvファイルでProVerifを実行したい場合 — proverif model.pv を直接実行してください

却下する根拠

根拠	なぜ間違っているか	必要なアクション
「到達可能性クエリはただの退屈な作業」	イベントに到達不可能な場合、他のすべてのクエリ結果は意味がない	理性チェックとして常に到達可能性クエリを最初に追加する
「すべてのメッセージに対してパブリックチャネルで十分」	プロセス内状態のプライベートチャネルは誤った攻撃を防止する	プロセス内状態スレッド処理にはプライベートチャネルを使用する
「前方秘匿性テストをスキップします」	一時的鍵は前方秘匿性検証を必要とする	図が一時的鍵を示すときはいつでもForwardSecrecyTestプロセスを追加する
「未使用の宣言は無害」	ProVerifは孤立した宣言から誤った結果を報告する可能性があります	未使用のすべての型、関数、イベントをクリーンアップする
「モデルがコンパイルするから正しい」	コンパイルするモデルは、デッド受信、型不一致、またはクエリを空虚に真にする不可能なガードを持つ可能性があります	セキュリティクエリを信頼する前に到達可能性を検証する
「最初に例を確認する必要はない」	例は期待される出力品質基準を定義しています	不慣れなプロトコルで作業する前に examples/simple-handshake/ を研究してください

---

ワークフロー

ProVerifモデルの進行状況:
- [ ] ステップ1: 参加者とチャネルを解析
- [ ] ステップ2: 暗号操作のインベントリ
- [ ] ステップ3: 型、関数、方程式を宣言
- [ ] ステップ4: イベントを識別して宣言
- [ ] ステップ5: セキュリティクエリを策定
- [ ] ステップ6: 参加者プロセスを記述
- [ ] ステップ7: メインプロセスを記述して完成させる
- [ ] ステップ8: 検証して配信

ステップ1: 参加者とチャネルを解析

Mermaid図から:

1. すべての participant または actor 宣言を抽出します。各々がProVerifプロセスになります。
2. メッセージ矢印(->>、-->、-x、--x)を数えます。異なる各 A ->> B: label は通信ステップをチャネル上に作成します。
3. チャネルモデルを決定します:
   • パブリックチャネル — セキュアチャネルが確立される前にネットワークを介して送信されるメッセージ(例:ClientHello、一時的鍵、ピアによってデコード対象となる暗号文)
   • プライベートチャネル — 単一パーティプロセス内の内部状態スレッド処理のみ(パーティ間メッセージ向けではない)
   • デフォルト: すべてのパーティ間メッセージ用に1つの共有パブリックチャネル c を宣言します。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.   (* 公開鍵 *)
type skey.   (* 秘密鍵 *)
type nonce.

2. 定数 — ドメイン分離またはラベルとして使用される固定文字列用:

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

3. 関数 — コンストラクタとデストラクタ。デストラクタはインライン 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.

(* デジタル署名 — verifyは成功時にメッセージを返し、失敗時に中止 *)
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から)、2番目は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.

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 — 署名メッセージ送信前にファイア *)
event endI(pkey, pkey, key).  (* pk_I, pk_R, session_key — 受け入れ後にファイア *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).

パラメータはセッションを一意に識別する必要があります: パーティの公開鍵、プラスセッション鍵またはトランスクリプトハッシュ。

ステップ5: セキュリティクエリを策定

セキュリティプロパティごとに1つのクエリを記述します。以下から選択します:

到達可能性(常に最初に追加 — 構造的理性チェック):

成功イベントが実際に到達可能であることを検証します。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: 参加者プロセスを記述

参加者ごとに1つの 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);
    (* 機密性証人: seラッション鍵の下で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プロトコル: 異なる役割ごとに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. チャネル宣言 (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(...) に互換性のある列型とマッチングパターン制約(=key vs 通常名)を持つ対応する get T(...) がある
• 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)。

記述後、簡単なサマリーを出力します:

Protocol:   <Name>
Output:     <filename>
Queries:    <各クエリとそれがテストするプロパティのリスト>
Assumptions: <モデリング決定と単純化のリスト>

---

決定木

├─ Mermaid図が提供されていない?
│  └─ ユーザーに確認: 「Mermaidシーケンス図を提供するか、
│     最初にcrypto-protocol-diagramスキルを実行してください。」
│
├─ 図が(対称暗号化だけでなく)DHを使用している?
│  └─ 交換法方程式でdh/dhpkを使用する
│     references/crypto-to-proverif-mapping.md → DHセクション を参照
│
├─ 図が非対称署名(Sign/Verify)を使用している?
│  └─ インライン reduc でsign/verifyを使用(方程式ではない)
│     verifyは成功時にメッセージを返す; 失敗時に中止するには let _ = verify(...) in を使用
│     署名鍵(skey)を検証鍵(pkey)と区別する
│
├─ プロトコルに「alt」ブロック(中止パス)がある?
│  └─ if/then のみとしてモデル化 — else分岐は中止(プロセスは終了)
│     図がそれを示さない限り、out(c, error_message) を追加しないでください
│
├─ プロトコルに N > 2 パーティがある?
│  └─ 役割ごとに1つのプロセスを記述し、複製に ! を使用
│     役割がインデックスのみで異なる場合、参加者インデックスをパラメータとして渡す
│
├─ 前方秘匿性がリクエストされている?
│  └─ セッション後に長期skをリークするForwardSecrecyバリアントをメインプロセスに追加
│     過去のsession_keyの機密性クエリを追加
│     references/security-properties.md → 前方秘匿性 を参照
│
├─ 型チェッカーがモデルを拒否している?
│  └─ ProVerifは型付け: すべての関数arg型が宣言と一致することを確認。
│     bitstringはキャッチオール; key/pkey/skey/nonceはより厳密。
│     必要に応じて明示的なコンストラクタでキャストする。
│
├─ プロトコルはプロセス間状態調整がある(例: 1つのプロセスが別のプロセスが
│  受け入れを記録するまで待機する必要がある)?
│  └─ ProVerifテーブルを使用(table/insert/get)
│     references/proverif-syntax.md → テーブル を参照
│
├─ 検証が数分後に終了しない?
│  └─ c 上のメッセージタプル構造に一致するnoselect指令を追加
│     references/proverif-syntax.md → noselect を参照
│
├─ プロトコルが直接出力されることはないが、その機密性を
│  検証すべき、プライベート型鍵を生成する?
│  └─ query attacker(sk) の代わりにキー露出オラクルパターンを使用
│     references/security-properties.md → キー露出オラクル を参照
│
└─ どのセキュリティプロパティを検証するか不確実?
   └─ デフォルトセット: セッション鍵の機密性 + 単射認証
      (両方向)。図が一時的鍵を示す場合は前方秘匿性を追加。

---

例

examples/simple-handshake/ に解いた例があります:

• diagram.md — 二者認証鍵交換(X25519 DH + Ed25519署名 + HKDF)用Mermaidシーケンス図
• sample-output.pv — スキルが生成すべき正確なProVerifモデル、機密性と単射認証クエリ付き

不慣れなプロトコルで作業する前にこれを研究してください。

---

サポートドキュメント

• references/crypto-to-proverif-mapping.md — Mermaid暗号注釈からProVerif関数宣言、方程式、プロセスパターンへのマッピングテーブル
• references/proverif-syntax.md — ProVerif言語リファレンス: 型、関数、方程式、プロセス、イベント、クエリ、および一般的な落とし穴
• references/security-properties.md — 正しいクエリの選択のための決定ガイド: 機密性、認証(弱 vs 単射)、前方秘匿性、非結合性、およびそれらのモデル化方法