基于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.