基于CPN 的安全協議形式化建模及安全分析方法

龔翔，馮濤，杜謹澤

（蘭州理工大學計算機與通信學院，甘肅 蘭州 730050）

1 引言

安全協議已成為現代計算機網絡正常運轉的基礎，但由于其設計階段的規范缺失和不可避免的邏輯缺陷，常會帶來潛在的安全隱患，使各種協議的開發和安全性驗證成為一項艱巨的任務[1]。

安全協議的形式化分析一直是網絡安全領域的研究熱點[2-6]。丹麥奧爾胡斯大學開發的有色Petri網（CPN,colored Petri net）工具軟件CPN-Tools，不僅實現了計算機上的CPN 可視化建模，還提供了全部狀態空間的自動計算以及生成狀態空間報告的功能，集成的SML（standard meta language）可以輔助完成各種安全協議的功能評價和狀態路徑搜索。

按照安全協議分析的目的，現有的CPN 協議分析目標可分為三類。第一類是對協議本身進行建模，按照狀態空間報告所提供的各種屬性（活性、公平性等）來判斷協議的設計是否正確，驗證協議的正確性[7-8]。第二類是在協議建模的基礎上引入攻擊者模型，構建恰當合理的安全評估模型以快速找到協議中存在的潛在威脅[9-10]。第三類在第二類的基礎上更進一步，提出協議改進方案并且利用安全評估模型驗證，分析改進結果[11-13]。本文著重研究通過CPN 對安全協議進行分析驗證的方法，并通過實例說明該方法的有效性。

然而，由于沒有統一標準，利用CPN 針對協議安全分析的方法是多種多樣的[14]。近年來，有較多文獻提供了不同解決方案，存在的主要問題如下。

1) 部分文獻中采用了正確性驗證方法驗證安全協議漏洞，在引入攻擊者模型后，通過建立模型的關聯矩陣，用線性代數的方法判定方程是否存在解，如果有解則認為某序列可達[15-16]；利用CPN-Tools 中計算樹邏輯庫ASKCTL 提供的公式驗證模型某屬性是否正確[10]；利用CPN-Tools 計算模型狀態空間之后，以死變遷、死節點的數量變化來說明安全性[11,13,17-18]。但是，這些方法只能判斷協議模型是否存在安全漏洞，無法給出具體漏洞存在的位置或攻擊路徑。

2) CPN 對于建模人員的經驗要求較高，主要難點聚焦在模型狀態空間爆炸問題上[11-12,19-20]。大多數文獻沒有提出控制狀態空間規模的有效方法。甚至部分研究者認為，CPN 建模的復雜度增大一定會使狀態空間不可控甚至趨于爆炸[11,19]。如何將模型的狀態空間維持在一個恰當范圍是具有挑戰的問題。文獻[21]提出了一種使用抑制弧來減少狀態空間的方法，該方法雖然可以減少狀態空間的節點數，但避開了模型中的特殊節點，當模型足夠大時，仍然存在狀態空間爆炸的可能。

3) 針對攻擊路徑的提取，文獻給出了以下2 種方法。一種方法是在得到模型狀態空間后，利用安全屬性違背條件確定要找的死狀態節點（以下簡稱死節點），再通過狀態空間搜索到達死節點途經的全部節點[22]。然而，節點中包括除目標屬性外的所有庫所狀態，逐一篩選庫所狀態導致過程極其煩瑣，利用這種方法通常僅能找出模型個別攻擊路徑，難以實現完整的自動搜索。另一種方法是基于on-the-fly[20]的方法，當生成狀態空間時，同時計算狀態的攻擊路徑，并存儲在狀態節點中[11,19]。路徑計算與狀態空間計算同時發生。在得到整個狀態空間并找到攻擊后，可以立即從狀態中提取所有的攻擊路徑。

本文針對上述問題提出解決思路，主要貢獻如下：改進了利用CPN 進行協議安全性分析的一般方法，以找到協議漏洞并提取攻擊路徑為目標，采用更細粒度的建模及控制方法。攻擊路徑的提取中，將on-the-fly 方法應用為多參數形式，配合SML代碼，得到清晰的結果。提出基于 HCPN（hierarchical CPN）的并行令牌在層次間的等待-同步行進（Line-Up）建模思想，并行的多令牌同時進出不同分層，消除了大量無用的狀態序列，控制了狀態空間規模，提高了并行處理的效率。本文提出的CPN 模型復雜度的增加不一定會增大狀態空間規模，評估實驗證明甚至可以通過增加模型復雜度的方法來減小狀態空間規模。該研究為未來的CPN安全協議分析工作建立藍本。

評估實驗方面，本文針對TMN（Tatebayashi,Matsuzaki,Newman）協議進行了安全性分析。此前已有較多針對TMN 協議安全性分析的研究，該協議包含的大量漏洞已在部分文獻中提出[19-20,23]。本文主要以TMN 協議為例說明所提方法的有效性。

2 背景知識

2.1 協議安全形式化分析

形式化分析方法是指采用數學或邏輯方法描述系統模型，通過一定形式的推理驗證系統是否滿足要求的方法。將形式化分析的方法用于安全協議驗證最早是由Needham 和Schroeder 提出的，后由Dolev和Yao具體采用并于1983年發表了重要成果[23]。此后，大量的安全協議形式化分析工具被開發，出現了許多可用于協議形式化分析的方法，例如早期的BAN 邏輯、串空間、狀態機等，這些方法的形式化驗證聚焦在定理證明上，沒有針對形式語義的分析工具。近年來，較強大的分析工具如ProVerif、Scyther、Tamarin Prover 等逐漸流行起來，它們可以針對協議進行形式化安全驗證及語義分析。CPN與狀態機類似，但因其狀態空間分析能力強大且通俗易懂，使其同樣成為主流的協議建模分析工具，在諸多領域被廣泛使用。

2.2 CPN 協議安全性形式化分析

CPN 是在原始Petri 網的基礎上拓展而來的，屬于高級Petri 網范疇。與原始Petri 網相比，CPN的優勢是其標記可以通過著色來代表多重含義，庫所類型可以定義為顏色集，而非單一數據；令牌可以是顏色集類型元素的多集，大大提高了Petri 網的數據表達能力。

CPN 的優點是建模過程比較靈活，自由度較高；借助CPN-Tools 能夠動態仿真模型，可視化界面允許用戶觀察模型每一步的執行過程，進行細粒度分析；模型較為直觀，沒有CPN 知識的觀察者也可以通過演示快速理解模型所表達的含義。而其缺點是高自由度使建模過程較為復雜，與現有其他自動協議安全驗證工具相比，CPN 建模人員需要更多安全協議的建模分析經驗。

CPN 與目前流行的幾種自動協議安全性驗證工具對比如下。ProVerif 聲稱可以計算多條攻擊路徑，是基于邏輯編程的方法。但它計算的攻擊路徑是受限的，多數情況下只能包含一條攻擊路徑[20]。ProVerif 計算的受限攻擊路徑集遠小于基于CPN 的方法提取的攻擊路徑集。

Scyther 是一種高性能的協議模型驗證工具，能提供多條攻擊路徑的計算及分析功能。但它所使用的算法是千篇一律的，對于所有的安全協議，Scyther 試圖用同一方法給出狀態空間分析，這樣確實可以找到部分攻擊路徑，但無法做到全面或根據不同協議有的放矢。

Tamarin Prover 能夠窮盡搜索狀態空間，最新的版本中加入了對異或運算的模擬支持。但該工具要求建模者與觀察者都有較高的專業知識，相對CPN 來說不夠簡單直觀。同時，它也存在Scyther中用同一方法應對所有被測協議，使攻擊路徑被片面計算的弊端。

因此，上述或同類自動驗證工具不需建模者研究其內部運行機制，寫出規定格式的腳本即可完成驗證工作。而CPN 建模過程的高自由度成為其優勢之一，狀態空間完全由建模者自行把控，能夠針對不同協議實現專屬的建模及分析方法。這也是CPN 協議驗證往往比自動協議驗證工具更有效的原因。

2.3 TMN 協議

TMN 協議是一種用于數字移動通信系統的安全密鑰交換協議。TMN 協議規定發起者與響應者之間可借助可信服務器交換密鑰。該協議發布至今已被證明有諸多安全隱患[24]，常被用作驗證形式化工具和方法的有效性[19-20]。

TMN 協議的工作過程如下。

其中，A 為發起者，B 為響應者，J 為服務器，Kaj為A 向J 發起請求時生成的新鮮隨機數（也稱為A與J 的臨時密鑰），KJP為服務器J 的公開密鑰，Kab為B收到請求后生成的用于與A通信的新鮮隨機數（會話密鑰），M1～M4為TMN 協議運行的4 個步驟。

2.4 Dolev-Yao 攻擊者模型

Dolev-Yao 攻擊者模型[23]包含2 種假設，首先，假設密碼系統是“完美的”，安全協議的一次執行序列是嚴格按照協議規范定義的消息步驟交替序列。其次，攻擊者具有比協議真實參與者更強大的計算能力，能夠竊聽、截獲、篡改和重放協議運行過程中真實實體間交換的消息，也能加解密、拆分和組合原始消息，偽造消息內容。Dolev 和Yao 的方法被概括為黑盒安全分析。

然而，Dolev-Yao 攻擊者模型在引入形式化分析方法時，由于其定義的攻擊者模型能力強大，能夠根據其截獲的消息拆分組合出任意消息，導致增加了許多無用的重復操作，使狀態空間規模發生爆炸。為此，在建立協議評估模型時需要對消息的合成進行進一步假設和約束，具體如下。

1) 通過公共信道交換所有消息，攻擊者可以竊聽到網絡中的任何消息。

2) 攻擊者了解目標安全協議的全部細節，能夠按規則拆分消息內容。

3) 攻擊者可以存儲截獲的或自身產生的消息。

4) 攻擊者可以根據記錄的消息偽造并發送消息。偽造消息是按協議規則合成的。

5) 如果得到了匹配的密鑰，攻擊者可以將密文解密。

6) 攻擊者能夠作為合法實體之一，與其他實體進行正常通信。

3 基于攻擊者的TMN 協議安全評估模型

3.1 基于攻擊者的協議形式化描述

在CPN-Tools 中將協議消息定義為product 類型，消息集PACKET 定義為union 類型，各步驟消息從屬于PACKET 消息集。函數keyPair 用于模擬驗證服務器公私鑰的匹配情況。

根據2.4 節的攻擊者能力假設，協議評估模型建模時加入攻擊者實體，且攻擊者參與每一次數據傳輸過程，原協議的4 個步驟被攻擊者分割為8 個步驟（如圖1 所示）。模型規模龐大，將其進行分層（Hierarchical）處理。

圖1 基于攻擊者的TMN 協議頂層CPN 模型

圖1 中，Entity A 和Entity B 分別代表實體A和B，Server J 代表服務器J，Intruder 代表攻擊者（簡稱IN），S1～S8代表分割后各步驟中的網絡信道接口。在實體A 和B 角色不變的情況下，攻擊者既可以扮演協議發起者的角色，也可以扮演協議響應者的角色。

此外，攻擊者的加入使模型中出現了多個可能的發起者和響應者，各個實體及服務器需加入處理并發會話的能力。Clark-Jacob 庫中的安全協議已被證明最多涉及2 次并發會話攻擊[19]。在不影響協議驗證結果的基礎上，為減少狀態空間數量，約定模型中協議并發最多運行2 次，且實體A 和B 最多參與一次協議運行，攻擊者最多可參與2 次。為便于描述，下文將第一次協議運行稱為進程1，第二次運行稱為進程2。

并發順序方面，攻擊策略可歸納為2 種情況，具體表示為

情況1M1，M1′,M2′,M2,M3,M3′,M4′,M4

情況2M1,M2,M3,M4,M1′,M2′,M3′,M4′

其中，M1′～M4′為攻擊者參與步驟。情況1 中攻擊者一旦接收到A 發起會話的消息，立即存入知識庫并轉發，同時組裝攻擊數據發起一個新的消息，稱為中間人（MitM,man in the middle）攻擊。情況2中攻擊者將竊聽的一次完整協議運行全部存入知識庫，之后試圖偽裝身份發起攻擊會話，稱為順序攻擊（SqA,sequence attack）。

因此，基于攻擊者的協議消息步驟分層也必須能夠處理二次并發過程，進程間不能產生錯亂。

攻擊者引入后的替代變遷Intruder 的第二層CPN 模型如圖2 所示。該模型由替代變遷M1～M4分別模擬協議運行4 個步驟中的各階段攻擊行為。

圖2 替代變遷Intruder 的第二層CPN 模型

3.2 TMN 協議CPN 底層形式化描述

本節根據建模假設，給出加入攻擊者后的TMN協議模型。模型所有層次中使用了多個融合庫所，融合庫所由庫所和Fusion ID 組成，相同Fusion ID的融合庫所名稱不同但可視為同一庫所。多個融合庫所出現在不同分層中。

實體A 底層CPN 模型如圖3 所示。實體A 發送時，A_Encry_Pack 變遷作為模型運行起點，由自身存儲的數據集中收集協議第一步消息m1所需數據，加密后發送，包括自身ID、接收方ID、生成的臨時密鑰Kaj，以及服務器公鑰KJP。此時由于攻擊者也是可通信實體之一，因此A 每次發起會話時可選擇與 B 或是 IN 進行通信。接收時，A_Decry_Pack 變遷是模型運行的最后一步，將接收的數據包解密并驗證，類型及ID 正確的情況下將會話密鑰存儲至Session_Key 庫所，密鑰交換成功。

圖3 實體A 底層CPN 模型

實體B 底層CPN 模型如圖4 所示。實體B 從S4處接收J 發來的第二步消息m2。Recv 庫所接收后觸發B_Encry_Pack 變遷組裝第三步消息m3，并由S5發送給J。帶有INT×前綴的庫所是為應對并發時狀態激增問題，加入進程序號的庫所類型。

圖4 實體B 底層CPN 模型

服務器J 底層CPN 模型如圖5 所示。服務器由S2接收A 發來的消息m1，經Decry_Unpack1 變遷解密拆分驗證并存儲后生成m2消息，并由S3發送給B。此外，J 從S6接收m3消息，經Decry_Unpack2變遷解密、拆分、驗證并存儲后處理，再由J_Encry_Pack 組裝生成第四步消息m4交由S7發送給A。

圖5 服務器J 底層CPN 模型

3.3 TMN 協議安全評估模型

根據TMN 協議步驟M1～M4分別描述TMN 協議安全評估模型，這些模型分別稱為基于攻擊者的TMN 協議安全評估模型

圖6 基于攻擊者的TMN 協議安全評估模型

1) 如果Attk_Conf 的值為SqA，則m1被發送至S2，Seqs_Lock 庫所不獲得令牌。監聽到實體A獲得會話密鑰后，SqA_Att_Trigger 變遷點火，Chosen 庫所獲得令牌，隨機選擇IN_Pack1或者Remake 庫所點火，IN_Pack1變遷隨機取出知識庫中累積的原始數據，包括未解密的密文，按規則合成攻擊消息m1′（上角標′代表有攻擊者參與的消息）后發至Sender1。而Remake 變遷則不通過知識庫，以合法實體身份，用自己生成的密鑰按規則生成消息m1′后發至Sender1。由Transmit1′發送m1′至S2。

2) 如果Attk_Conf 的值為MitM，則m1進入Line-Up 庫所Queue1 等待，Seqs_Lock 庫所得到令牌，Unpack1變遷點火，Chosen 庫所獲得令牌，與情況1)過程相同，生成消息m1′后發送至Sender1。Transmit1′變遷將m1′送入Line-Up 庫所Queue2，此時State_Control點火條件滿足，將m1和m1′同時發送至S2。

本文提出的Line-Up 建模方式，在該模型分層中體現在模型的右下方 Transmit1′ 變遷和State_Control 變遷及其連接弧和中間庫所上。當模型中存在多個令牌（并行進程）時，該方法可以使多個令牌同時進出某一分層。如不使用該方法，先到達的令牌將可能提前進入下一模型分層，造成不同進程間由于后續變遷點火的隨機錯位，產生大量無用狀態空間。該方法的使用在不影響結果判斷的同時縮減了狀態空間規模，提高了并行計算的效率。

后續模型分層中如出現某令牌等待另一令牌同時行進的情況均為Line-Up 建模，不再重復說明。

圖7 基于攻擊者的TMN 協議安全評估模型

具體過程如下。S3接收到m2消息后，根據Attk_Conf′的值點火不同變遷，如為SqA 則點火Transmit2變遷，將數據直接送入融合庫所Buffer2，如為MitM 則點火State_Control2變遷，將同時收到的2 個令牌送入Buffer2。Buffer2變遷可以點火Resolve 變遷，該變遷將不同進程的消息送入不同庫所中，形成2 條分支。

1) 進程1 消息進入Sender2庫所，由于消息目標對象不同，如果消息發送給B，則點火Transmit2變遷，之后該消息進入Line-Up 變遷Queue2_（1MitM攻擊）或者直接轉發（SqA 攻擊），交由S4發送給B。如果消息的目標對象是攻擊者IN，則點火IN_Reply 變遷，生成m3消息后交由下一分層處理。

2) 進程2 消息進入Sender2′庫所，由于是攻擊數據所以Transmit2′變遷會直接轉發或生成新的m2′消息，之后消息進入Line-Up 變遷Queue2_2（MitM 攻擊）或者直接轉發（SqA 攻擊），交由S4發送給B。

圖8 基于攻擊者的TMN 協議安全評估模型

S5接收到的消息由Transmit3變遷點火，之后由IN_Unpack2解密并拆包存儲，如果未成功解密則由IN_Pack2從知識庫中提取數據按格式組裝消息并發送至庫所Sender3；否則Remake 和IN_Pack2庫所隨機點火，重新生成或按格式組裝消息后發送至庫所Sender3。此外，如果進程1 中信息目標實體為IN，則直接將其組合好的m3消息發入Sender3。隨后Transmit3′變遷點火將消息由S6接口處發出。

基于攻擊者的TMN 協議安全評估模型HM4如圖9 所示。主要作用是分別處理進程1 和進程2的消息，將進程1 消息發回給A，進程2 消息自己處理，嘗試提取所需的密鑰，判斷是否攻擊成功。

圖9 基于攻擊者的TMN 協議安全評估模型

具體模型運行過程如下。Transmit4變遷從S7接口處接收m4消息并存入Buffer4中，接著進程被按序號交由不同變遷處理。進程 1 數據交給State_Control4變遷處理后交由Transmit4′發回A。進程2 由Receive 變遷嘗試解密，如解密成功則將得到的密鑰存入IN_Obtain_Key 庫所，Decry_Cipher_Attmpt 繼續嘗試由該密鑰解密其他知識庫中的密文消息，如成功則存入觀察庫所AB_Session_Key 中。IN_Obtain_Key 庫所或AB_Session_Key 庫所中存在會話密鑰，則認為攻擊成功。

4 安全評估模型分析

4.1 模型狀態空間報告

表1 為CPN-Tools 生成的模型狀態空間報告節選。模型狀態空間節點數為4 252，因加入了大量的控制變遷和庫所，模型的復雜度大大提升。盡管如此，控制效果仍非常顯著，目前的狀態空間大小使分析工作具有了較高可行性。由此可見，CPN 模型狀態空間增加直接原因是模型運行時可能出現的狀態及路徑變多，而非模型復雜度增大。

表1 TMN 協議安全評估模型狀態空間報告

最終模型的運行過程狀態一共有4 252 個節點，5 319 條弧。全部節點和弧為強連接圖，模型不存在循環結構。沒有統一的最終狀態所以不存在家節點。333 個死節點意味著生成圖共存在333 個終止狀態。

4.2 TMN 協議安全測試分析規則

搜索攻擊路徑的前提是確定違背安全屬性的不安全狀態。密鑰交換協議應滿足的安全屬性包括保密性、完整性和認證性[25]。

1) 保密性。通信實體之間交換的會話密鑰應為保密的，不能被除合法實體之外的第三方獲知。

2) 完整性。通信實體之間交換的消息不能被攻擊者篡改、刪除或替代。換言之，完整性是指收到的數據和原始數據之間保持完全一致的特性。

3) 認證性。認證性是安全通信的重要保障，協議需要通過認證對通信主體進行識別，當一方聲稱自己就是某個主體的身份時，另一方需要驗證該身份。

TMN 作為典型的密鑰交換協議，理應滿足上述安全屬性。但其在設計時沒有充分考慮認證屬性，使攻擊者實施偽裝成為可能，并借此實現各種可能的攻擊。因此，按照協議規則，在形式化驗證該協議時主要聚焦于保密性和完整性兩方面。

協議的安全分析和評估，即證明是否存在違背上述安全屬性的狀態。根據2.4 節假設的攻擊者能力，攻擊者通過截獲、篡改、偽造等能力，將收到的每一步消息拆分并存入自己知識庫，之后按協議消息格式任意組合攻擊消息并將其發送至其余協議參與者。在這過程中，一旦攻擊者獲得了他人有效的會話密鑰，即違背了協議的保密性。而如果攻擊者使實體A或B實際交換的密鑰與各自認可的會話密鑰出現差異，則違背了協議的完整性。違背一條或多條安全屬性均視為不安全狀態達成。雖然因Dolev-Yao 攻擊者模型引發的大量重復無用數據已在協議建模時被消除，但模型中仍存在不能構成攻擊的非攻擊路徑，此類路徑的存在給攻擊路徑提取工作帶來干擾，為制定正確有效的攻擊路徑提取規則，需排除可能的非攻擊路徑。

基于3.1 節中對攻擊者模型的分析，TMN 協議安全性評估模型中攻擊過程全部為二次并發過程，且實體A、B 分別只參與一次會話。因此加入攻擊者后模型可能出現的數據流向如下。

1) 進程1 是A→B 的情況，進程2 中所有角色均是由攻擊者IN 偽造的，分為以下三類。

其中，括號中為攻擊者偽裝的角色，p1、p2分別代表進程1 和進程2。上述3 種運行方向對于攻擊者而言，有兩類目標數據，分別為進程1 中A 和B 達成的會話密鑰Kab、A 的臨時密鑰Kaj。獲得Kaj后攻擊者可解密其知識庫中的{Kab}Kaj從而間接獲得Kab。而獲得Kab意味破壞了協議的保密性。此外，由于進程1 中消息1 和消息3 格式相同，攻擊者可在進程1 時調換消息1 和3 中加密數據的位置，從而使A 認為正確的會話密鑰是Kaj，而B 認為是Kab，在這種情況下如果攻擊者獲得Kaj則同時破壞了協議的保密性與機密性。

2) 進程1 是A→IN 的情況，分為以下四類。

除②中IN 兩次運行均為合法參與者身份不予考慮以外，其余三類均由A 請求與不同身份的IN發起密鑰交換請求，由于攻擊者具有合法實體的能力，不論是IN 偽裝成A（即IN(A)→B）還是IN偽裝成B（即A→IN(B)）均可在協議單次運行中實現。為避免內容重復，④中IN 可同時偽裝成A 和B，尋找攻擊路徑時以④為準，不再單獨處理①和③的情況。進程1 中A 與偽裝成B 的IN 交換密鑰Kis，進程2 中IN 偽裝成A 與B 交換密鑰Kab。攻擊者一旦成功則破壞了協議的機密性與完整性。

3) 進程1 是IN→B 的情況，同樣分為以下四類。

上述類型與進程1 是A→IN 的情況相比只有順序改變而無實質性變化，攻擊路徑搜索以進程1 是A→IN 為準。

由此可制定評估模型的安全分析測試規則如下。

規則1A 和B 交換密鑰Kab成功，攻擊者獲得A、B 的會話密鑰Kab。

規則2A 和B 交換密鑰Kab成功，攻擊者獲得A 的臨時密鑰Kaj，由Kaj解密{Kab}Kaj得Kab。

規則3A 和B 認可的會話密鑰分別是Kaj和Kab，攻擊者獲得密鑰Kaj，由Kaj解密{Kab}Kaj得Kab。

規則4A 和B 認可的會話密鑰分別是Kis和Kab，攻擊者獲得密鑰Kis和Kab。

由圖2 可知，攻擊者介入后，每一次正常實體間的通信過程都有攻擊者參與。首次會話的運行步驟由最初的4 個步驟變為8 個步驟，具體為：1)A→IN，2) IN→J，3) J→IN，4) IN→B，5) B→IN，6) IN→J，7) J→IN，8) IN→A。如果出現A 的通信目標是IN 的情況，則運行步驟變為6 個：1) A→IN，2) IN→J，3) J→IN，4) IN→J，5) J→IN，6) IN→A。而第二次會話由于可能出現IN 偽裝A 和B 而不發送給真實實體A、B 的情況（4 個步驟），或者IN發給B 的情況（6 個步驟）。為使攻擊路徑提取更加全面，防止不必要的疏漏，規定完整的步驟記錄為12 個步驟。

在此基礎上，由于采用了on-the-fly 路徑記錄方法，狀態空間生成的同時所有路徑記錄已經存在于狀態節點中，按條件提取后即可獲得協議的攻擊路徑。

4.3 搜索攻擊路徑

本節以安全分析測試規則1 為例，即A 和B 交換密鑰Kab成功，攻擊者獲得A、B 的會話密鑰Kab。在模型中體現為實體A 中的觀察庫所A_Session_Key獲得令牌Kab，且M4的攻擊者觀察庫所IN_Obtain_Key 中獲得令牌Kab 的情況。

編寫代碼在狀態空間計算后執行，結果如圖10所示。

圖10 規則1 查詢代碼運行結果

圖10 的節點編號代表通過SML 查詢出的全部結果。這些節點均為到達測試規則1 的死節點。繼續提取模型中 FLY 庫所所記錄的內容，例如Mark.M4′FLY8 1 4169 為提取編號為4169 的節點中FLY 庫所的內容，其結果如圖11 所示。

圖11 節點4169 的FLY 庫所內容

模型中出現的庫所數量遠大于FLY 庫所記錄的屬性數量，因此某些不同的狀態節點可能記錄的數據完全相同，導致2 個或多個節點內容重復。編碼將重復節點刪除后，圖10 中9 個節點變為6 個，如圖12 所示。

圖12 標識有效攻擊路徑的節點

利用SML 將所有節點中FLY 庫所的內容提取并轉化為文本，格式化后保存至TXT 文件中，可以得到圖11 中6 個節點中記錄的具體攻擊路徑，將其中之一歸納后示例攻擊路徑如下。

攻擊者成功獲得實體A、B 之間交換的會話密鑰Kab，實現了對協議的攻擊。這就意味著一條有效攻擊路徑已被找到。同理，批量導出實驗中前述安全測試規則的全部可達路徑，合計找到有效攻擊路徑25 條，表2 為每種測試規則產生的攻擊路徑數量。

表2 各測試規則下攻擊路徑數量

4.4 協議安全評估結論

綜上所述，CPN 建模的方法有效提取出25 條TMN 協議的攻擊路徑，其中Line-Up 并行建模方法起到了重要作用。引入Line-Up 控制前后的狀態空間對比如表3 所示。

表3 Line-Up 引入前后狀態空間數量對比

由此可見，引入Line-Up 控制方法后狀態空間被大規模減小了，使狀態空間數縮減到比較易于分析和操作的狀態，模型中大量無用狀態被消除，TMN 協議的安全性被有效驗證，同時提高了CPN模型并行處理的效率。這種針對安全協議并行建模狀態空間削減的規模及方法在先前的同類研究中沒有出現過。

本文方法與現有方法狀態空間規模對比如表4所示。文獻[19-20]均未采用有效的狀態空間控制方法，其狀態空間數已到達爆炸的邊緣。而本文在最終333 個死節點中提取出有效攻擊路徑，經歸納整理及合并重復路徑后，這些攻擊路徑基本涵蓋了目前已發現TMN 協議的所有攻擊路徑。模型的攻擊路徑提取效率比文獻[19-20]高。

表4 本文方法與現有方法狀態空間規模對比

4.5 評估方法優勢分析

通過實驗可知，在建模方法與效果方面，本文方法與其他利用CPN 對安全協議建模分析的方法相比，在效率和可行性方面具有較大優勢。

首先，利用CPN 進行協議模型檢測時，狀態空間爆炸是獲取有效數據的阻礙。多數研究工作選擇將模型狀態空間劃分成若干小塊，再分別研究每一塊的狀態空間。但即使如此，每一塊狀態空間的規模仍維持在了一個可觀的數量級。在這種情況下，模型檢測的效率是不高的。本文所述Line-Up方法屬于偏序規約范疇，通過修改并行進程的執行順序，在不影響分析結果的前提下，將運行過程中由于變量先后綁定問題出現的大量無用狀態剔除，使狀態空間維持在了一個較小的數量級。

其次，部分研究利用CPN 驗證了安全協議是否存在可能的安全問題，但沒有找到具體的攻擊路徑，研究粒度不夠細致，甚至沒有達到形式化分析的一般標準。本文提出的研究方法是配合改進后的狀態空間控制進行的，在為數不多的狀態空間之中通過on-the-fly 方法和SML，將違背協議安全聲明的“不安全狀態”到達路徑全部提取，從而保證了發現協議安全問題的同時能夠提出“反例”（攻擊路徑）。本文方法與同類CPN 協議安全性分析方法的對比如表5 所示。

表5 所列對比方法為近年來具有代表性的CPN形式化協議分析研究，其中所述協議均存在一定安全缺陷，而這些研究大多沒有實現狀態空間有效控制或攻擊路徑提取。因此，本文所述CPN 形式化協議建模分析方法具有較大優勢，能夠將狀態空間控制在一個合理可行的范圍，同時分析協議可能存在的漏洞并找到攻擊路徑。

表5 本文方法與同類CPN 協議安全性分析方法對比

5 結束語

本文提出了一種改進的基于CPN 對協議安全性分析的方法，該方法能夠提取出有效攻擊路徑。在并發控制狀態空間方面提出了Line-Up 偏序規約建模思想，保證了實驗客觀性的同時避免了因并發令牌先后進入其他模型分層造成的狀態空間爆炸。這樣增加了模型的復雜度，但剔除了CPN 并行建模中大量無用狀態從而大規模縮減了模型狀態空間。

實驗證明本文方法是有效的，通過與現有同類研究對比可知，本文方法在狀態空間的縮減、攻擊路徑提取、驗證效率和可行性等方面具有較大優勢。未來可以嘗試用于其他安全協議的安全性形式化驗證。然而本文也存在一些不足之處，由于篇幅所限協議驗證結果沒有給出全部攻擊路徑的細節描述，協議中各種漏洞是由安全機制不完善引起的，應進一步分析這些漏洞產生的原因。此外，本文選用的TMN 協議較落后，已不是主流安全協議，本文只是借其說明方法的有效性。

未來的工作將繼續研究CPN 形式化分析過程中存在的問題及解決方案，針對不同協議探究如何在保證正確性的情況下收斂其狀態空間規模。由于各種協議所保障的安全屬性不同，下一步將嘗試利用本文方法研究更多的安全協議，總結該方法的適用范圍以及如何驗證更多的安全屬性，并繼續采用CPN 形式化建模的方法為方案改進提供良好的支撐。