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