密码协议工程与基于新鲜性的协议安全研究

论文摘要

密码协议的安全性研究是网络安全研究的主要热点。本论文主要研究了如何应用系统工程思想和形式化方法来分析和设计密码协议,取得的主要研究结果如下:1.将系统工程思想引入密码协议设计,结合前人的研究成果,提出了10条密码协议工程原则:5条安全需求分析原则,4条详细设计原则以及1条安全性证明原则。将密码协议设计看作密码协议工程,从协议设计的不同阶段给出原则,是帮助研究人员按系统工程思想进行密码协议设计的有益尝试。实例分析表明,这些原则不仅较为完备,而且可操作性强,能帮助研究人员明确协议设计背后的隐含假设,发现和避免协议设计中的漏洞,简化协议设计。2.首次提出基于信任的新鲜性标识符分析密码协议的安全性,给出了新鲜性原则:对每个通信参与主体而言,密码协议的安全性取决于发送或者接收的、包含自身已相信新鲜的新鲜性标识符的单向变换。该原则找到了一条快捷、有效的密码协议安全性分析方法,论文示例了20多个经典密码协议的分析结果,分析出的针对协议的攻击或者安全隐患有12个是以往没有指出过的。新鲜性原则的特点是:①能有效区分消息是否新鲜,安全性的分析独立于并发运行环境的具体形式化描述,也独立于攻击者能力的具体形式化描述;②基于该原则得到的分析结果能够证明正确协议的安全性,也能够分析出不安全协议存在的安全属性缺失,以及由该缺失直接构造攻击的结构。3.基于新鲜性原则,提出了基于逻辑推理的信任多集形式化分析方法。以Needham-Schroeder公钥认证协议为例,说明了该分析方法的有效性、严谨性和自动化实现的可能。另外,针对无线网络的开放性和数据包易失的特点,扩展了信任多集方法,能有效用于无线密码协议分析。4.证明了保证认证协议安全的充分必要条件,这些条件在计算模型下分别满足基于匹配对话和不可区分性的4个可证安全定义。5.提出了信任多集自动分析工具的总体框架,通过在2种不同开发环境下信任多集自动分析工具初步实现的比较,给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。6.基于新鲜性原则和因果一致性的分布式逻辑时间,建立了信任多集形式化设计方法。构造了一个公钥认证协议,并证明了该协议达到了消息数和轮数的下限。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 密码协议的安全目标
• 1.2 密码协议的分类
• 1.3 课题研究背景
• 1.4 论文组织
• 第二章 密码协议工程原则与非形式化分析
• 2.1 基础理论
• 2.1.1 基础知识
• 2.1.2 计算模型下的安全性定义
• 2.1.3 协议分析的前提假设
• 2.1.4 密码协议的基本符号表示
• 2.2 Abadi 的谨慎工程原则
• 2.2.1 Abadi 的11 条谨慎工程原则
• 2.2.2 谨慎工程原则的局限性
• 2.3 密码协议工程原则
• 2.3.1 密码协议工程的需求分析原则
• 2.3.2 密码协议工程的详细设计原则
• 2.3.3 密码协议工程的安全性证明原则
• 2.4 本章小结
• 第三章 密码协议安全验证机理
• 3.1 密码协议的安全性
• 3.1.1 密码协议的安全目标
• 3.1.2 密码协议的安全定义
• 3.1.3 密码协议安全性分析的前提假设
• 3.2 基于信任的新鲜性的密码协议安全验证机理
• 3.2.1 基本概念
• 3.2.2 新鲜性原则
• 3.2.3 新鲜性分析方法
• 3.3 基于新鲜性验证机理的协议分析
• 3.3.1 若干经典的密码协议
• 3.3.2 若干实际应用的密码协议
• 3.3.3 其它密码协议
• 3.4 本章小节
• 第四章 基于信任多集的形式化分析方法
• 4.1 已有的形式化分析方法
• 4.1.1 Dolev-Yao 模型
• 4.1.2 基于逻辑推理的分析方法
• 4.1.3 基于计算模型的分析方法
• 4.1.4 基于模型检验的分析方法
• 4.1.5 基于定理证明的分析方法
• 4.2 信任多集形式化分析方法
• 4.2.1 定义与描述
• 4.2.2 推导规则
• 4.2.3 公理
• 4.3 基于信任多集方法的密码协议安全性分析
• 4.3.1 保证认证协议安全的量化指标
• 4.3.2 安全性条件验证
• 4.4 信任多集方法的应用
• 4.4.1 原始的 N-S 公钥密码协议分析
• 4.4.2 改进的N-S 公钥密码协议分析
• 4.5 与已有形式化方法的比较与分析
• 4.6 本章小结
• 第五章 基于信任多集的自动化分析
• 5.1 已有的自动化分析方法
• 5.1.1 基于逻辑推理的自动验证方法
• 5.1.2 基于模型检验的自动验证方法
• 5.1.3 基于定理证明的自动验证方法
• 5.2 基于信任多集的自动分析工具
• 5.2.1 BMF 工具的总体框架
• 5.2.2 BMF 工具的2 种初步实现
• 5.2.3 BMF 工具的实现
• 5.3 本章小结
• 第六章 基于信任多集的形式化设计方法
• 6.1 已有的密码协议形式化设计方法
• 6.2 信任多集形式化设计方法
• 6.2.1 信任多集形式化设计方法
• 6.2.2 认证密钥协议的消息数和轮数下限
• 6.3 信任多集形式化设计方法的应用
• 6.4 信任多集形式化设计方法的特点
• 6.5 本章小结
• 第七章 信任多集方法在无线通信环境的应用
• 7.1 扩展的信任多集形式化方法
• 7.2 IEEE 802.11i 标准中认证有关部分的分析
• 7.2.1 四次握手协议的分析
• 7.2.2 组密钥握手协议的分析
• 7.3 更多应用实例
• 7.3.1 传感器网络环境下一个基于Kerberos 的对密钥管理方案
• 7.3.2 基于身份的对称密钥协议
• 7.3.3 节点到节点的密钥管理协议
• 7.4 本章小结
• 第八章 总结与展望
• 参考文献
• 博士阶段完成的论文
• 博士阶段参加的科研项目
• 致谢
• 附录A 一些著名密码协议的安全性分析结果