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

Analysis for IEEE 802.11i Based on Kerberos Authentication Framework by Formal Methods

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

Formal methods have irreplaceable advantages for security protocol analysis,and strand space model have good scalability in the large number of formal methods.In this paper,it analyses the confidentiality and authentication of the IEEE 802.11i based on Kerberos authentication by strand space model.And it reaches the conclusions of agreement on security and reliability about protocol.Finally the inadequacies of formal methods and future research directions are also raised.