Scyther攻击输出图的解释（之二）

下面对 Needham-Schroeder 协议形式化分析 的攻击输出图 作一个解释：

Needham-Schroeder使用ns3表示， ns3 协议形式化描述结果以下：

 /*
 * Needham-Schroeder protocol
 */

// The protocol description

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);
    }
}
攻击输出图：

咱们能够看到左边运行代理是 Agent1  代理 角色 R ，右边是运行代理是Agent2 代理  I 角色，代理Agent2 认为响应角色是信任的 Eve （全部的信息泄露，不能保证），除此以外运行的头部方框包含新生成变量值信息和局部变量 ，  每一次消息发送的时候，都会被攻击者获取，在这个例子中，由于攻击者知道代理 Eve的私钥 sk(Eve)  ，可以解密消息得到随机变量 ni#2的值，

 通讯事件 ：发送事件指明一个发送消息，从上面的攻击图中能够看出，第一次发送发生在运行 2 的第一次发送事件，------》   send_1（Eve,{Agent#0, ni#2 }pk(Eve)），接受事件对应于消息的成功接受，在这次攻击中第一次接受事件 ，接收到的消息是：  recv_1（Agent#0，{Agent#0，ni#2}pk(Agent#1)） ,攻击者不能预测随机变量 ni#2的值，因此只能等待 运行 2 生成 ni#2以后，代理Agent1 才能接受到消息，

在攻击输出图中，红色箭头连线表示发送消息和接受消息不匹配，咱们知道攻击者在发送的消息以后构造要接受的消息，所以他必须使用发送消息的信息来构造接收到的消息。

在攻击输出图中，黄色箭头表示消息以彻底相同的方式发送和接受，代理不一样意 消息任意的发送，所以他被标记为 "redirect"  所以攻击者必须重定向该消息。

在攻击输出图中，绿色箭头表示收到的消息和接受到的消息彻底相同，表示两个代理之间 正常的通讯

 注意：若是接受事件没有传入箭头，表示接受术语能够从入侵者的初始知识生成，若是角色读取仅包含代理名称的原始消息，则入侵者能够从其初始知识生成该术语。

三、使用 Scyther command-line 工具验证

    通常都是使用GUI，由于简便，在使用command-line 的使用 若是Linux 系统问题会出现不少问题。 我在使用dot工具渲染输出图形的时候 报错提示出现 语法错误。（应该是渲染工具的问题）

四、高级主题