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

摘要

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

目录

文摘

英文文摘

论文说明：表格清单、插图清单

独创性声明及学位论文版权使用授权书

致谢

第一章绪论

第二章安全协议分析

第三章消息结构描述

第四章消息交换次序

第五章不变集及其生成

第六章主体进程表示

第七章事件图模型

第八章总结与展望

参考文献

攻读博士学位期间完成的论文