《形式化分析工具Scyther性能研究》------摘抄整理

本篇論文的主要創新點在--------使用 Scyther工具發現對部分 KCI攻擊搜索出現漏報的現象，並給出了存在的緣由，

    介紹了 形式化分析工具   AVispa全稱是   Automated Validation of Internet Security-sensitive Protocols and Applications ,較多使用在大型網絡安全協議的分析，提供模型運算和形式化語言用於描述協議特徵和行爲，整合了目前從查找協議攻擊到協議抽象驗證等方面許多形式化分析技術，擅長查找協議攻擊，可是在驗證和創建協議安全性能方面不足，

    Scyther使用Athena算法對協議進行分析，輔助定理證實和模型驗證等多種分析技術，高效準確，適合於包含主體的協議分析以及包含多變協議協同的分析，那麼Scyther工具運行的簡單的原理是，下面介紹圖：   -------操做流程    ------》向Scyther系統導入寫好的形式化描述協議代碼----------Scyther按照操做語義將協議劃分紅多邊主體規格，而後調用Athena算法對協議進行分析--------判斷Scyther系統可否搭建出安全性聲明的反例----------若是能 則輸出   Fail    -----------不能則輸出  OK 表示是安全的

   做者的實驗結果發現 ：經過底層算法分析，發現 Scyther不包含內嵌的代數運算的性質，這就是說該工具很難發現包含代數運算的攻擊，解決思路：------工具以後的提高版本 Tamarin工具在代數方面比較突出，支持結合律，交換律、DH指數運算以及雙線性對等代數運算性質。