| 中文摘要 | 第1-11页 |
| Abstract | 第11-13页 |
| 符号与缩略语 | 第13-15页 |
| 第一章 绪论 | 第15-31页 |
| ·研究背景及意义 | 第16-18页 |
| ·研究现状 | 第18-27页 |
| ·计算可靠性方法 | 第18-23页 |
| ·计算模型下的直接证明法 | 第23-24页 |
| ·基于可模拟性的方法 | 第24-26页 |
| ·研究现状评述 | 第26-27页 |
| ·研究思路 | 第27-28页 |
| ·研究内容和章节安排 | 第28-31页 |
| 第二章 CryptoVerif 的扩展与分析 | 第31-59页 |
| ·CryptoVerif 的协议模型和证明方法简述 | 第32-35页 |
| ·协议模型 | 第32-33页 |
| ·证明方法 | 第33-35页 |
| ·对Zhou-Gollmann 不可否认协议的辅助证明 | 第35-45页 |
| ·ZG 协议简介 | 第35-36页 |
| ·证据伪造攻击 | 第36-37页 |
| ·ZG 协议的建模 | 第37-39页 |
| ·安全属性的验证 | 第39-45页 |
| ·对Diffie-Hellman 密钥交换协议的自动证明 | 第45-56页 |
| ·DHKE 及相关假设 | 第45页 |
| ·DHKE 的形式化需求 | 第45-46页 |
| ·观测等价模型 | 第46-47页 |
| ·模型可靠性 | 第47-51页 |
| ·公钥Kerberos 协议安全属性的验证 | 第51-56页 |
| ·CryptoVerif 建模能力分析 | 第56-58页 |
| ·本章小结 | 第58-59页 |
| 第三章 计算模型下协议建模方法研究 | 第59-79页 |
| ·基于进程模型的协议描述语言 | 第60-67页 |
| ·描述语言的语法 | 第60-62页 |
| ·描述语言的执行语义 | 第62-63页 |
| ·密码算法的定义 | 第63-66页 |
| ·敌手能力模型 | 第66-67页 |
| ·执行迹属性的逻辑模型 | 第67-70页 |
| ·逻辑的语法 | 第67-68页 |
| ·逻辑的语义 | 第68-70页 |
| ·认证性建模 | 第70-71页 |
| ·协议建模示例 | 第71-75页 |
| ·Needham-Scheoder-Lowe 协议的建模 | 第71-73页 |
| ·Challenge-Response 协议的建模 | 第73-75页 |
| ·与CPCL 建模能力的比较 | 第75-76页 |
| ·本章小结 | 第76-79页 |
| 第四章 计算可靠的定性验证方法研究 | 第79-107页 |
| ·计算可靠的定性证明系统 | 第80-97页 |
| ·推理规则 | 第80页 |
| ·公理集 | 第80-97页 |
| ·证明系统的计算可靠性 | 第97-99页 |
| ·与CPCL 证明系统的比较 | 第99-101页 |
| ·证明系统的验证与测试 | 第101-105页 |
| ·NSL 协议认证性的证明 | 第101-105页 |
| ·验证结果分析 | 第105页 |
| ·本章小结 | 第105-107页 |
| 第五章 计算可靠的定量验证方法研究 | 第107-123页 |
| ·协议逻辑的概率扩展 | 第107-109页 |
| ·计算可靠的定量证明系统 | 第109-112页 |
| ·概率公理 | 第109-110页 |
| ·随机数概率公理 | 第110-111页 |
| ·密码学概率公理 | 第111-112页 |
| ·CPCL 的概率扩展能力分析 | 第112-113页 |
| ·定量证明系统的计算可靠性 | 第113-116页 |
| ·证明系统的验证与测试 | 第116-120页 |
| ·双向认证性的证明 | 第116-119页 |
| ·验证结果分析 | 第119-120页 |
| ·本章小结 | 第120-123页 |
| 第六章 总结与展望 | 第123-125页 |
| 致谢 | 第125-127页 |
| 参考文献 | 第127-139页 |
| 作者在学期间取得的学术成果 | 第139-141页 |
| 作者在学期间参与的主要科研项目 | 第141-143页 |
| 附录A 论文中用到的进程脚本 | 第143-152页 |
| A.1 ZG 协议的进程模型 | 第143-146页 |
| A.2 DHINIT 协议的进程模型 | 第146-152页 |
