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

无线Mesh网络是一种结合无线局域网和移动自组织网络的新型多跳网络,无线网络的开放性和资源受限性使得无线网络容易遭受重放、伪装等攻击。事件逻辑是一种描述并发与分布式系统中状态迁移和算法的形式化方法,可用于证明网络协议的安全性。以事件逻辑为基础提出一系列性质,其中包含多组合信息交互、不叠加、事件匹配、去重复、去未来,以降低协议分析过程中的冗余度以及复杂度,提高协议分析效率。对无线Mesh网络客户端双向认证协议进行分析,证明该协议能够抵抗中间人发起的重放攻击,无线Mesh客户端双向认证协议是安全的。此理论适用于类似复杂无线网络协议形式化分析。

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

Wireless mesh networks are a combination of wireless local area network (LAN) and mobile ad hoc network, and they are of a new multi-hop network structure. The openness of wireless networks 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 algorithm in concurrent and distributed systems, which can be used to prove the security of network protocols. 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 protocol 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.