1、Needham-Schroeder public Key Protocol （基于非对称的加密协议）
the Protocol's authors are Roger NeedHam and Michael Schroeder
定义 密钥对：
const pk: Function
secret sk: Function
inversekeys(pk ,sk):// pair of asymmetric keys
其中 const 定义全局常量，
（这篇博客存在草稿箱好长时间了，乘着今天把里面的几项工作做完，重新整理一遍，里面的几个安全属性的定义重新找了一下资料，在此补充完整）
在声明协议的安全属性的时候使用固定的术语原语：
Secret：声明保密，即使我们在不信任的网络上交换数据，某些信息也不会被泄露给入侵者
SKR：泄露会话秘钥（Session-key）的时候任然安全，类似于Secret
Aliveness： 参见论文（G.Lowe .A hierarchy of authentication specification.In Proc 10 IEEE Computer Security Roundation Workshop (CSFW) ,page31-44 IEEE,1
这个概念比较复杂----就是说如果在A的本地事件存一个时间窗口 I ，则A经过身份验证的B 使 A 确信B在 I 中还存活着。
Weakagree： 参见论文（G.Lowe .A hierarchy of authentication specification.In Proc 10 IEEE Computer Security Roundation Workshop (CSFW) ,page31-44 IEEE,1997）
Commit, Running ：所有的内射性协议要求在，角色的声明中，触发者中添加 Commit ，接受者添加 Running
Nisynch:声明非单射性
Niagree:
Reachable: 声明协议触发者传输的参数和消息是可以无误抵达接受者
Empty: 不做任何处理的的安全属性
声明全局变量的关键词：
声明局部变量的关键词：
2、符号化分析关注点
通俗的来讲，符号化分析集中在下面几个方面，
- 逻辑消息组件以及协议的功能（公钥和私钥、每个会话运行产生的常数）
- 消息结构（密钥对，加密算法，签名，哈希函数）
- 消息流（顺序、涉及参与的通信实体-角色）
另外的一些协议的元素可以抽象化，（可以忽略的字符串可以抽象出来），比如一些复杂的循环的控制结构可以被限制成在一定的次数内。
3、协议验证安全属性该如何声明
- 协议的单射性或者非单射性改如何判断？
具体的单射一致性和非单射一致性请参照之前非博客（非单射一致性和单射一致性的概念辨析），那么之后的就是对协议本身的分析是否添加单射性和非单射性
- 协议验证的安全属性特征添加的依据是什么？
具体的协议的安全要求都有自己的规范文档的描述，在Security中会提出协议的安全属性的要求，也就是协议的RFC文档，当然不同的协议在实现的安全属性上在实现上可能是一个不可逆的算法或者依赖于随机数，这个要根据协议自己安全属性的实现原理来分析，但是总体的协议安全属性目标，在协议的文档中是指出的。
- 我们需要验证哪些属性或者参数？
具体的要看协议中药保证的安全参数，比方说协议通过某种加密方式保证传输的一个随机数是安全的，哪我们就直接声明 这个随机数是安全的 。如果最厚根据协议分析得到在某次的会话中传输的依噶加密会话消息整体是安全的，那我们对这个消息的会话声明就 声明这个整体的传输的加密消息是安全的。具体的形式如下：
claim _r1(I, Secret,ni) 其中 I 是角色实体， Secret是声明的安全属性 ni 是被声明安全的随机数
claim_r2(I,Secret,hash(ni)) 其中整个 hash(ni) 被声明是安全的
- 在形式化描述的时候触发者和响应者之间的形式化描述有什么差别
关键字位置互换（在触发者产生的随机数用 fresh 声明，但是在接受者中需要使用 变量 var 指代）
发送者和接受者之间的关系需要互换，
安全属性声明的标签是唯一的，
4、对 Needham-Schroeder Public Key Protocol 协议的分析
因为参照的是官网上提供的Case-Study的这个协议的案列，上面的协议角色一共三个(这里只摘抄了两个角色的) ，我后续按照文章补充了形式化的代码 具体如下：
/* * Needham-Schroeder protocol */
protocol ns3(I,R)
{role I
{fresh ni: Nonce;
var nr: Nonce;
send_1(I,R, {ni,I}pk(R) );
recv_2(R,I, {ni,nr}pk(I) );
claim(I,Running,R,ni,nr);
send_3(I,R, {nr}pk(R) );
claim(I,Secret,ni);
claim(I,Secret,nr);
claim(I,Alive);
claim(I,Weakagree);
claim(I,Commit,R,ni,nr);
claim(I,Niagree);
claim(I,Nisynch);
}
role R{
var ni: Nonce;
fresh nr: Nonce;
recv_1(I,R, {ni,I}pk(R) );
claim(R,Running,I,ni,nr);
send_2(R,I, {ni,nr}pk(I) );
recv_3(I,R, {nr}pk(R) );
claim(R,Secret,ni);
claim(R,Secret,nr);
claim(R,Alive);
claim(R,Weakagree);
claim(R,Commit,I,ni,nr);
claim(R,Niagree);
claim(R,Nisynch);
}
}
5、graph输出的攻击图，如何描述，（这里补充说一下，绑定状态空间的目的是为了限定程序的终止运行）
目前国内使用形式化分析工具很少用到Scyther 工具，发表的论文大多是使用输出的攻击图指出目标协议存在安全隐患，但是并没有分析攻击图中输出的会话消息和敌手之间的具体的含义，这也是我想在大论文中准备要加上去的，另外对 Scyther工具的汉化过程存在核心部分在参数调用算法的时候报错的问题，有必要对Scyther整个的框架GUI部分的代码部分做一个全面的分析。这部分工作我会出现在在后续的大论文部分。