摘要 | 第2-4页 |
ABSTRACT | 第4-5页 |
符号说明 | 第9-11页 |
第一章 绪论 | 第11-16页 |
1.1 课题的背景及意义 | 第11-12页 |
1.2 安全协议形式化方法理论和工具 | 第12-14页 |
1.3 本文的主要研究内容 | 第14-15页 |
1.4 本章小结 | 第15-16页 |
第二章 串空间模型的基本理论和基于认证测试方法的安全协议验证 | 第16-33页 |
2.1 串空间模型 | 第16-20页 |
2.1.1 基本概念 | 第16-19页 |
2.1.2 攻击者的描述 | 第19-20页 |
2.2 基于认证测试方法的安全协议验证 | 第20-22页 |
2.2.1 认证测试方法概述 | 第20-21页 |
2.2.2 认证测试方法的基本概念 | 第21页 |
2.2.3 认证测试规则 | 第21-22页 |
2.2.4 三方协议的安全保证 | 第22页 |
2.3 认证测试方法在无线安全领域的应用 | 第22-28页 |
2.3.1 EAP-AKA 协议介绍 | 第23页 |
2.3.2 基本标识符 | 第23-24页 |
2.3.3 EAP-AKA 协议的形式化描述 | 第24-26页 |
2.3.4 EAP-AKA 协议的证明 | 第26-28页 |
2.4 基于消息类型检测的改进认证测试方法 | 第28-32页 |
2.4.1 消息类型的定义 | 第28-30页 |
2.4.2 消息类型的检测 | 第30-31页 |
2.4.3 基于消息类型检测的改进认证测试方法 | 第31-32页 |
2.5 本章小结 | 第32-33页 |
第三章 认证测试方法的扩展 | 第33-80页 |
3.1 认证测试方法的缺陷 | 第33-34页 |
3.2 协议主体的目标 | 第34页 |
3.3 协议矩阵定义 | 第34-36页 |
3.4 认证测试1 和认证测试2 的扩展 | 第36-72页 |
3.5 认证测试3 的扩展 | 第72-75页 |
3.6 基于扩展的认证测试方法的协议分析 | 第75-79页 |
3.6.1 Needham-Schroeder 协议验证 | 第75页 |
3.6.2 Yahalom 协议验证 | 第75-78页 |
3.6.3 EAP-AKA 协议验证 | 第78-79页 |
3.7 本章小结 | 第79-80页 |
第四章 自动化协议分析算法的设计 | 第80-89页 |
4.1 安全协议分析算法和工具发展现状 | 第80-81页 |
4.2 基于认证测试方法的安全协议分析方法 | 第81页 |
4.3 基于扩展的认证测试方法的P 算法的设计与分析 | 第81-88页 |
4.3.1 P 算法简述 | 第82页 |
4.3.2 算法描述及功能模块 | 第82-83页 |
4.3.3 P 算法流程 | 第83-88页 |
4.4 本章小结 | 第88-89页 |
第五章 基于P 算法的安全协议自动化验证系统原型系统设计与实现 | 第89-108页 |
5.1 自动化安全协议分析系统介绍 | 第89-90页 |
5.2 系统的总体设计 | 第90-92页 |
5.2.1 总体框架 | 第90-91页 |
5.2.2 功能模块及描述 | 第91-92页 |
5.3 形式化协议描述语言 | 第92-97页 |
5.3.1 形式化协议描述语言概述 | 第92-93页 |
5.3.2 形式化协议描述语言P 语言 | 第93-96页 |
5.3.3 形式化协议描述语言P 语言解析器 | 第96-97页 |
5.4 系统数据结构定义 | 第97-102页 |
5.4.1 协议描述的数据结构定义 | 第97-100页 |
5.4.2 协议证明的数据结构定义 | 第100-101页 |
5.4.3 P 算法数据结构的具体实现 | 第101-102页 |
5.5 基于P 算法的Needham-Schroeder 协议的验证 | 第102-104页 |
5.5.1 Needham-Schroeder 协议流程 | 第102-103页 |
5.5.2 Needham-Schroeder 协议的描述 | 第103页 |
5.5.3 协议验证过程 | 第103-104页 |
5.6 原型系统的测试与分析 | 第104-107页 |
5.6.1 功能性测试 | 第104-107页 |
5.7 本章小结 | 第107-108页 |
第六章.结论和展望 | 第108-110页 |
6.1 主要结论 | 第108-109页 |
6.2 研究展望 | 第109-110页 |
参考文献 | 第110-115页 |
致谢 | 第115-116页 |
攻读学位期间发表的学术论文目录 | 第116页 |