基于串空间模型的协议验证技术研究
| 第一章 概述 | 第1-14页 |
| ·课题的背景及意义 | 第9-10页 |
| ·该领域目前的国内外研究状况 | 第10-13页 |
| ·论文研究工作 | 第13-14页 |
| 第二章 安全协议与串空间模型 | 第14-28页 |
| ·安全协议 | 第14-18页 |
| ·基本概念 | 第14页 |
| ·安全协议的目标 | 第14-15页 |
| ·安全协议的缺陷 | 第15-16页 |
| ·安全协议的形式化分析 | 第16-18页 |
| ·串空间模型与理论 | 第18-28页 |
| ·基本概念 | 第18-19页 |
| ·束与因果依赖关系 | 第19-21页 |
| ·项与加密 | 第21-22页 |
| ·正确性的定义 | 第22-23页 |
| ·协议描述 | 第23-25页 |
| ·入侵者 | 第25-28页 |
| 第三章 可追究性逻辑语义与串 | 第28-33页 |
| ·可追究性逻辑 | 第28-29页 |
| ·Kailar逻辑的符号含义 | 第29页 |
| ·串空间的计算模型 | 第29-30页 |
| ·Kailar逻辑的串语义 | 第30-31页 |
| ·实例——Bolignano协议 | 第31-33页 |
| 第四章 认证性的分析与证明 | 第33-44页 |
| ·协议认证性的意义与要求 | 第33-34页 |
| ·认证性测试方法 | 第34-40页 |
| ·认证性测试方法的原理 | 第34页 |
| ·元素和新元素 | 第34-35页 |
| ·可入侵密钥和安全密钥 | 第35-36页 |
| ·变形边和被变形边 | 第36页 |
| ·认证性测试 | 第36-38页 |
| ·认证性测试方法的应用——NS协议的认证性分析 | 第38-40页 |
| ·认证性测试方法的缺陷及改进 | 第40-44页 |
| ·认证性测试方法的问题 | 第40-41页 |
| ·认证性测试方法的改进 | 第41-44页 |
| 第五章 软件实现 | 第44-56页 |
| ·Maude系统 | 第44-50页 |
| ·编程框架 | 第44-47页 |
| ·面向对象说明 | 第47-50页 |
| ·NS协议的Maude分析 | 第50-56页 |
| ·协议基本数据类型的定义 | 第50-51页 |
| ·NS协议的描述 | 第51-53页 |
| ·认证性测试方法的描述 | 第53-56页 |
| 第六章 结束语 | 第56-58页 |
| ·研究总结 | 第56页 |
| ·进一步的工作 | 第56-58页 |
| 参考文献 | 第58-64页 |
| 致谢 | 第64-65页 |
| 在读期间发表的论文 | 第65页 |
