Formal Analysis of Fair E-Commerce Protocols Based on ATL
基于ATL的公平电子商务协议形式化分析

Aiming at the shortcoming that traditional temporal logic such as LTL,CTL and CTL* regards protocols as close system to analyze, Dr Kremer(2003) proposes an ATL(Alternating-time Temporal Logic) logical method based on game to analyze fair E-commerce protocols, and analyses formally several typical protocols on their fairness and other properties. In this paper, ATL logical and its applications in formal analysis of E-commerce protocols are discussed, and Dr Kremer’ approach is ulteriorly extended to analyze security of protocols besides fairness. Finally, the strict formal analysis is made for ZDB protocol(1999) proposed by Zhou et al. With this new method, as a result there exists 2 possible attacks in the ZDB protocol under non-secrecy channels: leakiness of secret information and reply attacks.