《基于Scyther的秘钥创建协议设计》-------摘抄整理

本篇论文额主要创新点：   利用Scyther软件，经过对一个不安全的秘钥创建协议逐步添加并验证安全属性，最终创建一个安全的秘钥创建协议。

      经过形式化分析软件设计秘钥创建协议课能够提升协议设计效率，减小设计者在设计过程当中的认为错误，此外，该方法将协议的设计过程和协议的分析过程合成一块儿，协议设计的终止条件取决于自动化分析工具的分析结果。所以来讲，该方法设计的协议其安全性，能同时获得形式化分析工具的验证。

      这篇论文是比较基础的讲解Scyther工具的原理的 ----- 可是在协议形式化描述上没有系统的讲，

       那么以前屡次重复的概念我这里就省略不写。

     Scyther能够 进行多协议的并行分析，能够分析与时序相关的协议（这一点暂时我仍是没有碰见）、能够进行多秘钥设施（PKIs）模式化、能够寻找协议的多种攻击，

     Scyther软件使用 SPDL语言的三种使用方法：    验证给定的安全声明（声明参量的机密性或者主体的认证机密性）、自动生成安全声明（存活性、非单射一致性、非单射同步以及数据机密性）、经过完整的特征描述分析协议，即描述每个协议主体特征，描述全部主体执行协议的迹，经过迹类发现潜在的危险。

      Scyther软件围绕的安全属性：  机密性和 认证性。