1、性能分析
目前來說形式化的分析已經成為安全協議的一種很流行的方法，但是每種工具都用其不同適合的協議，Scyther軟件是一種形式化分析工具，極大的促進了協議的分析和設計，scyther工具在運行界面和安全模型以及搜索等方面的綜合性優勢，形式化分析的方法源自於數學原理和邏輯推理，使用嚴格的語法和與語義，可以准確的 、迅速的證明協議的安全性，並找到協議存在的漏洞。
scyther 可以針對協議的各個屬性進行分析 。
。，
2、Scyther協議形式化分析工具原理
使用描述性語言將要分析的洗衣、、協議進行拆分多個角度
3、EtherNet/IP 協議框架
4、Scyther 在linux在安裝
提示： 形式化分析工具Scyther 依賴的解釋器 Python 版本是2.7（不支持3.0以上），所以在ubuntu上安裝的時配置Python2.7. 如果要在Windows上安裝該工具。不僅要配置Python的環境變量還要配置Graphviz的環境，具體的參照官網上的說明文檔。
首先在GitHub上下載Scyther 源代碼 或者直接在Scyther tools 上下載 地址：https://people.cispa.io/cas.cremers/scyther/install-generic.html
將下載的 scyther-linux-v1.1.3 進行解壓
安裝 圖形工具 如果如下面文件依賴出現報錯 ，按照提示的修復
修復安裝
查看 圖形文件是否存在
出現報錯的時候是因為Python的圖形庫文件沒有安裝，存在依賴的dom 文件 。重新安裝一次 Graphviz ，如果依賴文件存在問題 使用修復安裝（remove 刪除一次殘留）
現在回到解壓的scyther-linux-v1.1.3 文件的個目錄下 執行 scyther-gui.py
安裝成功之后 顯示界面如下：
分析協議的時候Scyther自身的編譯語言 描述 協議的角色、執行體
攻擊向量參數的設置界面如下：
5、使用Scyther來分析工業以太網EtherNet/IP
6、Scyther 協議安全模型的驗證實例
第一部分： 打開協議模型 ，設置攻擊變量的參數執行分析
Scyther is a tool for the formal analysis o the security protocol under the perfect Cryptography , the result Window shows a summary of ths clamis in the proctol ,and the verfication results .here one can find whether the protocol is correct ， or false， and explanation of the possible outcomes of the verfication process ,most important ,if a protocol claim is incorrect , then there exists at least one attack on the protocol , A button is show next to the claim .press this buttom to view the attacks on the claim .as show in the figure (it's not EtherNet/IP ) it's Needham-Schroeder encryption protocol
第二部分： Scyther 的描述性語言語法
Scyther 使用的描述性語言基於C/Java 語法，可以使用java語法的注釋形式，空白的編譯的時候會被忽略（提高程序的可讀性）標識符說那個字符串+數字+^ 或者 -
1、Scyther 核心元素是在文件中的描述的協議定義，最小的一個協議定義如下，定義了連那個協議的角色，括號中可以定義角色的行為。
protocol ExampleProtocol(I,R) {
role I { };
role R { }
};
很多安全協議依賴隨機生成的值，我么可以在一個角色中使用 fresh 關鍵字聲明一個類型為Nonce的隨機變量 Na
role X (...){
fresh Na : Nonce;
send_1(X, Y, Na)；
}
代理可以使用變量來存儲接收到的術語 ，列如我們收到一個臨時變量 Na ,定義如下（變量一定要初始化，在發送事件中）
role Y (......){
var Na : Nonce；
recv_1(X ,Y , Na)；
}
任意兩個可以構造成一個屬於對，可以將屬於 x ,y 寫成 （x, y）,亦可以使用元祖的便是方式 （x, y ,z） ，在Scyther 中可以解釋成（（x , y）, z）。
任意一個術語可以作為對稱加密的秘鑰，使用術語 kir 加密 ni 寫成 { ni } kir 這樣表示對稱加密 ，除非kir 被明確的定義成非對稱加密術語