Scyther-Compromise 協議形式化安全分析如何改進協議

一、最終的目的是如何將協議的不安全因素進行改進，提高安全性能。對協議中有關的加密和認證的過程進行形式化分析驗證的時候經過添加敵手模型的（DY模型和eCK強安全模型），接受者和發送者之間的通訊過程可能存在被攻擊者干擾，即就是存在攻擊輸出。那麼咱們的目的就不光光是驗證了現有協議確實在哪個方面確實存在攻擊點位。而是經過對協議過程當中參加的實體或者產生的量進行不一樣方式的加密。

二、常見的修改措施

     Scyterg工具自己就有兩個功能，一是形式化安全分析下協議加密和認證存在的安全漏洞，二是經過逐步添加認證條件來改進協議安全屬性。做者在實例介紹中就對Needham_schroeder 協議作了改進，Scyther形式化分析的協議並非對協議算法的可靠性的驗證，

三、在協議形式化中修改以後如何反饋到協議本體源代碼本體設計