安全协议分析的形式化理论与方法--基于定理证明的安全协议建模研究
| 第一章 绪论 | 第1-24页 |
| ·引言 | 第16页 |
| ·课题研究背景 | 第16-18页 |
| ·安全协议分析的形式化建模理论 | 第18-22页 |
| ·Dolev-Yao模型 | 第18-20页 |
| ·模态逻辑 | 第20页 |
| ·有限状态机 | 第20-21页 |
| ·进程代数 | 第21-22页 |
| ·本文主要工作 | 第22-23页 |
| ·本文主要内容 | 第23-24页 |
| 第二章 安全协议分析 | 第24-36页 |
| ·引言 | 第24-25页 |
| ·密码协议安全目标 | 第25-29页 |
| ·安全目标分类 | 第25-26页 |
| ·安全目标规范 | 第26-29页 |
| ·安全目标验证方法及其理论基础 | 第29-33页 |
| ·逻辑推理方法 | 第29-30页 |
| ·模型检测方法 | 第30-32页 |
| ·定理证明方法 | 第32页 |
| ·类型检测方法 | 第32-33页 |
| ·安全协议的可验证性问题 | 第33-35页 |
| ·Ping-Pong协议 | 第34-35页 |
| ·关于密码协议安全性判定 | 第35页 |
| ·本章小结 | 第35-36页 |
| 第三章 消息结构描述 | 第36-48页 |
| ·引言 | 第36页 |
| ·消息空间结构 | 第36-41页 |
| ·消息空间 | 第37-38页 |
| ·语句运算 | 第38-41页 |
| ·语句结构及其性质 | 第41-47页 |
| ·语句运算假设 | 第41-43页 |
| ·语句结构分析 | 第43-47页 |
| ·本章小结 | 第47-48页 |
| 第四章 消息交换次序 | 第48-66页 |
| ·引言 | 第48-49页 |
| ·消息事件 | 第49-54页 |
| ·事件及其通信关系 | 第49-52页 |
| ·事件顺序关系 | 第52-54页 |
| ·路径描述 | 第54-62页 |
| ·可达路径 | 第54-60页 |
| ·主协议的独立性 | 第60-62页 |
| ·例子：Kerberos协议描述及其独立性分析 | 第62-65页 |
| ·本章小结 | 第65-66页 |
| 第五章 不变集及其生成 | 第66-80页 |
| ·引言 | 第66-67页 |
| ·不变集 | 第67-71页 |
| ·诚实性判定条件的可满足性 | 第71-76页 |
| ·诚实性判定 | 第71-74页 |
| ·判定条件的可满足性定理 | 第74-76页 |
| ·不变集生成算法 | 第76-78页 |
| ·例子：一类带MAC载荷安全协议的建模 | 第78-79页 |
| ·本章小结 | 第79-80页 |
| 第六章 主体进程表示 | 第80-100页 |
| ·引言 | 第80-81页 |
| ·关于Spi演算 | 第81-88页 |
| ·语法与形式语义 | 第81-85页 |
| ·进程等价 | 第85-87页 |
| ·基于Spi演算的安全目标验证 | 第87-88页 |
| ·进程描述语言 | 第88-99页 |
| ·通信事件及其关系 | 第88-89页 |
| ·进程及其演算算子 | 第89-93页 |
| ·进程演算算法 | 第93-97页 |
| ·进程互模拟关系 | 第97-99页 |
| ·本章小结 | 第99-100页 |
| 第七章 事件图模型 | 第100-122页 |
| ·引言 | 第100-102页 |
| ·事件图结构 | 第102-110页 |
| ·局部(子图) | 第103-105页 |
| ·结构约束条件 | 第105-110页 |
| ·事件图生成 | 第110-116页 |
| ·图元 | 第110-111页 |
| ·结构控制算子 | 第111-114页 |
| ·事件图生成算法 | 第114-116页 |
| ·事件图等价 | 第116-118页 |
| ·图元的互模拟 | 第116-117页 |
| ·事件图的冗余消除 | 第117-118页 |
| ·例子：NSL协议事件图的生成 | 第118-121页 |
| ·本章小结 | 第121-122页 |
| 第八章 总结与展望 | 第122-124页 |
| ·全文总结 | 第122-123页 |
| ·后续研究工作展望 | 第123-124页 |
| 参考文献 | 第124-134页 |
| 攻读博士学位期间完成的论文 | 第134页 |
