本篇论文额主要创新点： 利用Scyther软件，通过对一个不安全的秘钥建立协议逐步添加并验证安全属性，最终建立一个安全的秘钥建立协议。
通过形式化分析软件设计秘钥建立协议课可以提高协议设计效率，减少设计者在设计过程中的认为错误，此外，该方法将协议的设计过程和协议的分析过程合成一起，协议设计的终止条件取决于自动化分析工具的分析结果。因此来说，该方法设计的协议其安全性，能同时得到形式化分析工具的验证。
这篇论文是比较基础的讲解Scyther工具的原理的 ----- 但是在协议形式化描述上没有系统的讲，
那么之前多次重复的概念我这里就省略不写。
Scyther可以 进行多协议的并行分析，可以分析与时序相关的协议（这一点暂时我还是没有遇见）、可以进行多秘钥设施（PKIs）模式化、可以寻找协议的多种攻击，
Scyther软件使用 SPDL语言的三种使用方法： 验证给定的安全声明（声明参量的机密性或者主体的认证机密性）、自动生成安全声明（存活性、非单射一致性、非单射同步以及数据机密性）、通过完整的特征描述分析协议，即描述每一个协议主体特征，描述所有主体执行协议的迹，通过迹类发现潜在的危险。
Scyther软件围绕的安全属性： 机密性和 认证性。