安全协议自动验证工具的状态空间剪枝

• 作者: 刘学锋 周径野 石昊苏 薛锐
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: 形式化分析 串空间模型 模型检测 状态空间剪枝
• 年，卷（期）: 2004,（8）
• 所属期刊栏目: 信息安全
• 页码范围: 117-121
• 页数: 5页
• 分类号: TP309
• 字数: 6402字
• 语种: 中文

摘要

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法.概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构,提出一些剪枝规则对状态搜索空间进行剪枝.通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间,防止状态空间爆炸.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	薛锐	中国科学院软件研究所	20	275	7.0	16.0
2	石昊苏	中国科学院软件研究所	2	3	1.0	1.0
3	刘学锋	湘潭大学信息工程学院	1	3	1.0	1.0
4	周径野	湘潭大学信息工程学院	1	3	1.0	1.0