1、最终的目的是如何将协议的不安全因素进行改进，提升安全性能。对协议中有关的加密和认证的过程进行形式化分析验证的时候通过添加敌手模型的（DY模型和eCK强安全模型），接受者和发送者之间的通信过程可能存在被攻击者干扰，即就是存在攻击输出。那么我们的目的就不光光是验证了现有协议确实在哪一个方面确实存在攻击点位。而是通过对协议过程中参加的实体或者产生的量进行不同方式的加密。
2、常见的修改措施
Scyterg工具本身就有两个功能，一是形式化安全分析下协议加密和认证存在的安全漏洞，二是通过逐步添加认证条件来改进协议安全属性。作者在实例介绍中就对Needham_schroeder 协议做了改进，今晚先写到这-----
3、在协议形式化中修改之后如何反馈到协议本体源代码本体设计
Scyther-Compromise 协议形式化安全分析如何改进协议
原文：https://www.cnblogs.com/xinxianquan/p/11074792.html