| 图索引 | 第1-7页 |
| 摘要 | 第7-9页 |
| Abstract | 第9-12页 |
| 第一章 绪论 | 第12-30页 |
| ·研究背景 | 第12-14页 |
| ·相关研究工作 | 第14-25页 |
| ·类BAN逻辑方法 | 第16-18页 |
| ·基于模型检验的方法 | 第18-20页 |
| ·基于定理证明的方法 | 第20-24页 |
| ·其它相关工作 | 第24-25页 |
| ·研究对象与成果 | 第25-27页 |
| ·本文结构 | 第27-30页 |
| 第二章 安全协议描述与安全协议模型 | 第30-48页 |
| ·安全协议和安全协议攻击描述的标准方式 | 第30-32页 |
| ·安全协议模型 | 第32-39页 |
| ·基于线性逻辑的安全协议模型 | 第32-33页 |
| ·基于进程代数的安全协议模型 | 第33-35页 |
| ·抽象解释理论 | 第35-37页 |
| ·基于Horn逻辑的安全协议模型 | 第37-39页 |
| ·安全协议的扩展模型 | 第39-46页 |
| ·基于进程代数的安全协议扩展模型 | 第40-42页 |
| ·基于Horn逻辑的安全协议扩展模型 | 第42-45页 |
| ·基于进程代数安全协议扩展模型到基于Horn逻辑安全协议扩展模型的转换 | 第45-46页 |
| ·本章小结 | 第46-48页 |
| 第三章 安全协议验证与反例自动构造 | 第48-80页 |
| ·保密性验证方法 | 第48-64页 |
| ·不满足保密性的安全协议反例的自动生成 | 第64-72页 |
| ·认证性验证方法与安全协议反例自动生成 | 第72-73页 |
| ·简化的Needham-Schroeder公钥认证协议的验证与反例自动生成 | 第73-75页 |
| ·一个有效的安全协议验证策略 | 第75-78页 |
| ·本章小结 | 第78-80页 |
| 第四章 ACUN理论合一化问题的合一化算法 | 第80-92页 |
| ·基本合一化问题和自由常数合一化问题的最一般合一化算子的求解算法 | 第82-83页 |
| ·联合理论合一化问题和优化分解算法描述 | 第83-85页 |
| ·一般合一化问题的合一化算法 | 第85-91页 |
| ·带线性自由常数约束合一化问题的最一般合一化算子的求解算法 | 第85-87页 |
| ·一般合一化问题的合一化算法 | 第87-90页 |
| ·实例 | 第90-91页 |
| ·本章小结 | 第91-92页 |
| 第五章 XOR安全协议的验证 | 第92-104页 |
| ·保密性的验证方法 | 第92-99页 |
| ·认证性的验证方法 | 第99-100页 |
| ·验证简化的Needham-Schroeder公钥认证协议的变种协议 | 第100-104页 |
| 第六章 SPVT：—个安全协议验证工具原型 | 第104-118页 |
| ·安全协议描述语言 | 第104-110页 |
| ·基于进程代数安全协议扩展模型到基于Horn逻辑安全协议扩展模型的自动转换 | 第110-114页 |
| ·与安全协议逻辑程序解形式不动点迭代计算和安全性质验证实现相关的几个算法 | 第114-118页 |
| 第七章 结束语 | 第118-123页 |
| ·工作总结 | 第118-121页 |
| ·工作展望 | 第121-123页 |
| 致谢 | 第123-125页 |
| 攻读博士学位期间发表的论文 | 第125-126页 |
| 攻读博士学位期间参与的科研项目 | 第126-127页 |
| 参考文献 | 第127-137页 |
