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

摘要：

如何对电子商务协议进行分析与验证一直是研究的热点，基于ATL（交替时态逻辑）对电子商务协议中的公平交换协议（Fair Exchange Protocols）进行形式化分析与验证，并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议，并使用ATS（Alternating Transition Systems，交替转移系统）来为公平交换协议进行形式化建模，再用形式化验证工具MOCHA对公平交换协议的公平性（Fairness）、及时性（Timeli-ness）和不可滥用性（Abuse-Freeness）进行有效的验证；对验证结果进行分析与讨论，发现了该协议不满足公平性和不可滥用性，不符合设计的要求。

关键词：形式化验证、交替时态逻辑(ATL)、MOCHA工具、公平交换协议

分类号：TP301.2(计算技术、计算机技术)

资助基金：国家自然科学基金No.61003056，No.61272415；国家重点基础研究发展规划973No.2010CB328103。

在线出版日期：2015-10-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：32-36