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

龔翔，馮濤，杜謹澤

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

1 引言

安全協(xié)議已成為現(xiàn)代計算機網(wǎng)絡(luò)正常運轉(zhuǎn)的基礎(chǔ)，但由于其設(shè)計階段的規(guī)范缺失和不可避免的邏輯缺陷，常會帶來潛在的安全隱患，使各種協(xié)議的開發(fā)和安全性驗證成為一項艱巨的任務(wù)[1]。

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

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

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

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

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

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

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

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

2 背景知識

2.1 協(xié)議安全形式化分析

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

2.2 CPN 協(xié)議安全性形式化分析

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

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

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

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

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

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

2.3 TMN 協(xié)議

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

TMN 協(xié)議的工作過程如下。

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

2.4 Dolev-Yao 攻擊者模型

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

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

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

2) 攻擊者了解目標安全協(xié)議的全部細節(jié)，能夠按規(guī)則拆分消息內(nèi)容。

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

4) 攻擊者可以根據(jù)記錄的消息偽造并發(fā)送消息。偽造消息是按協(xié)議規(guī)則合成的。

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

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

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

3.1 基于攻擊者的協(xié)議形式化描述

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

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

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

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

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

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

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

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

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

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

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

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

3.2 TMN 協(xié)議CPN 底層形式化描述

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

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

圖3 實體A 底層CPN 模型

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

圖4 實體B 底層CPN 模型

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

圖5 服務(wù)器J 底層CPN 模型

3.3 TMN 協(xié)議安全評估模型

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4 安全評估模型分析

4.1 模型狀態(tài)空間報告

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

表1 TMN 協(xié)議安全評估模型狀態(tài)空間報告

最終模型的運行過程狀態(tài)一共有4 252 個節(jié)點，5 319 條弧。全部節(jié)點和弧為強連接圖，模型不存在循環(huán)結(jié)構(gòu)。沒有統(tǒng)一的最終狀態(tài)所以不存在家節(jié)點。333 個死節(jié)點意味著生成圖共存在333 個終止狀態(tài)。

4.2 TMN 協(xié)議安全測試分析規(guī)則

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.3 搜索攻擊路徑

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

編寫代碼在狀態(tài)空間計算后執(zhí)行，結(jié)果如圖10所示。

圖10 規(guī)則1 查詢代碼運行結(jié)果

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

圖11 節(jié)點4169 的FLY 庫所內(nèi)容

模型中出現(xiàn)的庫所數(shù)量遠大于FLY 庫所記錄的屬性數(shù)量，因此某些不同的狀態(tài)節(jié)點可能記錄的數(shù)據(jù)完全相同，導(dǎo)致2 個或多個節(jié)點內(nèi)容重復(fù)。編碼將重復(fù)節(jié)點刪除后，圖10 中9 個節(jié)點變?yōu)? 個，如圖12 所示。

圖12 標識有效攻擊路徑的節(jié)點

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

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

表2 各測試規(guī)則下攻擊路徑數(shù)量

4.4 協(xié)議安全評估結(jié)論

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

表3 Line-Up 引入前后狀態(tài)空間數(shù)量對比

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

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

表4 本文方法與現(xiàn)有方法狀態(tài)空間規(guī)模對比

4.5 評估方法優(yōu)勢分析

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

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

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

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

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

5 結(jié)束語

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

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

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