IEEE802.11中WEP认证协议的SPIN模型检测  

Model checking of WEP protocol via SPIN in IEEE802.11

作　　者：金秀[1] 张大方[1] 缪力[2] 

机构地区：[1]湖南大学计算机与通信学院,湖南长沙410082 [2]湖南大学软件学院,湖南长沙410082

出　　处：《计算机工程与设计》2008年第3期590-591,600,共3页Computer Engineering and Design

基　　金：国家自然科学基金项目(60673155);国防基础科研“十一五”基金项目(A1420060162)

摘　　要：用SPIN工具对WEP认证协议进行模型检测,不仅可以从状态空间上搜索出协议的漏洞,还可以各个角度分析WEP协议的运行逻辑。模型检测的方法先通过建立WEP认证协议的模型,转换成SPIN的输入语言Promela,然后通过建立WEP协议的性质转化成LTL语言,最后利用SPIN工具分析WEP认证协议。实验的结果说明WEP认证协议存在漏洞。The paper deal with model checking of WEP protocol via SPIN, not only searching the problem from states, but also analyzing WEP protocol logic from every point. The model checking is that model WEP protocol first, translating into Promela from SPIN, then change the properties of WEP protocol into LTL, the WEP protocol is analyzed at last. The result is show that there are some problem in the WEP protocol.

关 键 词：WEP协议 模型检测 认证 协议分析 逻辑验证 状态搜索 协议漏洞 

分 类 号：TP311.56[自动化与计算机技术—计算机软件与理论]