Scyther tools 协议形式化分析帮助文档翻译
一、Scyther软件做者网站的整理html
Scyther工具的网站主页：https://people.cispa.io/cas.cremers/index.htmllinux
首先 对Scyther软件的资料进行整理，做者的不少关于Scyther的资料都是公开在本身的官网上的。算法
协议使用角色序列做为参数，而后在体内进行定义：安全
三、对称角色协议：服务器
一些对手妥协模型规则，像SKR、LKR （aftercorrect），依靠合做关系。对这种协议在角色和算法上都对称，（像HMQV），这不是适当的合做关系，使用正确的合做关系，协议须要使用说明做为一个对称协议，指导Scyther使用适当的合做。函数
四、全局声明工具
在不少应用中使用全局常量，这包括字符串常量，标签、或者协议的定义。他们的建模和使用方法以下：性能
5.7 Miscellaneous 混杂的学习
5.7.1 Macro 宏定义网站
使用宏定义是容许的，是对特殊术语的缩写，其语法的使用方法以下：
macro MyShortCut= LargeTerm ;
像下面这样的，协议包含了复杂的消息或者重复的元素，宏定义能够简化协议的描述（规范）
注意的是 宏定义有全局性，能够处理同层语法层面 ，者容许协议消息的全局缩写
5.7.2 导入文件
在一个协议描述中可能导入其余文件 ，使用 include 导入相关的协议描述文件
5.7.3 one-role-pre-agent
操做语义容许代理执行任何角色，甚至是不一样的角色在同步。这种建模使用在最糟糕的场景中，敌手能够有不少种利用。可是在具体的设置中代理只执行一个角色，列如服务器和客户端集不相交，或者RFID标签和Reads 标签不相交，在这种状况下，咱们不考虑领代理能够执行多个角色的攻击，能够经过下面的方式建模
option "--one-role-per-agent"; //容许代理在多个角色中。 这将引发Scyther 忽略 多个
5.8 输入语言BNF语法的介绍
下面给出了所有的输入语言BNF语法的介绍： 在严格的语法定义中，不存在的像这样的声称的术语 (Niagree 或者 Nisynch ),也没有像以前使用预约义的了预约义的类型 像 Agent ,取而代之的是他们在Scyther工具自身定义常量。
第六章 创建安全模型 Modeling security protocols
6.1 Introduction
使用 Scyther软件对安全协议进行形式化的安全分析以前必须掌握 基本的符号模型。这些模型在 参考文献中有有详细的说明。
粗略的说，符号分析侧重于如下几个方面：
逻辑消息组件和协议预期的功能（公共秘钥和每次生成的或者不变的）
消息结构（配对，加密、签名、哈希加密）
消息流 （顺序、涉及到的参加的角色）
6.2 举例 Needham-Schroeder public key
正以下面的例子 ， 我么使用的协议模型 ,
SCyther使用基于角色描述的协议，最后添加对协议的安全要求，假设没有这种要求，Scyther不知道检查什么项目内容，
在这咱们会检查生成和接受的变量的安全性，将会检查费内射性协议和协议的同步性。
像上面这样就完成了发起者的在协议中定义。在这个简单协议中，响应者角色和发起者角色很是的相似。事实上，仅仅存在一点差异。以下：
关键词 fresh 和 var 交换了位置，在发起者角色中 ni 是被 I建立，是一个新的生成的值，可是对 响应者 R 角色来书 ni 是一个接受到的值，是一个变量。发送事假和接受事件的声明也交换位置，声明使用惟一的标签，因此在接受事件R中已经改变，在执行声明的角色是由 I 转换成 R 。
下面是完整的 Needham-Schroeder protocol 形式化的SPDL描述语言
/*
* Needham-Schroeder protocol
*/
// The protocol description
protocol ns3(I,R)
{
role I
{
fresh ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
recv_2(R,I, {ni,nr}pk(I) );
claim(I,Running,R,ni,nr);
send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr); ////**从左面的安全声明中能够看出，claim 能够在在发送事件和接受事件的声明中出现
claim_i3(I,Alive); ///也能够在事件声明以后，claim能够是多个。声称安全的
claim_i4(I,Weakagree);
claim_i5(I,Commit,R,ni,nr);
claim_i6(I,Niagree);
claim_i7(I,Nisynch);
}
role R
{
var ni: Nonce;
fresh nr: Nonce;
recv_1(I,R, {I,ni}pk(R) );
claim(R,Running,I,ni,nr);
send_2(R,I, {ni,nr}pk(I) );
recv_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Alive);
claim_r4(R,Weakagree);
claim_r5(R,Commit,I,ni,nr);
claim_r6(R,Niagree);
claim_r7(R,Nisynch);
}
}
7.2.1 指定安全属性
为了说明安全属性，角色 I 在术语上和角色 R 一致，变量 ni 和 nr ,想下面这样的插入声明：
在角色 I 的结尾，插入一个声明 claim （I ，Commit ，R，ni , nr）
参考的例子能够 看 ns3.Spdl 整个代码在 Scyther工具中的描述。正规的输出能够看参考文献4
8.使用 Scyther的 GUI 环境 或者 命令输出
Scyher 工具可使用两种主要的方式，一种是基于图形的使用GUI ，第二种是使用基于命令的接口，对于大多数用户来讲使用第一种是最佳的选择，在这节当中咱们详细的说明使用GUI做为输出。
8.1 输出结果
以下面所示，验证 Needham -Schroeder公钥协议输出结果。解释以下：在 ns3 协议中全部的初始化角色，I 是正确的对一个无界限的运行，不幸的是。全部声称响应的角色都是假的，Scyther工具报告发现的至少一个错误对四个声明中的。咱们能够显示这些错误，在结果输出的窗口中，Scyther工具为每一个声明显示单独的一行，每一行又分红几列，第一列显示声明发生的协议，第二列显示的是角色，第三列知名协议和标签，第四例显示声明的类型和参数，
8.2 状态空间绑定
在验证过程当中，Scyther工具探索全部可能协议行为的证据树，在墓中成都上，默认设置是绑定树的大小，确保验证程序的终止，然而，重要的是即便证实书的大小是绑定限制的，可是能够实现无界限的验证，在大多数状况下，验证程序在达到界限以前返回验证结果，然而，若是验证进程到达界限，将会在窗口中显示以下结果： NO attacks within bounds ，这种清空能够解释为Scyther工具没有发现任何攻击，由于到达界限，没有 探索完整个树，极可能任然存在协议的攻击。
默认的界限最大运行次数，或者协议的例子能够经过主界面的设置改变，若是设置最大运行次数是5 ，这时候Scyther 报告在界限中没有发现攻击，这就意味着在涉及运行次数为5 或者更小的时候没有攻击，可是当运行次数为6或者更多的时候将会 存在攻击。对于某些协议来讲增长运行的次数可能会出现更加完整的结果，可是对于某些协议来讲，任然是攻击次数不会增长的。 注意的是验证次数的增长必然会致使验证时间的消耗越大。若是计算机CPU和内存不够使用会死机。
8.3 攻击图输出
输出图的基本元素是箭头和几种方框，图中的箭头表示排序约束（是因为协议角色事件的前缀封闭性引发的，或者取决于入侵者的知识），方框表示运行的建立和运行通讯事件和声明事件。
8.3.1 运行 （Runs）
每个垂直轴表明一个运行（协议角色的实例），如此在这个攻击中咱们能够看到两个运行，么一个运行的开始都是从一个菱形，这表示建立一个运行，并提供有关运行的信息，
对于攻击左侧的运行咱们有以下的信息：（运行 Run 1 ）
能够看到每个运行都会分配一个运行的标识符，能够是任意的数字，为了表示区别不一样的运行，次运行执行协议中的R 角色，由一个代理名为 Agent1 的代理执行，认为正在和代理 Agent2 进行通讯，可是值得注意的是，虽然运行 2 （Run 2）由 Agent2 代理执行，可是这个代理并不认为他正和Agent1 进行通讯。下面是运行2 的信息 （Run 2）
在运行的右侧咱们看到这个运行表明角色的一个实例，从第二行里能够看出哪一个代理正在执行，和正在进行通讯的代理，在上图单位例子中，运行被代理角色 Agent2 代理执行，认为响应者是不受信任的角色代理 Eve ,
除此以外，运 行的头部包含新生成的变量和常量信息，（例如 Run 1 中的是 nr#1） ,和有关局部变量实例化的信息。（Run1 使用随机变量 ni#2 或者 run 2 实例化变量 ni ）
8.3.2 通讯事件 （Communication event）
发送事件指明发送一个消息，在运行 2 中（Run 2 ）第一次发送发生在此次攻击中是第一次发送事件，
每一次消息发送，攻击者能够高效的得到，在这种状况下，由于攻击者知道代理 Eve的公共秘钥 sk (Eve) 他能够解密消息和得到随机变量的的实例化的值 ni#2
接受事件对应着事件的成功接受，在运行 Run 0 第一次接受事件发生在此次攻击中是第一次接受到的事件，
着告诉咱们代理执行运行， Agent 1 接受一条信息显然来自 Agent1 ，接受到的信息是 {Agent#0 ，ni#2}pk(Agent#1) ,认为与之通讯的消息 随机变量 ni#2 被公钥加密，
传入箭头并不表示直接发送消息，相反，它代表约束顺序，只有在发生其余事件以后才能收到此消息，在这个例子中，我么能够看到仅仅当 Run 2 发送初始化消息以后才能被接受，缘由是随机变量的实例化 ni#2 （攻击者不可以预测这个变量）如此必须等待 直到 Run 2 产生它。
在输出图中链接箭头为红色并有标签 “construct” 是由发送事件和接受事件不匹配引发的（没有接受事件），咱们知道攻击者只能在发送的消息以后构造要接受的消息，所以必须攻击者使用本身发送的消息构造消息的接受状况，其余可能的状况包括绿色和黄色的箭头，黄色的箭头表示一个消息发送，接受者以彻底相同的形式接受，然而，代理不一样意任何消息的发送和任意消息的接受，这是由于重定向标签“redirect” 由于攻击者必须重定向消息，一个绿色的箭头表示（不在上面的输出图中）收到的和发送的消息是一致的。表示两个代理之间的正常的通讯关系。
要注意的是，接受事件没有传入箭头表示接受的术语能够经过攻击者初始知识生成。列如一个角色阅读到一个原文信息包括一个代理的名字，攻击者能够生成术语根据本身的初始知识。
8.3.3 声明
第九章 使用Scyther 的命令行工具
全部的Scyther GUI 工具提供的功能在 命令行工具下都是支持的，除此以外，命令行工具还具备GUI不具备的功能，
依靠不一样的操做系统的平台，Scyther 目录包含下面的执行文件
- Scyther/scyther-linux
- Scyther/scyther-w32
- Scyther/scyther-mac
在下面咱们假设，我么使用的Linux版本的操做系统，若是你使用的是不一样的版本，在你的操做系统上替换 下面的Scyther-linux
得到某些命令行的选项的参数列表 使切换 --help 运行可执行文件 ： Scyther-linux --help
如今分析 NeedHam-Schroeder 协议，生成一个 .dot文件 （输入语言为 Graphviz工具）为攻击使用 。使用命令： Scyther-linux --dot-output --output=tls1-attacks.dot TLS_1.spdl
下面使用 Graphviz工具进行输出结果文件 ：dot -Tpdf -O tls1-attacks.dot 可是执行发现出现dot文件执行错误。
根据错误提示调试以后，输出的结果 ，发现输出的结果并无使用 Graphviz 工具画出工具图（这部分缘由以后说明）
为了获得更加详细的命令行的选项参数列表 可使用命令： scysther -linux --expert --help
第十章 高级主题
10.1 建模多个非对称秘钥对
非对称秘钥一般被建模成两个函数，其中一个函数将代理映射到其公钥函数，另外一个函数将代理映射到其私钥。在默认的状况下没哟个代理 x 均有一对秘钥 公钥/私钥 (pk(x), sk(x))
建模其余的非对称秘钥，首先定义两个函数，例如用名字 pk2 表示公钥函数 ，使用 sk2 表示私钥函数 ：
const pk2: Function ;
secret sk2: Function ;
咱们也能够申明 表示非对称密钥对表示方法以下：
inversekeys (pk2 ,sk2);
若是按照上面的额定义，那么若是一个术语加密使用 pk2(x) 只能使用 sk2(x) 进行解密。反之亦然。
10.2 近似等式理论
Scyther工具底层操做语法目前只在语法上考虑对等，当两个术语相等当且仅当语法上相等的时候，然而，存在几种常见的加密结构，更加天然的使用肯定的等式。例如：
显然 Scyther 工具不能为这种等式理论提供直接的支持，可是存在一种直截了当的近似的方式，核心思想是替代平等术语建模，若是敌手掌握了等价类中的一个元素，咱们提供敌手全部的等价类中的术语。例如，等价类 {k(A,B), k(B, A)} 咱们提供敌手同 k(A,B),学习 k(B,A) 的能力，反之亦然。 我么能够适当的引入帮助器来建模协议 （定义 经过 前缀 @）
由于角色能够被任何代理X或者Y 进行实例化，这包括全部的组合代理。上述能够近似等到完善，一个明显的实际相关的漏洞是敌手可学习加密的消息，可是不秘钥，在这种状况下，咱们任然想模拟等式：
{M}k(A,B)={M}k(B,A) ，所以咱们调整咱们的帮助协议以下：
入股协议包含的非对称秘钥术语出如今其余位置，列如嵌套加密或哈希中，咱们会添加更多的角色，可是在实际中并非常常有效果，咱们可使用辅助协议规则更加紧密的提升性能。经过利用更多协议类型的信息，若是协议传输两种类型的加密消息：
{I , nI, nR }k(I, R) 和 {nI }k(I, R) 这时候这样修改辅助协议：
总的来讲，手动检查协议并提取全部的位置，其中来自等价类的术语做为子项，对于这些位置中的每个，创建一个适当的角色在辅助协议中。这也用来建模，像 Diffe-Hellman 幂，对于幂咱们引入一个抽象的函数符号，列如 exp 和一个公共不变的 常量 g ，咱们能够介绍一个辅助协议角色： exp（exp（g,X）,Y）=exp(exp(g,Y),X)
事实上这种近似类型的证实极其有效。从这一点上讲 ，从现实世界上协议全部已知的攻击均可以使用“real”相等理论来建模。当使用近似相等的时候在Scyther下。
须要注意的是虽然这种近似适用于保密和数据协议，他能够致使基于消息的洗衣失败（好比说同步），由于消息等价检查是语法上的，这种检查不能影响引入的辅助协议。
10.3 建模时间戳和全局计数器
Scyther工具底层模型当前不提供代理程序之间共享的变量，每个运行开始都以 clean slate ,独立于先前执行的任何运行。换句话说，全局更新状态不能直接建模。在下面的章节中咱们将提供适当的模型为常见的问题。
10.3.1 建模全局时间计数器
使用新生成的值对全局递增的计数器进行建模，这样确保每个运行使用不一样的值，可是这种计数器是粗略的，计数器接受者不能检查他是技术器先前的值仍是后继的值。
10.3.2 使用随机数建模时间戳
至少存在两种方式来建模时间戳，第一种模型适用于两次运行接受给定时间戳值得几率很是接近的协议，当时间戳很高或两次运行按照顺序发生时，可能会发生时间上的延迟。在这种状况下，能够将时间戳建模成新生成的值，列如 ; nonces ,为了迎合敌手一般知道时间的实事（所以也能够预测时间戳），咱们将一个发送事件添加到角色，该角色为对手提供将使用的时间戳的值。咱们在发送 send 前置标签 ！ T1 为时间戳 T1 ：
10.3.3 使用变量建模时间戳
当两个运行能够接受相同的时间戳值得时候，第二个模型更适用，这对于粗略的时间戳或一般以高并行性执行的角色（列如服务器角色）是常见的，在这种状况下，能够改成将时间戳加密为由对手肯定的值，与以前的解决方案相比， 这是经过预先接事假完成的
10.4 多协议攻击
Scyther 工具可使用在多协议攻击的检测中，（密切相关的协议使交叉协议攻击和选择协议的攻击）这些攻击取决于不一样子协议之间的相互做用，有时候，攻击者可使用来自一个协议的消息或者消息组件来攻击另外一个协议，
最简单的检查多协攻击的方法是结合两个协议的形式化描述在一个文件中实现，建立一个新的 .spdl 文件 在Scyther 工具下进行检测，
参考引文：