摘要
用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.
出处
《计算机工程与设计》
CSCD
北大核心
2008年第3期590-591,600,共3页
Computer Engineering and Design
基金
国家自然科学基金项目(60673155)
国防基础科研“十一五”基金项目(A1420060162)
关键词
WEP协议
模型检测
认证
协议分析
逻辑验证
状态搜索
协议漏洞
WEP protocol
model checking
authentication
protocol analysis
logic validate
search states
problem in protocol
