《安全协议形式化分析工具比较与研究 》-------摘抄整理

   Scyther软件是瑞士苏黎世大学 Cass Cremers开发的形式化分析工具，该工具对于无限会话以及无限状态集合的协议能够给出明确的终止，而且支持多协议的并行分析， Scyther系列的工具包括 Scyther 和Scyther-Compromise（在我得论文中使用的是 Scyther-Compromise ，可是做者分析TLS协议的时候使用Tamarin ）该工具基于模型改进算法，对状态集合轨迹有着明确的描述，对于攻击搜索，角色的执行以及安全性证实有着巨大的帮助，Scyther系统工具的应用特色包括下面几个方面：

           能够经过敌手能力组合方便的选择包括 eCK等强安全模型在内的安全模型、、、、、、支持协议的并行分析、、、、、

  Tamarin是由 Simon Meier等人提出的，该工具利用 Scyther工具的逆向搜索算法，提供两种行为方式，全自动分析和人机交互模式，Tamarin基于多重集合改写规则描述协议流程，利用一阶漏记话协议消息和时间节点，从而实现对协议属性的描述，支持具备复杂控制流的协议或者具备非单调易变全局状态的协议，支持eCK等强安全模型，支持多种代数性质；加密解密运算、运算结合律、Diffe-Hellman幂运算以及双线对运算， Tamarin 被用于分析大量秘钥创建协议，尤为是对带有循环结构普和易变全局变量的协议，如 TESLA协议，YubiKey协议和 YubiHSM协议。

 Scyther、Scyther-Compromise以及 Tamarin 工具攻击输出均为攻击流程图，而且三者在攻击搜索时间上差异不大，这是由于 Scyther和 Scyther-Compromise使用的状态空间显示和搜索算法类似，Scyther-Compromise在Scyther的基础上添加了强安全模的选项，从而你增长了搜索的时间，而 Tamarin是在Scyther基础上涉及的，使用Scyther的逆向算法。另外要说的是 Scyther-Compromise和Tamarin 工具不经支持Dolev-Yao模型，还支持 eCK等强安全模型，除了 在本文做者验证SSH协议的时候除了发现  Dolev-Yao模型下的单项认证漏洞以外，还发现强安全模型下的临时秘钥泄露攻击，

下面我给出了 Scyther-Compromise工具的设置选项的参数的 界面，能够自行设定攻击的轮数和， 强安全模型等其余一些。  在  Scyther-Compromise 工具中，将强安全模型选项组合起来描述，用户勾选不一样的敌手询问能力选项，并能够对协议进行不一样安全模型下的分析，极大的方便了用户的使用，可是Scyther-Compromise工具目前不支持协议运算的代数性质，对于出现代数运算的协议可能出现攻击漏报的现象，Tamarin工具的使用须要用户将强安全模型进行形式化描述，操做相对复杂，可是该工具支持多种代数运算，弥补了 Scyther-Compromise工具的不足之处。

    因此在个人论文分析中使用Scyther-Compromise工具分析TLS 协议。

   Scyther-Compromise开发者将强安全模型下的各类敌手询问能力做为勾选像项，如上图显示，者包括了向前安全、弱向前安全、完美向前安全、临时秘钥泄露、状态泄露等强安全安全属性。只要对不一样询问进行不一样组合的否选，能够实现协议在不一样安全模型下的分析， 虽然 Tamarin工具须要对强安全模型进行形式化描述，使用过程相对复杂，可是该工具支持加解密运算，运算结合律，Diffie-Hellman幂运算以及双线性对运算等代数运算性质，尤为是双线性对运算，这在其余工具中都不支持。

    那么我下面直接粘贴过来做者的对几款工具性能比较的表 ，

   下面是我本身根据资料整理的  关于  Scyther 和   Scyther-Compromise 以及   Tramarin 的  特性比较

工具	之间关系	安全模型比对	支持验证算法特色	安装配置操做
Scyther		没有强安全模型	不支持代数运算性质
Scyther-Compromise	基于  Scyther 算法，添加了强安全模型	强安全模型自动添加，多种敌手模型	不支持运算的代数性质	Linux操做系统上安装  须要网络支持，（Windows也能够，配置较麻烦）
Tramarin	使用Scyther的逆向搜索算法	强安全模型要手动形式化描述添加，操做复杂	支持代数运算性质，支持加解密，尤为是双线性对运算	基于网页的工具，使用过程是用户运行客户端程序，协议验证分析是在服务器端进行， 要求用户将协议描述上传至服务器端，服务器分析以后传至客户端，