Formal Analysis of Fair E-Commerce Protocols Based on ATL
Wen Jing-Hua①②③; Li Xiang①; Zhang Huan-guo②; Liang Min③; Zhang Mei③
①Institute of Software and Theory, Guizhou University, Guiyang 550025, China; ②School of Computer, Wuhan University, Wuhan 430072, China;③Information Institute, Guizhou Financial Institute, Guiyang 550004, China
Abstract：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.
2007, Vol. 29 
