一种验证非否认协议的新方法
doi: 10.3724/SP.J.1146.2006.00384
A New Verification Method for Non-repudiation Protocol
-
摘要: 为了描述非否认协议中的各种不确定因素，在Kailar逻辑系统中引入了表示缺省信息的否定词，以及相应的推理机制。提出了安全协议验证的新方法，主要特点是：可以直接对协议的动态运行过程进行推理；推理具有非单调性；避免过多的理想化假设；可以分析含有多个子协议的非否认协议，以及协议的可追究性和公平性。文中以一种基于离线TTP方式的非否认协议为例，验证了该协议在运行一次时具有可追究性，但多次运行时存在攻击。
-
关键词:
- 非否认协议;Kailar逻辑;协议验证
Abstract: For the description of the nondeterministic factors in the non-repudiation protocols, the Kailar logic system extended with the default negation and the corresponding reasoning mechanism is introduced. The extended system can be used to verify security protocols and it has several main characteristics. Firstly, the method can reason not only for the results but also for the dynamic procedure of the protocol run. Secondly, the reasoning is nonmonotonic. Thirdly, the ideal assumptions of the protocols can be reduced. Fourthly, the accountability and fairness of the security protocols with some sub-protocols can be analyzed. As an example, a non-repudiation protocol with offline TTP was verified. The protocol has accountability during one protocol run and gets the attack in the repeated runs. -
Abadi M, Glew N, and Horne B. Certified email with a light on-line trusted third party: design and implementation [C].Proceedings of the Eleventh International World Wide Web Conference.Honolulu, Hawaii, USA. 2002: 387-395.[2]Abadi M and Blanchet B. Analyzing security protocols with secrecy types and logic programs[J].Journal of the ACM.2005, 52(1):102-146[3]Gurgens S. On the security of fair non-repudiation protocols[J].International Journal of Information Security.2005, 4(4):253-262[4]Kremer S and Markowitch O. Optimistic non-repudiable information exchange[C]. 21st Symp.on Information Theory in the Benelux.Wassenaar. The Netherlands. 2000: 139-149.[5]Kremer S, Markowitch O, and Zhou J. An intensive survey of non-repudiation protocols[J].Computer Communications.2002, 25(17):1606-1621[6]Kailar R. Accountability in electronic commerce protocols[J]. IEEE Trans. on Software Eng. 1996, 22(5): 313-328.[7]周典萃，卿斯汉，周展飞. Kailar逻辑的缺陷. 软件学报. 1999, 10(12): 1238-1245. Zhou Dian-cui, Qing Si-han, and Zhou Zhan-fei. Limitations of Kailar logic. Journal of Software, 1999，10(12): 1238-1245.[8]卿斯汉. 安全协议. 北京：清华大学出版社. 2005: 190-210. Qing Si-han. Security protocols. Beijing: Tsinghua University Press. 2005: 190-210.[9]周典萃，卿斯汉，周展飞. 一种分析电子商务协议的新工具. 软件学报. 2001, 12(9): 1318-1328. Zhou Dian-cui, Qing Si-han, and Zhou Zhan-fei. A new approach for the analys is of electronic commerce protocols. Journal of Software, 2001,12(9): 1318-1328.[10]Li L, Zhang H, and Wang L. An improved non-repudiation protocol and its securty analysis[J].Wuhan University Journal of Natural Sciences.2004, 9(3):288-292 -
点击查看大图
计量
- 文章访问数: 2933
- HTML全文浏览量: 77
- PDF下载量: 738
- 被引次数: 0
下载:
