安全协议形式化分析理论与应用研究
| 作者简介 | 第1-6页 |
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-12页 |
| 第一章 绪论 | 第12-22页 |
| ·研究背景及意义 | 第12-15页 |
| ·发展历史及研究现状 | 第15-18页 |
| ·本文所做的工作 | 第18-20页 |
| ·研究思路 | 第18-19页 |
| ·研究内容 | 第19-20页 |
| ·论文结构 | 第20-22页 |
| 第二章 安全协议形式化分析方法综述 | 第22-38页 |
| ·安全协议 | 第22-26页 |
| ·基本概念 | 第22-23页 |
| ·安全属性 | 第23-24页 |
| ·安全协议分类 | 第24-26页 |
| ·形式化分析的必要性 | 第26-28页 |
| ·非形式化方法概念及不足 | 第26-27页 |
| ·形式化方法的概念及优点 | 第27页 |
| ·两者之间的关系 | 第27-28页 |
| ·形式化分析方法的构成 | 第28-30页 |
| ·形式化描述 | 第28-29页 |
| ·形式化设计 | 第29-30页 |
| ·形式化验证 | 第30页 |
| ·基于符号的形式化方法 | 第30-34页 |
| ·分类 | 第30-31页 |
| ·基础模型 | 第31-32页 |
| ·基于推理的模态逻辑方法 | 第32页 |
| ·基于模型检测的形式化方法 | 第32-33页 |
| ·基于定理证明的形式化方法 | 第33页 |
| ·三种基于符号的形式化方法比较 | 第33-34页 |
| ·基于计算复杂性的形式化方法 | 第34-36页 |
| ·CK模型 | 第34-35页 |
| ·BCP模型 | 第35页 |
| ·UC模型 | 第35页 |
| ·与基于符号的形式化方法比较 | 第35-36页 |
| ·小结 | 第36-38页 |
| 第三章 基于DDMP的协议形式化分析模型 | 第38-54页 |
| ·DDMP模型 | 第38-40页 |
| ·模型提出背景 | 第38-39页 |
| ·DDMP模型 | 第39页 |
| ·国内外研究现状 | 第39-40页 |
| ·协议演绎系统 | 第40-41页 |
| ·协议组合逻辑 | 第41-49页 |
| ·形式化系统构成 | 第41页 |
| ·协议建模 | 第41-43页 |
| ·语法与语义 | 第43-44页 |
| ·证明系统 | 第44-47页 |
| ·PCL与其它形式化方法比较 | 第47-49页 |
| ·安全协议形式化分析模型设计 | 第49-51页 |
| ·安全协议的系统模型 | 第49-50页 |
| ·形式化分析一般模型SPFAM | 第50-51页 |
| ·基于DDMP的协议形式化分析模型设计 | 第51-53页 |
| ·DDMP-SPFAM | 第51-52页 |
| ·基于DDMP的协议形式化分析算法 | 第52-53页 |
| ·小结 | 第53-54页 |
| 第四章 基于协议组合逻辑的安全协议证明 | 第54-62页 |
| ·引言 | 第54页 |
| ·基于PCL的协议证明方法 | 第54-55页 |
| ·Helsinki协议 | 第55-57页 |
| ·符号约定 | 第55-56页 |
| ·基本假设 | 第56页 |
| ·Helsinki协议 | 第56-57页 |
| ·Helsinki协议分析及改进 | 第57-58页 |
| ·协议缺陷分析 | 第57-58页 |
| ·协议改进 | 第58页 |
| ·改进型Helsinki协议建模 | 第58-59页 |
| ·协议本身建模 | 第58-59页 |
| ·安全属性建模 | 第59页 |
| ·改进型Helsinki协议的安全性证明 | 第59-60页 |
| ·小结 | 第60-62页 |
| 第五章 安全协议的可组合性分析与证明 | 第62-78页 |
| ·引言 | 第62-63页 |
| ·安全协议的可组合性分析与证明方法 | 第63-65页 |
| ·协议组合逻辑 | 第63页 |
| ·通用可组合安全框架 | 第63-64页 |
| ·两种可组合分析方法的比较 | 第64-65页 |
| ·PCL协议组合证明方法 | 第65-67页 |
| ·并行组合及安全性证明 | 第65-66页 |
| ·顺序组合及安全性证明 | 第66-67页 |
| ·Otway-Rees协议分析及改进 | 第67-71页 |
| ·符号约定 | 第67页 |
| ·协议描述 | 第67-69页 |
| ·协议缺陷分析 | 第69-70页 |
| ·协议改进 | 第70-71页 |
| ·改进型的Otway-Rees协议建模 | 第71-72页 |
| ·PCL扩展 | 第71页 |
| ·协议本身建模 | 第71-72页 |
| ·安全属性建模 | 第72页 |
| ·改进型的Otway-Rees协议证明 | 第72-76页 |
| ·子模块Q1 证明 | 第73页 |
| ·子模块Q2 证明 | 第73-75页 |
| ·子模块Q3 证明 | 第75-76页 |
| ·协议组合证明 | 第76页 |
| ·可组合安全的发展趋势 | 第76-77页 |
| ·小结 | 第77-78页 |
| 第六章 PDS扩展及安全协议设计 | 第78-90页 |
| ·前言 | 第78-79页 |
| ·安全协议的设计原则 | 第79-80页 |
| ·研究现状 | 第79页 |
| ·设计原则 | 第79-80页 |
| ·协议演绎系统 | 第80-84页 |
| ·符号约定 | 第81页 |
| ·组件集合 | 第81-82页 |
| ·操作集合 | 第82-84页 |
| ·PDS扩展 | 第84-86页 |
| ·协议组件扩展 | 第84-85页 |
| ·精炼操作扩展 | 第85页 |
| ·转换操作扩展 | 第85-86页 |
| ·安全协议演绎设计 | 第86-88页 |
| ·小结 | 第88-90页 |
| 第七章 全文总结与研究展望 | 第90-94页 |
| ·全文总结 | 第90页 |
| ·研究展望 | 第90-94页 |
| 致谢 | 第94-96页 |
| 参考文献 | 第96-106页 |
| 攻读博士学位期间的研究成果 | 第106-107页 |
