協議形式化安全分析 Scyther 並不是全部協議能夠照抄就搬

一、Scyther 形式化分析工具能夠對協議進行形式化描述，驗證協議的機密性和可認證性是否存在安全威脅。在攻擊時支持會話輪數無限次執行，同時支持在強安全模型和Delov-Yao模型。在對要形式化分析的協議算法方面並不支持含有  「」XOR「」 運算代數性質和 「」DH「」 代數運算性質以及含有雙線性對代數性質的協議。  目前Scyther 版本的Scyther-Compromise工具不支持運算代數性質，對含有代數運算的協議可能出現攻擊漏報現象除此以外Scyther工具自己不關注傳輸信道的加密方式，而是關注實例雙方傳遞的內容是否被雙方承認，

二、Scyther 自己採用的是黑盒驗證的思想，各個角色從本身的角度驗證是否可以知足安全目標或者安全屬性，若是咱們生命的安全屬性不能被知足則就存在攻擊路徑，咱們在對協議進行形式化安全分析的時候並非對協議的仿真，而是對協議中存在的加密和認證的環節進行高度抽象後進行形式化的描述。經過確認協議當中所涉及參加的角色，聲明角色和常量以及協議過程產生的隨機變量來形式化描述整個協議事件。而且須要對角色的行爲分別進行形式化的描述，聲明協議中所要達到的安全屬性。Scyther會根據聲明的安全屬性來驗證是否知足要求。若是形式化描述規範可以知足角色之間傳遞的內容認同，路徑輸出中不存在錯誤，

三、基於角色的攻擊輸出可能會存在 角色不一樣在攻擊模型下輸出的攻擊數量不一樣。聲明的安全屬性會對應着攻擊測試的驗證輸出。對存在的攻擊輸出至少一個攻擊（Scyther在界限內驗證對應聲明的安全屬性存在一個攻擊以後不會再驗證）

四、對於攻擊圖輸出

  對於攻擊輸出圖須要從新繪製成分別對每個角色的攻擊路徑圖，對應輸出的攻擊圖都會安全聲明的安全屬性標明 。