基于事件逻辑的无线Mesh网络认证协议安全性证明  

Security proof of wireless mesh network authentication protocol based on logic of events

作　　者：李娅楠[1] 肖美华[1] 李伟[1] 梅映天 钟小妹 

机构地区：[1]华东交通大学软件学院,江西南昌330013

出　　处：《计算机工程与科学》2017年第12期2236-2244,共9页Computer Engineering & Science

基　　金：国家自然科学基金(61562026);江西省自然科学基金(20161BAB202063);江西省对外科技合作项目(20151BDH80005);江西省主要学科学术和技术带头人资助计划(2017BCB22015)

摘　　要：无线Mesh网络是一种结合无线局域网和移动自组织网络的新型多跳网络,无线网络的开放性和资源受限性使得无线网络容易遭受重放、伪装等攻击。事件逻辑是一种描述并发与分布式系统中状态迁移和算法的形式化方法,可用于证明网络协议的安全性。以事件逻辑为基础提出一系列性质,其中包含多组合信息交互、不叠加、事件匹配、去重复、去未来,以降低协议分析过程中的冗余度以及复杂度,提高协议分析效率。对无线Mesh网络客户端双向认证协议进行分析,证明该协议能够抵抗中间人发起的重放攻击,无线Mesh客户端双向认证协议是安全的。此理论适用于类似复杂无线网络协议形式化分析。Wireless mesh networks are a combination of wireless local area network （LAN） and mo- bile ad hoc network, and they are of a new multi-hop network structure. The openness of wireless net- works and the limitation of resources make wireless networks vulnerable to replay attack, impersonation attack, and so on. Logic of events is a formal method to describe the protocol state transition and algo- rithm in concurrent and distributed systems, which can be used to prove the security of network proto- cols. Based on the logic of events, we propose a series of properties that include multiple combinations of information interaction, no stacking, event matching, dereplication and remove future. We utilize these rules to reduce the redundancy and complexity of the protocol validation process, and improve pro- tocol analysis efficiency. We study the bidirectional authentication protocol of wireless Mesh network clients, and conclude that the protocol can resist man-in-the-middle replay attacks. The mesh protocol is proved secure. The logic of events can be applied to the formal analysis and verification of similar complex wireless network protocols.

关 键 词：形式化方法 事件逻辑 无线Mesh网络认证协议 中间人攻击 

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