| 表目录 | 第1-8页 |
| 图目录 | 第8-9页 |
| 摘要 | 第9-10页 |
| ABSTRACT | 第10-11页 |
| 第一章 绪论 | 第11-14页 |
| ·研究背景 | 第11页 |
| ·研究现状 | 第11-12页 |
| ·本文的贡献 | 第12-13页 |
| ·本文的组织结构 | 第13-14页 |
| 第二章 形式化方法和辅助证明工具的研究 | 第14-21页 |
| ·形式化方法 | 第14-17页 |
| ·形式化描述 | 第14-15页 |
| ·形式化验证 | 第15-16页 |
| ·形式化方法的优点 | 第16-17页 |
| ·形式化方法的局限性 | 第17页 |
| ·辅助证明工具 | 第17-20页 |
| ·辅助证明工具研究 | 第17-18页 |
| ·6种辅助证明工具的比较 | 第18-20页 |
| ·结论 | 第20-21页 |
| 第三章 Coq的元语言与功能分析 | 第21-34页 |
| ·理论背景 | 第21-26页 |
| ·直觉主义逻辑 | 第21-23页 |
| ·简单类型λ-演算 | 第23-24页 |
| ·Curry-Howard同构 | 第24-26页 |
| ·归纳构造演算 | 第26-29页 |
| ·CIC的项 | 第26-27页 |
| ·CIC的类型规则(typing rules) | 第27页 |
| ·CIC的归约规则(reduction rules) | 第27-29页 |
| ·Coq功能研究 | 第29-33页 |
| ·Coq作为逻辑系统 | 第29-31页 |
| ·Ceq作为编程语言 | 第31-33页 |
| ·结论 | 第33-34页 |
| 第四章 协议安全性保证的研究与实现 | 第34-52页 |
| ·网络协议安全性保证问题的提出 | 第34页 |
| ·网络协议安全性保证的相关工作 | 第34-35页 |
| ·实例分析:停止等待协议的验证 | 第35-42页 |
| ·协议概述 | 第35-36页 |
| ·协议模型 | 第36-37页 |
| ·协议形式化 | 第37-41页 |
| ·正确性证明 | 第41-42页 |
| ·平台和工具 | 第42页 |
| ·小结 | 第42页 |
| ·安全协议安全性保证问题的提出 | 第42-43页 |
| ·安全协议安全性保证相关工作 | 第43-45页 |
| ·实例分析: Otway-Rees协议 | 第45-50页 |
| ·协议概述 | 第45-46页 |
| ·类型缺陷攻击 | 第46页 |
| ·协议模型 | 第46-47页 |
| ·协议形式化 | 第47-49页 |
| ·协议证明 | 第49-50页 |
| ·平台和工具 | 第50页 |
| ·小结 | 第50页 |
| ·结论 | 第50-52页 |
| 第五章 程序安全性保证的研究与实现 | 第52-61页 |
| ·程序安全性保证问题的提出 | 第52页 |
| ·程序安全性保证相关工作 | 第52-53页 |
| ·基于CIC的函数式语言的验证 | 第53-57页 |
| ·直接定义ML函数 | 第53-54页 |
| ·程序提取 | 第54-57页 |
| ·基于CIC的命令式语言的验证 | 第57-60页 |
| ·Hoare逻辑 | 第57-58页 |
| ·工具Why | 第58-60页 |
| ·结论 | 第60-61页 |
| 结束语 | 第61-62页 |
| 参考文献 | 第62-65页 |
| 作者简历 攻读硕士期间取得的学术成果 | 第65-66页 |
| 一、个人简历 | 第65页 |
| 二、攻读硕士期间取得的学术成果 | 第65-66页 |
| 致谢 | 第66页 |