公平交換協(xié)議的信道可信度形式化驗(yàn)證方法

楊晉吉,申涵瑞,陳清亮

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

1 引 言

隨著電子商務(wù)技術(shù)的發(fā)展,越來越多的電子商務(wù)應(yīng)用進(jìn)入人們?nèi)粘Ｉ?電子商務(wù)的安全性問題也變得更加重要.公平交換協(xié)議作為一種重要的電子商務(wù)安全協(xié)議,在保障電子商務(wù)應(yīng)用的安全性方面扮演了非常重要的角色.公平性、有效性和時(shí)限性是電子商務(wù)安全的核心屬性,設(shè)計(jì)出公平安全的公平交換協(xié)議是電子商務(wù)發(fā)展的迫切要求,針對(duì)公平交換協(xié)議進(jìn)行分析驗(yàn)證具有十分重要的意義.但由于公平交換協(xié)議的復(fù)雜性,公平交換協(xié)議的形式化驗(yàn)證領(lǐng)域仍存在許多問題,例如簡(jiǎn)易有效的針對(duì)安全屬性的分析方法和符合現(xiàn)代工業(yè)要求的公平交換協(xié)議等.

信道問題是公平交換協(xié)議分析中一個(gè)重要問題.在開放的網(wǎng)絡(luò)環(huán)境下,消息在信道傳輸?shù)倪^程中會(huì)由于信道錯(cuò)誤或惡意實(shí)體的主動(dòng)攻擊,導(dǎo)致消息的丟失、錯(cuò)誤或延遲[1].因此基于信道可信度對(duì)公平交換協(xié)議的核心屬性進(jìn)行定量分析在實(shí)際工程中具有重要的作用.

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

形式化驗(yàn)證是對(duì)公平交換協(xié)議進(jìn)行分析的重要方法.文獻(xiàn)[5]基于線性時(shí)態(tài)邏輯,使用模型檢測(cè)工具SPIN對(duì)普通文件傳輸協(xié)議進(jìn)行建模和驗(yàn)證.文獻(xiàn)[6]使用歸納法對(duì)不可否認(rèn)性協(xié)議進(jìn)行了分析.文獻(xiàn)[7]使用工具PRISM對(duì)分布式實(shí)時(shí)操作系統(tǒng)任務(wù)的可調(diào)度性問題進(jìn)行了量化分析.

目前關(guān)于公平交換協(xié)議的許多形式化方法目的是發(fā)現(xiàn)更多的攻擊路徑,定性判斷協(xié)議是否滿足給定性質(zhì).為了分析信道環(huán)境對(duì)協(xié)議執(zhí)行的影響,本文提出了基于信道可信度對(duì)公平交換協(xié)議進(jìn)行形式化驗(yàn)證的方法,重點(diǎn)對(duì)公平交換協(xié)議中的信道問題進(jìn)行定量分析.

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

2 概率模型檢測(cè)

自從20世紀(jì)80年代起,模型檢測(cè)(modelchecking)[8,9]已經(jīng)成為了一項(xiàng)驗(yàn)證計(jì)算機(jī)系統(tǒng)各項(xiàng)性質(zhì)的重要技術(shù).通過給定計(jì)算機(jī)系統(tǒng)的形式化模型和描述計(jì)算機(jī)系統(tǒng)性質(zhì)的時(shí)序邏輯命題,模型檢測(cè)技術(shù)可以實(shí)現(xiàn)自動(dòng)化驗(yàn)證該計(jì)算機(jī)系統(tǒng)是否滿足給定的性質(zhì).模型檢測(cè)工具可以通過遍歷計(jì)算機(jī)系統(tǒng)的所有相關(guān)狀態(tài)來確定計(jì)算機(jī)系統(tǒng)是否滿足所給性質(zhì).

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

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

2.1 離散時(shí)間馬爾可夫鏈

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

S是有限狀態(tài)集;

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

Γ:S→2AP是標(biāo)記函數(shù).

圖1是一個(gè)離散時(shí)間馬爾可夫鏈的實(shí)例.

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

2.2 概率計(jì)算樹邏輯

概率計(jì)算樹邏輯(Probabilistic Computation Tree Logic,PCTL)由Hansson和Jonsson最先提出,是一個(gè)對(duì)計(jì)算樹邏輯(Computation Tree Logic,CTL)的概率擴(kuò)展,用概率運(yùn)算符P～p定量地?cái)U(kuò)展了計(jì)算樹邏輯的路徑量詞A(all)和E(exists),能夠描述概率模型的定量屬性.

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

a∈AP,是原子命題;

X(next)表示下一狀態(tài);

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

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

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

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

以圖1所示的離散時(shí)間馬爾可夫鏈為例,可以描述其最終達(dá)到成功狀態(tài)的概率.

P=[Fsucc]

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

xs1=0.5·xs2+0.5·xs3

xs2=0.5·xs3+0.5·xs4

xs3=0

xs4=1

P=[Fsucc]=0.45

3 基于信道可信度的概率模型檢測(cè)

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

3.1 公平交換協(xié)議形式化建模

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

為了實(shí)現(xiàn)對(duì)公平交換協(xié)議的核心屬性進(jìn)行自動(dòng)化驗(yàn)證,本文使用模型檢測(cè)工具PRISM[12]對(duì)選用的電子合同簽署協(xié)議進(jìn)行形式化建模.首先通過離散時(shí)間馬爾可夫鏈對(duì)協(xié)議的主協(xié)議和爭(zhēng)端解決協(xié)議進(jìn)行描述.

電子合同簽署協(xié)議的主協(xié)議及爭(zhēng)端解決協(xié)議分別為:

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

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為合同內(nèi)容,ETTP為加密后的信息,RA為A的密鑰.

表1 符號(hào)表示
Table 1 Symbols′ expression

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

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

[] !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)爭(zhēng)端解決協(xié)議:

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初始狀態(tài)為終止?fàn)顟B(tài),當(dāng)協(xié)議出現(xiàn)爭(zhēng)端的情況時(shí),由A或B發(fā)起爭(zhēng)端解決協(xié)議.當(dāng)TTP收到消息5后,先檢查消息5是否完備.如果消息5完備,那么TTP就會(huì)把消息6發(fā)送給A,把消息7發(fā)送給B.其中,消息6包含B的密鑰,消息7包含A的密鑰.如果消息5不完備,那么TTP選擇終止協(xié)議.

[] 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 電子合同簽署協(xié)議模型Fig.2 Model of contract signing protocols

3.2 協(xié)議性質(zhì)驗(yàn)證和分析

目前國(guó)內(nèi)外已有很多針對(duì)公平交換協(xié)議進(jìn)行定性分析的研究,但隨著現(xiàn)代工業(yè)的發(fā)展,實(shí)際項(xiàng)目對(duì)相關(guān)數(shù)據(jù)有了進(jìn)一步的要求,因此本文對(duì)公平交換協(xié)議的公平性、有效性和時(shí)限性進(jìn)行了定量分析.

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

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

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

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

當(dāng)使用PRISM驗(yàn)證模型屬性時(shí),默認(rèn)情況下,將返回模型初始狀態(tài)的值.但由于實(shí)際需要,可以通過設(shè)置filters過濾器同時(shí)計(jì)算模型所有狀態(tài)的值.通過PRISM計(jì)算協(xié)議不滿足公平性的狀態(tài)概率可以描述為:

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

檢驗(yàn)屬性,得到結(jié)果:0.08192.同理,通過設(shè)置reliabilityAB,得到當(dāng)參與者A、B與TTP信道可信度為0.8時(shí),參與者A與參與者B信道可信度取不同值條件下協(xié)議不滿足公平性的狀態(tài)概率.

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

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

在傳統(tǒng)安全協(xié)議中,通常假設(shè)協(xié)議在不安全的信道上進(jìn)行,所有在信道上傳輸?shù)南⒍加锌赡鼙粩r截或篡改.而在公平交換協(xié)議中,如果協(xié)議只在不可靠信道上進(jìn)行,發(fā)往 TTP的消息可能丟失,這就等同于沒有TTP[11].因此本文針對(duì)TTP的信道可信度進(jìn)行了驗(yàn)證分析.首先驗(yàn)證當(dāng)TTP的信道可信度為1時(shí),電子合同簽署協(xié)議是否滿足公平性.

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

通過設(shè)置reliabilityAB得到在不同信道可信度的條件下協(xié)議不滿足公平性的狀態(tài)概率.由檢驗(yàn)結(jié)果可以得出,當(dāng)reliabilityAB取值為0.7時(shí),協(xié)議不滿足公平性的概率接近最大值,為0.10290.相較于reliabilityTTP取值為0.8時(shí)概率更大.

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

通過同時(shí)為reliabilityTTP和reliabilityAB設(shè)置不同值,得到協(xié)議不滿足公平性的概率與信道可信度的變化關(guān)系.

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

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

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

然后驗(yàn)證協(xié)議是否滿足強(qiáng)有效性,通過為reliabilityAB和reliabilityTTP設(shè)置不同值,得到當(dāng)A、B與TTP間信道可信度為不同值時(shí),協(xié)議滿足強(qiáng)有效性的概率.

圖6 協(xié)議滿足強(qiáng)有效性的概率Fig.6 Probability of the protocol satisfy the strong effectiveness

由檢驗(yàn)結(jié)果可知,協(xié)議滿足強(qiáng)有效性的概率隨reliabilityAB取值增大而增大;當(dāng)reliabilityAB為0時(shí),概率為0;當(dāng)reliabilityAB取值為1時(shí),概率為1.協(xié)議是否滿足強(qiáng)有效性與參與者A、B與TTP間信道可信度取值無關(guān).

時(shí)限性(Timeliness)保證了電子合同簽署協(xié)議能夠在A提出終止協(xié)議執(zhí)行后,能夠及時(shí)有效的終止協(xié)議.如果此時(shí)A已經(jīng)獲得了B簽署的合同,那么電子合同簽署協(xié)議應(yīng)該在B也獲得A簽署的合同之后終止協(xié)議.如果此時(shí)A還沒有獲得B簽署的合同,那么電子合同簽署應(yīng)該保證在協(xié)議結(jié)束時(shí),B也沒有獲得A簽署的合同.因此如果電子合同簽署協(xié)議滿足及時(shí)性,那么系統(tǒng)不存在這樣的狀態(tài):當(dāng)A請(qǐng)求終止協(xié)議時(shí),如果此時(shí)B還沒有簽署合同,那么系統(tǒng)在未來的某個(gè)狀態(tài)中出現(xiàn)了A簽署了合同而B沒有簽署合同的狀態(tài).因此可以把協(xié)議不滿足及時(shí)性描述為:

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

通過為reliabilityAB和reliabilityTTP設(shè)置不同值,得到當(dāng)A、B與TTP信道可信度為不同值時(shí),協(xié)議不滿足時(shí)限性的狀態(tài)概率.

由檢驗(yàn)結(jié)果可知,只有當(dāng)reliabilityAB取值為0或1時(shí),協(xié)議不滿足公平性概率為1;當(dāng)reliabilityAB取值為0.7時(shí),協(xié)議不滿足時(shí)限性的概率接近最小值,為0.75.協(xié)議是否滿足時(shí)限性與參與者A、B與TTP間信道可信度取值無關(guān).

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

圖7 協(xié)議不滿足時(shí)限性的概率Fig.7 Probability of the protocol does not satisfy the timeliness

4 總 結(jié)

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

[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.

附中文參考文獻(xiàn)：

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

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

[7] 霍燕燕,關(guān) 永,李曉娟,等.基于PRISM的分布式實(shí)時(shí)操作系統(tǒng)任務(wù)調(diào)度的形式化驗(yàn)證[J].小型微型計(jì)算機(jī)系統(tǒng),2015,36(9):2125-2129.

[10] 劉 陽,李宣東,馬 艷,等.隨機(jī)模型檢驗(yàn)研究[J].計(jì)算機(jī)學(xué)報(bào),2015,38(11):2145-2162.

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