无线局域网IEEE802.11认证协议的模型检测

摘要

无线局域网的安全性在无线技术中处于非常重要的地位，当IEEE802.11在被制定的时候，协议标准就着重的提出了开放式认证和共享密钥(WEP)认证来补充安全性方面的问题。通过认证协议可以使无线局域网连接更加安全和稳定，而作为新一代的安全标准IEEE802.11i提出了四次握手协议来对密钥进行管理和分配，弥补了共享密钥认证协议中密钥管理上的空白。 本文通过模型检测的方法来对协议进行模拟和检测。模型检测是关于自动验证并行或者分布式系统性质的算法和方法。它的重点和难点在于形式化建模。首先在传统的建模方式的基础上，根据认证协议的特点定义内部事件和外部事件状态模型的概念。在开始建立协议系统模型时，利用概念来形式化出SPIN工具需要的模型。其次，对共享密钥认证协议进行模型检测实验。实验结果表明了共享密钥认证协议具有很大的漏洞。根据实际中的传输情况，针对密钥上的缺陷对密钥管理中四次握手协议进行模型检测，找出协议在特定环境中的性质缺陷。最后通过2个模型检测的实验来对无线局域网IEEE802.11安全性进行分析和总结。 模型检测认证协议能帮助分析和理解协议标准，并通过协议的性质来检测协议标准中的错误。通过本文模型检测实验得到的共享密钥认证协议漏洞，可以证明共享密钥认证协议具有很大的缺陷，并不适合高安全性要求的无线局域网，同时也证明了四次握手协议对于改善密钥管理具有很大的帮助。虽然如此，四次握手协议在密钥传送中具有的性质缺陷也会影响到协议的安全性。本文的实验结论可以作为改进IEEE802.11认证协议的理论参考。

目录

文摘

英文文摘

论文说明：图表目录

声明

第1章绪论

1.1 IEEE802.11标准概述

1.2模型检测理论研究背景

1.3网络协议模型检测国内外研究现状

1.4论文主要内容

第2章 IEEE802.11认证协议

2.1 IEEE802.11WEP认证协议概述

2.1.1无线局域网网络结构

2.1.2 WEP认证协议

2.2 IEEE802.11I认证协议概述

2.2.1 802.11i的体系架构

2.2.2 IEEE802.11x的认证协议

2.2.3密钥管理和加密机制

2.3 小结

第3章协议的模型检测方法

3.1模型检测理论和系统建模方法

3.1.1模型检测理论

3.1.2系统建模方法

3.2协议状态模型化方法

3.3模型检测工具

3.3.1模型检测工具概述

3.3.2 SPIN模型检测工具

3.4小结

第4章 WEP认证协议的模型检测

4.1 WEP认证协议建模

4.1.1 WEP认证协议的帧格式

4.1.2 WEP认证协议过程

4.1.3 WEP认证协议状态模型

4.1.4 WEP认证协议的进程化语言模型

4.2 WEP认证协议模型性质分析和SPIN工具验证

4.2.1 WEP认证协议模型性质分析

4.2.2 SPIN工具验证

4.3 WEP认证协议的模型检测实验分析

4.4 小结

第5章四次握手协议的模型检测

5.1四次握手协议建模

5.1.1四次握手协议的帧格式

5.1.2四次握手协议具体过程

5.1.3四次握手协议状态模型

5.1.4四次握手协议的进程化语言模型

5.2四次握手协议模型性质分析和SPIN工具验证

5.2.1四次握手协议模型性质分析

5.2.2 SPIN工具的模型检验和性质验证

5.3四次握手协议的模型检测实验分析

5.4小结

总结

参考文献

致谢

附录A 攻读学位期间所发表的学术论文目录