基于ATL 的公平交換協議的形式化驗證

李 群，陳清亮

LI Qun,CHEN Qingliang

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

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

1 引言

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

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

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

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

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

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

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

2 ATL 基礎

ATL 是用來描述交互式開放系統的規格和屬性的時態邏輯。ATL 的定義是關于一個有限命題集合Π和一個有限參與者集合Σ={1,2,…,k}的命題邏輯，它的公式定義如下：

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

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

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

其中A?Σ；?、?1和?2是公式；＜＜＞＞是路徑量詞，＜＜A＞＞表示聯合A，系統所能達到的狀態；○（next，下一個狀態），□（always，總是），U（until，直到）是標準的時態操作符。通常，用＜＜A＞＞◇?來表示＜＜A＞＞tr ueU?。

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

Π是命題集合；

Σ是參與者集合；

Q是狀態集合；

Q0?Q是初始狀態集合；

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

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

3 形式化建模

本文使用ATL 來驗證一個電子合同簽署協議[13]，協議的形式化描述如下所示。

主協議：

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

爭端解決協議：

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

協議執行過程說明如下：

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

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

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

（4）A 收到MS4 后，檢查MS4 是否正確，如果正確，則協議運行結束；否則A 選擇發起爭端解決協議。

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

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

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

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

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

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

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

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

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

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

4 使用MOCHA 驗證

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

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

為該公平交換協議定義以下符號：

STOPx：模塊x是否選擇終止協議；

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

SENDmi：消息i是否被發送。

定義了符號之后，就可以對系統的規格進行建模。在協議中，參與者A 發送消息1、3 和5，接收消息2、4 和6。因此，對參與者A 建模如下所示。

（1）參與者A 的初始狀態為：

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

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

CHECKm5a=error

（2）參與者A 的狀態轉移為：

[]～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

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

（1）參與者TTP 的初始狀態為：

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

（2）參與者TTP 的狀態轉移為：

[]～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

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

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

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

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

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

5 結束語

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

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

[1] 李樺.公平交換協議研究[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] 李云峰.電子商務協議安全性的形式化分析方法研究[D].成都：西南交通大學，2009.

[11] 張穎.基于博弈的多參與者合同簽署協議的驗證[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] 王芷玲，張玉清，楊波.一個公平電子合同簽署協議的設計[J].計算機工程，2006，32（19）：159-161.

[14] Chen T，Forejt 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，Forejt 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.