Scyther GUI 攻击输出图的解释

一、在声明事件的安全属性的时候也就是整个过程要验证的 对象：

       Scythe 的安全属性  分为下面几种：

•    Secrecy: 表示数据传输过程当中是安全的，即便经过不信任的网络传也不能被攻击者得到
•    SKR： SKR表示的意义与 Secrecy相同，只是在session-key reveal 攻击模型中，将数据泄露给供给者。
•   （Commit，Running）：用于模型之间对数据传输的承认

   另外还有认证属性组：

I-SYNCH、NI-SYNCH、I-AGREE 、NI-AGREE

•    Reachable  用于检测声明是否被知足，因为Scyther的检测模式下
•    Empty   此声明不会被验证，只是Scyther为支持其余验工具时使用
•    Alive  存活性
•    Weakaggree    协议不一致

 二、攻击图输出的解释

一个攻击对应着一个攻击输出图，下图是TLS协议在强安全模型下的其中一个输出攻击图，下面对图上的参数做用一个说明， 在每个声称对应一行，每一行被分红好几列。

  第一列表示协议的名字 ，

第二列显示的是角色的名字，（比方说TLS协议中 a 就表示 客户端 ，b 表示服务端），

第三列表示的是惟一标识符  tlspaulson 表示协议 ，a1 表示声明的一个标签。

第四列显示声明类型，和声明参数

看上面的截图   在 Status（状态栏）下面是两列， 第五列显示协议验证过程的世界结果，当声称是错误的时候显示 Fail ，当声称是正确的时候显示的是 OK 。

第六列完善以前一列的称述，在有些状况下 scyther 验证过程不是完整的，（在下一章中详细介绍），若是这列的状态是  Verified （确认）表示声称是真的，若是状态是 Falsified （伪造）表示声称是错误的。若是这一列是空的，那么 状态  fail/ok 取决于 指定的边界设置。

第七列 是注释  用于进一步解释结果的状态，这一列的表示存在多种状况，分为下面几种：

•      至少存在 X 个攻击 （At least X attacks）:一些攻击在状态空间中可以发现， 因为问题的不肯定性的缘故，或者是由于搜索的分支和绑定的结构，不能肯定是否还存在其余攻击状态
•      在默认的Scyther 设置中 ，当找到一个攻击的时候Scyther会中止验证，
•      至存在 x 个 模式
•      肯定存在 X个 模式（Exactly X pattern）：这种是跟以前的两个一致的，只发生在有 ‘Reachable’的声明中，发现的状态并没与真正受到攻击，而是可达状态的类别。
•      限制范围内没有找到攻击（No attack within bounds）：限制范围内么有找到攻击，可是在状态界限以外可能存在攻击
•      没有攻击（No attacks）：在状态空间界限外或者内都没有发现攻击，能够创建证据没有攻击即便是状态空间没有界限设置，如此安全属性验证成功。

 三、状态空间的限制

        限制运行次数在Scyther中能够更改，若是设置运行次数为5，没有发现攻击，就是说在少于5次的运行中是不存在攻击的，可是不必定大于5次后任然是这样的结果，

四、攻击图

     如上面的图，每个垂直轴表示一个运行，运行是存菱形出开始，菱形表示运行的建立，并提供了运行了有关信息，