基于串空间模型分析与验证密码安全协议
| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 绪论 | 第8-12页 |
| ·研究背景 | 第8页 |
| ·本文研究的意义 | 第8-9页 |
| ·本文所做的工作 | 第9-12页 |
| 第二章 安全协议形式化分析综述 | 第12-24页 |
| ·密码学概述 | 第12-13页 |
| ·密码学简介 | 第12页 |
| ·基本概念 | 第12-13页 |
| ·密码体制 | 第13页 |
| ·安全协议 | 第13-18页 |
| ·协议和安全协议 | 第13-14页 |
| ·基本概念 | 第14-15页 |
| ·安全协议的功能 | 第15页 |
| ·安全协议的分类 | 第15-16页 |
| ·系统模型 | 第16-17页 |
| ·安全协议缺陷 | 第17-18页 |
| ·安全协议的形式化分析 | 第18-24页 |
| ·形式化分析概述 | 第18页 |
| ·基本假定 | 第18-19页 |
| ·形式化分析的历史 | 第19-20页 |
| ·形式化方法的分类 | 第20-24页 |
| 第三章 串空间理论与模型 | 第24-38页 |
| ·串空间简介 | 第24页 |
| ·串空间基础知识 | 第24-28页 |
| ·消息空间和代数假定 | 第24-25页 |
| ·基本概念 | 第25-26页 |
| ·丛和节点关系 | 第26-27页 |
| ·攻击者模型 | 第27-28页 |
| ·串空间理论应用实例 | 第28-34页 |
| ·NSL串空间 | 第29-30页 |
| ·响应者的认证性 | 第30-32页 |
| ·NS协议 | 第32页 |
| ·响应者随机数的秘密性 | 第32-33页 |
| ·发起者的秘密性和认证性 | 第33-34页 |
| ·理想和诚实 | 第34-38页 |
| ·理想 | 第34-35页 |
| ·入口点和诚实 | 第35-36页 |
| ·攻击者的能力 | 第36-38页 |
| 第四章 串空间理论扩展 | 第38-50页 |
| ·动机 | 第38页 |
| ·概念 | 第38-40页 |
| ·逻辑和模型 | 第40-41页 |
| ·语法 | 第40页 |
| ·语义 | 第40-41页 |
| ·安全协议目标的逻辑表示 | 第41-42页 |
| ·认证性目标 | 第41-42页 |
| ·秘密性目标 | 第42页 |
| ·安全协议验证算法 | 第42-50页 |
| ·命题公式化简 | 第42-43页 |
| ·模型检测算法 | 第43-45页 |
| ·下一状态函数 | 第45-47页 |
| ·状态删减规则 | 第47-50页 |
| 第五章 实验结果 | 第50-58页 |
| ·Needham-Schroeder公钥认证协议 | 第50-52页 |
| ·协议原型 | 第50页 |
| ·安全目标和假设 | 第50页 |
| ·实验结果 | 第50-52页 |
| ·Woo-Lam~4认证协议 | 第52-53页 |
| ·协议原型 | 第52页 |
| ·安全目标和假设 | 第52页 |
| ·实验结果 | 第52-53页 |
| ·TMN协议 | 第53-54页 |
| ·协议原型 | 第53-54页 |
| ·安全目标和假设 | 第54页 |
| ·实验结果 | 第54页 |
| ·Denning-Sacco协议 | 第54-55页 |
| ·原型及假设 | 第54-55页 |
| ·安全目标和假设 | 第55页 |
| ·实验结果 | 第55页 |
| ·部分实验结果 | 第55-58页 |
| 结论 | 第58-60页 |
| 参考文献 | 第60-64页 |
| 附录: AVSP程序系统 | 第64-68页 |
| 附.1 简介 | 第64页 |
| 附.2 协议文本范例 | 第64-65页 |
| 附.3 反例文本范例 | 第65-66页 |
| 附.4 程序界面 | 第66-68页 |
| 在学期间录用的文章 | 第68-70页 |
| 致谢 | 第70-71页 |
