| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第1章 引言 | 第8-12页 |
| ·安全协议的研究及意义 | 第8页 |
| ·国内外研究进展及我的研究工作 | 第8-10页 |
| ·论文各部分的结构安排 | 第10-12页 |
| 第2章 安全协议 | 第12-27页 |
| ·安全协议介绍 | 第12-15页 |
| ·安全协议的基本概念 | 第12-13页 |
| ·安全协议的分类 | 第13-15页 |
| ·安全协议的属性 | 第15-16页 |
| ·安全协议的漏洞 | 第16-23页 |
| ·重放攻击 | 第18-20页 |
| ·并行会话攻击 | 第20-21页 |
| ·Oracle 攻击 | 第21页 |
| ·类型攻击 | 第21-23页 |
| ·中间人攻击 | 第23页 |
| ·安全协议的设计原则 | 第23-26页 |
| ·Abadi 和Needham 的11 条原则 | 第24-25页 |
| ·Anderson 和Needham 的8 条原则 | 第25-26页 |
| ·本章小结 | 第26-27页 |
| 第3章 安全协议形式化分析方法 | 第27-53页 |
| ·形式化方法概述 | 第27-28页 |
| ·安全协议形式化分析方法分类 | 第28-31页 |
| ·信念逻辑方法 | 第29页 |
| ·模型检测方法 | 第29-31页 |
| ·推理验证方法 | 第31页 |
| ·入侵者模型 | 第31-33页 |
| ·Dolev-Yao 模型 | 第31-32页 |
| ·spi 演算 | 第32-33页 |
| ·概率模型 | 第33页 |
| ·BAN 逻辑 | 第33-39页 |
| ·推理规则 | 第34-36页 |
| ·理想化的协议 | 第36-37页 |
| ·BAN 逻辑分析协议步骤 | 第37页 |
| ·BAN 逻辑的优点和缺点 | 第37-38页 |
| ·BAN 逻辑的扩展 | 第38-39页 |
| ·CASPER/FDR | 第39-48页 |
| ·CSP 模型 | 第39-40页 |
| ·FDR 工具 | 第40页 |
| ·Casper/FDR 简介 | 第40-43页 |
| ·Casper/FDR 分析NSPK 协议 | 第43-48页 |
| ·颜色PETRI 网 | 第48-52页 |
| ·颜色Petri 网简介 | 第48-49页 |
| ·颜色Petri 网描述NSPK 协议 | 第49-50页 |
| ·颜色Petri 网分析NSPK 协议 | 第50-52页 |
| ·本章小结 | 第52-53页 |
| 第4章 安全协议组合分析验证方法 | 第53-80页 |
| ·安全协议的组合分析验证 | 第53-57页 |
| ·组合分析验证框图 | 第53-54页 |
| ·两个CAPSL 连接器 | 第54-57页 |
| ·CAPSL 规范语言 | 第57-63页 |
| ·安全协议的形式规范言简介 | 第57-58页 |
| ·CAPSL 简介 | 第58-62页 |
| ·NSPK 的CAPSL 规范 | 第62-63页 |
| ·CAPSL 到 CASPER/FDR 的连接器 | 第63-70页 |
| ·Casper/FDR | 第63-64页 |
| ·CAPSL 到 Casper 的连接器 | 第64-67页 |
| ·CAPSL 到 Casper 连接器的实验结果 | 第67-70页 |
| ·CAPSL 到 HLPSL/OFMC 的连接器 | 第70-78页 |
| ·HLPSL/OFMC | 第70-73页 |
| ·CAPSL 到 HLPSL 的连接器 | 第73-76页 |
| ·CAPSL 到 HLPSL 连接器的实验结果 | 第76-78页 |
| ·本章小结 | 第78-80页 |
| 第5章 结论 | 第80-82页 |
| ·论文主要结论 | 第80-81页 |
| ·进一步的研究工作 | 第81-82页 |
| 参考文献 | 第82-86页 |
| 致谢 | 第86-87页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第87页 |