协议形式化安全分析 Scyther 并不是全部协议能够照抄就搬

一、Scyther 形式化分析工具能够对协议进行形式化描述，验证协议的机密性和可认证性是否存在安全威胁。在攻击时支持会话轮数无限次执行，同时支持在强安全模型和Delov-Yao模型。在对要形式化分析的协议算法方面并不支持含有  “”XOR“” 运算代数性质和 “”DH“” 代数运算性质以及含有双线性对代数性质的协议。  目前Scyther 版本的Scyther-Compromise工具不支持运算代数性质，对含有代数运算的协议可能出现攻击漏报现象除此以外Scyther工具自己不关注传输信道的加密方式，而是关注实例双方传递的内容是否被双方承认，

二、Scyther 自己采用的是黑盒验证的思想，各个角色从本身的角度验证是否可以知足安全目标或者安全属性，若是咱们生命的安全属性不能被知足则就存在攻击路径，咱们在对协议进行形式化安全分析的时候并非对协议的仿真，而是对协议中存在的加密和认证的环节进行高度抽象后进行形式化的描述。经过确认协议当中所涉及参加的角色，声明角色和常量以及协议过程产生的随机变量来形式化描述整个协议事件。而且须要对角色的行为分别进行形式化的描述，声明协议中所要达到的安全属性。Scyther会根据声明的安全属性来验证是否知足要求。若是形式化描述规范可以知足角色之间传递的内容认同，路径输出中不存在错误，

三、基于角色的攻击输出可能会存在 角色不一样在攻击模型下输出的攻击数量不一样。声明的安全属性会对应着攻击测试的验证输出。对存在的攻击输出至少一个攻击（Scyther在界限内验证对应声明的安全属性存在一个攻击以后不会再验证）

四、对于攻击图输出

  对于攻击输出图须要从新绘制成分别对每个角色的攻击路径图，对应输出的攻击图都会安全声明的安全属性标明 。