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

作者：刘学锋; 石昊苏; 薛锐; 周径野

来源：计算机应用, 2004, (08): 117-121.

• 形式化分析
• 串空间模型
• 模型检测
• 状态空间剪枝 formal method
• strand space model
• model checking
• state space pruning

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

• 出版日期2004
• 单位湘潭大学; 中国科学院软件研究所