Scyther GUI 攻擊輸出圖的解釋

一、在聲明事件的安全屬性的時候也就是整個過程要驗證的 對象：

       Scythe 的安全屬性  分爲下面幾種：

•    Secrecy: 表示數據傳輸過程當中是安全的，即便經過不信任的網絡傳也不能被攻擊者得到
•    SKR： SKR表示的意義與 Secrecy相同，只是在session-key reveal 攻擊模型中，將數據泄露給供給者。
•   （Commit，Running）：用於模型之間對數據傳輸的承認

   另外還有認證屬性組：

I-SYNCH、NI-SYNCH、I-AGREE 、NI-AGREE

•    Reachable  用於檢測聲明是否被知足，因爲Scyther的檢測模式下
•    Empty   此聲明不會被驗證，只是Scyther爲支持其餘驗工具時使用
•    Alive  存活性
•    Weakaggree    協議不一致

 二、攻擊圖輸出的解釋

一個攻擊對應着一個攻擊輸出圖，下圖是TLS協議在強安全模型下的其中一個輸出攻擊圖，下面對圖上的參數做用一個說明， 在每個聲稱對應一行，每一行被分紅好幾列。

  第一列表示協議的名字 ，

第二列顯示的是角色的名字，（比方說TLS協議中 a 就表示 客戶端 ，b 表示服務端），

第三列表示的是惟一標識符  tlspaulson 表示協議 ，a1 表示聲明的一個標籤。

第四列顯示聲明類型，和聲明參數

看上面的截圖   在 Status（狀態欄）下面是兩列， 第五列顯示協議驗證過程的世界結果，當聲稱是錯誤的時候顯示 Fail ，當聲稱是正確的時候顯示的是 OK 。

第六列完善以前一列的稱述，在有些狀況下 scyther 驗證過程不是完整的，（在下一章中詳細介紹），若是這列的狀態是  Verified （確認）表示聲稱是真的，若是狀態是 Falsified （僞造）表示聲稱是錯誤的。若是這一列是空的，那麼 狀態  fail/ok 取決於 指定的邊界設置。

第七列 是註釋  用於進一步解釋結果的狀態，這一列的表示存在多種狀況，分爲下面幾種：

•      至少存在 X 個攻擊 （At least X attacks）:一些攻擊在狀態空間中可以發現， 因爲問題的不肯定性的緣故，或者是由於搜索的分支和綁定的結構，不能肯定是否還存在其餘攻擊狀態
•      在默認的Scyther 設置中 ，當找到一個攻擊的時候Scyther會中止驗證，
•      至存在 x 個 模式
•      肯定存在 X個 模式（Exactly X pattern）：這種是跟以前的兩個一致的，只發生在有 ‘Reachable’的聲明中，發現的狀態並沒與真正受到攻擊，而是可達狀態的類別。
•      限制範圍內沒有找到攻擊（No attack within bounds）：限制範圍內麼有找到攻擊，可是在狀態界限以外可能存在攻擊
•      沒有攻擊（No attacks）：在狀態空間界限外或者內都沒有發現攻擊，能夠創建證據沒有攻擊即便是狀態空間沒有界限設置，如此安全屬性驗證成功。

 三、狀態空間的限制

        限制運行次數在Scyther中能夠更改，若是設置運行次數爲5，沒有發現攻擊，就是說在少於5次的運行中是不存在攻擊的，可是不必定大於5次後任然是這樣的結果，

四、攻擊圖

     如上面的圖，每個垂直軸表示一個運行，運行是存菱形出開始，菱形表示運行的建立，並提供了運行了有關信息，