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

计算机工程与应用 ›› 2015, Vol. 51 ›› Issue (19): 32-36.

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

李群，陈清亮

暨南大学计算机科学系，广州 510632

出版日期:2015-09-30 发布日期:2015-10-13

Formal verification of fair exchange protocols based on Alternating-Time Temporal Logic

LI Qun, CHEN Qingliang

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

Online:2015-09-30 Published:2015-10-13

摘要/Abstract

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

关键词: 形式化验证, 交替时态逻辑（ATL）, MOCHA工具, 公平交换协议

Abstract: How to analyze and verify the e-commerce protocols has been a hot research. This paper bases on ATL（Alternating-Time Temporal Logic） to formal analyze and verify the fair exchange protocol, and chooses a electronic contract signing protocol for formal verification. It describes the fair exchange protocol by using the ATL language, and formal model of the fair exchange protocol by using ATS（Alternating Transition Systems）, and verifies the fairness, timeliness and abuse-freeness of the fair exchange protocol effective by using the formal verification tool MOCHA. The paper analyzes and discusses the result of the verification in the end, and finds that this protocol does not satisfy the fairness and abuse-freeness.

Key words: formal verification, Alternating-Time Temporal Logic（ATL）, MOCHA, fair exchange protocol

李群，陈清亮. 基于ATL的公平交换协议的形式化验证[J]. 计算机工程与应用, 2015, 51(19): 32-36.

LI Qun, CHEN Qingliang. Formal verification of fair exchange protocols based on Alternating-Time Temporal Logic[J]. Computer Engineering and Applications, 2015, 51(19): 32-36.

[1]	孙浩然1，2，施智平1，2，3，关永1，3，王瑞2，3. 穿刺机器人运动安全性的形式化分析与建模[J]. 计算机工程与应用, 2018, 54(18): 263-270.
[2]	董玲玲1，关永1，李晓娟1，施智平1，张杰2，华伟1. 用LTL模型检验的方法验证SpaceWire检错机制[J]. 计算机工程与应用, 2012, 48(22): 88-94.
[3]	林基艳，吴振强. 并行分类信任链传递模型[J]. 计算机工程与应用, 2009, 45(31): 98-101.
[4]	高伟^1,2,李飞¹,崔少燕¹. 一种基于BLS签名的优化公平交换协议[J]. 计算机工程与应用, 2008, 44(32): 87-89.
[5]	王金双,杨华兵,张兴元,王元元,张毓森. 电梯控制系统在Isabelle/HOL中的活动性证明[J]. 计算机工程与应用, 2008, 44(27): 216-218.