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 成立才会执行
角色定义就是时间的序列声明，包括定义、发送、接受、或许和事件申明，而协议定义的在协议体内会用一系列的角色定义
6、使用scyther 建立协议安全模型的时需要掌握的技能
逻辑消息组件以及在协议中的预期功能、 消息结构 、消息流
7、使用Scyther形式化分析协议注意的关键步骤
协议中的逻辑消息组件和内部的功能（公钥和私钥，每次运行或者 不变的常量）
消息结构 ： 配对 加密 签名 散列
消息流 顺序 ， 涉及的事件
8、在做实验之前首先要弄懂scyther 的已经验证过得几个简单的例子，从中首先弄清楚 scyther 验证的 协议 Needham-Schroeder protocol ,,协议有由角色定义，角色反过来由事件定义, scyther 输入文件中最为核心的是 协议的定义
role I {
fresh ni: Nonce ;
var nr: Nonce;
send_1(I,R ,{I,ni}pk(R));
recv_2(R,I,{ni,nr}pk(I));
send_3(I,R, {nr}pk(R));
claim_i1(I,secret ,ni);
claim_i2(I,Secret,nr);
claim_i3(I,Niagree);
claim_i4(I,Nisynch);
}
role R{
var ni: Nonce;
fresh nr: Nonce ;
recv_1(I,R,{I,ni}pk(R) );
send_2(R,I,{ni,nr}pk(I));
recv_3(I,R,{nr}pk(R));
clamin_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Niagree);
claim_r4(R,Nisynch);
}
9、协议
// 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_i3(I,Alive);
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);
}
}
对上面的标签做一个说明，第三例表示唯一标识符，第四列表示标签。
