无线通讯的移动性和便捷性促使无线局域网(WLAN)得到越来越广泛的应用，与此同时，各种针对WLAN的攻击不断发生，建立并完善一种面向WLAN的安全标准成为亟待解决的关键问题。本文就这个问题进行形式化的研究分析。 本文以IEEE制定的802.11i安全标准为研究内容，重点对其中用于密钥管理和临时加密密钥生成的四次握手协议进行详细验证，发现该协议面临一种拒绝服务类型的攻击。在他人提出的两种对四次握手协议改进方案的基础上，本文提出了采用数字信封技术的一种全新的改进方案，通过同时使用协商主密钥和公钥加密重要交互参数，保证其后用于数据通信加密的密钥可以正确生成，有效防止拒绝服务攻击，并简化了握手过程以降低网络传输开销。 本文采用了两种基于高级Petri网的形式化验证技术：一种是基于Petri的模型检测技术，给出协议的形式化模型并将待验证的安全性质用时序逻辑公式加以描述，之后运行模型检测工具得到验证结果；另一种在协议的Petri网模型上使用网状态方程推导是否存在不安全的协议状态，若这些状态可达则说明协议可能遭受恶意攻击。通过分析验证结果，可以明确协议产生安全漏洞的根源，并据此提出切实可行的改进措施。 本课题的研究成果为802.11i安全标准的不断完善提供了理论分析依据和有效的改进建议，可促进该协议体系的不断发展。