基于SPIN的网络认证协议高效模型检测

• 作者: 张大方 缪力 谭志华
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 网络认证协议 模型检测 简单进程元语言解释器(SPIN) 模型简化策略 密钥管理(PKM)协议
• 年，卷（期）: 2012,（21）
• 所属期刊栏目: 网络、通信、安全
• 页码范围: 62-67
• 分类号: TP393
• 字数: 6321字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2012.21.014

摘要

为了有效地提高网络认证协议建模和验证的效率,基于模型检测方法提出一个通用的网络认证协议模型描述方法,结合模型检测工具SPIN可以方便地进行性质验证.通过一些模型的简化策略,不仅可以对不同协议进行高效建模,而且减小了模型的状态空间.与现有的文献相比,自动化程度较高,模型验证的效率较好.基于该方法,对PKM认证协议进行了模型检测,实验证明该模型分析验证方法的有效性,可用于其他网络认证协议的分析验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张大方	湖南大学信息科学与工程学院	295	2498	22.0	33.0
2	缪力	湖南大学信息科学与工程学院	35	167	8.0	10.0
3	谭志华	湖南大学信息科学与工程学院	5	20	2.0	4.0