Friday, January 10, 2020

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