基于Spi演算的密码协议自动化分析技术研究

论文摘要

密码协议是网络通信和许多分布式系统的安全基础,协议的正确性和安全性对于保证攻击者不能获得秘密信息或实施不公平认证起着至关重要的作用。由于在协议的设计过程中对协议运行环境的安全需求估计不足或采用技术不当,往往会导致密码协议存在安全漏洞或缺陷,且这些漏洞与缺陷往往只有在遭到恶意攻击时才会暴露出来,通过静态测试和手工验证方法,无法检测到协议的某些缺陷和对协议的潜在攻击,因此,密码协议自动化分析技术成为了研究热点。 本文主要从分析和实现的角度对密码协议自动化分析技术进行了研究,所做的工作主要有以下几个方面: (1) 在对Spi演算研究的基础上,提出了一种扩展的Spi演算,并根据扩展Spi演算语法定义了密码协议的秘密性和认证性,给出了其便于自动化实现的分析方法。 (2)构建了一个基于扩展Spi演算的类型系统,给出了该类型系统的类型规则及相应的类型操作,并证明了如果一个进程在该类型系统被证明是类型完善的,则该进程不会泄漏秘密级别的数据。 (3)通过基于扩展Spi演算的类型系统证明了一个典型密码协议秘密性。 (4)利用逻辑程序方法,设计了一个以扩展Spi演算作为对密码协议形式化描述的自动化分析器,并介绍了其基本原理,证明了该分析器在密码协议秘密性的分析方法上与基于扩展Spi演算的类型系统是一致的。在秘密性分析的基础上给出了该分析器对密码协议认证性的分析原理。 (5)给出了扩展Spi演算对密码协议的描述到霍恩子句的转换规则,设计实现了协议分析器的自动翻译部分,完成了扩展Spi演算描述的协议到霍恩子句的自动转换。

论文目录

• 目录
• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 引言
• 1.2 密码协议形式化分析方法
• 1.3 密码协议自动化分析技术研究现状
• 1.4 逻辑程序设计语言Prolog
• 1.4.1 Prolog语言简介
• 1.4.2 事实与规则
• 1.4.3 询问
• 1.5 论文主要研究内容
• 第二章 Spi演算及其对密码协议的分析方法
• 2.1 Spi演算
• 2.1.1 Spi演算语法
• 2.1.2 自由与受限
• 2.1.3 反应关系
• 2.1.4 测试等价
• 2.2 Spi演算对密码协议的形式化分析
• 2.3 本章小结
• 第三章 扩展Spi演算及其对密码协议安全属性的分析
• 3.1 扩展Spi演算
• 3.1.1 基本语法
• 3.1.2 秘密性
• 3.1.3 认证性
• 3.1.4 协议实例分析
• 3.2 基于扩展Spi演算的类型系统
• 3.2.1 基本原理
• 3.2.2 构建基于扩展Spi演算类型系统的基本条件
• 3.2.3 基于扩展Spi演算的类型系统
• 3.2.4 基于扩展Spi演算类型系统的安全属性
• 3.3 类型系统对密码协议秘密性的分析
• 3.4 本章小结
• 第四章 基于扩展Spi演算的密码协议自动化分析器
• 4.1 密码协议自动化分析器
• 4.1.1 分析器工作原理
• 4.1.2 分析器输入语法
• 4.1.3 自动翻译器
• 4.1.4 逻辑推导模块
• 4.2 描述协议的事实与规则
• 4.2.1 模式与事实
• 4.2.2 攻击者初始知识
• 4.2.3 攻击者计算能力
• 4.2.4 协议的描述
• 4.2.5 进程转换
• 4.2.6 规则基础
• 4.3 分析器对密码协议安全属性的分析
• 4.3.1 秘密性
• 4.3.2 单射一致性和非单射一致性
• 4.4 本章小结
• 第五章 自动翻译器的设计与实现
• 5.1 词法分析
• 5.2 语法分析
• 5.3 转换算法
• 5.4 本章小结
• 结束语
• 致谢
• 参考文献
• 附录：函数Ф的定义