Automatic Analysis of Fair Ezchange Protocols in TLA
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.
fair ezchange protocol non-repudiation fairness automatic analysis Temporal logic of Action
Nan Liu Wei Xu Yue-fei Zhu
Network Engineering Department, Zhengzhou Information Science and Technology Institute P.O.Box 1001-770, Zhengzhou, Henan 450002, China
国际会议
Second International Symposium on Electronic Commerce and Security(第二届电子商务与安全国际研究大会)(ISECS 2009)
南昌
英文
874-877
2009-05-22（万方平台首次上网日期，不代表论文的发表时间）