基于ATL的公平交换协议的形式化验证.pdf

32 2015，51(19) ComputerEngineeringandApplications~t算机工程与应用 @理论研 究、研发设计◎ 基于ATL的公平交换协议的形式化验证 李 群，陈清亮 LIQun，CHENQingliang 暨南大学 计算机科学系，广州 510632 DepartmentofComputerScience，JinanUniversity，Guangzhou510632，China LIQun，CHENQingliang．FormalverificationoffairexchangeprotocolsbasedonAlternating-TimeTemporal Logic．ComputerEngineeringandApplications，2015，51(19)：32-36． Abstract：How toanalyzeandverifythee—commerceprotocolshasbeenahotresearch．ThispaperbasesonATL(Alter— nating—TimeTemporalLogic)toformalanalyzeandverifythefairexchangeprotocol，andchoosesaelectroniccontract signingprotocolforformalverification．ItdescribesthefairexchangeprotocolbyusingtheATL language．andformal modelofthefairexchangeprotocolbyusingATS(AltematingTransitionSystems)，andverifiesthefairness，timeliness andabuse-~eenessofthefairexchangeprotocoleffectivebyusingtheformalverificationtoolMOCHA．Thepaperanalyzes anddiscussestheresultoftheverification intheend，and findsthatthisprotocoldoesnotsatisfy thefairnessand abuse．freeness． Keywords：formalverification；Alternating—TimeTemporalLogic(ATL)；MOCHA；fairexchangeprotocol 摘 要：如何对电子商务协议进行分析与验证一直是研究的热点，基于ATL(交替时态逻辑)对 电子商务协议 中的公 平交换协议 (FairExchangeProtocols)进行形式化分析与验证 ，并选取 了其中的一个电子合 同签署协议进行形式化 验证。用ATL语言来形式化描述公平交换协议，并使用ATS(AlternatingTransitionSystems，交替转移系统)来为公 平交换协议进行形式化建模，再用形式化验证工具MOCHA对公平 交换协议的公平性 (Fairness)、及时性 (Timeli— ness)和不可滥用性 (Abuse．Freeness)进行有效的验证；对验证结果进行分析与讨论 ，发现 了该协议不满足公平性和 不可滥用性 ，不符合设计 的要求。 关键词 ：形式化验证；交替时态逻辑(ATL)；MOCHA工具；公平交换协议 文献标志码：A 中图分类号 ：TP301．2 doi：10．37788．issn．1002．8331．1410．0375 1 引言 换的各方能够公平的获得各 自想要的利益 ，也就是说 ， 电子商务是一种各个参与者通过计算机和Internet 在完成交换后，进行交换的各方要么都获得各 自想要的 技术来实现交易的业务 ，人们可以通过电子商务的形 利益 ，要么都不获得这些利益”。 式，实现商品或服务的交换。电子商务以Internet技术 公平交换协议的应用是实现公平交换的关键。所 为支撑 ，突破了时间和地域的限制 ，以一种便捷、廉价和 谓公平交换协议是指在正常情况下完成了协议之后，参 自由的方式得到了广泛应用。随着 Internet技术的发 加协议的各方都能够得到各 自期望的利益 ；非正常情况 展 ，电子商务已经成为了当代经济活动的主要形式之