IEEE 802.11i协议的形式化分析  

Formal analysis of IEEE 802.11i

作　　者：吴开贵[1] 徐成[1] 廖振岚[1] 

机构地区：[1]重庆大学计算机学院,重庆400044

出　　处：《计算机应用》2008年第5期1125-1127,共3页journal of Computer Applications

基　　金：国家自然科学基金资助项目(30400446)

摘　　要：在Furqan提出运用串空间理论对IEEE802.11i协议进行形式化验证的基础上,对IEEE802.11i协议的串空间模型进行了改进,并证明了Furqan没有证明的保密性以及服务器的认证性。分析结果证明,在目前的攻击者模型中,IEEE802.11i协议是安全的。As one of the most representative theorem proving techniques used to analyze security protocols, the strand spaces theory has been successfully applied to prove a plenty of typical protocols. Based on the related document, we improved the Strand Space Model （SSM） of IEEE 802. 11 i protocols, and verified the security and authentication property. The result of the analysis proves the correctness of the IEEE 802. 11 i protocols in the present penetrator model,

关 键 词：IEEE 802.11i协议 串空间 形式化分析 

分 类 号：TP393.04[自动化与计算机技术—计算机应用技术]