《形式化工具Scyther優化與實例分析》--------論文摘抄整理

Scyther 工具在輸出方面操做便捷，攻擊輸出方面方面使用圖形的方式便於理解。這個詳細的不在此說明了

         重要的敵手攻擊能力的說明：  -------  支持   Delov-Yao模型，能夠本身定義安全模型，而且支持強安全模型。這就是說能夠爲敵手定義更強的安全攻擊能力。-------決定了敵手能力在徹底掌握通訊網絡的基礎上，具有腐化長期私鑰和臨時祕鑰等能力，

        本篇論文中做者的主要共貢獻是 將 scyther工具的設置界面的漢化  ，添加了  工具分析協議的運行時間 兩個部分。

  

 

   做者對TLS協議的驗證是使用了 軟件中自身攜帶的協議 對其 佐證本身的 改進，   TLS協議在客戶端和服務器之間創建通訊時，首先要對協議的版本、密碼算法、認證方式、以及公鑰加密技術進行協商，以後進入握手協議階段。這部分我在個人論文中說的會很詳細，在Scyther 工具中使用  SPDL語言 描述協議。對協議的描述是基於角色的，利用 claim時間能夠對角色的認證性、變量性的機密性等進行描述。

      做者的實驗結果是  在  Scyther工具 使用  Delov-Yao模型下對 TLS協議分析，驗證目標屬性是TLS 握手協議中祕鑰協商的機密性結果是安全   。（對做者的結果驗證結果以下）

       

 

      敵手在經過長期私鑰泄露詢問得知主體長期私鑰，而在祕鑰傳輸過程當中惟一保證傳輸機密性的就是主體的長期私鑰，在這種強安全模型面前，TLS握手協議傳輸的祕鑰是不安全的。

      如今我驗證做者說的實驗結果以下：

         如上圖所示  安全做者說的   參數設置形式 。（強安全模式）   執行結果以下：  驗證結果和該論文做者說的是一致的，可是 好幾處驗證結果做者忽略沒有寫  ，在後面個人論文中會加入