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

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

3、基于角色的攻擊輸出可能會存在 角色不同在攻擊模型下輸出的攻擊數量不同。聲明的安全屬性會對應著攻擊測試的驗證輸出。對存在的攻擊輸出至少一個攻擊（Scyther在界限內驗證對應聲明的安全屬性存在一個攻擊之后不會再驗證）

4、對于攻擊圖輸出

? 對于攻擊輸出圖需要重新繪制成分別對每一個角色的攻擊路徑圖，對應輸出的攻擊圖都會安全聲明的安全屬性標明 。

?

轉載于:https://www.cnblogs.com/xinxianquan/p/11070862.html

新人創作打卡挑戰賽發博客就能抽獎！定制產品紅包拿不停！

總結

以上是生活随笔為你收集整理的协议形式化安全分析 Scyther 并非所有协议可以照抄就搬的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。