Title :
Automatic Analysis of Fair Exchange Protocols in TLA
Author :
Liu, Nan ; Xu, Wei ; Zhu, Yue-Fei
Author_Institution :
Network Eng. Dept., Zhengzhou Inf. Sci. & Technol. Inst., Zhengzhou, China
Abstract :
Fair exchange protocols have been studied intensively in recent years. But a lot of methods are still performed manually. In this paper an automatic method is proposed for analyzing fair exchange protocols. In this method we formalize security properties of fairness and non-repudiation in TLA (temporal logic of action) and define common predicates to make the analysis automatic. An "end" rule is introduced to solve the different type of channels. Protocol of fair Zhou-Gollmann has been analyzed in our own implemented tool and an attack trace can be found.
Keywords :
cryptographic protocols; electronic commerce; temporal logic; fair Zhou-Gollmann protocol; fair exchange protocols; temporal logic of action; Algebra; Automata; Automatic logic units; Electronic commerce; Information analysis; Information science; Information security; Protection; Protocols; Web and internet services; Temporal logic of Action; automatic analysis; fair exchange protocol; fairness; non-repudiation;
Conference_Titel :
Electronic Commerce and Security, 2009. ISECS '09. Second International Symposium on
Conference_Location :
Nanchang
Print_ISBN :
978-0-7695-3643-9
DOI :
10.1109/ISECS.2009.159
