IEEE 802.11i基于Kerberos架构认证的形式化分析

作者：周世健; 张旭辉; 刘炜

来源：中国电子科学研究院学报, 2010, (02): 182-186.

• IEEE 802.11i协议
• Kerberos协议
• 形式化方法
• 串空间模型

形式化方法对安全协议的分析有着无可替代的优势,串空间模型又是众多形式化方法中有良好扩展性的方法之一。利用串空间模型对IEEE 802.11i的认证方式中基于Kerberos架构认证进行了机密性和认证性证明,并得出其安全性可靠的结论。最后也提出了形式化方法的不足之处和未来研究方向。