| 安全协议的扩展Horn逻辑模型及其验证方法 |
| |
| 引用本文： | 李梦君,李舟军,陈火旺. 安全协议的扩展Horn逻辑模型及其验证方法[J]. 计算机学报, 2006, 29(9): 1666-1678 |
| |
| 作者姓名： | 李梦君 李舟军 陈火旺 |
| |
| 作者单位： | 1. 国防科学技术大学计算机学院,长沙,410073
2. 北京航空航天大学计算机科学与工程学院,北京,100083 |
| |
| 基金项目： | 国家自然科学基金;国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．
|
| 关 键 词： | 安全协议 扩展Horn逻辑模型 形式化验证 |
| 收稿时间： | 2006-04-04 |
| 修稿时间： | 2006-04-042006-06-02 |
Security Protocol''''s Extended Horn Logic Model and Its Verification Method |
| |
| LI Meng-Jun,LI Zhou-Jun,CHEN Huo-Wang. Security Protocol''''s Extended Horn Logic Model and Its Verification Method[J]. Chinese Journal of Computers, 2006, 29(9): 1666-1678 |
| |
| Authors: | LI Meng-Jun LI Zhou-Jun CHEN Huo-Wang |
| |
| Abstract: | Based on analyzing and pointing out the limitations for constructing counter-examples of the security protocol's Horn logic model and its verification method proposed by Bruno Blanchet and Martin Abadi,the security protocol's extended Horn logic model and the modified-version verification method are presented such that the counter-examples are able to be constructed from them automatically.In the authors' verifier SPVT developed based on the functional programming language Objective Caml,these algorithms are implemented and their correctness are proved. |
| |
| Keywords: | security protocol extended Horn logic model formal verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
