标签：message role 匹配 实验 运行 fresh secret protoc 秘密
1、协议的主要的核心是定义一个协议在协议中声明角色：
Protocol ExampleProtocol(I,R){
role I{ };
role R{ }；//在角色中一开始我们没有定义角色的行为
} ////在协议中声明两个角色，分别是 I 和 R
很多安全协议依赖生成一个随机的值，他们可以在一个角色中使用 fresh 声明一个临时的值，列如下面 在角色X中 使用 fresh 声明一个Nonce 类型的临时值 ：
role X(.....){
fresh Na：Nonce;
send_1(X,Y,Na)；
}
代理可以使用变量存储接受的值（术语），列如，使用 Na 接受一个临时变量：
roel Y(.....){
var Na:Nonce;
recv_1(X,Y,Na)；
}
对于局部变量，对于新生成的值以及变量像Na ,对于角色 都是局部变量。这样我们可以指定一个新生成的临时变量Na 在一个角色中，另一个Na在另一个Na 中不会出现冲突。变量必须出现在接受事件中，不允许未初始化的变量出现在发送事件中。第一次接受事件之后触发执行 ，分配一个值，之后再不能改变。
任何两个术语可以结合成一个术语对，可以写成N个术语对，例如： （x,y,z）再Scyther 中解释成 （（x,y）,z）
2、对称秘钥
任何术语都可以作为堆成加密的秘钥，使用术语 kir 加密 ni 可以表示成 {ni }kir ，除非将 kir 明确的制定为非对称秘钥的一部分，不然除此之外解释为对称加密。
对称秘钥： 对称秘钥的基本结构 定义形式 k （X,Y） 表示长期的对称秘钥共享 X和 Y之间。
3、非对称秘钥
公钥基础的结构是预定义的（PKI）， sk(X) 表示 X 的长期私钥， pk(X)表示对应的公钥，随机数数 ni 在触发者 I 中使用公钥 pk(I) 加密，接受者只能使用私钥 skI(I) 解密。
4、预先定义类型
Nonce 标准类型（经常使用），因此定义在角色内部
Ticket 变量类型（可以被任何术语替代）
5、用户定义类型
使用关键字 usertypes
usertypes MyAtomicMessages;
protocol X (X,R){
Role I{
var y:MyAtomicMessage;
recv_1(I,R, y) }
}
这中新申明的类型实例化只能使用自身的类型来实例化，
在事件中，每个接受事件和发送事件都是配套的，但是如果我们仅仅想模拟向对手发送或者接受（单向事件）的时候 Scyther 工具就会提示错误，可以使用标签提前对事件进行标注，如下面：
send_!1(I ,I LeakToAdversary );
事件申明在角色规范中建模特定的安全属性，例如下面的声明事件模型中 Ni 表示 秘密
claim (I,Secret ,Ni) ;
下面事件中的匹配事件中Y 由 hash (X,Y,R )替代,但是这种规则避免复制
var X : Nonce ；
var Y ;
recv(R,I,X);
match (Y,hash（X,I，R）);
send(I,R,Y，{Y}sk(I));
另外，说明匹配事件match(pt,m) ,存在一个 ∂使得 ∂pt=m才会执行，相反不匹配事件表示 mot match(pt,m) 不存在替代 ∂ 使得 ∂pt=m 成立才会执行
角色定义就是时间的序列声明，包括定义、发送、接受、或许和事件申明，而协议定义的在协议体内会用一系列的角色定义
4、使用Scyther形式化分析协议注意的关键步骤
协议中的逻辑消息组件和内部的功能（公钥和私钥，每次运行或者 不变的常量）
消息结构 ： 配对 加密 签名 散列
消息流 顺序 ， 涉及的事件
5、在做实验之前首先要弄懂scyther 的已经验证过得几个简单的例子，从中首先弄清楚 scyther 验证的 协议 Needham-Schroeder protocol ,,协议有由角色定义，角色反过来由事件定义, scyther 输入文件中最为核心的是 协议的定义
标签：message role 匹配 实验 运行 fresh secret protoc 秘密
原文地址：https://www.cnblogs.com/xinxianquan/p/10581911.html
