司亞利，劉文遠，盧 貝

（1.燕山大學(xué) 里仁學(xué)院，河北 秦皇島066004；2.燕山大學(xué) 信息科學(xué)與工程學(xué)院，河北 秦皇島066004）

0 引 言

安全協(xié)議是實現(xiàn)網(wǎng)絡(luò)安全的關(guān)鍵技術(shù)之一，許多安全協(xié)議在設(shè)計或?qū)崿F(xiàn)后，由于漏洞的存在而受到攻擊［1］，所以協(xié)議的安全性認證至關(guān)重要。在采用形式化方法分析安全協(xié)議方面，Petri網(wǎng)技術(shù)是一個重要研究內(nèi)容。文獻［2－7］針對不同的安全協(xié)議，從不同角度提出了基于顏色Petri網(wǎng)（CPN）的形式化建模與分析方法。進而，針對一種常見并且危害性最大的重放攻擊形式，相關(guān)形式化分析成果也陸續(xù)提出。Aurn等設(shè)計并提出一種分析協(xié)議優(yōu)勢和缺陷的重放攻擊分析方法［8］；張衛(wèi)華等提出更加簡便高效的CPN 規(guī)劃識別及多步驟攻擊檢測方法［9］；Fan Kai等利用并發(fā)簽名和可信第三方來阻止惡意支付，以保證電子商務(wù)交易協(xié)議的安全性和公平性［10］，但是缺少形式化分析方法的認證。

電子商務(wù)協(xié)議屬于一種特殊的安全協(xié)議，除了繼承安全協(xié)議的性質(zhì)，還有自身特殊的性質(zhì)，如公平性、可追究性、原子性和時限性等。目前在電子商務(wù)協(xié)議的形式化分析中，多數(shù)側(cè)重于研究協(xié)議的特殊性質(zhì)，而極少關(guān)注電子商務(wù)協(xié)議的安全屬性，缺少關(guān)于攻擊的形式化分析方法。因此，針對電子商務(wù)協(xié)議中的重復(fù)攻擊問題，提出一種基于顏色Petri網(wǎng)的攻擊形式化建模方法，并利用逆向狀態(tài)分析和CPN Tools兩種方法分析CMP1協(xié)議中不安全狀態(tài)的可達性，從而得到攻擊結(jié)果。

1 CPN 的電子商務(wù)協(xié)議攻擊分析方法

目前，關(guān)于電子商務(wù)協(xié)議的攻擊分析研究較少，并缺乏形式化工具的應(yīng)用分析。本節(jié)提出一種針對電子商務(wù)協(xié)議攻擊的顏色Petri網(wǎng)建模方法，然后采用理論和實驗兩種方法分析所定義的不安全狀態(tài)是否可達，如果可達表明存在被攻擊的漏洞，反之則說明協(xié)議是安全的。在對電子商務(wù)協(xié)議的攻擊建模和分析過程中，遵循的操作步驟是：首先建立電子商務(wù)協(xié)議正常執(zhí)行的模型；其次加入攻擊者模型；再次定義協(xié)議的不安全狀態(tài)；最后是協(xié)議的攻擊結(jié)果分析。具體闡述如下。

1.1 建立協(xié)議正常執(zhí)行的模型

一個顏色Petri網(wǎng)可以表示成一個七元組：CPN＝｛P，T，F(xiàn)，C，I＋，I－，M0｝。其中P 表示庫所的有限集合，T是變遷的有限集合，P ∪T ≠，P ∩T ≠。F ∈（P×T）∪（T×P）是有向弧集合，它建立庫所顏色和變遷的每種顏色之間的對應(yīng)關(guān)系。C 是定義在P ∪T 上的顏色集，I＋和I－分別稱為P×T 的輸入函數(shù)和輸出函數(shù)，M0是初始標(biāo)識。利用CPN ML（machine language）語法聲明模型中的顏色集、變量、常量和函數(shù)，建立分層顏色Petri網(wǎng)模型，把每個實體定義成一個替代變遷。

（1）協(xié)議消息與CPN 元素的對應(yīng)關(guān)系。建模的基礎(chǔ)準(zhǔn)備是對電子商務(wù)協(xié)議進行形式化語義描述，而已有的規(guī)范語義大多針對特定的協(xié)議進行設(shè)計，通用性不強，如果分析其它協(xié)議就需要對原有語義加以擴展。本文為了把通用的協(xié)議消息說明和CPN 方法相結(jié)合，抽象出通用協(xié)議的基本要素，并在此基礎(chǔ)上建立與顏色Petri網(wǎng)元素的對應(yīng)關(guān)系：

原子消息，即私鑰、公鑰、會話密鑰、明文等不可拆分的消息，對應(yīng)簡單顏色集（unit類型）。如：colset SK＝with ska｜skb｜skc；顏色集SK 聲明了3個會話密鑰集。

復(fù)合消息，是原子消息經(jīng)過若干運算操作（加密、哈希運算、拼接、簽名等）后形成的消息，對應(yīng)復(fù)合顏色集（product類型）。例如用公鑰加密的消息｛m｝pk 可聲明為colset MES ＝product M＊PK 。

各主體之間傳遞的復(fù)雜消息，對應(yīng)CPN 中的聯(lián)合顏色集（union類型）。

電子商務(wù)協(xié)議的整個執(zhí)行過程，對應(yīng)顏色Petri網(wǎng)仿真（CPN Simulation）。

（2）根據(jù)上一步驟的對應(yīng)關(guān)系，建立協(xié)議在正常執(zhí)行狀態(tài)下的CPN 模型。

首先，對各主體的公鑰、私鑰和會話密鑰等建立對應(yīng)的公鑰顏色集、私鑰顏色集、會話密鑰集及各自的顏色變量。

其次，把協(xié)議中的每條消息抽象成原子消息或復(fù)合消息，定義相應(yīng)的簡單顏色集、復(fù)合顏色集、顏色變量，同時建立協(xié)議的不可否認證據(jù)。

再次，建立主體之間傳輸?shù)膹?fù)雜消息顏色集。根據(jù)協(xié)議的執(zhí)行語句，如果是多個復(fù)合消息的拼接，則建立一個union類型的顏色集來表示整個協(xié)議主體間交換消息的集合。

最后，建立顏色Petri網(wǎng)。對于比較復(fù)雜的電子商務(wù)協(xié)議，采用層次清晰的分層結(jié)構(gòu)。在頂層建立協(xié)議的完整執(zhí)行流程模型，把每一個實體定義成一個替代變遷。為了體現(xiàn)主體功能的獨立集中性，主體處理的消息在底層模型實現(xiàn)。同時，按照協(xié)議的需求為變遷和輸出弧進行程序判定，來達到最完善的協(xié)議建模。

1.2 加入攻擊者的模型

分析攻擊者的攻擊流程，并把攻擊者模型加入到第1.1節(jié)建立的模型中。具體方法是先分析并寫出協(xié)議可能遭受的攻擊及其流程，畫出帶有攻擊者的協(xié)議流程圖。然后，采用第1.1節(jié)的建模方法建立攻擊者模型，最后將攻擊者模型加入到正常執(zhí)行的模型中，即在分層CPN 模型的頂層加入攻擊者替代變遷，形成完整的帶有攻擊者的CPN 模型。

1.3 定義協(xié)議的不安全狀態(tài)

安全協(xié)議認證的攻擊者目標(biāo)比較簡單，一般是通過攻擊協(xié)議以獲取會話密鑰，并冒充他人身份進行會話以實現(xiàn)欺詐等非法活動。然而，電子商務(wù)協(xié)議比安全協(xié)議復(fù)雜，不同協(xié)議主體的交換消息又大不相同，難以定義攻擊目標(biāo)。因此，如何定義電子商務(wù)協(xié)議的不安全狀態(tài)成為關(guān)鍵問題。

經(jīng)過深入研究發(fā)現(xiàn)，為了分析電子商務(wù)協(xié)議的可追究性和公平性，在協(xié)議的具體步驟設(shè)計時都已經(jīng)定義了發(fā)方不可否認證據(jù)EOO（evidence of origin）和收方不可否認證據(jù)EOR（evidence of recipt），這是參與方相互交換消息的重要組成部分，同時也是保證自身利益的不可否認證據(jù)。利用這個特性，本文提出在分析重放攻擊時，把電子商務(wù)協(xié)議的攻擊目標(biāo)定義成EOO 和EOR 中最為敏感的重要信息，如電子現(xiàn)金、用戶信息、交易貨物等。這種方法既準(zhǔn)確，又能保證不同協(xié)議的不安全狀態(tài)定義有據(jù)可依。以CMP1協(xié)議為例，EOO 是｛m｝SKa，EOR 是｛h（m）｝SKb，用本方法提取出的攻擊目標(biāo)是發(fā)送方發(fā)出的原始消息m。

1.4 分析協(xié)議的攻擊結(jié)果

Petri網(wǎng)中分析網(wǎng)模型的方法有很多，其中狀態(tài)方程分析協(xié)議模型準(zhǔn)確，CPN Tools對模型進行分析和仿真方便快捷。因此，本文在提出新的建模方法后，先利用Petri網(wǎng)的逆向分析方法進行理論分析，然后利用顏色Petri網(wǎng)的CPN Tools仿真工具對模型進行仿真分析，從而得出結(jié)論。

（1）理論分析。逆向狀態(tài)分析方法，也就是求解網(wǎng)的狀態(tài)方程，體現(xiàn)了倒推的思想。設(shè)CPN＝｛P，T，F(xiàn)，M0｝是一個有界Petri網(wǎng)，P ＝｛p1，p2，…，pm｝，T ＝｛t1，t2，…，tn｝，則CPN 的結(jié)構(gòu)可以用一個n 行m 列的關(guān)聯(lián)矩陣（incidence matrix）C ＝ cijn×m來表示［11］，其中aij＝－，i（｛1，2， …，n｝，j（｛1，2， …，m｝，＝

CPN 的標(biāo)識（即不安全狀態(tài)）能夠用一個非負整數(shù)向量M＝［M（p1），M（p2），…，M（pm）］T來表示，得到狀態(tài)方程M＝M0＋CTX。最后，分析協(xié)議的安全性通過解狀態(tài)方程實現(xiàn)，如果無解說明該狀態(tài)是安全的；反之有解則說明不安全，并給出變遷發(fā)生序列（也就是攻擊劇情）。

（2）實驗分析。建立協(xié)議的CPN 模型后，利用CPN Tools工具進行仿真分析，檢驗所提方法的正確性和有效性。CPN Tools具有交互性好和時效性強等優(yōu)點，并且有自動化分析過程。運行CPN Tools中的狀態(tài)空間，利用ML查詢函數(shù)判斷定義的不安全狀態(tài)是否可達。如果可達，則該協(xié)議存在漏洞，肯定是不安全的。如果不可達，則說明該協(xié)議是安全的。

2 實例分析

以經(jīng)典的CMP1（certified electronic mail）電子商務(wù)協(xié)議為例，利用提出的方法對其進行建模分析。

2.1 協(xié)議的描述

CMP1協(xié)議正常執(zhí)行的具體描述如下：

EOO：｛m｝SKaEOR：｛h（m）｝SKb；

（1）A →B：h（m），｛K｝Kttp，｛｛m｝SKa｝K；

（2）B →T：｛h（m）｝SKb，｛K｝Kttp，｛｛m｝SKa｝K；

（3）T →B：｛｛m｝SKa｝SKt；

（4）T →A：｛｛h（m）｝SKb，（B，m）｝SKt。

第（1）步表示參與方A 選擇一個會話密鑰K，把消息m的摘要h（m）、用K 對簽名｛m｝SKa加密所生成的密文｛｛m｝SKa｝K、加密后的會話密鑰｛K｝Kttp發(fā)送給B。第（2）步，B簽名摘要h（m）生成｛h（m）｝SKb，和A 發(fā)送消息的后兩部分轉(zhuǎn)發(fā)給可信第三方T。T 解密后獲?。鹠｝SKa來檢驗A 的簽名，通過｛h（m）｝SKb驗證B的簽名；對｛｛m｝SKa｝K獲得的消息m 計算摘要h（m），和從｛h（m）｝SKb獲得的h（m）進行比較，如果相同，則協(xié)議順利執(zhí)行第（3）步，把｛m｝SKa用T 的私鑰簽名后發(fā)給B；若不一致則終止協(xié)議。第（4）步，T 用私鑰對B 簽名后的摘要和（B，m）進行簽名，并發(fā)送給A。

2.2 帶有攻擊者的CMP1協(xié)議流程

第1步：A →B：h（m），｛K｝Kttp，｛｛m｝SKa｝K；

第2步：B →T：｛h（m）｝SKb，｛K｝Kttp，｛｛m｝SKa｝K；

攻擊者：I（B）→T：｛h（m）｝SKb，｛K｝Kttp，｛｛m｝SKa｝K；

第3步：T →B：｛｛m｝SKa｝SKt；

攻擊者：T →I（B）：｛｛m｝SKa｝SKt；

第4步：T →A：｛｛h（m）｝SKb，（B，m）｝SKt；

攻擊者：T →I（A）：｛｛h（m）｝SKb，（B，m）｝SKt。

上面給出的是帶有攻擊者的協(xié)議流程。攻擊者I在第1步截獲A 發(fā)送給B的消息，并在第2步冒充B給T 轉(zhuǎn)發(fā)消息，T 正常執(zhí)行比較消息摘要和驗證簽名的操作，如果通過驗證，繼續(xù)執(zhí)行第3、4步，給A 和B 發(fā)送T 簽過名的消息。攻擊者在此過程中可冒充A 或B的身份接收從T 反饋的消息。

2.3 帶有攻擊者的CPN 模型

colset ID＝with A｜B｜T｜I；

colset M＝with ml；

colset PK＝with pka｜pkb｜pkt；

colset SK＝with ska｜skb｜skt；

colset EOO＝product M＊SK；

colset EOR＝product H＊SK；

colset EOO＿K＝product EOO＊KEY；

colset EOO＿S＝product EOO＊SK；

colset MSG ＝union s：H ＋k ＿e：K ＿E ＋keoo：EOO＿K＋eor：EOR＋seoo：EOO＿S＋bm：BM＋skey：SK；

首先給出的是帶有攻擊者的CPN 模型中部分顏色集聲明。ID 定義了主體A 和B、可信第三方和攻擊者這4個參與協(xié)議的主體身份；M 是主體發(fā)出的原始消息，PK 和SK分別是主體的公鑰和私鑰。EOO 和EOR 是product類型的顏色集，定義協(xié)議中的發(fā)方和收方不可否認證據(jù)。顏色集MSG 是union類型，表示每個主體間發(fā)送的消息，它組合了幾個獨立而又相關(guān)的顏色集。然后，定義各個顏色集的顏色變量，定義功能函數(shù)VeriSig（sk：SK，pk：PK），用于檢驗主體的簽名信息。

根據(jù)2.1節(jié)和2.2節(jié)的協(xié)議流程，采用自頂而下的分層建模方法，首先建立協(xié)議的Top層模型，然后分別建立各主體的模型。

圖1是帶有攻擊者的CMP1協(xié)議顏色Petri網(wǎng)的頂層模型。模型中，A、B、T 和I是替代變遷，分別對應(yīng)相應(yīng)的變遷子頁，用于實現(xiàn)各主體的具體內(nèi)部消息轉(zhuǎn)換。T2A、A2B、Ib2T、Ia2B等庫所表示主體之間發(fā)送消息，T2A 表示T 發(fā)送信息給A，Ib2T 表示攻擊者I冒充主體B發(fā)送了一條消息給T。

圖1 TOP層模型

圖2是主體A 的模型。具體的執(zhí)行流程是：A 簽名消息m，提取出發(fā)方不可否認證據(jù)eoo，再用密鑰K 加密eoo生成keo，作為第一部分消息。用Hash函數(shù)對消息m 進行運算，生成消息摘要h（m），作為第二部分消息。用可信第三方T 的公鑰對密鑰K 加密，作為第三部分的消息。然后，組合三部分消息發(fā)送給接收方B。在協(xié)議的第4 步A收到T 發(fā)送的消息后，對其解密，從而得到收方不可否認證據(jù)eor。

圖2 主體A 的模型

圖3為攻擊者I的模型。攻擊者有很多攻擊手段，模型中，I截獲A 給B發(fā)送的消息，然后冒充A 直接給B 轉(zhuǎn)發(fā)消息；類似的，I截獲B 給T 發(fā)送的消息，并冒充B 給T轉(zhuǎn)發(fā)消息。針對協(xié)議第3步和第4步，I截獲從T 發(fā)送出來的消息，利用T 的公鑰解密消息，最終I獲得從A 發(fā)送出的原始消息m，以達到攻擊目標(biāo)。

圖3 攻擊者的模型

接下來建立帶有攻擊者的CMP1協(xié)議的主體B 模型。攻擊者冒充主體A 給B發(fā)送消息m，B收到消息后對h（m）進行簽名，并與另外兩部分消息組合起來轉(zhuǎn)發(fā)給T。B 在收到T 反饋的消息后，解密獲得發(fā)方不可否認證據(jù)。

圖4是可信第三方T 的模型。T 分解B 發(fā)送的消息，得到eoo以驗證A 的簽名，對eor驗證B的簽名。T 對eoo解密得到的消息m 計算摘要h（m），對比eor中的摘要，如果二者相同，則可信第三方公布消息，為各主體獲取使用。在這里，攻擊者具有冒充A 或B提取消息的可能。

圖4 可信第三方T 的模型

2.4 帶有攻擊者的CPN 模型分析

方法一：理論分析。根據(jù)建立好的CPN 模型，利用逆向狀態(tài)分析方法對模型進行分析，具體過程按照第1.4節(jié)的理論分析部分進行。

建立CMP1協(xié)議的關(guān)聯(lián)矩陣，包括協(xié)議關(guān)聯(lián)矩陣的A模型子矩陣C1（見表1）、I模型的子矩陣C2（見表2）、B模型的子矩陣C3和T 模型的子矩陣C4（略）。

協(xié)議的初始狀態(tài)是MT0＝［0，0，0，0，0，0，SK，M，HASH，KEY，PK，0，0，0，…，0］。此時只有A、B和I擁有知識集，例如主體的公私鑰等。

表1 關(guān)聯(lián)矩陣的子矩陣C1

表2 關(guān)聯(lián)矩陣的子矩陣C2

不安全狀態(tài)是MT＝［0，0，0，0，0，0，SK，M，HASH，KEY，PK，0，…，M，0，…，EOO，EOR］，即攻擊者成功截獲了A 給B發(fā)送的消息m。A 和B均取得對方的不可否認證據(jù)，但是沒有發(fā)現(xiàn)他人竊取了消息。

得到并求解狀態(tài)方程M＝M0＋CTX。利用線性函數(shù)的有解判定式可知方程有解，并且找到了一個可執(zhí)行的變遷序列：σ＝sa，hs，keo，ek，g1，stb，get，sb，g2，stt，get，dek，deo，dem，com，reh，g3，deh，geoo，dem。

因此得出，攻擊者能夠竊取關(guān)鍵信息m，CMP1 協(xié)議存在不安全狀態(tài)。

方法二：利用工具分析。先將已經(jīng)建立好的CMP1協(xié)議的顏色Petri網(wǎng)模型根據(jù)第1節(jié)提出的方法錄入到CPN Tools中，接下來運行狀態(tài)空間分析和ML查詢函數(shù)。

在仿真工具CPN Tools中單擊EnterStateSpace tool，對模型所有可能的連通狀態(tài)、狀態(tài)空間和強連通分量狀態(tài)圖進行計算并保存。得到的狀態(tài)空間報告如下所示，報告顯示出整個模型共生成220 個結(jié)點和751 條弧，共產(chǎn)生3個死結(jié)點，即218，219，220。

接下來分析協(xié)議的可追究性，查詢結(jié)果如圖5 所示，攻擊者I成功地獲得了A 給B 發(fā)送的消息。因此，CMP1協(xié)議存在重放攻擊的危險。

圖5 查詢結(jié)果

至此，采用兩種方法分析得出的結(jié)論是一致的，能夠說明本文提出方法是正確、有效的。

3 結(jié)束語

本文提出了一種基于顏色Petri網(wǎng)的電子商務(wù)協(xié)議攻擊分析的建模方法，從協(xié)議的不可否認證據(jù)中提取不安全信息，定義成不安全狀態(tài)，并給出了具體的建模和分析過程。繼而以CMP1 協(xié)議為例，用所提方法建立協(xié)議的CPN 模型，經(jīng)過理論分析和實驗仿真后得出CMP1協(xié)議存在漏洞的結(jié)論，同時說明了所提出方法的有效性。本方法具有很好的通用性，能夠?qū)ζ渌娮由虅?wù)協(xié)議進行攻擊建模和分析。

［1］Fan Yutao，Su Guiping，He Liu，et al.Study on a CPN－based auto－analysis tool for security protocols ［C］／／Proceedings of the 4th International Symposium on Information Science and Engineering，2012：179－182.

［2］Yang Xu，Xie Xiaoyao.Modeling and analysis of security protocols using colored Petri nets ［J］.Journal of Computers，2011，6 （1）：19－27.

［3］Zhao Jianjie，Gu Dawu，Zhang Lei.Security analysis and enhancement for three－party password－based authenticated key exchange protocol［J］.Security and Communication Networks，2012，5 （3）：273－278.

［4］Kenneth G Paterson，Gaven J Watson.Authenticated－encryption with padding：A formal security treatment［G］.Lecture Notes in Computer Science 6805：Cryptography and Security：From Theory to Applications2012：83－107.

［5］SU Guiping，SUN Sha.Formal analysis of non－repudiation protocol based on colored Petri net model［J］.China Information Security，2011，9 （8）：54－55 （in Chinese）. ［蘇桂平，孫沙.基于CPN 模型的不可否認協(xié)議分析 ［J］.信息安全與通信保密，2011，9 （8）：54－55.］

［6］Alessandro Armando，Giancarlo Pellegrino，Roberto Carbone，et al.From model－checking to automated testing of security protocols：Bridging the gap ［G］.Lecture Notes in Computer Science 7305：Tests and Proofs，2012：3－18.

［7］Huang Hejiao，Zhou Qiang.Petri－net－based modeling and resolving of black hole attack in WMN ［C］／／Proceedings of the International Computer Software and Applications Conference，2012：409－414.

［8］Aurn Kumar Singh，Arun K Misra.Analysis of cryptographically replay attacks and its mitigation mechanism ［J］.Advances in Intelligent and Soft Computing，2012，132：787－794.

［9］ZHANG Weihua，F(xiàn)AN Zhihua.Method of plan recognition and multi－step attack detecting based on CPN ［J］.Computer Engineering and Design，2007，28 （11）：2516－2520 （in Chinese）.［張衛(wèi)華，范植華.基于CPN 的規(guī)劃識別及多步驟攻擊檢測方法 ［J］.計算機工程與設(shè)計，2007，28 （11）：2516－2520.］

［10］Fan Kai，Wang Yue，Li Hui.Fairness electronic payment protocol［J］.International Journal of Grid and Utility Computing，2012，3 （1）：53－58.

［11］Yu Yuedua，Yu Huininga，Liang Qia.Reachability analysis of logic Petri nets using incidence matrix ［J］.Enterprise Information Systems，2013：1－18.