基于事件逻辑的WMN客户端与LTCA认证协议安全性分析
|
摘要
无线Mesh网络是一种新型的宽带无线网络结构,融合无线局域网与点对点模式两者的优势,是无线网络研究的热点之一.基于事件逻辑理论,结合事件结构、事件类、公理簇以及随机数引理,提出置换规则保证用户交互信息在性质置换过程中的等价转换.通过事件逻辑构建客户端与LTCA认证协议的基本序列,对协议交互动作进行形式化描述并证明协议强认证性质.在合理假设下,无线Mesh网络客户端与LTCA间认证协议的安全性得证,研究表明事件逻辑理论不仅可以论证无线网络协议的安全属性,还能对安全协议不同身份主体间的认证性进行证明.通过流程图简化协议形式化证明步骤,阐述事件逻辑理论证明协议安全属性过程,比较分析事件逻辑理论与其他逻辑推理方法,表明事件逻辑理论具有通用性.
Wireless mesh network is a new type of broadband wireless network structure, which combines the advantages of wireless local area network and ad-hoc network. The research on wireless mesh network is one of the emerging research focuses about wireless networks. Based on the logic of events, the substitution rule is proposed to ensure the equivalent conversion of user interaction information in the process of property substitution by combining event structures, event classes, axiom clusters and random number lemma. With the basic sequences of authentication protocol between client and LTCA constructed by logic of events, the protocol actions between client and LTCA are formally described, and strong authentication property of the protocol is proved. Under reasonable assumptions, the security property of the authentication protocol between WMN client and LTCA is verified, and the research shows that both the security attributes of wireless network protocols and the authentication property between different principals of cryptographic protocols can be proved by logic of events. By simplifying the formal proof steps with flow chart, the process of logic of events proving protocol's security property is described, similarly, by comparing and analyzing logic of events with other logical reasoning methods, the universal applicability of logic of events is shown.
Wireless mesh network is a new type of broadband wireless network structure, which combines the advantages of wireless local area network and ad-hoc network. The research on wireless mesh network is one of the emerging research focuses about wireless networks. Based on the logic of events, the substitution rule is proposed to ensure the equivalent conversion of user interaction information in the process of property substitution by combining event structures, event classes, axiom clusters and random number lemma. With the basic sequences of authentication protocol between client and LTCA constructed by logic of events, the protocol actions between client and LTCA are formally described, and strong authentication property of the protocol is proved. Under reasonable assumptions, the security property of the authentication protocol between WMN client and LTCA is verified, and the research shows that both the security attributes of wireless network protocols and the authentication property between different principals of cryptographic protocols can be proved by logic of events. By simplifying the formal proof steps with flow chart, the process of logic of events proving protocol's security property is described, similarly, by comparing and analyzing logic of events with other logical reasoning methods, the universal applicability of logic of events is shown.
引文
[1]Lu Laifeng.Study on theory and applications of security protocols formal analysis[D].Xian:Xidian University,2012 (in Chinese)(鲁来凤.安全协议形式化分析理论与应用研究[D].西安:西安电子科技大学,2012)
[2]Xu Yiyun.The analysis and detection attack and tactics[J].Network Security Technology & Application,2011(2):14- 15 (in Chinese)(许奕芸.黑客入侵技术的分析和检测[J].网络安全技术与应用,2011(2):14- 15)
[3]Liu Zhongqiang,Yu Chengli.Starting from Wannacry blackmail virus,this paper explores the security defense strategy of computer viruses in LAN [J].Secret Science and Technology,2017(6):18- 21 (in Chinese)(刘中强,于成丽.从Wannacry勒索病毒着手探究局域网内计算机病毒的安全防御策略[J].保密科学技术,2017(6):18- 21)
[4]Chen Xingyue.Cybersecurity capability construction:Coordination of consciousness,management and technology -thoughts triggered by the “eternal blue” event[J].Journal of Information Security Reserach,2017,3(8):765- 768 (in Chinese)(陈兴跃.网络安全能力建设:意识、管理和技术的协同——“永恒之蓝”勒索蠕虫爆发事件引发的思考[J].信息安全研究,2017,3(8):765- 768)
[5]Zhang Weipeng.Research on attack techniques in wireless mesh network [D].Xian:Xidian University,2014 (in Chinese)(张威鹏.无线Mesh网络攻击技术研究[D].西安:西安电子科技大学,2014)
[6]Sharma P K,Mahajan R,Surender.A security architecture for attacks detection and authentication in wireless mesh networks[J].Cluster Computing,2017,20(3):2323- 2332
[7]Ji Qingguang,Feng Dengguo.Towards analyzing some kinds of critically formal models for network security protocols[J].Chinese Journal of Computers,2005,28(7):1071- 1083 (in Chinese)(季庆光,冯登国.对几类重要网络安全协议形式模型的分析[J].计算机学报,2005,28(7):1071- 1083)
[8]Guo Ping.Research on authentication architecture and related technologies of wireless networks [D].Nanjing:Nanjing University of Science and Technology,2012 (in Chinese)(郭萍.无线网络认证体系结构及相关技术研究[D].南京:南京理工大学,2012)
[9]Liu Xinqian.Formal analysis of provable network security protocol based on logic of events[D].Nanchang:East China Jiaotong University,2016 (in Chinese)(刘欣倩.基于事件逻辑的可证明网络安全协议形式化分析[D].南昌:华东交通大学,2016)
[10]Xiao Meihua,Liu Xinqian,Li Yanan,et al.Security certification of three-party network protocols based on strong authentication theory[J].Journal of Frontiers of Computer Science and Technology,2016,10(12):1701- 1710 (in Chinese)(肖美华,刘欣倩,李娅楠,等.基于强认证理论的三方网络协议安全性证明[J].计算机科学与探索,2016,10(12):1701- 1710)
[11]Bickford M.Unguessable Atoms:A logical foundation for security[C] //Proc of the 2nd Int Conf on Verified Software:Theories,Tools,Experiments.Berlin:Springer,2008:30- 53
[12]Xiao Meihua.Proving authentication property of modified needham-schroeder protocol with logic of events[C] //Proc of Int Conf on Computer Information Systems and Industrial Applications.Paris:Atlantis,2015:379- 384
[13]Xiao Meihua,Ma Chenglin,Deng Chunyan.A novel approach to automatic security protocol analysis based on authentication event logic[J].Chinese Journal of Electronics,2015,24(1):187- 192
[14]Bickford M.Automated proof of authentication protocols in a logic of events[C] //Proc of Int Joint Conf on All Aspects of Automated Reasoning.Berlin:Springer,2010:13- 30
[15]Constable R,Bickford M.Intuitionistic completeness of first-order logic[J].Annals of Pure & Applied Logic,2011,165(1):164- 198
[16]Tan Yongzhou.Research on authentication protocol of wireless mesh networks based on lightweight CA[D].Xiangtan,Hunan:Hunan University of Science and Technology,2015 (in Chinese)(谭永洲.基于轻量级CA的无线Mesh网络认证研究[D].湖南湘潭:湖南科技大学,2015)
[17]Guo Ping,Fu Desheng,Zhu Jiezhong,et al.Scheme of lite and tolerant certification authority for wireless mesh network[J].Computer Science,2013,40(12):200- 204 (in Chinese)(郭萍,傅德胜,朱节中,等.无线Mesh网络轻量级容侵CA方案[J].计算机科学,2013,40(12):200- 204)
[18]Liu Xinqian,Xiao Meihua,Cheng Daolei,et al.Proving security properties of modified needham-schroeder protocol based on logic of event[J].Computer Engineering and Science,2015,37(10):1850- 1855 (in Chinese)(刘欣倩,肖美华,程道雷,等.基于事件逻辑理论的改进Needham-Schroeder协议安全性证明[J].计算机工程与科学,2015,37(10):1850- 1855)
[19]Li Yanan,Xiao Meihua.Li Wei,et al.Security certification of the authentication protocol of wireless mesh networks based on logic of events[J].Computer Engineering and Science,2017,39(12):2236- 2244 (in Chinese)(李娅楠,肖美华,李伟,等.基于事件逻辑的无线Mesh网络认证协议安全性证明[J].计算机工程与科学,2017,39(12):2236- 2244)
[20]Mei Chong.Research on security protocol analysis and checking based on Petri nets[D].Guiyang:Guizhou University,2008 (in Chinese)(梅翀.基于Petri网的安全协议分析与检测方法的研究[D].贵阳:贵州大学,2008)
[21]Zhang Xiaohong.The research of automatic validation algorithm for security protocols based on formal methods[D].Changsha:Hunan University,2010 (in Chinese)(张孝红.基于形式化方法的安全协议自动化验证算法的研究[D].长沙:湖南大学,2010)
[2]Xu Yiyun.The analysis and detection attack and tactics[J].Network Security Technology & Application,2011(2):14- 15 (in Chinese)(许奕芸.黑客入侵技术的分析和检测[J].网络安全技术与应用,2011(2):14- 15)
[3]Liu Zhongqiang,Yu Chengli.Starting from Wannacry blackmail virus,this paper explores the security defense strategy of computer viruses in LAN [J].Secret Science and Technology,2017(6):18- 21 (in Chinese)(刘中强,于成丽.从Wannacry勒索病毒着手探究局域网内计算机病毒的安全防御策略[J].保密科学技术,2017(6):18- 21)
[4]Chen Xingyue.Cybersecurity capability construction:Coordination of consciousness,management and technology -thoughts triggered by the “eternal blue” event[J].Journal of Information Security Reserach,2017,3(8):765- 768 (in Chinese)(陈兴跃.网络安全能力建设:意识、管理和技术的协同——“永恒之蓝”勒索蠕虫爆发事件引发的思考[J].信息安全研究,2017,3(8):765- 768)
[5]Zhang Weipeng.Research on attack techniques in wireless mesh network [D].Xian:Xidian University,2014 (in Chinese)(张威鹏.无线Mesh网络攻击技术研究[D].西安:西安电子科技大学,2014)
[6]Sharma P K,Mahajan R,Surender.A security architecture for attacks detection and authentication in wireless mesh networks[J].Cluster Computing,2017,20(3):2323- 2332
[7]Ji Qingguang,Feng Dengguo.Towards analyzing some kinds of critically formal models for network security protocols[J].Chinese Journal of Computers,2005,28(7):1071- 1083 (in Chinese)(季庆光,冯登国.对几类重要网络安全协议形式模型的分析[J].计算机学报,2005,28(7):1071- 1083)
[8]Guo Ping.Research on authentication architecture and related technologies of wireless networks [D].Nanjing:Nanjing University of Science and Technology,2012 (in Chinese)(郭萍.无线网络认证体系结构及相关技术研究[D].南京:南京理工大学,2012)
[9]Liu Xinqian.Formal analysis of provable network security protocol based on logic of events[D].Nanchang:East China Jiaotong University,2016 (in Chinese)(刘欣倩.基于事件逻辑的可证明网络安全协议形式化分析[D].南昌:华东交通大学,2016)
[10]Xiao Meihua,Liu Xinqian,Li Yanan,et al.Security certification of three-party network protocols based on strong authentication theory[J].Journal of Frontiers of Computer Science and Technology,2016,10(12):1701- 1710 (in Chinese)(肖美华,刘欣倩,李娅楠,等.基于强认证理论的三方网络协议安全性证明[J].计算机科学与探索,2016,10(12):1701- 1710)
[11]Bickford M.Unguessable Atoms:A logical foundation for security[C] //Proc of the 2nd Int Conf on Verified Software:Theories,Tools,Experiments.Berlin:Springer,2008:30- 53
[12]Xiao Meihua.Proving authentication property of modified needham-schroeder protocol with logic of events[C] //Proc of Int Conf on Computer Information Systems and Industrial Applications.Paris:Atlantis,2015:379- 384
[13]Xiao Meihua,Ma Chenglin,Deng Chunyan.A novel approach to automatic security protocol analysis based on authentication event logic[J].Chinese Journal of Electronics,2015,24(1):187- 192
[14]Bickford M.Automated proof of authentication protocols in a logic of events[C] //Proc of Int Joint Conf on All Aspects of Automated Reasoning.Berlin:Springer,2010:13- 30
[15]Constable R,Bickford M.Intuitionistic completeness of first-order logic[J].Annals of Pure & Applied Logic,2011,165(1):164- 198
[16]Tan Yongzhou.Research on authentication protocol of wireless mesh networks based on lightweight CA[D].Xiangtan,Hunan:Hunan University of Science and Technology,2015 (in Chinese)(谭永洲.基于轻量级CA的无线Mesh网络认证研究[D].湖南湘潭:湖南科技大学,2015)
[17]Guo Ping,Fu Desheng,Zhu Jiezhong,et al.Scheme of lite and tolerant certification authority for wireless mesh network[J].Computer Science,2013,40(12):200- 204 (in Chinese)(郭萍,傅德胜,朱节中,等.无线Mesh网络轻量级容侵CA方案[J].计算机科学,2013,40(12):200- 204)
[18]Liu Xinqian,Xiao Meihua,Cheng Daolei,et al.Proving security properties of modified needham-schroeder protocol based on logic of event[J].Computer Engineering and Science,2015,37(10):1850- 1855 (in Chinese)(刘欣倩,肖美华,程道雷,等.基于事件逻辑理论的改进Needham-Schroeder协议安全性证明[J].计算机工程与科学,2015,37(10):1850- 1855)
[19]Li Yanan,Xiao Meihua.Li Wei,et al.Security certification of the authentication protocol of wireless mesh networks based on logic of events[J].Computer Engineering and Science,2017,39(12):2236- 2244 (in Chinese)(李娅楠,肖美华,李伟,等.基于事件逻辑的无线Mesh网络认证协议安全性证明[J].计算机工程与科学,2017,39(12):2236- 2244)
[20]Mei Chong.Research on security protocol analysis and checking based on Petri nets[D].Guiyang:Guizhou University,2008 (in Chinese)(梅翀.基于Petri网的安全协议分析与检测方法的研究[D].贵阳:贵州大学,2008)
[21]Zhang Xiaohong.The research of automatic validation algorithm for security protocols based on formal methods[D].Changsha:Hunan University,2010 (in Chinese)(张孝红.基于形式化方法的安全协议自动化验证算法的研究[D].长沙:湖南大学,2010)