安全协议形式化分析方法的关键技术研究

论文摘要

计算机网络正以惊人的速度向各个领域渗透,其中的安全问题也变得越来越突出和复杂,解决安全问题对许多网络应用来说已是头等大事。从目前解决安全问题的方式来看,安全协议是解决网络安全问题最有效的手段之一。如何保证安全协议的安全性是安全协议研究领域的一个关键问题。为了保证和验证安全协议的安全性,研究人员提出了形式化的方法。经过二十多年的发展,安全协议的形式化方法得到了快速的发展和广泛的应用,已经成为公认的,在安全协议验证和设计领域最为合理、有效的方法。形式化方法通过建立科学的理论模型,对安全协议进行严格的数学和逻辑推导,以此来证明安全协议的安全性或指出安全协议中存在的安全缺陷;同时,形式化方法还可用来指导安全协议的设计。虽然形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是,这些方法仍然存在很多问题。通过综合分析这些方法,我们发现,现有分析方法中有两个固有缺陷:一是没有明确的形式化的方法来统一描述多种安全属性;二是缺乏一般化的形式语言模型作为分析安全协议的统一框架。针对上述两个固有缺陷,我们从三个层面逐步深入地进行了研究:首先,我们深入研究了三类典型且重要的形式化分析方法:类BAN逻辑、串空间、SPI演算,分析了他们的固有缺陷,有效地改进了他们的部分缺陷。其次,我们提出了一种用有向图来描述协议运行的分析方法,该方法部分解决了目前协议分析方法共性问题中的第二个固有缺陷。最后,我们提出了一个安全协议的统一分析框架,在更高的抽象层次上对安全协议运行和安全属性及其验证方法进行形式化建模,并在这个框架指导下,基于符号迹的方法设计了一种新的协议分析方法,实例分析表明该方法是有效的。我们提出的安全协议统一分析框架是解决目前安全协议分析方法两个固有缺陷的一次有意义的尝试,取得了一定的科研成果。本文的主要创新点如下:（1）改进类BAN逻辑在“理想化协议”步骤和单调性信任关系方面的缺陷,提出了基于消息唯一起源的动态逻辑方法。通过消息唯一起源的概念,解决了“相信事情的发生”和“相信事情的真实性”两种不同信任的区别,在此基础上建立了动态逻辑方法。（2）定义了新的类BAN逻辑语义模型,分析了类BAN逻辑的本质缺陷。该模型定义了“可能世界”及“可达关系”的概念。在这种模态逻辑框架下,我们给出了类BAN逻辑的真值赋值函数。从理论上证明了类BAN逻辑的逻辑语义缺陷是不可逾越的。（3）提出了安全属性的统一形式化描述方法,尝试用匹配关系来描述安全属性。在研究过程中,我们对此做了进一步的改进,安全属性被最终定义为:实体的时序消息与属性消息之间的推导关系。该定义脱离具体协议,是对安全属性的抽象建模,因此,更具有普适性。（4）将进程演算与实体消息推理结合起来,采用匹配关系来描述安全属性,提出了组合分析方法。该方法一方面弥补了进程演算缺乏数据结构来表示实体知识的缺陷,另一方面明确指出了在符号迹的分析过程中,如何及何时进行带符号的消息推理。由于采用了与协议无关的安全属性形式化描述方法,该方法扩展性很强。（5）提出了安全协议有向图分析法,部分解决了当前分析方法在协议运行的形式化建模方面的缺陷。该方法将协议规范中的每个协议步骤分解为有序动作序列,给出协议的有向图生成规则以及能够准确地跟踪协议消息的多种构造途径的消息构造逆向搜索算法。（6）提出“安全属性建模+协议运行建模”模式的统一分析框架。在统一框架的基础上,采用时序消息的推导关系来描述安全属性,为符号迹方法增加时间概念和基于时间的消息推理规则,从而有效地构造了基于符号迹的安全协议分析方法。这种统一分析框架对于安全协议的设计和分析方法的设计具有十分重要的意义。

论文目录

• 摘要
• ABSTRACT
• 缩略语
• 第一章 绪论
• 1.1 课题研究背景
• 1.2 安全协议分析方法的基本概念和研究进展
• 1.2.1 安全协议分析方法的基本概念
• 1.2.2 安全协议分析方法的研究进展
• 1.3 本文研究问题的提出及解决的思路
• 1.4 本文工作与结构
• 1.4.1 研究内容及主要工作
• 1.4.2 本文结构
• 第二章 四种形式化分析方法的基本概念
• 2.1 类BAN 逻辑基本概念
• 2.1.1 逻辑语法与语义
• 2.1.2 分析方法
• 2.2 串空间的基本概念
• 2.2.1 基本串空间理论
• 2.2.2 认证测试理论
• 2.3 SPI 演算的基本概念
• 2.3.1 SPI 演算符号
• 2.3.2 形式语义
• 2.3.3 测试等价
• 2.4 符号迹方法的基本概念
• 2.4.1 符号语法
• 2.4.2 分析方法
• 2.4.3 提炼概念
• 2.5 本章小结
• 第三章 类BAN 逻辑方法的改进及其本质缺陷证明
• 3.1 逻辑方法的缺陷分析
• 3.2 一种新的动态逻辑方法
• 3.2.1 消息唯一起源概念及其判定规则
• 3.2.2 集合定义与实体动作
• 3.2.3 推理模型与规则
• 3.2.4 实例分析
• 3.3 新模态语义模型及对类BAN 逻辑语义缺陷的证明
• 3.3.1 计算模型
• 3.3.2 新语义模型构造
• 3.3.3 逻辑语义缺陷证明
• 3.4 本章工作与其他相关工作的比较
• 3.5 本章小结
• 第四章 串空间理论和SPI 演算的缺陷分析及SPI 演算的改进
• 4.1 串空间理论缺陷分析
• 4.2 SPI 演算缺陷分析
• 4.3 基于SPI 演算的组合分析方法
• 4.3.1 基于匹配关系的安全属性形式化描述
• 4.3.2 带符号的消息推理
• 4.3.3 组合分析模型
• 4.3.4 实例分析
• 4.4 本章工作与其他相关工作的比较
• 4.5 本章小结
• 第五章 基于有向图的协议分析方法
• 5.1 形式化分析方法的缺陷
• 5.2 协议消息计算模型
• 5.3 协议有向图模型
• 5.4 基于有向图的协议安全性分析
• 5.4.1 协议消息生成的逆向搜索算法
• 5.4.2 逆向搜索算法分析认证协议的安全性
• 5.4.3 实例分析
• 5.5 本章工作与其他相关工作的比较
• 5.6 本章小结
• 第六章 安全协议的统一分析框架及基于符号迹方法的实现
• 6.1 协议分析的统一框架
• 6.1.1 认证协议设计框架
• 6.1.2 基于符号迹的统一分析框架
• 6.2 基于统一框架的符号迹协议分析方法
• 6.2.1 协议运行的形式化建模
• 6.2.2 基于时序关系的消息推理
• 6.2.3 安全属性的形式化描述
• 6.2.4 协议的符号迹分析
• 6.2.5 实例分析
• 6.3 本章工作与其他相关工作的比较
• 6.4 本章小结
• 第七章 结束语
• 7.1 全文总结
• 7.2 研究展望
• 致谢
• 参考文献
• 作者攻读博士期间完成的论文
• 作者攻读博士期间参加的科研项目