随着无线网络的普及和应用,人们对无线网络的依赖程度越来越高。尤其是作为下一代无线网络的WLAN Mesh网络,以其容量较高,迅速部署,逐步投资等优势正成为人们关注的焦点。而无线网络传输媒体的开放性、无线终端的移动性和网络拓扑结构的动态性,使得无线网络更容易被攻破。在WLAN Mesh网络环境中,安全的接入网络并在实体之间安全地建立会话密钥是认证密钥协商协议所要解决的核心问题,是安全通信的基础,也是网络安全的基础,但其设计分析及其复杂,并具有挑战性。因此,安全协议的形式化分析和证明对于安全协议的设计和分析至关重要,而由A.Datta等提出的DDMP组合理论是协议设计与安全性分析方面的最新理论成果,它包括协议演绎系统(PDS)和协议组合逻辑(PCL)。我们着眼于认证密钥协商协议中的这些焦点问题,提出了一种基于协议组合逻辑安全的认证密钥协商方案。本文对协议的形式化设计与方法进行了比较深入的研究,首先利用形式化方法对WMEN认证密钥协商方案SKE进行形式化分析,发现SKE协议存在KCI攻击和交错攻击。基于BDH困难问题,借鉴基于身份的密钥协商的思想提出了一种新的WMEN安全认证密钥协商协议,最后使用形式化方法对新协议进行正确性和安全性证明。同时对新方案与相关方案进行分析对比,新方案更加安全和高效。