摘  要： 利用有色Petri網(wǎng)建模工具CPN tools中的查詢函數(shù)對(duì)安全屬性進(jìn)行描述,，搭建一個(gè)能夠覆蓋大部分安全性質(zhì)的CPN查詢函數(shù)庫(kù),，提出一種基于CPN的通用和規(guī)范的安全協(xié)議形式化分析語(yǔ)言,，該語(yǔ)言可以像用面向?qū)ο缶幊陶Z(yǔ)言編程一樣對(duì)安全協(xié)議進(jìn)行建模,。
關(guān)鍵詞： 有色Petri網(wǎng)；安全協(xié)議,；形式化分析,；面向?qū)ο缶幊陶Z(yǔ)言

　如何在一個(gè)無(wú)法確定的操作環(huán)境下，保證計(jì)算機(jī)間傳送信息的安全性,，從而確保通信雙方主體之間的“信任”以及通信數(shù)據(jù)的秘密和完整,，其中安全協(xié)議對(duì)保障網(wǎng)絡(luò)安全起到至關(guān)重要的作用。但一些著名的協(xié)議在使用了相當(dāng)長(zhǎng)的時(shí)間后,，相繼被發(fā)現(xiàn)存在有若干安全漏洞,。由于安全協(xié)議的運(yùn)行是處于某種不安全的環(huán)境中，很難用人工識(shí)別的方法來(lái)分析其安全性,，必須借助形式化的分析方法或工具來(lái)完成,。
　關(guān)于安全協(xié)議的形式化分析，國(guó)內(nèi)外學(xué)者基于不同的模型進(jìn)行了不少有益的研究,。如Yasinsac提出的通用安全協(xié)議分析語(yǔ)言CPAL[1],、Millen開(kāi)發(fā)的通用認(rèn)證協(xié)議說(shuō)明語(yǔ)言CAPSL[2]、李夢(mèng)君等人用擴(kuò)展Horn邏輯模型對(duì)安全協(xié)議進(jìn)行分析和驗(yàn)證方法[3],、懷進(jìn)鵬等人用代數(shù)模型來(lái)研究協(xié)議的安全性[4],、WE等人基于有色Petri網(wǎng)CPN(Coloured Petri Net)提出一種集成的安全協(xié)議分析模型[5]。
　現(xiàn)有的方法大多針對(duì)個(gè)別協(xié)議進(jìn)行分析,，很少能夠通用于大部分的安全協(xié)議,，并且大部分的方法還停留在理論上，缺少自動(dòng)分析的工具[6],。
　本文利用CPN tools建模語(yǔ)言(CPN ML)中的查詢函數(shù)對(duì)安全屬性進(jìn)行描述,，然后對(duì)CPN tools工具在規(guī)范協(xié)議描述、簡(jiǎn)化協(xié)議建模,、自動(dòng)檢測(cè)進(jìn)行擴(kuò)展三方面,，搭建一個(gè)能夠覆蓋大部分安全性質(zhì)的CPN查詢函數(shù)庫(kù)，提出一種基于CPN的通用和規(guī)范的安全協(xié)議形式化分析語(yǔ)言,，該語(yǔ)言可以像用面向?qū)ο缶幊陶Z(yǔ)言編程一樣對(duì)安全協(xié)議進(jìn)行建模。
1 基于CPN的安全協(xié)議
1.1 有色Petri網(wǎng)(CPN)理論研究
　Petri網(wǎng)是一種可用于多種系統(tǒng)的圖形化,、數(shù)學(xué)化建模工具,，為描述和研究具有并行、異步,、分布式和隨機(jī)性等特征的復(fù)雜系統(tǒng)提供了強(qiáng)有力的手段,。
　作為一種圖形化工具，可以把Petri網(wǎng)看作與數(shù)據(jù)流圖和網(wǎng)絡(luò)相似的方法來(lái)描述系統(tǒng)模型,；作為一種數(shù)學(xué)化工具,，它可以用來(lái)建立狀態(tài)方程,、代數(shù)方程和其他描述系統(tǒng)行為的數(shù)學(xué)模型。
在CPN模型中,，有色標(biāo)志表示系統(tǒng)中不同的資源,，同時(shí)每個(gè)位置都與特定的顏色集綁定，表示該位置中只能存放相應(yīng)顏色的標(biāo)志,。在弧上和變遷上標(biāo)注的條件表達(dá)式和運(yùn)算函數(shù)是用于解釋弧的權(quán)值,、運(yùn)算所用的顏色以及變遷觸發(fā)的條件。
　CPN tools是一個(gè)專用于有色Petri網(wǎng)編輯,、模擬和分析的工具,，除了有強(qiáng)大的CPN分析工具外，它還有簡(jiǎn)潔緊湊的CPN圖形編輯工具,，幾乎所有的CPN元素(除數(shù)據(jù)類型,、變量申明外)都能在模型圖中表示。
　CPN是將Petri網(wǎng)具有相似性質(zhì)的元素分類,，用不同顏色區(qū)分不同類別,，每一種顏色用一種標(biāo)識(shí)符號(hào)來(lái)表示，將某種屬性賦予標(biāo)記,。

1.2 基于CPN的安全協(xié)議
　安全協(xié)議的形式化分析與驗(yàn)證是一個(gè)復(fù)雜的過(guò)程,，首先都要用形式化方法的語(yǔ)義對(duì)安全協(xié)議進(jìn)行描述與建模。然而,，從協(xié)議的非形式化描述,，尤其是自然語(yǔ)言描述轉(zhuǎn)變成形式化說(shuō)明的過(guò)程可能會(huì)有錯(cuò)誤發(fā)生，將直接導(dǎo)致后續(xù)分析的不確定性,。同時(shí)一些形式化方法的提出都是從個(gè)別安全協(xié)議出發(fā)來(lái)設(shè)計(jì)規(guī)范的術(shù)語(yǔ),，遇見(jiàn)了新的協(xié)議形式，再對(duì)原有規(guī)范加以擴(kuò)展,，這樣的形式化術(shù)語(yǔ)存在通用性差的問(wèn)題,。所以在進(jìn)行安全協(xié)議的形式化描述與建模之前，需要采用通用的安全協(xié)議形式化說(shuō)明加以規(guī)范,。
　為了使得通用安全協(xié)議說(shuō)明更加適合于Petri網(wǎng)方法,，本文在CAPSL的基礎(chǔ)上抽象出通用安全協(xié)議的基本要素，在此基礎(chǔ)上建立與Petri網(wǎng)要素的一一對(duì)應(yīng),，如表1所示,。

2 對(duì)安全協(xié)議的描述和函數(shù)庫(kù)的創(chuàng)建
　CPN tools提供給每個(gè)變遷一個(gè)用CPN ML語(yǔ)言編程的程序編輯區(qū)。當(dāng)變遷發(fā)生時(shí),，執(zhí)行所編輯的程序,，完成所需的功能。程序編輯區(qū)有三條固定的語(yǔ)句：input(),、output(),、action(),，分別表示輸入?yún)?shù)、輸出參數(shù)和執(zhí)行語(yǔ)句,。
2.1 用CPN ML語(yǔ)言對(duì)安全屬性進(jìn)行描述
　安全協(xié)議的重要安全性質(zhì)包括：機(jī)密性,、認(rèn)證性、完整性,。描述如下：
機(jī)密性：針對(duì)受保護(hù)的特定內(nèi)容t的泄密狀態(tài)來(lái)進(jìn)行定義：
PredAllNodes(fn n=>cf(t,，Mark.Intruder′BUFF1 n)>0)
該函數(shù)表示搜索所有的狀態(tài)結(jié)點(diǎn)，如果有結(jié)點(diǎn)滿足斷言函數(shù)fn,，說(shuō)明機(jī)密信息t泄露,。
認(rèn)證性：實(shí)體經(jīng)過(guò)解密或者驗(yàn)證簽名來(lái)實(shí)現(xiàn)認(rèn)證，并在其緩沖區(qū)中保留認(rèn)證成功的證據(jù),，類型為AUT的顏色集colset AUT=with auth,； 同時(shí)保留被認(rèn)證者的身份的名稱。用查詢函數(shù)來(lái)定義：
PredAllNodes(fn n=>cf(auth,，Mark.A′BUFF1 n)>0 andalso
cf(auth,， Mark. B′BUFF 1 n) >0 andalso cf(t， Mark.In’BUFF 1 n)>0)
完整性：安全協(xié)議確保交互的消息不能被篡改,、刪除和替代,，或者至少消息的改變是可以被發(fā)現(xiàn)的。用形式化定義來(lái)表示：
　PredAllNodes(fn n=>cf(auth,，Mark.A′BUFF 1 n)>0
andalso cf(auth,，Mark.B’BUFF 1 n)>0 andalso
(cf(t， Mark.A′BUFF 1 n)>0 andalso cf(t′,，Mark.A′BUFF 1 n)<=0)
2.2 搭建安全協(xié)議的CPN查詢函數(shù)庫(kù)
　先建立好一個(gè)函數(shù)模型庫(kù),，對(duì)應(yīng)于常見(jiàn)的密碼學(xué)操作，并不斷地?cái)U(kuò)展,。上層實(shí)體通過(guò)函數(shù)調(diào)用的方式,，利用分層建模的設(shè)置子頁(yè)面工具將上層操作變遷與函數(shù)對(duì)應(yīng)起來(lái)。
通用安全協(xié)議的功能層其實(shí)就是安全協(xié)議函數(shù)庫(kù),，即在底層先建立好一個(gè)函數(shù)模型庫(kù),，對(duì)應(yīng)于常見(jiàn)的密碼學(xué)操作，并不斷地?cái)U(kuò)展,。上層實(shí)體只需要通過(guò)函數(shù)調(diào)用的方式,，利用分層建模的設(shè)置子頁(yè)面工具將上層操作變遷與函數(shù)對(duì)應(yīng)起來(lái)就可以了。
　在上面描述和對(duì)擴(kuò)展的基礎(chǔ)上,，建立一個(gè)安全性質(zhì)查詢函數(shù)庫(kù)。本文建立了一個(gè)能夠覆蓋絕大部分安全性質(zhì)的查詢函數(shù)庫(kù),，用戶只需要調(diào)用相應(yīng)函數(shù)即可完成協(xié)議的相關(guān)安全性質(zhì)的檢查而不需要自己利用CPN ML語(yǔ)言編寫(xiě)查詢函數(shù),。
2.3 一種基于CPN的通用安全協(xié)議形式化分析方法
　本項(xiàng)目利用前面基于CPN的安全協(xié)議描述,、對(duì)CPN tools的擴(kuò)展、CPN的安全協(xié)議操作函數(shù)庫(kù)的建立,，再結(jié)合實(shí)體模型中類似面向?qū)ο蟮念?、派生?duì)象概念，利用通用和規(guī)范的方法建模,，提出一種基于CPN的通用安全協(xié)議形式化分析語(yǔ)言,，該語(yǔ)言使用時(shí)就像用面向?qū)ο缶幊陶Z(yǔ)言進(jìn)行編程一樣方便有效。
基于CPN的安全協(xié)議形式化分析語(yǔ)言工作流程圖如圖1所示,。

　針對(duì)具體協(xié)議,，將安全屬性用CPN ML查詢函數(shù)進(jìn)行形式化描述：首先用斷言函數(shù)定義不安全狀態(tài)，即協(xié)議滿足安全屬性時(shí)不可能出現(xiàn)的狀態(tài),，如會(huì)話密鑰泄露時(shí)的狀態(tài),；再定義搜索函數(shù)對(duì)狀態(tài)空間的所有狀態(tài)進(jìn)行斷言函數(shù)的測(cè)試，尋找符合的結(jié)點(diǎn)標(biāo)識(shí),；最后運(yùn)行搜索查詢函數(shù),，分析實(shí)驗(yàn)結(jié)果。
3 應(yīng)用舉例
　本文以ASW(Asokan-Shoup-Waidner)協(xié)議為例,，利用本文提出的基于CPN模型對(duì)協(xié)議的安全性進(jìn)行分析,。
3.1 基于CPN模型對(duì)協(xié)議建模
　ASW協(xié)議由exchange、abort,、resolve_A和resolve_B 4個(gè)子協(xié)議構(gòu)成,。在正常情況下，只執(zhí)行exchange子協(xié)議,。僅當(dāng)A或B認(rèn)為協(xié)議執(zhí)行出現(xiàn)問(wèn)題時(shí),，才執(zhí)行其他子協(xié)議。
協(xié)議的exchange子協(xié)議具體描述如下：
　EOO=(me1,，Na),；EOR=(me1，me2,，Nb),；EOD=affidavit_token
　其中，Na,、Nb分別為A與B生成的臨時(shí)值,；m為A向B發(fā)送的電子郵件；C={m,，Na,，Ka，Kb}Kttp是加密電子郵件,。
　Exchange sub-protocol：
A→B：me1=Ka,，Kb,，TTP，C,，h(m),，{Ka，Kb,，TTP,，C，h(m)}Ka-1
      IF B gives up THEN quit ELSE
B→A：me2=h(Nb),，{me1,，h(Nb)}Kb-1
      IF A gives up THEN abort ELSE
A→B：me3=m，Na
      IF B gives up THEN resolve_B ELSE
B→A：me4=Nb
      IF A gives up THEN resolve_A ELSE
Abort sub-protocol：
A→TTP：ma1=aborted,，me1,，{aborted，me1}Ka-1
      IF B has resolved THEN resolve_A ELSE
TTP→A：abort_token=aborted,，ma1,，{aborted，ma1}Kttp-1
Resolve_B sub-protocol：
B→TTP：mrb1=Kb,，me1,，me2，Nb
      IF aborted THEN
TTP→B：mrb2=abort_token
      ELSE
TTP→B：mrb3=m,， a
Resolve A sub-protocol：
A→TTP：mra1=Ka,，me1，me2,，m,，Na
      IF aborted THEN
TTP→A：mra2=abort_token
      ELSE
TTP→A：affidavit_token=affidavit，mra1,，{affidavit,，mra1}Kttp-1
　在exchange子協(xié)議中，如圖2所示,，Alice生成me1并發(fā)送給B,。如果A在合理的時(shí)間范圍內(nèi)沒(méi)有收到me2，A將異常終止協(xié)議,；否則,，A將me3發(fā)送給B。如果等待me4的時(shí)間超時(shí)了,，A將異常終止協(xié)議并激活resolve_A子協(xié)議,；否則，exchange子協(xié)議成功運(yùn)行結(jié)束。函數(shù)gen_time(result)隨機(jī)生成了一個(gè)延遲時(shí)間,。條件if temptime<timeout,， then 1′1 else 1′0判斷超時(shí)是否發(fā)生。在這個(gè)模型中,，由于使用了隨機(jī)數(shù)作為延遲時(shí)間，超時(shí)的發(fā)生是隨機(jī)的,。如果me1的接收是超時(shí)的,Bob將退出協(xié)議,，否則Bob生成臨時(shí)值Nb，并將me2發(fā)送給A,。接著,，如果B沒(méi)有及時(shí)收到消息me3，B將激活resolve_B子協(xié)議,，否則,，B將消息me4發(fā)送給A。

3.2分析和驗(yàn)證
　本文分別針對(duì)在exchange子協(xié)議異常終止和正常結(jié)束的兩種情況下進(jìn)行模型檢測(cè),。因此在計(jì)算完全部狀態(tài)空間后,，修改了函數(shù)fun Verif_Fairness，分別執(zhí)行了以下兩個(gè)ML查詢函數(shù)：
fun Verif_Fairness_suc (con_id：INT,， succeed：SIGNAL)：
Node list
=PredAllNodes (fn n=>
cf(con_id,，Mark.Alice' veri_result2 1 n)<>
cf(con_id，Mark.Bob' veri_result2 1 n) andalso
cf(succeed,，Mark.Alice’end 1 n)==1) ),；
fun Verif_Fairness_fail (amsg：AMSG，,，emsg：EMSG,，
rmsg：RMSG)：Node list
=PredAllNodes (fn n=>
cf(amsg， Mark.TTP' abort_token 1 n)<>empty andalso
cf(emsg,， Mark.TTP' TTP2B 1 n)<>empty andalso
cf(rmsg,， Mark.TTP’ TTP2A 1 n)<>empty) )；
　函數(shù)fun Verif_Fairness_suc查詢的是在exchange子協(xié)議正常結(jié)束的情況下,，是否有不滿足公平性的狀態(tài),。結(jié)果為0，說(shuō)明當(dāng)exchange子協(xié)議成功結(jié)束后,，協(xié)議滿足可追究性和公平性,。相反，fun Verif_Fairness_fail的查詢結(jié)果列出了一些不安全狀態(tài),，說(shuō)明當(dāng)協(xié)議異常終止后,，不滿足安全性。
　本文將面向?qū)ο蠓椒捌涓拍?如類、對(duì)象,、函數(shù)等)引入建模中,，并直接嵌入通用安全協(xié)議描述中，以此為基礎(chǔ)的協(xié)議建模就具有了抽象,、重用,、繼承等性質(zhì)，簡(jiǎn)化了建模過(guò)程,，使得圖型化的CPN建模能夠像面向?qū)ο缶幊陶Z(yǔ)言一樣方便和有效,。利用CPN tools提供的復(fù)制和分層次工具實(shí)現(xiàn)函數(shù)調(diào)用以及派生實(shí)體的快速建模，將面向?qū)ο笏枷胫械呐缮鷮?shí)體與函數(shù)調(diào)用思想應(yīng)用于建模過(guò)程中,。本文提出通用的安全協(xié)議分析語(yǔ)言,，具有通用性、易用性,、圖形化等特點(diǎn),。
參考文獻(xiàn)
[1] 李夢(mèng)君，李舟軍,，陳火旺.安全協(xié)議的擴(kuò)展Horn邏輯模型及其驗(yàn)證方法[J].計(jì)算機(jī)學(xué)報(bào),，2006，29(9)：1666-1678.
[2] 懷進(jìn)鵬,，李先賢.密碼協(xié)議的代數(shù)模型及其安全性[J].中國(guó)科學(xué)(E輯),，2003，33(12).
[3] 馮登國(guó),，范紅．安全協(xié)議理論與方法[M].北京：科學(xué)出版社,，2003.
[4] YASINSEC A. A formal semantics for evaluating cryptographic protocols[D]. University of Virginia， 1996.
[5] MILLEN J. CAPSL： common authentication protocol specification language [R]. Technical Report MP97B48,， The MITRE Corporation,， 1997.
[6] Wei Jin， Su Guiping. An integrated model to analyze cryptographic protocols with colored Petri Nets. In Proceeing[C]. 11th IEEE Symposium on  High Assurance Systems Engineering Symposium,，2008.