Scyther 論文相關資料整理

一、Scyther 的特色使用方法

    Scyther能夠提供軌跡的簡單描述，方便分析協議可能出現的攻擊和表現，使用Athena算法，該軟件表現以下特色：

      該軟件有明確的終止，能工提供無限會話協議安全性的證實，嫩共證實過程的樹狀圖，相比其餘軟件能工提供更加有效的證實結構，輸出證實過程的樹狀圖；提供協議的多種可能的表現和攻擊，實現了多協議的並行分析，解決了傳統軟件的狀態空間爆炸問題，該工具提供的圖表現的人際交互界面，GUI的命令輸入框在大型的協議分析中使用比較方便。Scyther使用SPDL語言，主要有三種使用方法，一是驗證給定的安全聲明（聲明參量的機密性或者主體的認證性等 ）

    利用 Scyther-Compromise工具能夠方便的更改協議的安全模型，該工具將敵手的能力經過選項的方式提供用戶選擇，這一點相比其餘工具具備很大的優點，安全模型均須要用戶利用形式化描述語言進行描述，Scyther-Compromise工具經過勾選方式添加長期私鑰泄露，會話祕鑰泄露，隨機數泄露以及狀態泄露以及狀態泄露等強安全模型等強安全模型下的敵手模型。

   有在強安全模型下，攻擊搜索的狀態空間增長，所以TLS協議分析耗時增長，不管是客戶端仍是服務器端都不能保證協議協商的機密性，強安全模型下TLS握手協議可收到逛逛街流程圖以下面的圖，敵手經過長期私鑰泄露詢問得知主體長期私鑰，而在私鑰傳輸的過程當中惟一保證傳輸機密性的主要的長期私鑰，這就證實了在強安全模型下，TLS握手協議傳輸是不安全的。