802.11i认证协议可验安全性形式化分析

摘要

IEEE 802.11标准组提出了802.11i标准以增强无线局域网的安全性能.在802.11i标准中采用了802.1X标准实现无线局域网用户的认证和接入控制过程.针对802.1X认证协议的三方交互结构提出一种扩展Bellare-Rogaway模型,对802.11i认证和密钥交换机制进行可验安全性分析.通过分析,证明802.11i认证协议存在缺陷并给出了相应的中间人攻击方法.