标签：设置 toc 攻击 包含 秘钥 img 自身 图片 read
1、Scyther软件作者网站的整理
Scyther工具的网站主页：https://people.cispa.io/cas.cremers/index.html
首先 对Scyther软件的资料进行整理，作者的很多关于Scyther的资料都是公开在自己的官网上的。
协议使用角色序列作为参数，然后在体内进行定义：
3、对称角色协议：
一些对手妥协模型规则，像SKR、LKR （aftercorrect），依靠合作关系。对这种协议在角色和算法上都对称，（像HMQV），这不是适当的合作关系，使用正确的合作关系，协议需要使用说明作为一个对称协议，指导Scyther使用适当的合作。
4、全局声明
在很多应用中使用全局常量，这包括字符串常量，标签、或者协议的定义。他们的建模和使用方法如下：
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
正如下面的例子 ， 我么使用剪短的协议模型
标签：设置 toc 攻击 包含 秘钥 img 自身 图片 read
原文地址：https://www.cnblogs.com/xinxianquan/p/10732914.html
