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 模型進度：
- [ ] 步驟 1：解析參與者與通道
- [ ] 步驟 2：盤點加密操作
- [ ] 步驟 3：宣告型別、函數與方程式
- [ ] 步驟 4：識別並宣告事件
- [ ] 步驟 5：制定安全查詢
- [ ] 步驟 6：撰寫參與者進程
- [ ] 步驟 7：撰寫主進程並完成
- [ ] 步驟 8：驗證並交付

步驟 1：解析參與者與通道

從 Mermaid 圖表：

1. 提取每個 participant 或 actor 宣告。每個成為一個 ProVerif 進程。
2. 計算訊息箭頭（->>、-->>、-x、--x）。每個不同的 A ->> B: label 在通道上建立一個通訊步驟。
3. 決定通道模型：
   • 公開通道：用於在安全通道建立前透過網路傳送的任何訊息（例如 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：宣告型別、函數與方程式

按以下順序建立加密前綴：

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），第二個是 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：識別並宣告事件

事件標記協議執行中的安全相關時刻。透過識別以下內容來提取：

• 開始事件（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：撰寫主進程並完成

主進程：

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(...) 都有對應的 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）？
│  └─ 使用 sign/verify 搭配內聯 reduc（非 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 — 雙向認證金鑰交換（X25519 DH + Ed25519 簽章 + HKDF）的 Mermaid sequenceDiagram
• sample-output.pv — 技能應產生的確切 ProVerif 模型，包含機密性和單射認證查詢

在處理不熟悉的協議之前，先研讀此範例。

---

支援文件

• references/crypto-to-proverif-mapping.md —
  從 Mermaid 加密註解到 ProVerif 函數宣告、方程式和進程模式的對應表
• references/proverif-syntax.md —
  ProVerif 語言參考：型別、函數、方程式、進程、事件、查詢和常見陷阱
• references/security-properties.md —
  選擇正確查詢的決策指南：機密性、認證（弱 vs 單射）、前向安全性、不可連結性，以及如何建模它們