无线认证协议的模型检验分析研究

On the Model Checking of Wireless Authentication Protocols

模型检验作为一种有效的分析和验证手段,在对有线认证协议的形式化分析上已得到了成功的应用,但关于无线认证协议的相关工作目前还比较少。论文应用模型检验方法对D.S.Wong等提出的无线认证协议(Server-specificMAKEP)的安全性进行分析,在分析过程中充分考察了无线环境中移动装置和无线网络的特点,验证结果表明了该方法用于分析无线认证协议的有效性。

As an effective formal analysis and verification method,model checking has been successfully applied to wired authentication protocols.However,there exists much work to do in wireless authentication protocols.In this paper, the security of the wireless authentication protocol（Server-specific MAKEP） is analyzed using model checking.Where the features of mobile device and wireless network in wireless environment are considered.The result shows that our technique is an effective way to analyze wireless authentication protocols.