复杂安全协议的建模与验证

论文摘要

随着网络的发展,互联网络的安全问题变得越来越棘手,越来越重要,安全协议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问题最有效的手段之一,使用安全协议在开放的互联网络上可以实现身份认证等多项安全功能。由于在计算机网络中,相互通信的双方不能通过生物特征识别对方,因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码体制基础上的一种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。然而,设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明的安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。设计和开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领域的一个研究热点,也是验证复杂安全协议的关键环节。本文以Bruno Blanchet提出的Horn逻辑模型为基础,对反例构造算法和复杂协议验证方法进行了系统、深入的研究,主要工作包括以下几个方面:1.基于Horn逻辑的安全协议反例的自动构造算法。Bruno Blanchet提出了基于Horn逻辑的安全协议模型,该模型可高效地验证安全协议。为了将消息的角色信息保留在模型中,本文设计了相关的数据结构,给出了反例自动构造的算法实现,使验证工具能从不满足安全性质的消解序列中自动地构造出标准形式的反例,从而方便人们使用基于Horn逻辑的验证工具验证协议。2.不动点计算的不停机性预测。安全协议验证的不停机性源于不动点计算的不停机性。通过研究安全协议逻辑程序解形式不动点计算不终止的特征,本文给出了不动点计算不终止的预测方法。基于此方法,可以在协议验证时自适应地选择（精确或抽象）验证方法验证（停机或不停机的）安全协议。3.抽象与精化迭代验证框架。安全协议的正确性验证问题是不可判定的,使用抽象解释理论能够有效地验证安全协议。通过研究Horn逻辑模型中协议验证的特点,给出了安全协议基于抽象-精化的迭代验证理论框架。抽象验证保证停机,而精化过程可有效地去除虚假反例。因此,抽象-精化迭代框架可对Horn逻辑模型中验证过程不停机的安全协议进行有效验证。为了提高抽象模型的精度,本文进一步提出了局部抽象-精化迭代验证的理论框架。局部抽象可以提高整个验证过程的验证效率,为复杂协议的验证提供了有效的途径。4.时间敏感安全协议的建模与验证。通过将描述时间的事件加入到进程代数模型中,使得时间戳能方便有效地在协议模型中描述出来。将时间元素的线性约束加入到基于Horn逻辑的安全协议模型中,使得Horn逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解的关系,找到了确定时间相关元素的时间先后关系的办法,提出了两阶段验证方法。一条规则是否可用,此时还需考察其所对应的约束系统是否可满足。因此,本文对该模型下的约束系统进行了研究,提出了一个高效判断其可满足性的判定算法,并证明了该算法是多项式时间算法。由于约束系统中存在大量冗余的不等式,本文还深入研究了该系统,针对其本身的特性,提出了约束的抽象理论简化约束系统,该方法能有效地降低时空开销。5.设计并实现了一个高效的安全协议验证工具SPVT-II。本文提出了不停机性预测和抽象-精化迭代验证框架的实现算法,在安全协议自动分析工具SPVT的基础上,结合抽象-精化迭代验证框架,设计并实现了一个自适应选择验证方法的高效的协议验证工具SPVT-II。该工具既能发现协议中可能的反例,也能尽可能地减少虚假反例的产生。6. Kerberos协议协议的分析与验证。本文通过对Kerberos协议进行分析,将公钥Kerberos协议的认证服务交换阶段进行了建模,并用SPVT-II对协议模型进行了自动化的验证。实验结果表明SPVT-II能自动发现PKINIT-26中认证服务阶段的攻击。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景
• 1.2 研究对象和成果
• 1.3 相关工作
• 1.3.1 基于理想加密假设的安全协议分析与验证
• 1.3.2 基于计算语义的安全方案和协议的分析与验证
• 1.3.3 抽象解释理论
• 1.3.4 时间敏感安全协议的验证
• 1.3.5 安全协议验证工具
• 1.3.6 基于分析工具的复杂安全协议的分析与验证
• 1.4 本文结构
• 第二章 安全协议模型与验证基础
• 2.1 引言
• 2.2 安全协议的预备知识
• 2.3 安全协议的进程代数模型
• 2.4 安全协议的Horn 逻辑模型
• 2.4.1 Horn 逻辑语法
• 2.4.2 诚实角色模型
• 2.4.3 安全协议攻击者模型
• 2.4.4 安全性质
• 2.5 安全协议验证
• 2.6 小结
• 第三章 安全协议的反例构造算法
• 3.1 引言
• 3.2 反例构造原理
• 3.3 反例构造算法
• 3.3.1 基本数据结构
• 3.3.2 逻辑弱推导树构造算法
• 3.3.3 拆分结点算法
• 3.3.4 攻击序列生成算法
• 3.3.5 算法优化与复杂性分析
• 3.4 实验
• 3.5 小结
• 第四章 安全协议抽象-精化迭代验证框架
• 4.1 引言
• 4.2 不停机性的动态刻画与预测
• 4.2.1 不动点计算的不停机特征
• 4.2.2 不动点计算的不停机性预测
• 4.3 不动点计算的抽象与精化
• 4.3.1 抽象不动点计算
• 4.3.2 抽象不动点的精化迭代
• 4.4 不动点计算的局部抽象与精化
• 4.4.1 局部抽象不动点计算
• 4.4.2 局部抽象不动点的迭代精化
• 4.5 实验
• 4.6 小结
• 第五章 时间敏感安全协议的建模与验证
• 5.1 引言
• 5.2 进程代数模型
• 5.3 带时间约束的Horn 逻辑模型
• 5.3.1 带时间约束的 Horn 逻辑语法
• 5.3.2 进程代数模型到 Horn 逻辑模型的转换
• 5.3.3 安全协议攻击者模型
• 5.3.4 安全性质
• 5.4 验证
• 5.5 约束系统
• 5.5.1 约束系统的特性
• 5.5.2 约束系统的求解算法
• 5.6 约束系统的抽象
• 5.7 时间敏感安全协议的分析与验证
• 5.7.1 Denning-Sacco协议的分析与验证
• 5.7.2 大嘴青蛙协议的分析与验证
• 5.8 小结
• 第六章 安全协议验证工具 SPVT-II
• 6.1 引言
• 6.2 工具的结构
• 6.2.1 协议输入与模型转化部分
• 6.2.2 协议精确验证部分
• 6.2.3 抽象协议验证部分
• 6.2.4 反例检测与生成部分
• 6.3 SPVT-II 的主要操作
• 6.4 实验
• 6.5 小结
• 第七章 Kerberos 协议的分析与验证
• 7.1 引言
• 7.2 Kerberos 协议简介
• 7.3 协议的建模与验证
• 7.3.1 诚实角色模型
• 7.3.2 验证结果
• 7.4 小结
• 结束语
• 致谢
• 参考文献
• 作者在学期间取得的学术成果
• 附录A 本文使用到的安全协议
• A.1 简化 Needham-Schroeder 公钥协议
• A.2 Woo-Lam 认证协议版本Π
• A.3 Woo-Lam认证协议版本Π1
• A.4 Woo-Lam认证协议版本Π2
• A.5 Woo-Lam 认证协议版本Π3
• A.6 Woo-Lam 认证协议版本Πf
• A.7 Otway-Rees 认证协议
• A.8 Yahalom 认证协议
• A.9 Neuman-Stubblebine 认证协议
• A.10 Kao-ehow 重复认证协议
• 附录B Objective Caml 语言
• B.1 Objective Caml 简介
• B.2 模块函数介绍
• B.2.1 表模块List
• B.2.2 哈希表模块 Hashtbl
• B.2.3 字符串模块 String
• B.2.4 常用运算符