Scyther 论文相关资料整理

一、Scyther 的特色使用方法

    Scyther能够提供轨迹的简单描述，方便分析协议可能出现的攻击和表现，使用Athena算法，该软件表现以下特色：

      该软件有明确的终止，能工提供无限会话协议安全性的证实，嫩共证实过程的树状图，相比其余软件能工提供更加有效的证实结构，输出证实过程的树状图；提供协议的多种可能的表现和攻击，实现了多协议的并行分析，解决了传统软件的状态空间爆炸问题，该工具提供的图表现的人际交互界面，GUI的命令输入框在大型的协议分析中使用比较方便。Scyther使用SPDL语言，主要有三种使用方法，一是验证给定的安全声明（声明参量的机密性或者主体的认证性等 ）

    利用 Scyther-Compromise工具能够方便的更改协议的安全模型，该工具将敌手的能力经过选项的方式提供用户选择，这一点相比其余工具具备很大的优点，安全模型均须要用户利用形式化描述语言进行描述，Scyther-Compromise工具经过勾选方式添加长期私钥泄露，会话秘钥泄露，随机数泄露以及状态泄露以及状态泄露等强安全模型等强安全模型下的敌手模型。

   有在强安全模型下，攻击搜索的状态空间增长，所以TLS协议分析耗时增长，不管是客户端仍是服务器端都不能保证协议协商的机密性，强安全模型下TLS握手协议可收到逛逛街流程图以下面的图，敌手经过长期私钥泄露询问得知主体长期私钥，而在私钥传输的过程当中惟一保证传输机密性的主要的长期私钥，这就证实了在强安全模型下，TLS握手协议传输是不安全的。