《安全協議形式化分析工具比較與研究 》-------摘抄整理

   Scyther軟件是瑞士蘇黎世大學 Cass Cremers開發的形式化分析工具，該工具對於無限會話以及無限狀態集合的協議能夠給出明確的終止，而且支持多協議的並行分析， Scyther系列的工具包括 Scyther 和Scyther-Compromise（在我得論文中使用的是 Scyther-Compromise ，可是做者分析TLS協議的時候使用Tamarin ）該工具基於模型改進算法，對狀態集合軌跡有着明確的描述，對於攻擊搜索，角色的執行以及安全性證實有着巨大的幫助，Scyther系統工具的應用特色包括下面幾個方面：

           能夠經過敵手能力組合方便的選擇包括 eCK等強安全模型在內的安全模型、、、、、、支持協議的並行分析、、、、、

  Tamarin是由 Simon Meier等人提出的，該工具利用 Scyther工具的逆向搜索算法，提供兩種行爲方式，全自動分析和人機交互模式，Tamarin基於多重集合改寫規則描述協議流程，利用一階漏記話協議消息和時間節點，從而實現對協議屬性的描述，支持具備複雜控制流的協議或者具備非單調易變全局狀態的協議，支持eCK等強安全模型，支持多種代數性質；加密解密運算、運算結合律、Diffe-Hellman冪運算以及雙線對運算， Tamarin 被用於分析大量祕鑰創建協議，尤爲是對帶有循環結構普和易變全局變量的協議，如 TESLA協議，YubiKey協議和 YubiHSM協議。

 Scyther、Scyther-Compromise以及 Tamarin 工具攻擊輸出均爲攻擊流程圖，而且三者在攻擊搜索時間上差異不大，這是由於 Scyther和 Scyther-Compromise使用的狀態空間顯示和搜索算法類似，Scyther-Compromise在Scyther的基礎上添加了強安全模的選項，從而你增長了搜索的時間，而 Tamarin是在Scyther基礎上涉及的，使用Scyther的逆向算法。另外要說的是 Scyther-Compromise和Tamarin 工具不經支持Dolev-Yao模型，還支持 eCK等強安全模型，除了 在本文做者驗證SSH協議的時候除了發現  Dolev-Yao模型下的單項認證漏洞以外，還發現強安全模型下的臨時祕鑰泄露攻擊，

下面我給出了 Scyther-Compromise工具的設置選項的參數的 界面，能夠自行設定攻擊的輪數和， 強安全模型等其餘一些。  在  Scyther-Compromise 工具中，將強安全模型選項組合起來描述，用戶勾選不一樣的敵手詢問能力選項，並能夠對協議進行不一樣安全模型下的分析，極大的方便了用戶的使用，可是Scyther-Compromise工具目前不支持協議運算的代數性質，對於出現代數運算的協議可能出現攻擊漏報的現象，Tamarin工具的使用須要用戶將強安全模型進行形式化描述，操做相對複雜，可是該工具支持多種代數運算，彌補了 Scyther-Compromise工具的不足之處。

    因此在個人論文分析中使用Scyther-Compromise工具分析TLS 協議。

   Scyther-Compromise開發者將強安全模型下的各類敵手詢問能力做爲勾選像項，如上圖顯示，者包括了向前安全、弱向前安全、完美向前安全、臨時祕鑰泄露、狀態泄露等強安全安全屬性。只要對不一樣詢問進行不一樣組合的否選，能夠實現協議在不一樣安全模型下的分析， 雖然 Tamarin工具須要對強安全模型進行形式化描述，使用過程相對複雜，可是該工具支持加解密運算，運算結合律，Diffie-Hellman冪運算以及雙線性對運算等代數運算性質，尤爲是雙線性對運算，這在其餘工具中都不支持。

    那麼我下面直接粘貼過來做者的對幾款工具性能比較的表 ，

   下面是我本身根據資料整理的  關於  Scyther 和   Scyther-Compromise 以及   Tramarin 的  特性比較

工具	之間關係	安全模型比對	支持驗證算法特色	安裝配置操做
Scyther		沒有強安全模型	不支持代數運算性質
Scyther-Compromise	基於  Scyther 算法，添加了強安全模型	強安全模型自動添加，多種敵手模型	不支持運算的代數性質	Linux操做系統上安裝  須要網絡支持，（Windows也能夠，配置較麻煩）
Tramarin	使用Scyther的逆向搜索算法	強安全模型要手動形式化描述添加，操做複雜	支持代數運算性質，支持加解密，尤爲是雙線性對運算	基於網頁的工具，使用過程是用戶運行客戶端程序，協議驗證分析是在服務器端進行， 要求用戶將協議描述上傳至服務器端，服務器分析以後傳至客戶端，