Scyther-Compromise 协议形式化安全分析如何改进协议

一、最终的目的是如何将协议的不安全因素进行改进，提高安全性能。对协议中有关的加密和认证的过程进行形式化分析验证的时候经过添加敌手模型的（DY模型和eCK强安全模型），接受者和发送者之间的通讯过程可能存在被攻击者干扰，即就是存在攻击输出。那么咱们的目的就不光光是验证了现有协议确实在哪个方面确实存在攻击点位。而是经过对协议过程当中参加的实体或者产生的量进行不一样方式的加密。

二、常见的修改措施

     Scyterg工具自己就有两个功能，一是形式化安全分析下协议加密和认证存在的安全漏洞，二是经过逐步添加认证条件来改进协议安全属性。做者在实例介绍中就对Needham_schroeder 协议作了改进，Scyther形式化分析的协议并非对协议算法的可靠性的验证，

三、在协议形式化中修改以后如何反馈到协议本体源代码本体设计