802.11i双向认证协议的模型检查

摘要：

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要.采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误.模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点.使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性.提出了一种使用PROMELA建模认证协议的方法.

关键词：模型检查、协议验证、认证协议、SPIN、EAP-TLS

所属期刊栏目：32

分类号：TP393.08;TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目60673155,90718008

在线出版日期：2010-05-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：25-28