龔翔，馮濤，杜謹(jǐn)澤

（蘭州理工大學(xué)計(jì)算機(jī)與通信學(xué)院，甘肅 蘭州 730050）

1 引言

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

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

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

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

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

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

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

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

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

2 背景知識(shí)

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

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

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

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

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

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

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

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

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

2.3 TMN 協(xié)議

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

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

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

2.4 Dolev-Yao 攻擊者模型

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

圖3 實(shí)體A 底層CPN 模型

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

圖4 實(shí)體B 底層CPN 模型

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

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

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

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

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

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

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

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

后續(xù)模型分層中如出現(xiàn)某令牌等待另一令牌同時(shí)行進(jìn)的情況均為L(zhǎng)ine-Up 建模，不再重復(fù)說(shuō)明。

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

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

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

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

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

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

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

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

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

4 安全評(píng)估模型分析

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

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

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

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

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

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

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

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

3) 認(rèn)證性。認(rèn)證性是安全通信的重要保障，協(xié)議需要通過(guò)認(rèn)證對(duì)通信主體進(jìn)行識(shí)別，當(dāng)一方聲稱自己就是某個(gè)主體的身份時(shí)，另一方需要驗(yàn)證該身份。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.3 搜索攻擊路徑

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

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

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

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

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

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

圖12 標(biāo)識(shí)有效攻擊路徑的節(jié)點(diǎn)

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

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

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

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

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

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

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

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

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

4.5 評(píng)估方法優(yōu)勢(shì)分析

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

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

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

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

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

5 結(jié)束語(yǔ)

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

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

未來(lái)的工作將繼續(xù)研究CPN 形式化分析過(guò)程中存在的問(wèn)題及解決方案，針對(duì)不同協(xié)議探究如何在保證正確性的情況下收斂其狀態(tài)空間規(guī)模。由于各種協(xié)議所保障的安全屬性不同，下一步將嘗試?yán)帽疚姆椒ㄑ芯扛嗟陌踩珔f(xié)議，總結(jié)該方法的適用范圍以及如何驗(yàn)證更多的安全屬性，并繼續(xù)采用CPN 形式化建模的方法為方案改進(jìn)提供良好的支撐。