下面对 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"  因此攻击者必须重定向该消息。

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

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

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

    一般都是使用GUI，因为简便，在使用command-line 的使用 如果Linux 系统问题会出现很多问题。 我在使用dot工具渲染输出图形的时候 报错提示出现 语法错误。（应该是渲染工具的问题）

4、高级主题