基于ATL 的公平交換協(xié)議的形式化驗(yàn)證

李 群，陳清亮

LI Qun,CHEN Qingliang

暨南大學(xué) 計(jì)算機(jī)科學(xué)系，廣州510632

Department of Computer Science，Jinan University，Guangzhou 510632,China

1 引言

電子商務(wù)是一種各個(gè)參與者通過計(jì)算機(jī)和Internet技術(shù)來實(shí)現(xiàn)交易的業(yè)務(wù)，人們可以通過電子商務(wù)的形式，實(shí)現(xiàn)商品或服務(wù)的交換。電子商務(wù)以Internet 技術(shù)為支撐，突破了時(shí)間和地域的限制，以一種便捷、廉價(jià)和自由的方式得到了廣泛應(yīng)用。隨著Internet 技術(shù)的發(fā)展，電子商務(wù)已經(jīng)成為了當(dāng)代經(jīng)濟(jì)活動的主要形式之一。在電子商務(wù)中，人們關(guān)心的核心問題就是能否保證公平交換（Fair Exchange）。所謂公平交換是指進(jìn)行交換的各方能夠公平的獲得各自想要的利益，也就是說，在完成交換后，進(jìn)行交換的各方要么都獲得各自想要的利益，要么都不獲得這些利益[1]。

公平交換協(xié)議的應(yīng)用是實(shí)現(xiàn)公平交換的關(guān)鍵。所謂公平交換協(xié)議是指在正常情況下完成了協(xié)議之后，參加協(xié)議的各方都能夠得到各自期望的利益；非正常情況下結(jié)束協(xié)議時(shí)，參加協(xié)議的各方都不能得到利益[1]。

對于公平交換協(xié)議來說，一次完整有效的公平交換應(yīng)該在有限的時(shí)間內(nèi)執(zhí)行完畢，如果協(xié)議沒有成功完成，那么這次交換的結(jié)果應(yīng)該和沒有交換的結(jié)果是一致的。如果在協(xié)議執(zhí)行過程中出現(xiàn)有爭端的情況，那么應(yīng)該提供爭端解決機(jī)制以保證公平交換協(xié)議的順利執(zhí)行。

一個(gè)新的公平交換協(xié)議在設(shè)計(jì)的時(shí)候就應(yīng)該考慮好所需要滿足的屬性要求，如最重要的公平性、及時(shí)性和不可濫用性等。在新的公平交換協(xié)議被應(yīng)用之前，必須要確保該協(xié)議是真的滿足這些必要屬性的。如何驗(yàn)證一個(gè)公平交換協(xié)議是否滿足某些屬性也成為了時(shí)下研究的熱點(diǎn)。驗(yàn)證的方法有很多，如人工審查、測試和形式化驗(yàn)證等。人工審查和測試都不是理想的驗(yàn)證方法，因?yàn)槿斯彶楹蜏y試都無法證明協(xié)議不存在某個(gè)缺陷，也不能證明它滿足某些屬性。而形式化驗(yàn)證則是根據(jù)協(xié)議的形式規(guī)范和屬性，使用數(shù)學(xué)的方法來證明協(xié)議的正確性或非正確性。形式化驗(yàn)證可以有效地驗(yàn)證一個(gè)協(xié)議是否存在某個(gè)缺陷或者滿足某些屬性。

形式化驗(yàn)證可以分為三大類：等價(jià)性檢查、形式模型檢測和定理證明。在使用形式化驗(yàn)證方法驗(yàn)證協(xié)議的規(guī)范時(shí)，主要用的是形式模型檢測。形式模型檢測是用時(shí)態(tài)邏輯來描述系統(tǒng)屬性和規(guī)范，通過有效的搜索方法來檢查給定的系統(tǒng)是否滿足規(guī)范。其中使用最為廣泛的時(shí)態(tài)邏輯有CTL（Computation Tree Logic）、LTL（Liner Temporal Logic）和ATL[2]等。這里無法證明一個(gè)協(xié)議是無缺陷的，只能夠證明該協(xié)議滿足某些必要的屬性。驗(yàn)證一個(gè)公平交換協(xié)議一般驗(yàn)證其三大屬性：公平性、及時(shí)性和不可濫用性。公平性能夠保證參與到協(xié)議中的各方的投入和收獲能夠平均；及時(shí)性能夠保證協(xié)議在需要終止的時(shí)候能及時(shí)的終止，不會因?yàn)椴患皶r(shí)而產(chǎn)生不公平的結(jié)果；不可濫用性能夠保證協(xié)議不會被參與者所濫用而獲取利益。

國內(nèi)外關(guān)于運(yùn)用形式化方法對協(xié)議進(jìn)行分析與驗(yàn)證的研究工作有很多：文獻(xiàn)[3]基于擴(kuò)展的CTL——CTLC，對委托協(xié)議（Commitment Protocols）的活性（Liveness）和安全性（Safety）做了驗(yàn)證；文獻(xiàn)[4]對基于LTL 的模型檢查問題的復(fù)雜性進(jìn)行了討論和分析；文獻(xiàn)[5]基于LTL，使用工具SPIN 對普通文件傳輸協(xié)議（Trivial File Transfer Protocol，TFTP）進(jìn)行建模和驗(yàn)證；文獻(xiàn)[6]基于LTL，把自動推理技術(shù)應(yīng)用于安全協(xié)議（Security Protocols）的形式化分析，并提出了一個(gè)用于安全協(xié)議的通用模型檢測框架；文獻(xiàn)[7]基于ATL 對通信協(xié)議（Communication Protocols）的公平性進(jìn)行形式化分析與驗(yàn)證，發(fā)現(xiàn)了該文獻(xiàn)所驗(yàn)證的協(xié)議——TMN 協(xié)議不滿足公平性，并提出了改進(jìn)該協(xié)議的方案；文獻(xiàn)[8]基于ATL，對非抵賴性協(xié)議的公平性進(jìn)行分析與討論，并提出了在形式化分析與驗(yàn)證協(xié)議的公平性時(shí)可能會出現(xiàn)的問題；文獻(xiàn)[9]基于ATL，對多方參與的合同簽署協(xié)議（Contract Signing Protocols）的公平性和及時(shí)性做出分析與驗(yàn)證；文獻(xiàn)[10]基于多智能代理博弈系統(tǒng)（MIAG）對電子商務(wù)協(xié)議安全性的形式化分析方法進(jìn)行了研究和創(chuàng)新，并提出了一個(gè)新的分析模型；文獻(xiàn)[11]基于博弈理論，采用形式化方法對合同簽署協(xié)議的公平性和不可濫用性進(jìn)行形式化分析與驗(yàn)證。

本文采用基于ATL 的方法，對于電子商務(wù)協(xié)議中廣泛應(yīng)用的公平交換協(xié)議進(jìn)行形式化分析與驗(yàn)證。與文獻(xiàn)[3-6]相比較，文獻(xiàn)[3-6]采用的CTL 或LTL 都是以封閉系統(tǒng)的方式來描述協(xié)議系統(tǒng)，無法有效地描述協(xié)議系統(tǒng)中各參與者之間的交互，而本文采用的ATL 則是以開放系統(tǒng)的方式來描述協(xié)議系統(tǒng)，能夠有效克服采用CTL 或LTL 等傳統(tǒng)邏輯方法以封閉系統(tǒng)方式分析協(xié)議的缺點(diǎn)，更好地描述協(xié)議各參與者之間的合作與競爭關(guān)系。與文獻(xiàn)[7-11]相比較，文獻(xiàn)[7-11]只片面關(guān)注協(xié)議的某一些屬性，并對其進(jìn)行分析與驗(yàn)證，而本文則將基于ATL 的形式化分析與驗(yàn)證方法具體應(yīng)用到使用更為廣泛的公平交換協(xié)議，并且對公平交換協(xié)議的公平性、及時(shí)性和不可濫用性進(jìn)行了全面的分析和有效的驗(yàn)證，同時(shí)，本文的建模方式也更易于理解。

2 ATL 基礎(chǔ)

ATL 是用來描述交互式開放系統(tǒng)的規(guī)格和屬性的時(shí)態(tài)邏輯。ATL 的定義是關(guān)于一個(gè)有限命題集合Π和一個(gè)有限參與者集合Σ={1,2,…,k}的命題邏輯，它的公式定義如下：

（S1）p是公式，其中，p∈Π。

（S2）??，?1∨?2是公式，其中，?、?1和?2都是公式。

（S3）＜＜A＞＞○?，＜＜A＞＞□?，＜＜A＞＞?1U?2是公式。

其中A?Σ；?、?1和?2是公式；＜＜＞＞是路徑量詞，＜＜A＞＞表示聯(lián)合A，系統(tǒng)所能達(dá)到的狀態(tài)；○（next，下一個(gè)狀態(tài)），□（always，總是），U（until，直到）是標(biāo)準(zhǔn)的時(shí)態(tài)操作符。通常，用＜＜A＞＞◇?來表示＜＜A＞＞tr ueU?。

ATS[2]是Kripke Structures[12]的一個(gè)擴(kuò)充，用來形式化描述交互式開放系統(tǒng)的狀態(tài)變遷。ATS 的形式化定義為ATS=(Π,Σ,Q,Q0,π,δ)，其中：

Π是命題集合；

Σ是參與者集合；

Q是狀態(tài)集合；

Q0?Q是初始狀態(tài)集合；

π:Q→2Π是一個(gè)映射，表示在每個(gè)狀態(tài)下，值為真的命題的集合；

在ATL 中，一個(gè)參與者擁有的策略是指在所有可能的系統(tǒng)狀態(tài)下，他能夠做出的所有選擇，這些選擇將會影響系統(tǒng)所到達(dá)的下一個(gè)狀態(tài)。通俗的講，策略就是告訴參與者在每一個(gè)狀態(tài)下應(yīng)該如何抉擇。在交互式開放系統(tǒng)中，所有參與者選擇自己的策略，進(jìn)行博奕后產(chǎn)生的結(jié)果決定了系統(tǒng)的狀態(tài)遷移。這里使用ATL 來驗(yàn)證交互式開放系統(tǒng)是否在不論其子系統(tǒng)如何選擇自己的策略的情況下都能夠一定滿足某個(gè)屬性。

3 形式化建模

本文使用ATL 來驗(yàn)證一個(gè)電子合同簽署協(xié)議[13]，協(xié)議的形式化描述如下所示。

主協(xié)議：

MS1：A→B：

msg1=SIGA（IDB，C，ETTP（IDA，RA））

MS2：B→A：

msg2=SIGB（IDA，msg1，ETTP（RB））

MS3：A→B：RA

MS4：B→A：RB

爭端解決協(xié)議：

MS5：A、B→TTP：

msg1=SIGA（IDB，C，ETTP（IDA，RA））

msg2=SIGB（IDA，msg1，ETTP（RB））

MS6：TTP→A：msg2，RB

MS7：TTP→B：msg1，RA

協(xié)議執(zhí)行過程說明如下：

（1）A 發(fā)送消息MS1 給B，B 收到MS1 后，檢查MS1是否正確，如果正確，則B 發(fā)送消息MS2 給A；否則B 選擇終止協(xié)議。

（2）A 收到MS2 后，檢查MS2 是否正確，如果正確，則A 發(fā)送消息MS3 給B；否則A 選擇終止協(xié)議。

（3）B 收到MS3 后，檢查MS3 是否正確，如果正確，則B發(fā)送消息MS4給A；否則B選擇發(fā)起爭端解決協(xié)議。

（4）A 收到MS4 后，檢查MS4 是否正確，如果正確，則協(xié)議運(yùn)行結(jié)束；否則A 選擇發(fā)起爭端解決協(xié)議。

（5）B 發(fā)送了MS2 之后，若沒有收到MS3，則B 選擇發(fā)起爭端解決協(xié)議；同樣，A 發(fā)送了MS3 之后，若沒有收到MS4，則A 也選擇發(fā)起爭端解決協(xié)議。

（6）TTP 收到MS5 后，檢查MS5 是否正確，如果正確，則把MS6 發(fā)送給A，MS7 發(fā)送給B；否則，TTP 選擇終止協(xié)議。

在這個(gè)協(xié)議中，通信信道被假設(shè)為可操作的，即只要A 向B 發(fā)送的消息X，則B 在一定時(shí)間內(nèi)總能收到消息X，因此通信信道不作為形式化建模的一部分。所以，只需對三個(gè)實(shí)體進(jìn)行建模，即參與者A、參與者B 和TTP?，F(xiàn)在要驗(yàn)證這個(gè)協(xié)議的三大屬性：公平性、及時(shí)性和不可濫用性。假設(shè)參與者A 是誠實(shí)的，參與者B 是不誠實(shí)的。因此，可以對協(xié)議的公平性、及時(shí)性和不可濫用性做如下的形式化描述。

（1）協(xié)議的公平性可形式化描述為：

?＜＜B,TTP ＞＞◇(ContractA ∧?＜＜A ＞＞◇ContractB)

即參與者B 與TTP 合作，沒有一個(gè)策略能夠使得協(xié)議達(dá)到一個(gè)狀態(tài)——參與者B 獲得了參與者A 的簽名，但是參與者A 在該狀態(tài)下卻沒有一個(gè)策略能夠獲得參與者B 的簽名。

（2）協(xié)議的及時(shí)性可形式化描述為：

即參與者A 總有一個(gè)策略能夠使得協(xié)議達(dá)到一個(gè)狀態(tài)——參與者A 能夠停止協(xié)議，同時(shí)，如果參與者A 還沒有得到參與者B 的簽名，那么即使參與者B 與TTP 合作也沒有一個(gè)策略使得最終參與者B 獲得參與者A 的簽名而參與者A 卻沒有獲得參與者B 的簽名。

（3）協(xié)議的不可濫用性可形式化描述為：

即參與者B沒有一個(gè)策略能夠使得協(xié)議達(dá)到一個(gè)狀態(tài)——參與者B 有一個(gè)策略能夠獲得參與者A 的簽名，同時(shí)，參與者B 又有一個(gè)策略使得協(xié)議終止，且此時(shí)參與者A沒有一個(gè)策略能夠獲得參與者B 的簽名。

4 使用MOCHA 驗(yàn)證

在對系統(tǒng)的規(guī)范進(jìn)行描述時(shí)，需要為每個(gè)實(shí)體做三件事：定義變量、初始化變量值和更新變量值。定義變量可以方便的使用符號化方式來描述系統(tǒng)規(guī)格和系統(tǒng)狀態(tài)的變遷；初始化變量是為了構(gòu)造系統(tǒng)的初始狀態(tài)；更新變量值是為了模擬系統(tǒng)的運(yùn)行，描述系統(tǒng)的狀態(tài)變遷。變量類型有三種：Private、Interface 和External。Private 是私有變量，只能在實(shí)體內(nèi)部使用；Interface 可以被其他實(shí)體所使用；External 是引用其他實(shí)體所定義的interface 類型的變量。在MOCHA 中，協(xié)議的每一個(gè)動作被描述為：[]守衛(wèi)條件（Guarded）→命令（Command）。守衛(wèi)條件是一個(gè)bool 表達(dá)式，當(dāng)守衛(wèi)條件取值為真時(shí)，則執(zhí)行命令，否則不執(zhí)行命令，命令通常是一個(gè)更新系統(tǒng)狀態(tài)的語句。

在對系統(tǒng)的屬性進(jìn)行描述時(shí)，會用到兩類符號：路徑量詞（path quantifier）和時(shí)態(tài)操作符（temporal operators）。路徑量詞有兩個(gè)：E（Existential，存在）和A（Universal，所有）。時(shí)態(tài)操作符有五個(gè)：N（Next，下一個(gè)時(shí)態(tài)）；F（Eventually，最后）；G（Always，總是）；U（Until，直到）和W（While，當(dāng)……時(shí)）。使用路徑量詞、時(shí)態(tài)操作符和命題就可以組成一個(gè)ATL 公式，如A Gp表示所有可到達(dá)的狀態(tài)都滿足p，A Fp表示所有路徑都包含p狀態(tài)。

為該公平交換協(xié)議定義以下符號：

STOPx：模塊x是否選擇終止協(xié)議；

CHECKmi：消息i是否能夠通過檢查；

SENDmi：消息i是否被發(fā)送。

定義了符號之后，就可以對系統(tǒng)的規(guī)格進(jìn)行建模。在協(xié)議中，參與者A 發(fā)送消息1、3 和5，接收消息2、4 和6。因此，對參與者A 建模如下所示。

（1）參與者A 的初始狀態(tài)為：

STOPa=false；SENDm1=false；SENDm3=false；

SENDm5a=false；CHECKm1=error；CHECKm3=error；

CHECKm5a=error

（2）參與者A 的狀態(tài)轉(zhuǎn)移為：

[]～STOPa& ～SENDm1->SENDm1'：=true；CHECKm1'：=pass

[]～STOPa& ～SENDm1->SENDm1'：=true；CHECKm1'：=error

[]～STOPa& ～SENDm3 & SENDm2 &（CHECKm2=pass）->SENDm3'：=true；CHECKm3'：=pass

[]～STOPa& ～SENDm3 & SENDm2 &（CHECKm2=pass）->SENDm3'：=true；CHECKm3'：=error

[]～STOPa& SENDm2 &（CHECKm2=error）->STOPa'：=true

[]～STOPa& ～SENDm5a& SENDm4 &（CHECKm4=error）->STOPa'：=true；SENDm5a'：=true；CHECKm5a'：=pass

[]～STOPa& ～SENDm5a& SENDm4 &（CHECKm4=error）->STOPa'：=true；SENDm5a'：=true；CHECKm5a'：=error

[]～STOPa& ～SENDm5a& SENDm3 & ～SENDm4->STOPa'：=true；SENDm5a'：=true；CHECKm5a'：=pass

[]～STOPa& ～SENDm5a& SENDm3 & ～SENDm4->STOPa'：=true；SENDm5a'：=true；CHECKm5a'：=error

[]～STOPa& SENDm6->STOPa'：=true

在協(xié)議中，參與者B 發(fā)送消息2、4 和5，接收消息1、3 和7，與參與者A 的行為相似，因此不再贅述。TTP 作為整個(gè)協(xié)議的仲裁方，也參與到協(xié)議的運(yùn)行中，因此也可以把TTP 當(dāng)作協(xié)議的一個(gè)參與者，它發(fā)送消息6 和7，接收消息5。消息5 可能是由參與者A 發(fā)送的，也有可能是參與者B 發(fā)送的，因此使用SENDm5a 和SENDm5b來區(qū)別由參與者A 和參與者B 發(fā)送的消息5。對參與者TTP 建模如下所示。

（1）參與者TTP 的初始狀態(tài)為：

STOPttp'：=false；SENDm6'：=false；SENDm7'：=false

（2）參與者TTP 的狀態(tài)轉(zhuǎn)移為：

[]～STOPttp & ～SENDm6 & ～SENDm7 & SENDm5a&（CHECKm5a=pass）->SENDm6'：=true；SENDm7'：=true

[]～STOPttp & ～SENDm6 & ～SENDm7 & SENDm5b&（CHECKm5b=pass）->SENDm6'：=true；SENDm7'：=true

[]～STOPttp & SENDm5a&（CHECKm5a=error）->STOPttp'：=true

[]～STOPttp & SENDm5b&（CHECKm5b=error）->STOPttp'：=true

接下來，對系統(tǒng)的屬性進(jìn)行建模。首先是公平性，公平性保證參與者A 與參與者B 能夠都獲得對方的簽名，或者都沒有獲得。也就是說，如果協(xié)議滿足公平性，那么不存在這樣一種系統(tǒng)狀態(tài)——在協(xié)議終止的時(shí)候參與者A 簽署了協(xié)議，但是參與者B卻沒有簽署該協(xié)議。因此，可以把協(xié)議出現(xiàn)的不公平的情況描述為：

其中STOPa& STOPb& STOPttp是協(xié)議終止的狀態(tài)，（SENDm3 & CHECKm3=pass）和SENDm7 是參與者A簽署了協(xié)議的兩種情況，（～SENDm4 & ～SENDm6）和（SENDm4 & CHECKm4=error）是參與者B 沒有簽署協(xié)議的兩種情況。

其次是及時(shí)性，及時(shí)性保證在某個(gè)參與者想要終止協(xié)議時(shí)，如果他還沒有獲得對方的簽名，則就算對方與TTP 合作也不能夠使得對方獲得他的簽名而他卻沒辦法獲得對方的簽名，這樣就保證了協(xié)議在被要求終止的時(shí)候能夠在處理完必要工作后及時(shí)的終止，不會出現(xiàn)不公平的現(xiàn)象。也就是說，如果協(xié)議滿足及時(shí)性，那么不存在這樣一種系統(tǒng)狀態(tài)——參與者A 想要終止協(xié)議時(shí)，若參與者B 沒有簽署協(xié)議，那么在未來的狀態(tài)中，會存在參與者A 簽署了協(xié)議而參與者B 卻沒有簽署協(xié)議的狀態(tài)。因此，可以把協(xié)議出現(xiàn)的不及時(shí)的情況描述為：

最后是不可濫用性，不可濫用性保證協(xié)議不會被其參與者所濫用而獲取利益。在公平交換協(xié)議中，所謂濫用是指某個(gè)參與者可以證明他能夠獲得對方的簽名，而且他還有一種策略能夠在獲得對方的簽名后終止協(xié)議，使得對方?jīng)]有辦法來獲得他的簽名，顯然，這也是一種不公平的情況。對于參與者B 來說，他有兩種方式可以拿到參與者A 的簽名而自己卻不簽署協(xié)議。第一種是通過欺騙參與者A，讓參與者A 先簽署協(xié)議，然后參與者B 在收到參與者A 的簽名后終止協(xié)議，這樣就變成了參與者A 簽署了協(xié)議而參與者B 卻沒有簽署該協(xié)議的不公平的情況。第二種是通過欺騙仲裁TTP，使得TTP發(fā)送參與者A 的簽名給參與者B，同時(shí)還要使得TTP 不發(fā)送參與者B 的簽名給參與者A，并終止協(xié)議執(zhí)行。對于第二種情況，如果協(xié)議滿足不可濫用性，那么不存在這樣一種系統(tǒng)狀態(tài)——在參與者B 要求TTP 提供仲裁之后，TTP 僅發(fā)送了消息7 而沒有發(fā)送消息6 并停止了協(xié)議的運(yùn)行。因此，可以把協(xié)議出現(xiàn)的被濫用的情況描述為：

在Windows 7系統(tǒng)平臺上，使用Chrome瀏覽器訪問MOCHA 工具Web 版（http：//mtc.epfl.ch/cgi-bin/mochatrial.cgi）對該協(xié)議進(jìn)行了驗(yàn)證與分析。在理想的情況下，公平交換協(xié)議滿足公平性、及時(shí)性和不可濫用性，因此式（1）、（2）和（3）的驗(yàn)證結(jié)果應(yīng)該都為failed。MOCHA工具驗(yàn)證結(jié)果顯示：式（1）為passed，式（2）和（3）為failed，結(jié)果說明該電子合同簽署協(xié)議不滿足公平性，因此也不滿足不可濫用性，但是能夠滿足及時(shí)性。因此說該電子合同簽署協(xié)議的設(shè)計(jì)是不符合要求的。根據(jù)MOCHA 工具給出的反例可以看到，當(dāng)參與者B 把正確的消息2 發(fā)送給參與者A 之后，此時(shí)，參與者B 處于發(fā)送了消息2 卻沒有收到消息3 的狀態(tài)，根據(jù)協(xié)議，參與者B可以發(fā)起爭端解決協(xié)議。如果參與者B 發(fā)送了一個(gè)錯(cuò)誤的消息5 給TTP，那么，此時(shí)參與者A 由于收到一個(gè)正確的消息2，因此參與者A 會把消息3 發(fā)送給B，而TTP收到了一個(gè)錯(cuò)誤的消息5，因此TTP 會選擇終止協(xié)議。若參與者A 發(fā)送消息3 在先，TTP 終止協(xié)議在后，那么當(dāng)協(xié)議終止時(shí)，只有參與者A 簽署了協(xié)議，而參與者B 卻沒有簽署協(xié)議。因此，這個(gè)電子合同簽署協(xié)議是可能存在不公平的情況的。式（3）驗(yàn)證結(jié)果為failed，因此可以知道TTP 不會有意去幫助參與者B 來謀取利益。但是由于該協(xié)議不滿足公平性，所以仍然會被參與者所利用來獲取不公平的利益，因此不滿足不可濫用性。

5 結(jié)束語

基于ATL，以開放系統(tǒng)的方式來描述公平交換協(xié)議，對公平交換協(xié)議的各參與者之間的博弈關(guān)系進(jìn)行了有效的描述。本文對一個(gè)電子合同簽署協(xié)議的公平性、及時(shí)性和不可濫用性進(jìn)行形式化分析和驗(yàn)證，通過對驗(yàn)證結(jié)果的分析可以得到結(jié)論：該協(xié)議能夠滿足及時(shí)性，但是不滿足公平性和不可濫用性，因此說該電子合同簽署協(xié)議的設(shè)計(jì)是不符合要求的。通過對MOCHA 工具給出的反例的分析，能夠清楚地分析出該協(xié)議不滿足公平性的情況，以確保結(jié)論的正確性。同時(shí)，本文也存在不足之處：所驗(yàn)證的電子合同簽署協(xié)議較為簡單，是僅有兩個(gè)參與者參與的簡單公平交換協(xié)議。

今后，將繼續(xù)研究用本文的方法對復(fù)雜的、多參與者參與的公平交換協(xié)議或其他方面的協(xié)議進(jìn)行形式化分析與驗(yàn)證。同時(shí)，將會對一些較新的領(lǐng)域進(jìn)行研究和探索，如文獻(xiàn)[14-15]把基于ATL 的形式化分析與驗(yàn)證方法應(yīng)用于多參與者參與且具有競爭關(guān)系的隨機(jī)系統(tǒng)（Stochastic Systems）的自動驗(yàn)證技術(shù)上，文獻(xiàn)[16]把基于ATL 的形式化分析與驗(yàn)證方法應(yīng)用于多智能體系統(tǒng)（Multi-agent Systems）的驗(yàn)證技術(shù)上，這些都是未來的工作方向。

[1] 李樺.公平交換協(xié)議研究[D].成都：電子科技大學(xué)，2012.

[2] Alur R，Henzinger T A，Kupferman O.Alternating-time temporal logic[J].Journal of the ACM（JACM），2002，49（5）：672-713.

[3] El-Menshawy M，Bentahar J，Dssouli R.Symbolic model checking commitment protocols using reduction[M]//Declarative Agent Languages and Technologies VIII.Berlin Heidelberg：Springer，2011：185-203.

[4] Bauland M，Mundhenk M，Schneider T，et al.The tractability of model-checking for LTL：The good，the bad，and the ugly fragments[J].Electronic Notes in Theoretical Computer Science，2009，231：277-292.

[5] Alrabaee S，Bataineh A，Khasawneh F A，et al.Using model checking for trivial file transfer protocol validation[C]//Proceedings of International Conference on Communications and Networking（ComNet），2014：1-7.

[6] Armando A，Carbone R，Compagna L.LTL model checking for security protocols[J].Journal of Applied Non-Classical Logics，2009，19（4）：403-429.

[7] Jiang Y，Gong H.Modeling and formal analysis of communication protocols based on game[J].Information Technology Journal，2013，12（3）：470-473.

[8] Jamroga W，Mauw S，Melissen M.Fairness in non-repudiation protocols[M]//Security and Trust Management.Berlin Heidelberg：Springer，2012：122-139.

[9] Zhang Y，Zhang C，Pang J，et al.Game-based verification of multi-party contract signing protocols[M]//Formal Aspects in Security and Trust.Berlin Heidelberg：Springer，2010：186-200.

[10] 李云峰.電子商務(wù)協(xié)議安全性的形式化分析方法研究[D].成都：西南交通大學(xué)，2009.

[11] 張穎.基于博弈的多參與者合同簽署協(xié)議的驗(yàn)證[D].濟(jì)南：山東大學(xué)，2010.

[12] Browne M C，Clarke E M，Grümberg O.Characterizing finite Kripke structures in propositional temporal logic[J].Theoretical Computer Science，1988，59（1）：115-131.

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

[14] Chen T，F(xiàn)orejt V，Kwiatkowska M，et al.Automatic verification of competitive stochastic systems[J].Formal Methods in System Design，2013，43（1）：61-92.

[15] Chen T，F(xiàn)orejt V，Kwiatkowska M，et al.PRISM-games：A model checker for stochastic multi-player games[M]//Tools and Algorithms for the Construction and Analysis of Systems.Berlin Heidelberg：Springer，2013：185-191.

[16] Pilecki J，Bednarczyk M A，Jamroga W.Synthesis and verification of uniform strategies for multi-agent systems[M]//Computational Logic in Multi-Agent Systems.Berlin Herdelberg：Springer，2014：166-182.