安全协议分析的形式化理论与方法 ——基于定理证明的安全协议建模研究

论文摘要

安全的密码协议是网络通信和应用必不可少的组件之一,是构筑信息安全体系的基础。设计安全和有效的密码协议是协议工程领域中的主要研究内容。在设计、描述（建模）、验证、性能分析、实现、测试和维护等协议工程的各个环节中,协议验证是最为关键的一个环节。协议分析和协议综合是实现协议验证的两种有效途径,前者更为有效和实用。 自上个世纪七十年代末以来,人们提出多种安全协议分析的形式化理论,包括Dolev-Yao模型、模态逻辑、Paulson归纳法、串空间模型以及Spi演算理论等,并从这些理论中归纳出基于模态逻辑推理、基于模型状态检验、基于定理证明和基于类型检测等安全目标验证方法。前两类方法只能推理密码协议的不安全性,不能给出其安全目标的可信证明,而后一类方法又不具有完备性,唯有基于定理证明的安全目标验证方法试图给出密码协议的安全性证明。 本文在基于定理证明的安全协议形式化建模方面系统地研究了安全协议的消息语句空间和消息事件空间的性质、主体进程表示理论以及安全目标的分类、形式化描述和安全协议的可验证性等问题,主要工作和贡献如下: 1.研究消息语句空间性质,提出用于消息语句结构定性和定量分析的理论与方法。消息语句空间及其语句运算构成消息代数。其语句运算包括f-语句运算、求逆密钥运算以及语句的加密和连接运算。这些运算可以完备地生成现有安全协议运行中主体角色（包括攻击者）的各种消息语句。消息代数中的代数运算规则和子句关系是定量和定性语句结构分析的理论工具。 2.研究消息事件空间性质,提出用于消息事件动态分析的消息交换关系理论。由利用前驱关系排序主体角色消息事件集中的消息事件得到的消息事件序列为进程顺序合成运算提供了语义模型。通过定义可达路径对特征消息语句单元在消息交换中的迁移状况的刻画,给出组合（并发运行）协议中的主协议（观察对象）保持其独立性的判定定理。

论文目录

• 第一章 绪论
• 1.1 引言
• 1.2 课题研究背景
• 1.3 安全协议分析的形式化建模理论
• 1.3.1 Dolev-Yao模型
• 1.3.2 模态逻辑
• 1.3.3 有限状态机
• 1.3.4 进程代数
• 1.4 本文主要工作
• 1.5 本文主要内容
• 第二章 安全协议分析
• 2.1 引言
• 2.2 密码协议安全目标
• 2.2.1 安全目标分类
• 2.2.2 安全目标规范
• 2.3 安全目标验证方法及其理论基础
• 2.3.1 逻辑推理方法
• 2.3.2 模型检测方法
• 2.3.3 定理证明方法
• 2.3.4 类型检测方法
• 2.4 安全协议的可验证性问题
• 2.4.1 Ping-Pong协议
• 2.4.2 关于密码协议安全性判定
• 2.5 本章小结
• 第三章 消息结构描述
• 3.1 引言
• 3.2 消息空间结构
• 3.2.1 消息空间
• 3.2.2 语句运算
• 3.3 语句结构及其性质
• 3.3.1 语句运算假设
• 3.3.2 语句结构分析
• 3.4 本章小结
• 第四章 消息交换次序
• 4.1 引言
• 4.2 消息事件
• 4.2.1 事件及其通信关系
• 4.2.2 事件顺序关系
• 4.3 路径描述
• 4.3.1 可达路径
• 4.3.2 主协议的独立性
• 4.4 例子：Kerberos协议描述及其独立性分析
• 4.5 本章小结
• 第五章 不变集及其生成
• 5.1 引言
• 5.2 不变集
• 5.3 诚实性判定条件的可满足性
• 5.3.1 诚实性判定
• 5.3.2 判定条件的可满足性定理
• 5.4 不变集生成算法
• 5.5 例子：一类带MAC载荷安全协议的建模
• 5.6 本章小结
• 第六章 主体进程表示
• 6.1 引言
• 6.2 关于Spi演算
• 6.2.1 语法与形式语义
• 6.2.2 进程等价
• 6.2.3 基于Spi演算的安全目标验证
• 6.3 进程描述语言
• 6.3.1 通信事件及其关系
• 6.3.2 进程及其演算算子
• 6.3.3 进程演算算法
• 6.3.4 进程互模拟关系
• 6.4 本章小结
• 第七章 事件图模型
• 7.1 引言
• 7.2 事件图结构
• 7.2.1 局部（子图）
• 7.2.2 结构约束条件
• 7.3 事件图生成
• 7.3.1 图元
• 7.3.2 结构控制算子
• 7.3.3 事件图生成算法
• 7.4 事件图等价
• 7.4.1 图元的互模拟
• 7.4.2 事件图的冗余消除
• 7.5 例子：NSL协议事件图的生成
• 7.6 本章小结
• 第八章 总结与展望
• 8.1 全文总结
• 8.2 后续研究工作展望
• 参考文献
• 攻读博士学位期间完成的论文