工業以太網EtherCAT協議形式化安全評估及改進

馮 濤 王帥帥 龔 翔 方君麗

(蘭州理工大學計算機與通信學院 蘭州 730000)(fengt@lut.cn)

傳統的工業控制系統隨著工業大數據[1]和物聯網[2]的迅猛發展，變得更加互聯互通，大量的以太網協議被應用到工業控制系統中，工業以太網協議在其中扮演著重要角色[3].但是由于工業控制系統在設計之初是封閉隔離的，所以大多協議未采用加密認證等信息安全手段[4]，使得攻擊者能夠很容易對數據進行監聽、篡改和竊取等，從而達到破壞系統的目的[5-6].隨著控制系統的網絡化發展以及工業協議的開放化，協議暴露出許多安全隱患，因此需要重點對協議的安全性進行研究.

本文的主要貢獻包括3個方面:

1) 提出了一種基于有色Petri網理論和Dolev-Yao攻擊方法的模型檢測方法;

2) 對EtherCAT協議的安全機制進行了詳細分析，利用建模工具對協議進行了建模，并且驗證了模型一致性.引入Dolev-Yao攻擊者模型對協議進行了安全評估，發現協議存在的漏洞;

3) 對協議存在的漏洞提出了相應的新方案，并對新方案進行了安全性驗證.

1 相關工作

對協議進行安全評估一般使用的是形式化分析方法，包括模型檢測方法、定理證明方法、類型檢測方法以及模態邏輯方法等.文獻[7]分析的模態邏輯方法雖然能夠對安全協議進行建模和驗證，但是該方法抽象度過高，無法對協議交互的細節進行描述，無法展現協議運行的整體過程.文獻[8]中分析了定理證明方法能夠不限制協議的運行次數，但是不能夠實現自動化.文獻[9]中指出類型檢測方法能夠得出安全協議的結論，但是不能表現出攻擊序列.基于模型檢測的安全評估方法，能夠對協議的行為進行安全建模，但是面臨狀態爆炸問題.針對于EtherCAT協議的安全研究，文獻[10]通過基于機器學習的異常檢測方法對EtherCAT進行了分析，發現該方法不僅能夠進行異常檢測，還可以標記攻擊類型，但是未給出相應的改進方案；文獻[11]中通過建立面向數據流的模型對EtherCAT進行分析，發現該方法能夠對協議進行直觀、準確的圖形表示，并且能夠驗證協議的正確性，但是建模效率較低，一旦出錯就得重新建模.

綜上所述，目前已有的對工業以太網協議安全研究的工作大多集中在協議自身安全功能的實現，對協議的安全評估還處于起步階段，針對工業以太網協議安全評估模型的建立，以及攻擊者模型的建立，存在一定的問題.本文針對EtherCAT協議中的安全機制FSoE進行重點研究，以文獻[12]中的有色Petri網理論和Dolev-Yao攻擊方法為指導，利用建模工具CPN Tools對協議進行安全評估，挖掘協議漏洞，提出新的改進方案，并且對新方案進行安全性驗證.

相比已有的研究工作，本文提出了基于有色Petri網理論和Dolev-Yao攻擊方法的模型檢測方法對協議進行安全分析；對協議的模型進行一致性驗證，并且引入攻擊者模型對協議進行安全評估；對協議安全評估的結果，提出針對性的新方案，并對新方案進行安全性驗證.

2 相關理論

2.1 EtherCAT及其運行原理

EtherCAT協議是由EtherCAT技術集團(ETG)支持[13]的一種流行的實時工業以太網，該協議使用了以太網標準IEEE802.3的物理層和鏈路層，并且由Beckhoff定義.它是一種開放的實時以太網通信技術協議，具有高速低延時、適用性強、符合以太網標準、刷新周期短、同步性能好等特點，支持多種網絡連接拓撲結構.

EtherCAT協議的工作原理如圖1所示,Ether-CAT主從站之間的交互行為是由主站主動發起的，主站通過標準的以太網數據幀的形式將EtherCAT數據幀發送給從站，報文在經過每個從站時，從站對報文中與自己相關的數據信息進行相應處理，在報文的指定位置進行數據的讀寫，并且對計數器信息WKC(working counter)進行加1操作來表示從站對報文進行了處理，然后將數據幀傳輸到下一個從站節點，經過最后一個從站節點的處理后進行返回，最終通過第1個節點返回到主站[14-16].

Fig. 1 The operation principle of EtherCAT protocol

2.2 安全機制FSoE簡介

現代通信系統不僅要實現控制數據的確定傳輸，還要在相同的介質中進行安全關鍵控制數據的傳輸.

EtherCAT使用FSoE(fail safe over EtherCAT)機制來實現該目的.EtherCAT安全技術是基于IEC 61508開發的，由TüV認證，并符合IEC 61784-3標準.該協議可支持功能安全等級SIL 3的安全應用場合.安全數據幀可被看作一個“安全容器”，其中包含了安全關鍵過程數據以及一些用于保證數據安全性的額外信息[17].

安全數據幀如圖2所示，其至少可以傳輸1B的安全數據(Safedata)，也可以傳輸1 B或2 B倍數的Safedata，每2 B的Safedata被2 B的CRC校驗.Safedata的長度在FSoE從屬安全設備描述中定義，其最大數量不受協議的限制；CRC校驗結果包括4種因素，分別為最后接收到的FSoE幀的CRC、傳輸數據(ConnlD,CMD,Data)、CRC的索引以及會話ID；其中的連接ID指示FSoE主節點和FSoE從節點之間的連接，它應該是系統中唯一的連接ID，必須在配置中進行檢查.

Fig. 2 Data frame structure of FSoE

2.3 CPN及建模工具

Petri網的概念是由德國科學家Carl Adam Petri最早提出的，后來出現了許多擴展的概念，例如時間Petri網、隨機Petri網、CPN等[18-20].形式化建模工具CPN Tools具有編輯、模擬、狀態空間分析和性能分析等特性，而且能夠通過回饋機制對產生的錯誤進行精準定位.CPN建模能夠進行增量語法檢查及代碼生成，在一定程度上保證了模型的正確性.該工具是由丹麥奧胡斯大學基于Design/CPN開發的，使用良好的人機界面技術對用戶圖形界面(GUI)進行了設計，不僅能夠對有色Petri網進行編輯、模擬和分析，而且支持時間CPN和分層CPN，借助CPN工具，用戶不僅可以輕松建模，還可以仿真和分析并行系統[21-22].

3 EtherCAT協議建模

在創建大型的、比較復雜的Petri網時，用傳統的CPN模型是比較麻煩的，我們基于模塊編程化思想，利用CPN建模工具內的替代變遷的概念可以將CPN網絡結構拆分成多個小塊.具有替代變遷的網絡是多層次的網絡，我們可以先從廣義上建立一個簡化的網絡模型，然后再利用高層次中的替代變遷關聯到更為詳細的子頁面中去，這樣可以逐步細化自己的模型.

工業以太網的協議模型一般由3個部分組成，分別為發送端、接收端和中間的通信網絡，但是一般用于工業上的協議通信都比較復雜，建立傳統的模型可重用性較低，而且不能很好地表現其功能，利用分層建模的方法可以降低復雜度，本文將協議建模劃分為頂層、中層和底層3個層次.

3.1 EtherCAT協議消息流模型

EtherCAT主從站之間存在2種通信模式，分別為過程數據通信和郵箱數據通信.EtherCAT使用安全機制FSoE來保證協議的安全性，該安全機制使用了過程數據通信模式，如圖3所示為其信息的傳輸過程.

1) 主站發起會話連接請求，請求信息包括主站地址、從站地址以及會話連接ID.

2) 從站處理接收到的信息，如果連接成功，則回復連接成功消息和連接ID，如果失敗，則進行重置操作.

3) 主從站成功建立連接后，進行安全數據傳輸，主站將安全數據進行分段處理，拆分為多個字節，然后對拆分后的安全數據分別進行本地CRC校驗，最后將安全數據、CRC校驗數據、命令信息、連接ID和計數器信息一并發給從站.

4) 從站接收到數據后，會將安全數據在本地進行CRC校驗，然后與接收到的校驗數據進行對比，如果相同則進行相應的命令操作，然后將計數器信息加1后，回復主站計數信息；如果不同，則進行重置操作.

Fig. 3 Message flow model of EtherCAT protocol

3.2 EtherCAT協議的CPN模型建立

本文將Ethernet協議的安全機制FSoE的主從站交互過程進行具體建模，該安全機制使用的是過程數據通信模式.

EtherCAT協議的頂層CPN模型如圖4所示，頂層模型從整體上模擬了協議的會話過程，包括協議的通信雙方、通信網絡以及傳輸信息.圖4中雙線矩形代表替代變遷，橢圓代表消息庫所，通信的主站用替代變遷Master表示，通信從站用替代變遷Slave表示，通信網絡用替代變遷NET表示.

協議的中層模型由5個替代變遷和9個庫所組成，如圖5所示.主站向從站發起建立連接信息的過程由替代變遷Connection表示；從站對主站的連接信息進行處理和回復的過程由替代變遷Connection′表示；主站向從站發送安全數據的過程由替代變遷Safedata表示；從站對安全數據處理和回復的過程由Safedata′表示.

Fig. 4 Top level model of EtherCAT protocol

Fig. 5 Middle level model of EtherCAT protocol

Fig. 6 Internal model of alternative transition Connection

EtherCAT協議的底層模型包括5個部分，我們按照協議主從站整體的交互順序，依次對會話連接過程和安全數據傳輸過程做詳細介紹.圖6對替代變遷Connection的內部模型進行了詳細描述.變遷Conn_MAC將主站地址信息Mac_M和從站地址信息Mac_S合并成地址信息，變遷Combination將地址信息和連接ID合并為連接請求信息，通過庫所Send_conn發送到從站；從站回復的確認信息由庫所Rec_ConnID進行接收，確認信息通過變遷R_ConnID進行處理，然后將連接ID通過庫所ConnID發送給安全數據.

圖7對替代變遷NET的內部模型進行了詳細描述.變遷Transmit_conn和Transmit ConnID分別模擬了在建立連接過程中，主站向從站發起連接請求信息的傳輸路徑以及從站向主站回復信息的傳輸路徑；同樣在安全數據傳輸過程中，主站向從站發送安全數據的傳輸路徑和從站向主站回復計數信息的傳輸路徑由變遷Transmit Safedata和Transmit WKC表示.

圖8對替代變遷Connection′的內部模型進行了詳細描述.庫所Rec_conn用來接收主站發送的連接信息，變遷R_conn message對接收到的信息進行處理，然后將接收到的消息存儲到庫所ReceiveMAC中，變遷Reply將連接ID信息和確認信息進行整合，通過庫所Send_ConnID發送給主站，如果連接失敗則從站會進行重置操作.

Fig. 7 Internal model of alternative transition NET

Fig. 8 Internal model of alternative transition Connection′

Fig. 9 Internal model of alternative transition Safedata

Fig. 10 Internal model of alternative transition Safedata′

圖9對替代變遷Safedata的內部模型進行了詳細描述.變遷CRCdata首先對安全數據進行本地的CRC校驗，然后將安全數據和CRC檢驗數據進行合并；變遷Combination′將接收到的確認連接ID信息、CMD命令信息和計數信息WKC進行合并；最后這些數據由庫所Safeoutput一并發送給從站；計數器WKC的更新信息由庫所Rec_WKC進行接收.

圖10對替代變遷Safedata′的內部模型進行了詳細描述.庫所Safeinput用來接收主站發送的安全數據信息，變遷Safe_Message將接收的安全數據信息進行分解，從站對安全數據進行本地的CRC校驗，然后與接收到的CRC校驗數據進行對比，如果相同則按照接收到的命令信息進行操作，并將接收到的計數信息加1，由庫所Send_WKC返回給主站.如果本地生成的CRC檢驗值與接收到的校驗數據不同，則進行重置操作.

3.3 EtherCAT模型一致性驗證

我們將對建議的原始EtherCAT協議的CPN模型進行一致性驗證，使用了狀態空間[23]分析工具.首先我們對所建立的模型給出了預期結果，模型會成功進行會話連接和安全數據傳輸，整個交互過程中不會產生重置操作.通過對表1的狀態空間結果分析，可以發現狀態空間節點、有向弧與強連通節點、強連通弧的數目相同，說明我們建立的原始模型不存在導致狀態無限循環和迭代行為，所有狀態節點都是可達的；主狀態節點和活變遷為0，說明原始模型沒有始終處于激活狀態的活變遷，同時也不存在任意可達的狀態；死節點為1，表示全部請求都被從站執行；存在2個死變遷Reset和Reset1，變遷Reset是用來表示連接失敗后的重置操作，變遷Reset1是表示數據傳輸過程中CRC校驗失敗后的重置操作，這2個變遷均為死變遷說明模型不存在連接失敗和數據傳輸失敗的情況，與預期結果一致.

Table 1 State Space Analysis of the Original Model of EtherCAT Protocol

4 基于攻擊者安全評估模型

Dolev和Yao發表了一篇重要論文，其對協議安全研究發展產生了深刻的影響[24].該論文的主要觀點就是在假設密碼系統是“完美”的基礎上只討論協議本身的安全屬性，這樣能夠不去討論密碼算法的安全性而是專心研究協議的內在安全性質;而且Dolev和Yao提出了攻擊者模型，攻擊者具體強大的計算能力，不僅能夠對協議運行過程中真實實體間交換的信息進行竊聽、截獲、篡改、重放操作，還可以對這些信息進行加密、解密、拆分和組合[25-26].

由于EtherCAT協議具有高度的實時性，數據幀經過每個從站的時間極小，在從站中數據幀的接收與解碼、數據的提取與插入、數據幀的轉發都是由硬件來實現的，因此本文將嘗試對主從站之間的網絡通道引入攻擊模型.

4.1 引入攻擊者模型

根據Dolev-Yao攻擊者模型中，攻擊者所具備的對網絡信道發起各類中間人攻擊的強大能力，對原始模型的網絡傳輸層引入重放、欺騙和篡改的中間人攻擊.

如圖11所示，我們對原始模型的網絡傳輸層面引入中間人攻擊包括重放、欺騙和篡改攻擊，圖11中藍色部分標注的庫所和變遷模擬了重放攻擊，變遷TA截獲協議第一次傳輸時的信息，庫所distri能夠存儲分解和待分解的信息，庫所P2和P3存儲原子信息.變遷TC采用攻擊者的分解規則后將形成的原子消息保存到庫所P3中，變遷TH采用攻擊者的過度規則將無法解密的信息采用過度規則保存到庫所P4中.變遷TD將采用攻擊者的合成規則將原子消息合成后保存到庫所P5中.使用并發控制庫所SP對合成規則對應的變遷TD加以限制，初始狀態可使能之外，每當有分解的信息產生后再進行點火合成.變遷TF將攻擊者的信息合成發送到信道端口庫所.圖11中的紅色標注的弧上的表達式和變遷庫模擬了篡改攻擊，表達式中引入的攻擊者attack，通過變遷ATTACK發起攻擊.圖11中的紫色部分模擬了欺騙攻擊，包括了原始網絡傳輸過程中的全部變遷Transmit conn,Transmit ConnID,Transmit,SafeData,Transmit WKC.

Fig. 11 Attacker model

4.2 EtherCAT模型安全性評估

由表2所示的攻擊者模型的狀態空間報告可知狀態空間節點、有向弧與強連通節點、強連通弧的數目相同，說明該協議的攻擊者模型所有狀態節點都是可達的，引入攻擊者模型后，其狀態空間節點和弧的數量相對于原始模型來說增加不是太多，說明引入攻擊者模型后不會出現狀態空間過大或者爆炸的情況，降低了狀態空間節點規模，減少了不被接受者認可的消息，在保證攻擊能力的基礎上提高了攻擊模型效率.說明我們引入的攻擊者模型是有效的.

Table 2 State Space Comparison of Models

將原始模型和加入攻擊模型后的狀態空間進行對比，我們發現死節點變成6個，死變遷變成8個.通過對死節點進一步的查詢分析，發現有2個死節點是由于引入重放攻擊和篡改攻擊導致從站進行了重置操作而產生的，剩下的4個死變遷是因為引入欺騙攻擊致使協議產生不可預期的終態而導致的；通過對死變遷進行分析，發現有2個死變遷是由于引入重放攻擊使得會話連接在從站無法使能，另外2個死變遷是由于引入欺騙攻擊導致從站沒有接收到從站的返回信息，其余4個死變遷則是因為引入篡改攻擊導致在安全數據傳輸過程中CRC校驗錯誤而未使能.通過狀態空間的對比分析，可以發現攻擊者模型對原始模型的會話連接和安全數據傳輸過程發起了有效攻擊，側面反映出原始協議存在中間人進行重放、欺騙和篡改的漏洞.

5 EtherCAT協議新方案

5.1 新方案加固方法

通過引入攻擊者模型對協議進行安全評估，發現協議存在中間人進行重放、欺騙和篡改的漏洞，針對安全評估結果，我們在協議的會話連接過程中引入秘鑰分發中心進行認證加固，為了確保安全數據的安全傳輸，我們在安全數據傳輸過程中加入Hash值.

如圖12所示為改進后的消息流圖，改進后的消息傳輸過程為：

1) 主站向秘鑰中心發生請求，包括主站地址、從站地址和連接ID.

2) 秘鑰分發中心對接收到的數據進行處理，將地址信息和公鑰Ks用從站的私鑰Kb進行加密，與公鑰Ks和接收到的其他信息，一起用主站的私鑰Ka進行加密，然后回復給主站.

3) 主站用自己的私鑰對從站回復的消息進行解密，得到公鑰Ks后，將其余需要發送給從站的消息發送給從站.

4) 從站用自己的私鑰Kb將收到的消息進行解密，獲得公鑰Ks，利用公鑰將新產生的會話連接ID進行加密，然后回復給主站.

5) 主站用公鑰將從站回復的消息進行解密，獲得會話ID后，在本地對會話ID進行函數運行，最后用公鑰加密函數運算的結果，發送給從站進行認證.

6) 從站用公鑰進行解密接收到的消息，并且對解密后的會話ID 進行認證.

7) 建立會話連接之后，主站發起安全數據傳輸，首先將安全數據進行本地Hash，然后將安全數據、Hash值、命令信息、計數信息和連接ID一并發送給從站.

8) 從站首先對接收到的信息進行拆分，然后對安全數據進行本地Hash,用本地生成的Hash值與接收到的Hash值進行比對，如果相同則進行相應的命令操作，并且將技術信息加1，回復給主站.

Fig. 12 Message flow model of the new scheme

Fig. 13 Middle level model of new scheme model

5.2 EtherCAT協議新方案模型

我們將原始協議進行加固，并且進行CPN建模.改進后的中層模型加入了秘鑰分發中心，由6個替代變遷和13個庫所組成，如圖13所示.其中，秘鑰分發過程由替代變遷Key Distribution表示，主從站連接建立以及認證的過程由替代變遷Connection和Connection′來表示，安全數據的傳輸過程由替代變遷Safedata和Safedata′表示.改進后的中層模型整體上描述了秘鑰分發、連接認證和安全數據傳輸的過程.

圖14對新方案替代變遷Connection的內部模型進行了詳細描述.主從站的地址信息和連接ID由變遷Combination進行合并，然后通過庫所SendMAC發送到秘鑰分發中心；秘鑰分發中心返回的消息由庫所RecKs進行接收；主站利用自己的私鑰Ka對收到的消息進行解密，同時對收到的消息進行確認；將解密后需要發送給從站的消息通過庫所SendKb發送給從站；利用解密后的公鑰Ks對庫所RecSid′接收到的從站返回信息進行解密，對解密后獲得的連接ID通過變遷Function進行函數運算；利用公鑰Ks對函數運算的結果通過變遷變遷EncFID進行加密，最后由通過庫所SendfSid發送給從站.

Fig. 14 Internal model of alternative transition Connection of new scheme model

圖15對新方案替代變遷Key Distribution的內部模型進行了詳細描述.秘鑰分發中心將主站的請求信息和要分發的公鑰Ks通過變遷Ks-Msg1進行整合；將收到的地址信息和公鑰Ks通過變遷Kb-Msg進行整合；將要回復主站的消息通過變遷ComMsg進行打包；利用主站私鑰Ka對打包消息通過變遷KComMsg進行加密，最后由庫所RecKs發送給主站.

圖16對新方案替代變遷Combination′的內部模型進行了詳細描述，從站利用自身私鑰Kb對接收到的消息通過變遷DecMsg進行解密；利用解密后獲得的公鑰Ks對新產生的連接ID通過變遷EncID進行加密，加密后的消息由庫所RecSid發送給主站；利用公鑰對主站發送的認證消息通過變遷DecFID進行解密，通過解密后獲得的連接ID進行連接認證.

Fig. 15 Internal model of alternative transition Key Distribution of new scheme model

Fig. 16 Internal model of alternative transition Connection′ of new scheme model

圖17對新方案替代變遷Safedata的內部模型進行了詳細描述，新方案主要改進在于，通過變遷HashSafedata對安全數據進行本地Hash處理，最后將Hash值與安全數據一并發送給從站.

圖18對新方案替代變遷Safedata′的內部模型進行了詳細描述，新方案的主要改進在于，將接收到的安全數據通過變遷HashSafedata進行本地Hash處理，通過變遷Comparison對新產生的Hash值Hdata′和接收到的Hash值Hdata進行對比處理，相同則證明數據沒有被篡改，然后進行相關命令的操作，并且將計數器加1返回給主站.如果不同則進行重置操作.

Fig. 17 Internal model of alternative transition Safedata of new scheme model

Fig. 18 Internal model of alternative transition Safedata′ of new scheme model

5.3 新方案安全評估模型

我們利用相同的方式，引入Dolev-Yao攻擊模型，對新方案模型的網絡層面進行中間人攻擊，包括篡改、欺騙和重放攻擊.如圖19所示，藍色部分模擬重放攻擊，紅色部分模擬篡改攻擊，紫色部分模擬欺騙攻擊.

Fig.19 Security evaluation model of new scheme

5.4 新方案模型安全性驗證

我們將新方案模型安全評估的狀態空間與改進前進行對比，如表3所示.我們可以發現由于引入了秘鑰分發中心進行認證以及對數據加入了Hash值，增加了許多庫所和變遷，使得新方案的的狀態空間節點和弧數目有所增加.利用改進前協議存在的3類中間人攻擊對新方案進行安全性驗證.由表3 的狀態空間對比結果可以發現，新方案模型的狀態空間死節點減少成一個，通過進一步查詢得知，這個死節點表示協議運行后的終態，而改進前的多個死節點是由于攻擊狀態而造成的，說明新方案未遭受攻擊.新方案的死變遷相較于改進前的死變遷數目有所變化，進一步分析發現這些死變遷均發生在網絡層面，是由于攻擊者無法發起有效攻擊而造成的.攻擊者無法獲取協議連接過程的會話秘鑰，而無法對獲取的信息進行解密分解，從而無法發起重放攻擊；在數據傳輸層面，新方案對協議的傳輸消息進行了Hash處理，由于Hash值的不可逆性，所以攻擊者無法對消息發起篡改攻擊；由于新方案對協議加入了認證，所以攻擊者無法對協議進行欺騙攻擊.

Table 3 Comparison of the State Space of the Safety Assessment Model

通過分析表明，由于攻擊者無法獲得消息的會話秘鑰、認證秘鑰以及無法篡改數據的Hash值，使得攻擊者無法發起攻擊，從而證明了新方案能夠防御之前的3種中間人攻擊，滿足協議安全機制需求.

5.5 新方案性能分析和分析方法對比

本節我們對新方案進行性能分析，新方案通過引入秘鑰分發中心對協議主從站建立連接的過程進行認證加固，秘鑰靠秘鑰分發中心分發，不需要主從站生成，因此對協議通信的整體時間消耗較小.新方案在安全數據傳輸中加入了Hash值，不需要對安全數據進行過多的加密操作，因此不需要對平臺進行過大的升級，只是對整個通信來說，增加了計算、通信和存儲數據的開銷.所以改進方案對協議運行的開銷不大，僅僅增加了計算和存儲成本.本文在對協議進行引入秘鑰分發中心和Hash函數改進時，增加了協議消息交互的步驟，在增強協議安全性的同時會對協議的實時性有所影響.

我們將本文用到的形式化分析方案與其他分析方法做比較，文獻[10]中通過基于機器學習的異常檢測方法對EtherCAT進行了分析，發現該方法不僅能夠進行異常檢測，還可以標記攻擊類型；文獻[11]中通過建立面向數據流的模型對EtherCAT進行分析，發現該方法能夠對協議進行直觀、準確的圖形表示，并且能夠驗證協議的正確性.通過表4的對比分析，我們可以看出本文的基于有色Petri網理論和Dolev-Yao攻擊方法為指導模型檢測方法不僅能夠進行直觀、準確的圖形化描述和驗證協議功能的正確性，還可以發現協議的攻擊類型，對協議通過引入攻擊者進行異常檢測.同時方案對引入的攻擊模型進行了改進，解決了傳統模型檢測方法的狀態空間爆炸的問題，可以用該分析方案對其他工業以太網協議進行安全分析與研究.

Table 4 Comparison of Protocol Formal Analysis Methods

6 總結與展望

本文將研究的重點放在工業以太網應用熱門的EtherCAT協議的安全機制FSoE上，首先通過對協議安全機制消息流的分析，利用建模工具CPN Tools對協議進行HCPN建模；然后在原始模型的基礎上加入攻擊者模型，并且通過對原始模型和攻擊模型狀態空間表進行對比，對模型進行安全性評估發現協議存在重放、竊聽和篡改3類中間人攻擊；最后針對協議所存在的3類攻擊提出了新的方案，并且對新方案進行再次建模，引入攻擊者模型進行再次攻擊，通過分析改進前和新方案的狀態空間表，得出新方案可以有效防御重放、竊聽和篡改3類中間人攻擊.但是本文研究目的是為了改進協議的安全性，對協議的實時性考慮不足，而且只對協議進行了中間人攻擊，并未考慮協議是否存在其他形式的攻擊.下一步將考慮協議在保證安全的情況下是否滿足實時性要求，還有在其他攻擊形式下是否還存在安全的不足.