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

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

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

4、對于攻擊圖輸出

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

?

轉(zhuǎn)載于:https://www.cnblogs.com/xinxianquan/p/11070862.html

新人創(chuàng)作打卡挑戰(zhàn)賽發(fā)博客就能抽獎！定制產(chǎn)品紅包拿不停！

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。