| 摘要 | 第1-13页 |
| ABSTRACT | 第13-16页 |
| 第一章 绪论 | 第16-30页 |
| ·研究背景 | 第16-21页 |
| ·研究对象和成果 | 第21-23页 |
| ·相关工作 | 第23-29页 |
| ·基于理想加密假设的安全协议分析与验证 | 第23-24页 |
| ·基于计算语义的安全方案和协议的分析与验证 | 第24-25页 |
| ·抽象解释理论 | 第25-26页 |
| ·时间敏感安全协议的验证 | 第26-27页 |
| ·安全协议验证工具 | 第27-28页 |
| ·基于分析工具的复杂安全协议的分析与验证 | 第28-29页 |
| ·本文结构 | 第29-30页 |
| 第二章 安全协议模型与验证基础 | 第30-42页 |
| ·引言 | 第30-31页 |
| ·安全协议的预备知识 | 第31-32页 |
| ·安全协议的进程代数模型 | 第32-33页 |
| ·安全协议的Horn 逻辑模型 | 第33-37页 |
| ·Horn 逻辑语法 | 第33-34页 |
| ·诚实角色模型 | 第34-35页 |
| ·安全协议攻击者模型 | 第35-36页 |
| ·安全性质 | 第36-37页 |
| ·安全协议验证 | 第37-40页 |
| ·小结 | 第40-42页 |
| 第三章 安全协议的反例构造算法 | 第42-58页 |
| ·引言 | 第42-43页 |
| ·反例构造原理 | 第43-47页 |
| ·反例构造算法 | 第47-54页 |
| ·基本数据结构 | 第47-48页 |
| ·逻辑弱推导树构造算法 | 第48-49页 |
| ·拆分结点算法 | 第49-51页 |
| ·攻击序列生成算法 | 第51-52页 |
| ·算法优化与复杂性分析 | 第52-54页 |
| ·实验 | 第54-57页 |
| ·小结 | 第57-58页 |
| 第四章 安全协议抽象-精化迭代验证框架 | 第58-82页 |
| ·引言 | 第58-59页 |
| ·不停机性的动态刻画与预测 | 第59-67页 |
| ·不动点计算的不停机特征 | 第61-66页 |
| ·不动点计算的不停机性预测 | 第66-67页 |
| ·不动点计算的抽象与精化 | 第67-74页 |
| ·抽象不动点计算 | 第67-71页 |
| ·抽象不动点的精化迭代 | 第71-74页 |
| ·不动点计算的局部抽象与精化 | 第74-78页 |
| ·局部抽象不动点计算 | 第74-76页 |
| ·局部抽象不动点的迭代精化 | 第76-78页 |
| ·实验 | 第78-80页 |
| ·小结 | 第80-82页 |
| 第五章 时间敏感安全协议的建模与验证 | 第82-110页 |
| ·引言 | 第82-84页 |
| ·进程代数模型 | 第84-85页 |
| ·带时间约束的Horn 逻辑模型 | 第85-89页 |
| ·带时间约束的 Horn 逻辑语法 | 第86页 |
| ·进程代数模型到 Horn 逻辑模型的转换 | 第86-88页 |
| ·安全协议攻击者模型 | 第88页 |
| ·安全性质 | 第88-89页 |
| ·验证 | 第89-93页 |
| ·约束系统 | 第93-98页 |
| ·约束系统的特性 | 第93-95页 |
| ·约束系统的求解算法 | 第95-98页 |
| ·约束系统的抽象 | 第98-103页 |
| ·时间敏感安全协议的分析与验证 | 第103-107页 |
| ·Denning-Sacco协议的分析与验证 | 第103-105页 |
| ·大嘴青蛙协议的分析与验证 | 第105-107页 |
| ·小结 | 第107-110页 |
| 第六章 安全协议验证工具 SPVT-II | 第110-130页 |
| ·引言 | 第110-112页 |
| ·工具的结构 | 第112-122页 |
| ·协议输入与模型转化部分 | 第112-114页 |
| ·协议精确验证部分 | 第114-119页 |
| ·抽象协议验证部分 | 第119-120页 |
| ·反例检测与生成部分 | 第120-122页 |
| ·SPVT-II 的主要操作 | 第122-124页 |
| ·实验 | 第124-128页 |
| ·小结 | 第128-130页 |
| 第七章 Kerberos 协议的分析与验证 | 第130-140页 |
| ·引言 | 第130-132页 |
| ·Kerberos 协议简介 | 第132-135页 |
| ·协议的建模与验证 | 第135-138页 |
| ·诚实角色模型 | 第135-137页 |
| ·验证结果 | 第137-138页 |
| ·小结 | 第138-140页 |
| 结束语 | 第140-144页 |
| 致谢 | 第144-148页 |
| 参考文献 | 第148-158页 |
| 作者在学期间取得的学术成果 | 第158-160页 |
| 附录A 本文使用到的安全协议 | 第160-176页 |
| A.1 简化 Needham-Schroeder 公钥协议 | 第160-162页 |
| A.2 Woo-Lam 认证协议版本Π | 第162-164页 |
| A.3 Woo-Lam认证协议版本Π1 | 第164-165页 |
| A.4 Woo-Lam认证协议版本Π2 | 第165-166页 |
| A.5 Woo-Lam 认证协议版本Π3 | 第166-167页 |
| A.6 Woo-Lam 认证协议版本Πf | 第167-169页 |
| A.7 Otway-Rees 认证协议 | 第169-170页 |
| A.8 Yahalom 认证协议 | 第170-172页 |
| A.9 Neuman-Stubblebine 认证协议 | 第172-174页 |
| A.10 Kao-ehow 重复认证协议 | 第174-176页 |
| 附录B Objective Caml 语言 | 第176-178页 |
| B.1 Objective Caml 简介 | 第176-177页 |
| B.2 模块函数介绍 | 第177-178页 |
| B.2.1 表模块List | 第177页 |
| B.2.2 哈希表模块 Hashtbl | 第177-178页 |
| B.2.3 字符串模块 String | 第178页 |
| B.2.4 常用运算符 | 第178页 |