李 群，陳清亮

LI Qun,CHEN Qingliang

暨南大學 計算機科學系，廣州510632

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

1 引言

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

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

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

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

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

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

本文采用基于ATL 的方法，對于電子商務(wù)協(xié)議中廣泛應(yīng)用的公平交換協(xié)議進行形式化分析與驗證。與文獻[3-6]相比較，文獻[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é)議的缺點，更好地描述協(xié)議各參與者之間的合作與競爭關(guān)系。與文獻[7-11]相比較，文獻[7-11]只片面關(guān)注協(xié)議的某一些屬性，并對其進行分析與驗證，而本文則將基于ATL 的形式化分析與驗證方法具體應(yīng)用到使用更為廣泛的公平交換協(xié)議，并且對公平交換協(xié)議的公平性、及時性和不可濫用性進行了全面的分析和有效的驗證，同時，本文的建模方式也更易于理解。

2 ATL 基礎(chǔ)

ATL 是用來描述交互式開放系統(tǒng)的規(guī)格和屬性的時態(tài)邏輯。ATL 的定義是關(guān)于一個有限命題集合Π和一個有限參與者集合Σ={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)所能達到的狀態(tài)；○（next，下一個狀態(tài)），□（always，總是），U（until，直到）是標準的時態(tài)操作符。通常，用＜＜A＞＞◇?來表示＜＜A＞＞tr ueU?。

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

Π是命題集合；

Σ是參與者集合；

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

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

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

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

3 形式化建模

本文使用ATL 來驗證一個電子合同簽署協(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é)議運行結(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é)議。

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

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

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

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

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

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

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

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

4 使用MOCHA 驗證

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

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

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

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

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

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

定義了符號之后，就可以對系統(tǒng)的規(guī)格進行建模。在協(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 作為整個協(xié)議的仲裁方，也參與到協(xié)議的運行中，因此也可以把TTP 當作協(xié)議的一個參與者，它發(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)的屬性進行建模。首先是公平性，公平性保證參與者A 與參與者B 能夠都獲得對方的簽名，或者都沒有獲得。也就是說，如果協(xié)議滿足公平性，那么不存在這樣一種系統(tǒng)狀態(tài)——在協(xié)議終止的時候參與者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é)議的兩種情況。

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

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

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

5 結(jié)束語

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

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

[1] 李樺.公平交換協(xié)議研究[D].成都：電子科技大學，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].成都：西南交通大學，2009.

[11] 張穎.基于博弈的多參與者合同簽署協(xié)議的驗證[D].濟南：山東大學，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] 王芷玲，張玉清，楊波.一個公平電子合同簽署協(xié)議的設(shè)計[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.