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工具渲染輸出圖形的時候 報錯提示出現 語法錯誤。（應該是渲染工具的問題）

四、高級主題