| 目录 | 第1-5页 |
| 摘要 | 第5-6页 |
| ABSTRACT | 第6-7页 |
| 第一章 绪论 | 第7-16页 |
| ·引言 | 第7页 |
| ·密码协议形式化分析方法 | 第7-10页 |
| ·密码协议自动化分析技术研究现状 | 第10-11页 |
| ·逻辑程序设计语言Prolog | 第11-15页 |
| ·Prolog语言简介 | 第11-13页 |
| ·事实与规则 | 第13页 |
| ·询问 | 第13-15页 |
| ·论文主要研究内容 | 第15-16页 |
| 第二章 Spi演算及其对密码协议的分析方法 | 第16-24页 |
| ·Spi演算 | 第16-21页 |
| ·Spi演算语法 | 第16-18页 |
| ·自由与受限 | 第18-19页 |
| ·反应关系 | 第19-20页 |
| ·测试等价 | 第20-21页 |
| ·Spi演算对密码协议的形式化分析 | 第21-23页 |
| ·本章小结 | 第23-24页 |
| 第三章 扩展Spi演算及其对密码协议安全属性的分析 | 第24-46页 |
| ·扩展Spi演算 | 第24-30页 |
| ·基本语法 | 第24-27页 |
| ·秘密性 | 第27-28页 |
| ·认证性 | 第28-29页 |
| ·协议实例分析 | 第29-30页 |
| ·基于扩展Spi演算的类型系统 | 第30-43页 |
| ·基本原理 | 第31页 |
| ·构建基于扩展Spi演算类型系统的基本条件 | 第31-33页 |
| ·基于扩展Spi演算的类型系统 | 第33-39页 |
| ·基于扩展Spi演算类型系统的安全属性 | 第39-43页 |
| ·类型系统对密码协议秘密性的分析 | 第43-45页 |
| ·本章小结 | 第45-46页 |
| 第四章 基于扩展Spi演算的密码协议自动化分析器 | 第46-67页 |
| ·密码协议自动化分析器 | 第46-52页 |
| ·分析器工作原理 | 第46-47页 |
| ·分析器输入语法 | 第47-50页 |
| ·自动翻译器 | 第50页 |
| ·逻辑推导模块 | 第50-52页 |
| ·描述协议的事实与规则 | 第52-59页 |
| ·模式与事实 | 第52-53页 |
| ·攻击者初始知识 | 第53-54页 |
| ·攻击者计算能力 | 第54-55页 |
| ·协议的描述 | 第55-56页 |
| ·进程转换 | 第56-58页 |
| ·规则基础 | 第58-59页 |
| ·分析器对密码协议安全属性的分析 | 第59-66页 |
| ·秘密性 | 第60-64页 |
| ·单射一致性和非单射一致性 | 第64-66页 |
| ·本章小结 | 第66-67页 |
| 第五章 自动翻译器的设计与实现 | 第67-74页 |
| ·词法分析 | 第67-69页 |
| ·语法分析 | 第69-72页 |
| ·转换算法 | 第72-73页 |
| ·本章小结 | 第73-74页 |
| 结束语 | 第74-76页 |
| 致谢 | 第76-77页 |
| 参考文献 | 第77-81页 |
| 附录：函数Ф的定义 | 第81-83页 |