Otway-Rees协议改进及形式化证明

doi:10.3969/j.issn.1000-436x.2012.z1.033

Journal on Communications ›› 2012, Vol. 33 ›› Issue (Z1): 250-254.doi: 10.3969/j.issn.1000-436x.2012.z1.033

• Papers • Previous Articles Next Articles

Improvement and formal proof on protocol Otway-Rees

Lai-feng LU¹,Xin-dong DUAN²,Jian-feng MA³

¹ College of Mathematics and Information Science,Shaanxi Normal University,Xi’an 710062,China
² School of Software Nan Yang Institute of Technology,Nanyang 430074,China
³ Ministry of Education Key Laboratory of Computer Networks and Information Security,Xidian University,Xi’an 710071,China

Online:2012-09-25 Published:2017-08-03
Supported by:
The National Natural Science Foundation of China;The Natural Science Foundation of Shaanxi Province;The Natural Science Foundation of Shaanxi Province;The Fundamental Research Funds for the Central Universities;The Fundamental Research Funds for the Central Universities;The Fundamental Research Funds for the Central Universities

Abstract

Abstract:

Choosing the authentication key distribution protocol Otway-Rees as the research object,using protocol composition logic (PCL) as proof tool,the security protocol analysis and formal proof was studied.Firstly,this paper gave the forms of security attack,analyzed the Otway-Rees defects and put forward the amended protocol (named as AOR protocol).Then,PCL was extended.And then PCL was used to describe and prove the behavior of each entity and the safety of the protocol attribute formally.Finally,the conclusion was given that the amended AOR protocol has the security attribute of key confidentiality.

Key words: security protocol, formal methods, protocol composition logic, protocol Otway-Rees

Lai-feng LU,Xin-dong DUAN,Jian-feng MA. Improvement and formal proof on protocol Otway-Rees[J]. Journal on Communications, 2012, 33(Z1): 250-254.

Figures/Tables 4

References 10

[1]	范红, 冯登国 . 安全协议理论与方法[M]. 北京: 科学出版社, 2003. FAN H , FENG D G . Theories and Methods for Security Protocols[M]. Beijing: Science PressPress, 2003.
[2]	卿斯汉 . 安全协议20年研究进展[J]. 软件学报, 2003,14(10): 1740-1752. QING S H . Twenty years development of security protocols research[J]. Journal of Software, 2003,14(10): 1740-1752.
[3]	李建华, 张爱新, 薛质 ,等. 网络安全协议的形式化分析与验证[M]. 北京:机械工业出版社. 2010. LI J H , ZHANG A X , XUE Z ,et al. Formal Analysis and Verification of Network Security Protocols[M]. Beijing:China Machine Press. 2010.
[4]	OTWAY D , REES O . Efficient and timely mutual authentication[J]. Operating Systems Review, 1987,21(1): 8-10.
[5]	DATTA A . Security Analysis of Network Protocol:Compositional Reasoning and Complexity Theoretic Foundations[D]. Computer Science Department,Stanford University,September 2005. 8-72.
[6]	DATTA A , DEREK A , MITCHELL J ,et al. Secure protocol composition[A]. Proceedings of the 2003 ACM workshop on Formal methods in security engineering[C]. 2003. 11-23.
[7]	DURGIN N , MITCHELL J , PAVLOVIC D . A compositional logic for proving security properties of protocols[J]. Journal of Computer Security, 2003,11(4): 677-721.
[8]	ROY A , DATTA A , DEREK A ,et al. Secrecy analysis in protocol composition logic[A]. Advances in Computer Science-ASIAN.2006.Secure Software and Related Issues[C]. 2006. 197-213.
[9]	DATTA A , ROY A , MITCHELL J C ,et al. Protocol composition logic(PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007,172(1): 311-358.
[10]	BURROWS M , ABADI M , NEEDHAM R . A logic of authentication[J]. ACM Transactions on Computer Systems, 1990,8(1): 18-36.

Metrics

Recommended 0

No Suggested Reading articles found!

[1]	Xiang GONG, Tao FENG, Jinze DU. Formal modeling and security analysis method of security protocol based on CPN [J]. Journal on Communications, 2021, 42(9): 240-253.
[2]	Bo MENG,Xudong HE,Jinli ZHANG,Lili YAO,Jintian LU. Security analysis of security protocol Swift implementations based on computational model [J]. Journal on Communications, 2018, 39(9): 178-190.
[3]	Xuefeng LI,Junwei ZHANG,Jianfeng MA. UCAP:a PCL secure user authentication protocol in cloud computing [J]. Journal on Communications, 2018, 39(8): 94-105.
[4]	Wen GU,Ji-hong HAN,Lin YUAN. SSMCI:verification mechanism for security protocols centered on the attacker [J]. Journal on Communications, 2017, 38(10): 175-188.
[5]	Jing YANG,Dan FAN,Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking [J]. Journal on Communications, 2015, 36(Z1): 266-276.
[6]	. Towards session identification using principal behavior for multi-party secure protocol [J]. Journal on Communications, 2015, 36(11): 190-200.
[7]	. Research of platform identity attestation based on trusted chip [J]. Journal on Communications, 2014, 35(8): 13-106.
[8]	Qian-ying ZHANG,Deng-guo FENG,Shi-jun ZHAO. Research of platform identity attestation based on trusted chip [J]. Journal on Communications, 2014, 35(8): 94-106.
[9]	. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 13-116.
[10]	. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 17-154.
[11]	Chun-xiang GU,Huan-xiao WANG,Yong-hui ZHENG,Dan XIN,Nan LIU. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 117-125.
[12]	Zheng-da JIAO,Jian-feng MA,Cong SUN,Qing-song YAO. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 146-153.
[13]	Rong-sen LI,Wen-hua DOU. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 116-125.
[14]	. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 15-125.
[15]	. Analysis and improvement for authentication protocols ofmobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 8-66.

Improvement and formal proof on protocol Otway-Rees

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 4

References 10

Related Articles 15

Metrics

Recommended 0