基于Horn逻辑扩展模型的时间敏感安全协议验证

• 作者: 周倜 李梦君 李舟军 陈火旺
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 安全协议 扩展的Horn逻辑模型 时间敏感 约束条件 形式化验证
• 年，卷（期）: 2006,（z2）
• 所属期刊栏目: 网络和通信安全
• 页码范围: 534-540
• 页数: 7页
• 分类号: TP309
• 字数: 7859字
• 语种: 中文

摘要

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们在验证时间敏感安全协议时的不足,提出了带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证方法,并给出了相应的定义和定理,使得带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证能够分析依赖时间的安全协议的安全性质.通过在验证中加入时间约束条件,得到了大嘴青蛙协议的攻击序列,并可从约束条件中导出避免攻击的条件.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	北京航空航天大学计算机学院	136	2221	23.0	43.0
2	陈火旺	国防科学技术大学计算机学院	53	2116	23.0	45.0
3	周倜	国防科学技术大学计算机学院	3	7	1.0	2.0
4	李梦君	国防科学技术大学计算机学院	16	294	7.0	16.0