Scyther Formal Verification 入門與安全特性

1. 使用 Scyther 的動機
Scyther 是一套自動挖掘網絡協議 (Network Protocol) 漏洞的軟件。由於用手計算／用算式去推算漏洞的步驟十分繁複，系統性也不高，所以研究人員都偏向採用這類驗證工具（Formal Verification Tools）去找不同協議的問題。

Scyther v1.1.3 截圖

Scyther 屬於進程演算 (process calculi) 的驗證工具，特點在於每一個協議參與者均會有一個 Role（角色），而研究人員則只需要按著不同的角色去編寫程序。同類型的例子還有 AVISPA 和 ProVerif。相比起 rule-based 的 Tamarin Prover，Scyther 更簡單直覺，但壞處則是原生支援的算法也比 Tamarin 少。

---

2. Scyther 中的不同名詞

在進程演算的工具中，Agent 主要指「執行 Role 的代理人」，在 Scyther 中它的角色並不明顯。此外，Nonce 則指「一次性編碼」（number used once），大概就是 token 的意思。

另外，Scyther 的 Threat Model 是基於 Dolev-Yao Model。簡單來說，它指的是攻擊者對網絡有全權控制（包括但不限於截取信息、更改順序、修改信息內容、扮作信息接收者等）。但另一方面，它也假設了加密算法完全可靠（也就是說攻擊者唯一知道加密內容的方法，就是要找出密碼）。所以，這種假設專門針對協議上的邏輯問題，並排除了加密算法的漏洞、或者是電腦病毒、內鬼泄露機密等其他因素。

還有以下數個，在 Scyther 的協議中常見的 Role Terms:

• Var - 變數名
• Fresh - 新鮮變數名，會隨著建立新實體 (instantiation) 時派一個新的初始值
• Role - 角色（例如 Alice 和 Bob）
• Func - 函數名
• sk(RoleTerm) / pk(RoleTerm) / k(RoleTerm, RoleTerm) - 密鑰（私鑰／公鑰／對稱）
• pk(rt)^-1 = sk(rt) - 公鑰的 inverse key 就是私鑰，反之亦然
• Run - 類似 Thread / Process 的概念，就是經過實體化（instantiation）的 Role。
• RunTerm - 在 run 中的已實體化變數 
• RunEvent - 將 Role 實體化成 Run 的事件 (Event)
• Agents - 執行 Role 的代理人
• RID - unique run identifier

而 Scyther 的基本文法也十分清晰：

• send(R, R', rt) - 由 R 傳送到 R'，內容為 rt
• claim(R, c) - R 需要滿足 security claim c 
• claim(R, secret, rt) - R 需要確保變數 rt 的機密性 (secret to adversary)

---

3. Scyther 中的不同驗證強度 (Aliveness / Synchronization / Agreement)
對方存在 Aliveness:

• Weak Aliveness - 對方存在，且成功運行協議（假設對方絕對可信）
• Weak Aliveness in the Correct Role - 對方存在，且身份正確（Alice 找 Bob，而非兩個 Alice）
• Recent Aliveness - 對方近期存在，且成功運行協議（利用 token 確保對方未死）
• Recent Aliveness in the Correct Role - 對方近期存在，且身份正確（確保 Alice 找到未死的 Bob）

成功同步 Synchronization:

• Non-injective (non one-to-one) Synchronization - 成功運行整個協議（不會因被攻擊，以致只運行到一半）
• Injective Synchronization - 成功運行整個協議，而且對方也是一對地成功運行

協議內容同步 Agreement:

• Non-injective Agreement - 運行協議後，變數 (Variables) 得到預期的結果
• Injective Agreement - 運行協議後，變數得到預期結果，而且只能一對一地運行（不能有 Intruder 先發送一個請求，然後 Alice 接手回應的情景） 
• Weakagree - 所有協議執行者，均扮演著預期的角色。例如有三個人，他們知道自己是A，B 和 C，而其餘兩個人都正確知道，自己正在跟 B,C / A,C / A,B 對話。

安全強度表：

---

4. Scyther 的實例
參考 /scyther-mac-v1.1.3/Protocols/needham-schroeder-lowe.spdl
運行截圖：

---

Reference:

[1] The Scyther Tool - https://people.cispa.io/cas.cremers/scyther/index.html
[2] Operational Semantics and Verification of Security Protocols - https://www.springer.com/gp/book/9783540786351