公平交換協議的信道可信度形式化驗證方法

楊晉吉,申涵瑞,陳清亮

1(華南師范大學 計算機學院,廣州 510631) 2(暨南大學 計算機科學系,廣州 510632)

1 引 言

隨著電子商務技術的發展,越來越多的電子商務應用進入人們日常生活,電子商務的安全性問題也變得更加重要.公平交換協議作為一種重要的電子商務安全協議,在保障電子商務應用的安全性方面扮演了非常重要的角色.公平性、有效性和時限性是電子商務安全的核心屬性,設計出公平安全的公平交換協議是電子商務發展的迫切要求,針對公平交換協議進行分析驗證具有十分重要的意義.但由于公平交換協議的復雜性,公平交換協議的形式化驗證領域仍存在許多問題,例如簡易有效的針對安全屬性的分析方法和符合現代工業要求的公平交換協議等.

信道問題是公平交換協議分析中一個重要問題.在開放的網絡環境下,消息在信道傳輸的過程中會由于信道錯誤或惡意實體的主動攻擊,導致消息的丟失、錯誤或延遲[1].因此基于信道可信度對公平交換協議的核心屬性進行定量分析在實際工程中具有重要的作用.

目前國內外已有很多關于公平交換協議的研究.文獻[2]對Ray協議進行安全性分析,驗證該協議為一個使用在線可信第三方的公平交換協議.文獻[3]基于交替時態邏輯對公平交換協議的安全屬性進行了定性分析.文獻[4]證明了Ben-Or等協議存在針對協議參與者的攻擊策略,并分析了攻擊者的成功概率和需要的信息時延.

形式化驗證是對公平交換協議進行分析的重要方法.文獻[5]基于線性時態邏輯,使用模型檢測工具SPIN對普通文件傳輸協議進行建模和驗證.文獻[6]使用歸納法對不可否認性協議進行了分析.文獻[7]使用工具PRISM對分布式實時操作系統任務的可調度性問題進行了量化分析.

目前關于公平交換協議的許多形式化方法目的是發現更多的攻擊路徑,定性判斷協議是否滿足給定性質.為了分析信道環境對協議執行的影響,本文提出了基于信道可信度對公平交換協議進行形式化驗證的方法,重點對公平交換協議中的信道問題進行定量分析.

本文第2節介紹了概率模型檢測相關的基本理論,給出本文使用的概率模型檢測框架,第3節基于信道可信度對公平交換協議進行了形式化驗證,使用PRISM模型檢測工具對協議進行建模并對協議核心屬性進行定量分析,最后對全文進行總結.

2 概率模型檢測

自從20世紀80年代起,模型檢測(modelchecking)[8,9]已經成為了一項驗證計算機系統各項性質的重要技術.通過給定計算機系統的形式化模型和描述計算機系統性質的時序邏輯命題,模型檢測技術可以實現自動化驗證該計算機系統是否滿足給定的性質.模型檢測工具可以通過遍歷計算機系統的所有相關狀態來確定計算機系統是否滿足所給性質.

隨著計算機系日趨龐大和復雜,很多實際的系統被賦予隨機行為特征[9,10].這樣的系統可以通過對狀態之間的轉換概率進行建模.概率模型包括離散時間馬爾可夫鏈(discrete-time Markov Chain,DTMC)、連續時間馬爾科夫鏈(continuous-time Markov Chain,CTMC)和馬爾可夫決策過程(Markov decision processes,MDP)等.通過概率模型描述具體的計算機系統,用模型檢測的方法對隨機系統進行自動化的形式驗證,定量分析系統滿足用戶的功能或非功能需求性質的程度,即概率模型檢測(probabilistic modelchecking).

本文通過離散時間馬爾可夫鏈對公平交換協議進行形式化建模,然后通過概率計算樹邏輯對公平交換協議的核心屬性進行定量分析.

2.1 離散時間馬爾可夫鏈

離散時間馬爾可夫鏈(discrete-time Markov Chain,DTMC)是最常見的概率模型.

S是有限狀態集;

Δ:S×S→[0,1]是遷移概率函數;

Γ:S→2AP是標記函數.

圖1是一個離散時間馬爾可夫鏈的實例.

圖1 離散時間馬爾可夫鏈實例Fig.1 A simple DTMC

2.2 概率計算樹邏輯

概率計算樹邏輯(Probabilistic Computation Tree Logic,PCTL)由Hansson和Jonsson最先提出,是一個對計算樹邏輯(Computation Tree Logic,CTL)的概率擴展,用概率運算符P～p定量地擴展了計算樹邏輯的路徑量詞A(all)和E(exists),能夠描述概率模型的定量屬性.

定義2.關于原子命題集合AP的PCTL狀態公式Φ可定義為Φ∷=true|a|Φ∧Φ|Φ|P～p(Ψ),路徑公式Ψ可定義為Ψ∷=XΦ|ΦUΦ|ΦU≤nΦ,其中:

a∈AP,是原子命題;

X(next)表示下一狀態;

U(until)表示直到某狀態;

U≤n是U的變體,要求n次遷移或小于n次遷移內滿足U的語義;

～∈{≤,<,≥,>};

p∈[0,1]是概率界限值.

以圖1所示的離散時間馬爾可夫鏈為例,可以描述其最終達到成功狀態的概率.

P=[Fsucc]

可以通過集合S中各狀態的遷移概率值求解上述公式.

xs1=0.5·xs2+0.5·xs3

xs2=0.5·xs3+0.5·xs4

xs3=0

xs4=1

P=[Fsucc]=0.45

3 基于信道可信度的概率模型檢測

本文提出基于信道可信度對公平交換協議的核心屬性進行定量分析.為了實現定量分析公平交換協議的核心屬性,本文首先針對公平交換協議的實體分別進行了形式化建模,在建模過程中設計信道可信度對協議的影響,然后基于信道可信度定量分析公平交換協議的核心屬性.

3.1 公平交換協議形式化建模

公平交換協議(Fair Exchange Protocols)是使用最為廣泛的電子商務協議,本文選用了一個電子合同簽署協議(Contract Signing Protocols)[11]為例,對其進行形式化建模與驗證.協議實體主要包含參與者A、參與者B與可信第三方(Trusty Third Party,TTP),通過對協議實體進行建模可以分析協議是否滿足公平交換協議的主要安全屬性:公平性(Fairness)、有效性(Effectiveness)和時限性(Timeliness).在電子合同簽署的過程中,參與者之間難免會出現爭端的情況,因此,一個完備的電子合同簽署協議通常需要有一個主協議和一個爭端解決協議.主協議用來處理普通的電子合同簽署過程,爭端解決協議用來處理在電子合同簽署過程中出現的爭端.

為了實現對公平交換協議的核心屬性進行自動化驗證,本文使用模型檢測工具PRISM[12]對選用的電子合同簽署協議進行形式化建模.首先通過離散時間馬爾可夫鏈對協議的主協議和爭端解決協議進行描述.

電子合同簽署協議的主協議及爭端解決協議分別為:

1)電子合同簽署協議的主協議:

Step1.A→B:MSG1=SIGA(IDB,C,ETTP(IDA,RA))

Step2.B→A:MSF2=SIGB(IDA,MSG1,ETTP(RB))

Step3.A→B:MSG3=RA

Step4.B→A:MSG4=RB

其中,IDA為A的ID信息,C為合同內容,ETTP為加密后的信息,RA為A的密鑰.

表1 符號表示
Table 1 Symbols′ expression

符 號含 義SendMessagei二值變量，false表示消息i未被發送，true表示消息i已被發送．checkMessagei變量，0表示消息i未檢驗，1表示消息i通過檢驗，2表示消息i未能通過檢驗．stopX二值變量，false表示模塊X正常運行，true表示模塊X選擇終止協議reliabilityAB參與者A與參與者B間信道可信度reliabilityTTP參與者A、B與TTP間信道可信度

每一步的信息接收方在接收信息后,通過檢查信息是否完備選擇下一步操作.例如,在第二步時,當B收到A發送的消息1后,先檢查消息1是否完備.如果消息1完備,那么B向A發送消息2,消息2中包含A的ID信息、消息1、加密后B的密鑰以及B的簽名;如果消息1不完備,那么B選擇終止協議.

[] !stopB & sendMessage1 & (checkMessage1=0) & !sendMessage2->reliabilityAB:(checkMessage1′=1)+(1-reliabilityAB):(checkMessage1′=2);

[] !stopB & sendMessage1 & (checkMessage1=2) & !sendMessage2->1:(stopB′=true);

[] !stopB & sendMessage1 & (checkMessage1=1) & !sendMessage2->1:(sendMessage2′=true);

2)爭端解決協議:

Step5.A,B→TTP:MSG5=msg1+msg2

msg1=SIGA(IDB,C,ETTP(IDA,RA))

msg2=SIGB(IDA,MSG1,ETTP(RB))

Step6.TTP→A:MSG6=MSG2,RB

Step7.TTP→B:MSG7=MSG1,RA

TTP初始狀態為終止狀態,當協議出現爭端的情況時,由A或B發起爭端解決協議.當TTP收到消息5后,先檢查消息5是否完備.如果消息5完備,那么TTP就會把消息6發送給A,把消息7發送給B.其中,消息6包含B的密鑰,消息7包含A的密鑰.如果消息5不完備,那么TTP選擇終止協議.

[] stopTTP & sendMessage5B & (checkMessage5B=0)->1:(stopTTP′=false);

[] stopTTP & !sendMessage5B & sendMessage5A & (checkMessage5A=0)->1:(stopTTP′=false);

[] !stopTTP & sendMessage5B & (checkMessage5B=0)->reliabilityTTP:(checkMessage5B′=1)+(1-reliabilityTTP):(checkMessage5B′=2);

……

[] !stopTTP & !sendMessage5B & sendMessage5A & (checkMessage5A=0)->reliabilityTTP:(checkMessage5A′=1)+(1-reliabilityTTP):(checkMessage5A′=2);

圖2 電子合同簽署協議模型Fig.2 Model of contract signing protocols

3.2 協議性質驗證和分析

目前國內外已有很多針對公平交換協議進行定性分析的研究,但隨著現代工業的發展,實際項目對相關數據有了進一步的要求,因此本文對公平交換協議的公平性、有效性和時限性進行了定量分析.

公平性(Fairness)保證了電子合同簽署協議的簽署雙方要么都能夠獲得對方簽署過的合同,要么都無法獲得對方簽署過的合同.因此如果電子合同簽署協議滿足公平性,那么系統不存在這樣的狀態:在協議結束的時候,只有A簽署了合同,而B沒有簽署合同.因此可以把協議不滿足公平性描述為:

label "unfair"=stopA & stopB & stopTTP & ((sendMessage3 & checkMessage3=1) | sendMessage7) & ((sendMessage4 & checkMessage4=2) | (!sendMessage4 & !sendMessage6))

其中,stopA & stopB & stopTTP是協議結束的標志;sendMessage3 & checkMessage3=1和sendMessage7是A簽署合同的兩種情況;sendMessage4 & checkMessage4=2和!sendMessage4 & !sendMessage6是B沒有簽署合同的兩種情況.

通過定義reliabilityAB和reliabilityTTP可以描述參與者A、B和TTP之間的信道可信度.假設參與者A、B間信道可信度為0.8.首先驗證當參與者A、B與TTP間的信道可信度為0.8時,電子合同簽署協議是否滿足公平性,因此將reliabilityAB和reliabilityTTP都設置為0.8.

當使用PRISM驗證模型屬性時,默認情況下,將返回模型初始狀態的值.但由于實際需要,可以通過設置filters過濾器同時計算模型所有狀態的值.通過PRISM計算協議不滿足公平性的狀態概率可以描述為:

filter(state,P=? [ F "unfair" ],"init")

檢驗屬性,得到結果:0.08192.同理,通過設置reliabilityAB,得到當參與者A、B與TTP信道可信度為0.8時,參與者A與參與者B信道可信度取不同值條件下協議不滿足公平性的狀態概率.

檢驗結果如圖所示,橫軸代表參與者A、B間信道可信度,縱軸代表協議不滿足公平性的狀態概率.由檢驗結果可以得出,只有當reliabilityAB取值為0或1時,協議不滿足公平性概率為0,即協議滿足公平性;當reliabilityAB取值為0.7時,協議不滿足公平性的概率接近最大值,為0.08232.

圖3 協議不滿足公平性的概率Fig.3 Probability that the protocol does not satisfy the fairness

在傳統安全協議中,通常假設協議在不安全的信道上進行,所有在信道上傳輸的消息都有可能被攔截或篡改.而在公平交換協議中,如果協議只在不可靠信道上進行,發往 TTP的消息可能丟失,這就等同于沒有TTP[11].因此本文針對TTP的信道可信度進行了驗證分析.首先驗證當TTP的信道可信度為1時,電子合同簽署協議是否滿足公平性.

圖4 協議不滿足公平性的概率Fig.4 Probability of the protocol does not satisfy the fairness

通過設置reliabilityAB得到在不同信道可信度的條件下協議不滿足公平性的狀態概率.由檢驗結果可以得出,當reliabilityAB取值為0.7時,協議不滿足公平性的概率接近最大值,為0.10290.相較于reliabilityTTP取值為0.8時概率更大.

圖5 協議不滿足公平性的概率Fig.5 Probability of the protocol does not satisfy the fairness

通過同時為reliabilityTTP和reliabilityAB設置不同值,得到協議不滿足公平性的概率與信道可信度的變化關系.

有效性(Effectiveness)保證了電子合同簽署協議的簽署雙方在滿足協議設計者所設定的通信信道質量,并且簽署雙方都誠實的條件下,協議簽署雙方都能獲得對方簽署過的合同.Kremer依據強度不同定義了兩種有效性[13]:弱有效性和強有效性.弱有效性是在排除了協議簽署主體不誠實和信道質量不可靠這兩項不利因素后,協議應當滿足的屬性.強有效性是在排除協議簽署主體不誠實這項不利因素后,協議應當滿足的屬性.因此可以把協議滿足有效性描述為:

label "effective"=stopA & stopB & stopTTP & ((sendMessage3 & checkMessage3=1) | sendMessage7) & ((sendMessage4 & checkMessage4=1) | sendMessage6)

首先驗證協議是否滿足弱有效性,將reliabilityAB和reliabilityTTP都設置為1,得到協議滿足若有效性的概率為1.因此可以判定協議滿足弱有效性.

然后驗證協議是否滿足強有效性,通過為reliabilityAB和reliabilityTTP設置不同值,得到當A、B與TTP間信道可信度為不同值時,協議滿足強有效性的概率.

圖6 協議滿足強有效性的概率Fig.6 Probability of the protocol satisfy the strong effectiveness

由檢驗結果可知,協議滿足強有效性的概率隨reliabilityAB取值增大而增大;當reliabilityAB為0時,概率為0;當reliabilityAB取值為1時,概率為1.協議是否滿足強有效性與參與者A、B與TTP間信道可信度取值無關.

時限性(Timeliness)保證了電子合同簽署協議能夠在A提出終止協議執行后,能夠及時有效的終止協議.如果此時A已經獲得了B簽署的合同,那么電子合同簽署協議應該在B也獲得A簽署的合同之后終止協議.如果此時A還沒有獲得B簽署的合同,那么電子合同簽署應該保證在協議結束時,B也沒有獲得A簽署的合同.因此如果電子合同簽署協議滿足及時性,那么系統不存在這樣的狀態:當A請求終止協議時,如果此時B還沒有簽署合同,那么系統在未來的某個狀態中出現了A簽署了合同而B沒有簽署合同的狀態.因此可以把協議不滿足及時性描述為:

label "untimely"=(stopA & ((!sendMessage4 & !sendMessage6) | (sendMessage4 & checkMessage4=2))) => (stopA & stopB & stopTTP & ((sendMessage3 & checkMessage3=1) | sendMessage7) & ((!sendMessage4 & !sendMessage6) | (sendMessage4 & checkMessage4=2)))

通過為reliabilityAB和reliabilityTTP設置不同值,得到當A、B與TTP信道可信度為不同值時,協議不滿足時限性的狀態概率.

由檢驗結果可知,只有當reliabilityAB取值為0或1時,協議不滿足公平性概率為1;當reliabilityAB取值為0.7時,協議不滿足時限性的概率接近最小值,為0.75.協議是否滿足時限性與參與者A、B與TTP間信道可信度取值無關.

綜上所述,電子合同簽署協議滿足核心屬性的概率隨信道可信度的變化而變化.其中,協議滿足公平性的概率隨參與者A、B和TTP間的信道可信度增大而減小,協議滿足有效性和時限性的概率與參與者A、B和TTP間的信道可信度無關;協議滿足公平性、有效性和時限性的概率隨參與者A和參與者B間的信道可信度變化而變化,當信道可信度取0.7時協議滿足公平性概率接近最小為0.89710,協議滿足有效性的概率隨信道可信度的增大而增大,當信道可信度取0.7時協議滿足時限性概率接近最大為0.25.由檢驗結果可知,協議各實體間信道可信度對協議的公平性、有效性和時限性有不同程度的影響,因此對相應信道進行控制或改善,可以提高協議的安全性.

圖7 協議不滿足時限性的概率Fig.7 Probability of the protocol does not satisfy the timeliness

4 總 結

本文提出基于信道可信度對公平交換協議的核心屬性進行定量分析,運用概率模型檢測的形式化驗證方法,以一個電子合同簽署協議為例,對公平交換協議的核心屬性進行分析驗證.首先基于離散時間馬爾可夫鏈對協議參與者A、B和TTP進行抽象建模,然后8在協議進行的過程中,添加了信道可信度對協議進程的影響,在狀態遷移中加入了信道可信度,最后針對公平交換協議的核心屬性進行定量分析.本文對公平交換協議的公平性、有效性和時限性等核心屬性進行了量化分析,利用檢驗結果,可以對應用環境進行具體分析,對相應信道進行控制或改善,使得概率在可控的范圍內,提高協議的安全性.同時將不同信道可信度條件下協議滿足核心屬性的概率在同一坐標下進行對比,可以使設計人員做出更直觀的判斷,有利于對系統的設計.定量形式化分析結果可以為開發人員提供參考依據,進一步增加系統的可靠性和正確性,此方法同樣適用于其他安全協議.在下一步的研究中可以將此方法推廣應用于其他安全協議及分布式系統的形式化驗證等領域.

[1] Asokan N.Fairness in electronic commerce[M].University of Waterloo,1998.

[2] Xu Jing-fang,Cui Guo-hua,Cheng Qi,et al.Security analysis and improvement of fair exchange protocols using the theory of cross validation[J].Journal of Chinese Computer Systems,2009,30(2):

345-348.

[3] Li Qun,Chen Qing-liang.Formal verification of fair exchange protocols based on alternating-time temporal logic[J].Computer Engineering and Applications,2015,51(19):32-36.

[4] Norman G,Shmatikov V.Analysis of probabilistic contract signing[C].Formal Aspects of Security,First International Conference,FASec 2002,London,UK,DBLP,2002:81-96.

[5] Alrabaee S,Bataineh A,Khasawneh F A,et al.Using model checking for trivial file transfer protocol validation[C].Fourth International Conference on Communications and Networking,2014:1-7.

[6] Bella G,Paulson L C.Accountability protocols:formalized and verified[J].Acm Transactions on Information & System Security,2006,9(2):138-161.

[7] Huo Yan-yan,Guan Yong,Li Xiao-juan,et al.Formal verification of distributed real-time operating system task scheduling based on PRISM[J].Journal of Chinese Computer Systems,2015,36(9):2125-2129.

[8] Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C].DBLP,2008:196-215.

[9] Baier C,Katoen J P.Principles of model checking (representation and mind series)[M].The MIT Press,2008.

[10] Liu Yang,Li Xuan-dong,Ma Yan,et al.Survey for stochastic model checking[J].Chinese Journal of Computers,2015,38(11):2145-2162.

[11] Wang Zhi-ling,Zhang Yu-qing,Yang Bo.Design of a fair contract signing protocol[J].Computer Engineering,2006,32(19):159-161.

[12] Kwiatkowska M,Norman G,Parker D.PRISM 4.0:verification of probabilistic real-time systems[C].In Ganesh Gopalakrishnan,Shaz Qocleer,Computer Aided Verification,Proceeding of 23rd International Conference,CAV2011,Snowbird,UT,USA,2011:585-591.

[13] Kremer S.Formal analysis of optimistic fair exchange protocols[D].Brussels:Université Libre de Bruxelles,2004.

附中文參考文獻：

[2] 許靜芳,崔國華,程 琦,等.關于公平交換協議中使用正交驗證理論的安全性分析及改進[J].小型微型計算機系統,2009,30(2):345-348.

[3] 李 群,陳清亮.基于ATL的公平交換協議的形式化驗證[J].計算機工程與應用,2015,51(19):32-36.

[7] 霍燕燕,關 永,李曉娟,等.基于PRISM的分布式實時操作系統任務調度的形式化驗證[J].小型微型計算機系統,2015,36(9):2125-2129.

[10] 劉 陽,李宣東,馬 艷,等.隨機模型檢驗研究[J].計算機學報,2015,38(11):2145-2162.

[11] 王芷玲,張玉清,楊 波.一個公平電子合同簽署協議的設計[J].計算機工程,2006,32(19):159-161.