| 安全协议自动验证工具的状态空间剪枝 |
| |
| 引用本文： | 刘学锋,石昊苏,薛锐,周径野. 安全协议自动验证工具的状态空间剪枝[J]. 计算机应用, 2004, 24(8): 117-121 |
| |
| 作者姓名： | 刘学锋 石昊苏 薛锐 周径野 |
| |
| 作者单位： | 湘潭大学,信息工程学院,湖南,湘潭,411105;中国科学院,软件研究所,北京,100080 |
| |
| 基金项目： | 国家自然科学基金项目 (60 2 730 2 7，60 3730 4 8)，国家 863计划项目 (2 0 0 2AA1 4 4 0 50 )，国家 973计划项目 (G1 9990 3580 2 ) |
| |
| 摘 要： | 串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。
|
| 关 键 词： | 形式化分析 串空间模型 模型检测 状态空间剪枝 |
| 文章编号： | 1001-9081(2004)08-0117-05 |
State space pruning in automatic verification of security protocol |
| |
| LIU Xue-feng,SHI Hao-su,XUE Rui,ZHOU Jing-ye. State space pruning in automatic verification of security protocol[J]. Journal of Computer Applications, 2004, 24(8): 117-121 |
| |
| Authors: | LIU Xue-feng SHI Hao-su XUE Rui ZHOU Jing-ye |
| |
| Affiliation: | LIU Xue-feng~1,SHI Hao-su~2,XUE Rui~2,ZHOU Jing-ye~1 |
| |
| Abstract: | Strand Space Model (SSM) is a practical, intuitive and strict formal method for security protocol analysis. Based on SSM, we presented the frame of an automatic verification system of security protocol, AVSP, combined with theorem proving and model checking. We emphasized pruning methods of the state space in it. The experiment results got by authentic property verification of Needham-Schroeder show that these pruning methods can perfectly reduce state search space and prevent state explosion. |
| |
| Keywords: | formal method strand space model model checking state space pruning |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
