| 基于Horn逻辑扩展模型的时间敏感安全协议验证 |
| |
| 引用本文： | 周倜,李梦君,李舟军,陈火旺. 基于Horn逻辑扩展模型的时间敏感安全协议验证[J]. 计算机研究与发展, 2006, 43(Z2) |
| |
| 作者姓名： | 周倜 李梦君 李舟军 陈火旺 |
| |
| 摘 要： | 分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们在验证时间敏感安全协议时的不足,提出了带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证方法,并给出了相应的定义和定理,使得带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证能够分析依赖时间的安全协议的安全性质.通过在验证中加入时间约束条件,得到了大嘴青蛙协议的攻击序列,并可从约束条件中导出避免攻击的条件.
|
| 关 键 词： | 安全协议 扩展的Horn逻辑模型 时间敏感 约束条件 形式化验证 |
Verification of Time Sensitive Security Protocols Based on the Extended Horn Logic Model |
| |
| Zhou Ti,Li Mengjun,Li Zhoujun,Chen Huowang. Verification of Time Sensitive Security Protocols Based on the Extended Horn Logic Model[J]. Journal of Computer Research and Development, 2006, 43(Z2) |
| |
| Authors: | Zhou Ti Li Mengjun Li Zhoujun Chen Huowang |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
