无线局域网的安全性在无线技术中处于非常重要的地位,当IEEE802.11在被制定的时候,协议标准就着重的提出了开放式认证和共享密钥(WEP)认证来补充安全性方面的问题。通过认证协议可以使无线局域网连接更加安全和稳定,而作为新一代的安全标准IEEE802.11i提出了四次握手协议来对密钥进行管理和分配,弥补了共享密钥认证协议中密钥管理上的空白。本文通过模型检测的方法来对协议进行模拟和检测。模型检测是关于自动验证并行或者分布式系统性质的算法和方法。它的重点和难点在于形式化建模。首先在传统的建模方式的基础上,根据认证协议的特点定义内部事件和外部事件状态模型的概念。在开始建立协议系统模型时,利用概念来形式化出SPIN工具需要的模型。其次,对共享密钥认证协议进行模型检测实验。实验结果表明了共享密钥认证协议具有很大的漏洞。根据实际中的传输情况,针对密钥上的缺陷对密钥管理中四次握手协议进行模型检测,找出协议在特定环境中的性质缺陷。最后通过2个模型检测的实验来对无线局域网IEEE802.11安全性进行分析和总结。模型检测认证协议能帮助分析和理解协议标准,并通过协议的性质来检测协议标准中的错误。通过本文模型检测实验得到的共享密钥认证协议漏洞,可以证明共享密钥认证协议具有很大的缺陷,并不适合高安全性要求的无线局域网,同时也证明了四次握手协议对于改善密钥管理具有很大的帮助。虽然如此,四次握手协议在密钥传送中具有的性质缺陷也会影响到协议的安全性。本文的实验结论可以作为改进IEEE802.11认证协议的理论参考。