基于事件逻辑的WMN客户端与LTCA认证协议安全性分析  

Security Analysis of Authentication Protocol of WMN Client and LTCA Based on Logic of Events

作　　者：肖美华[1] 李娅楠[1,2] 宋佳雯 王西忠 李伟 钟小妹[1] Xiao Meihua;Li Yanan;Song Jiawen;Wang Xizhong;Li Wei;Zhong Xiaomei(School of Software,East China Jiaotong University,Nanchang 330013;China Railway Construction Heavy Industry,Changsha 410100)

机构地区：[1]华东交通大学软件学院,南昌330013 [2]中国铁建重工集团有限公司,长沙410100

出　　处：《计算机研究与发展》2019年第6期1275-1289,共15页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61163005,61562026);江西省自然科学基金项目(20161BAB202063);江西省主要学科学术和技术带头人资助计划项目(20172BCB22015)~~

摘　　要：无线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.

关 键 词：事件类 事件逻辑理论 置换规则 强认证性质 WMN客户端与LTCA认证协议 通用性 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术] TN925.93[自动化与计算机技术—计算机科学与技术]