Needham |
您所在的位置:网站首页 › Needham-Schroeder › Needham |
1、Needham-Schroeder Public key Protocol 协议的通信认证的过程 顺序图的 1、 A-> S : A, B 2、 S->A: {Ks, B }Ks-1 3、 A->B : {Na, A }Ks 4、 B->S: B ,A 5、 S->B: {Ka, A}Ks-1 6、B->A : {Na, Nb}Ka 7、 A-> B : {Nb}Ks 2、下面我们画一个验证的顺序图 (原来的图片没有找到 ,拍一张图片)
3、现在我么来形式化描述这个协议 首先第一步声明变量 : 首先声明非对称密钥 const pk:Function ; secret sk:Function ; inversekeys(pk, sk); 第二步 定义协议 protocol NeedhamSchroeder(I, R , S){ } 第三步定义 协议中参加的角色对象 role I { #这里 I 指代的就是图上的 Alice const Ni: Nonce; // 全局变量 var Nr: Nonce; // 局部变量 send_1(I ,S, (I, R)); 发送的消息 从 I 发给 S 对照上面的图 从 Alice 发给 Server recv_2(S ,I {pk(R), R }sk(S)); I 接受到的消息 , 对应上面的图 从 Server 发给 Alice ........# 后面的形式化 过程根据上图一次添加上 ........# 形式化的规律就是 在一个角色对象中 智能描述该对象直接参与 的通信 claim_I1(I, Secret, Ni); claim_I2(I ,Secret, Nr); # 声明安全属性的时候 是根据协议的安全目标来定义 claim_I3(I, Nisynch) } 在协议的最后规范的描述中 我们添加协议中信任的参与者,这些参与者的秘密信息不能信任 const Alice ,Bob ,Server ,Compromised :Agent untrusted Compromised ; const nc: Nonce; Compromised sk(Compromised); 第四步添加配置敌手的模型和参数 开始验证协议
具体的信息显示 可以根据上面的图来 观测 ,如果发现存在攻击 显示 Fail 不存在攻击 显示 NO 我们关心的就是上面声明 出现 验证过程中 发现符合安全声明的 部分
附录 全部的形式化 描述 protocol needhamschroederpk(I,R,S){ role I { fresh Ni: Nonce; var Nr: Nonce;send_1(I,S,(I,R)); recv_2(S,I, {pk(R), R}sk(S)); send_3(I,R,{Ni,I}pk(R)); recv_6(R,I, {Ni, Nr}pk(I)); send_7(I,R, {Nr}pk(R)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); claim_I3(I,Nisynch); } role R { fresh Nr: Nonce; var Ni: Nonce; recv_3(I,R,{Ni,I}pk(R)); send_4(R,S,(R,I)); recv_5(S,R,{pk(I),I}sk(S)); send_6(R,I,{Ni,Nr}pk(I)); recv_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); claim_R3(R,Nisynch); } role S { recv_1(I,S,(I,R)); send_2(S,I,{pk(R),R}sk(S)); recv_4(R,S,(R,I)); send_5(S,R,{pk(I),I}sk(S)); }}
|
CopyRight 2018-2019 办公设备维修网 版权所有 豫ICP备15022753号-3 |