基于计算语义的安全协议验证逻辑

• 作者: 冯超 唐朝京 鲁智勇
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 加密算法 安全性 形式逻辑 计算语义
• 年，卷（期）: 2014,（6）
• 所属期刊栏目: 学术论文
• 页码范围: 1179-1185
• 页数: 7页
• 分类号: TP309
• 字数: 9007字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2014.06.022

摘要

提出了一个基于计算语义的安全协议验证逻辑，能准确描述安全协议中的各种计算行为和通信行为。设计了基于该逻辑的证明系统，能对密码学中常用加密算法的各类安全属性规范直接描述，具有密码学可靠性。发现了计算协议组合逻辑在加密算法安全性建模时存在的不可靠性，并提出了解决方法。通过对Needham-Schroeder-Lowe协议安全性的证明，验证了逻辑的证明能力。与大部分验证方法不同的是，本逻辑属于由密码学算法安全性到协议安全性的正向推理方法，兼具符号方法的易用性和计算方法的可靠性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐朝京	国防科技大学电子科学与工程学院	97	885	15.0	24.0
2	冯超	国防科技大学电子科学与工程学院	9	62	3.0	7.0
3	鲁智勇		2	5	2.0	2.0