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

• 作者: 张大方 缪力 黄谷
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 模型检查 协议验证 认证协议 SPIN EAP-TLS
• 年，卷（期）: 2010,（4）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 25-28
• 页数: 4页
• 分类号: TP393.08|TP311.5
• 字数: 3778字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.04.007

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张大方	湖南大学软件学院	295	2498	22.0	33.0
2	缪力	湖南大学软件学院	35	167	8.0	10.0
3	黄谷	湖南大学软件学院	2	2	1.0	1.0