Needham-Schroeder Scyther工具形式化过程

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));
    }
}