计算机工程与应用Issue(19)：32-36,5.DOI:10.3778/j.issn.1002-8331.1410-0375
基于ATL的公平交换协议的形式化验证
Formal verification of fair exchange protocols based on Alternating-Time Temporal Logic
摘要
Abstract
How to analyze and verify the e-commerce protocols has been a hot research. This paper bases on ATL(Alter-nating-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.关键词
形式化验证/交替时态逻辑(ATL)/MOCHA工具/公平交换协议Key words
formal verification/Alternating-Time Temporal Logic(ATL)/MOCHA/fair exchange protocol分类
信息技术与安全科学引用本文复制引用
李群,陈清亮..基于ATL的公平交换协议的形式化验证[J].计算机工程与应用,2015,(19):32-36,5.基金项目
国家自然科学基金（No.61003056，No.61272415）；国家重点基础研究发展规划（973）（No.2010CB328103）。 （）
