| 摘要 | 第5-7页 |
| ABSTRACT | 第7-8页 |
| 縮略词 | 第14-15页 |
| 第一章 引言 | 第15-19页 |
| 1.1 研究背景及意义 | 第15-16页 |
| 1.2 论文的贡献 | 第16-17页 |
| 1.3 论文的组织 | 第17-19页 |
| 第二章 相关研究概述 | 第19-41页 |
| 2.1 安全协议及其性质 | 第19-21页 |
| 2.1.1 安全协议分类 | 第19-20页 |
| 2.1.2 安全属性 | 第20-21页 |
| 2.2 形式化建模方法 | 第21-22页 |
| 2.3 安全协议形式化分析方法 | 第22-27页 |
| 2.3.1 基于推理证明的模态逻辑方法 | 第23-24页 |
| 2.3.2 定理证明方法 | 第24-25页 |
| 2.3.3 基于类型检测的方法 | 第25-26页 |
| 2.3.4 模型检测方法 | 第26-27页 |
| 2.4 攻击者模型 | 第27-31页 |
| 2.4.1 Dolev-Yao攻击者模型 | 第27-29页 |
| 2.4.2 安全协议的攻击分类 | 第29-31页 |
| 2.5 攻击序列生成方法 | 第31-33页 |
| 2.5.1 基于定理证明的攻击序列生成方法 | 第31-32页 |
| 2.5.2 基于模型检测的攻击序列生成方法 | 第32-33页 |
| 2.6 基于CP-nets模型的形式化方法 | 第33-39页 |
| 2.6.1 CP-nets模型形式化定义 | 第33-36页 |
| 2.6.2 CP-nets的主要分析技术 | 第36-38页 |
| 2.6.3 CP-nets应用现状 | 第38-39页 |
| 2.7 本文研究的问题 | 第39-40页 |
| 2.8 本章小结 | 第40-41页 |
| 第三章 安全协议的形式化建模 | 第41-69页 |
| 3.1 方法概述 | 第41-42页 |
| 3.2 安全协议建模约束 | 第42-43页 |
| 3.3 Dolev-Yao攻击者模型的改进 | 第43-52页 |
| 3.3.1 Dolev-Yao攻击者模型 | 第43-45页 |
| 3.3.2 一种改进的攻击者模型 | 第45-47页 |
| 3.3.3 应用实例：NS协议 | 第47-52页 |
| 3.4 多并发会话划分分析方法 | 第52-57页 |
| 3.5 并发行为控制 | 第57页 |
| 3.6 实例系统：TMN协议 | 第57-68页 |
| 3.6.1 建模约束条件 | 第58-59页 |
| 3.6.2 TMN协议的数据建模 | 第59页 |
| 3.6.3 TMN协议的CP-nets建模 | 第59-64页 |
| 3.6.4 TMN协议的CP-nets模型安全属性验证分析 | 第64-68页 |
| 3.7 小结 | 第68-69页 |
| 第四章 基于CP-nets的安全协议模型验证与攻击序列生成 | 第69-94页 |
| 4.1 方法概述 | 第69-70页 |
| 4.2 ATG-CPN模型形式化定义 | 第70-73页 |
| 4.3 安全属性描述 | 第73-76页 |
| 4.3.1 保密性属性形式化定义 | 第73-75页 |
| 4.3.2 认证性属性形式化定义 | 第75-76页 |
| 4.4 基于安全属性违背事件的攻击序列生成算法—状态空间搜索法 | 第76-80页 |
| 4.4.1 安全属性违背事件 | 第77-78页 |
| 4.4.2 算法的形式描述 | 第78-79页 |
| 4.4.3 NS协议的攻击序列生成 | 第79-80页 |
| 4.5 On-the-fly安全协议攻击序列生成 | 第80-86页 |
| 4.5.1 ATG_X-CPN模型描述 | 第81-85页 |
| 4.5.2 On-the-fly攻击序列生成方法 | 第85-86页 |
| 4.6 实例分析：TMN协议系统 | 第86-92页 |
| 4.6.1 TMN协议的ATG-CPN模型 | 第86-87页 |
| 4.6.2 基于状态空间搜索方法的攻击序列生成与分析 | 第87-92页 |
| 4.7 本章小结 | 第92-94页 |
| 第五章 基于攻击目的的攻击序列选择 | 第94-112页 |
| 5.1 方法概述 | 第94-95页 |
| 5.2 安全协议的主要攻击方式 | 第95-100页 |
| 5.2.1 攻击者的攻击策略和攻击行为 | 第96-99页 |
| 5.2.2 攻击策略的评判 | 第99-100页 |
| 5.3 攻击目的AP-CPN形式化描述 | 第100-106页 |
| 5.4 基于攻击目的的攻击序列选择方法 | 第106-107页 |
| 5.5 实例分析：TMN协议系统 | 第107-111页 |
| 5.5.1 TMN协议的攻击策略评判 | 第107-108页 |
| 5.5.2 TMN协议的攻击策略建模 | 第108-110页 |
| 5.5.3 TMN协议的攻击序列选择生成 | 第110-111页 |
| 5.6 本章小结 | 第111-112页 |
| 第六章 结论及进一步工作 | 第112-114页 |
| 6.1 论文的主要结论 | 第112-113页 |
| 6.2 进一步的研究工作 | 第113-114页 |
| 参考文献 | 第114-121页 |
| 致谢 | 第121-122页 |
| 攻读博士学位期间发表论文 | 第122页 |
| 攻读博士学位期间主持和参加的科研项目 | 第122页 |
