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

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

单位：华东交通大学软件学院; 江西南昌330013