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

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