Automatic Analysis of Fair Exchange Protocols in TLA

被引：0
作者：
Liu, Nan [1 ]
Xu, Wei [1 ]
Zhu, Yue-fei [1 ]
机构：
[1] Zhengzhou Informat Sci & Technol Inst, Network Engn Dept, Zhengzhou 450002, Henan, Peoples R China
来源：
PROCEEDINGS OF THE SECOND INTERNATIONAL SYMPOSIUM ON ELECTRONIC COMMERCE AND SECURITY, VOL II | 2009年
关键词：
fair exchange protocol; non-repudiation; fairness; automatic analysis; Temporal logic of Action; NON-REPUDIATION PROTOCOLS;
D O I：
10.1109/ISECS.2009.159
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：218 / 221
页数：4
相关论文
共 10 条
[1]  
BELLA G, 2001, THEOREM PROVING HIGH, P3
[2]   Security analysis of efficient (Un-) fair non-repudiation protocols [J].
Gürgens, S ;
Rudolph, C .
FORMAL ASPECTS OF COMPUTING, 2005, 17 (03) :260-276
[3]  
KLAY F, 2008, 5 INT WORKSH FORM AS, P165
[4]   An intensive survey of fair non-repudiation protocols [J].
Kremer, S ;
Markowitch, O ;
Zhou, JY .
COMPUTER COMMUNICATIONS, 2002, 25 (17) :1606-1621
[5]  
KREMER S, 2004, THESIS U LIBRE BRUXE
[6]  
Santiago J, 2007, LECT NOTES COMPUT SC, V4462, P90
[7]   Formal analysis of a non-repudiation protocol [J].
Schneider, S .
11TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP - PROCEEDINGS, 1998, :54-65
[8]  
Zhou J., 1998, P INT REFINEMENT WOR, P370
[9]   An efficient non-repudiation protocol [J].
Zhou, JY ;
Gollmann, D .
10TH COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 1997, :126-132
[10]  
Zhou JY, 2000, LECT NOTES COMPUT SC, V1751, P46
1