DocumentCode
3056631
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
Volume
2
fYear
2009
fDate
22-24 May 2009
Firstpage
218
Lastpage
221
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Electronic Commerce and Security, 2009. ISECS '09. Second International Symposium on
Conference_Location
Nanchang
Print_ISBN
978-0-7695-3643-9
Type
conf
DOI
10.1109/ISECS.2009.159
Filename
5209776
Link To Document