| 摘要 | 第1-8页 |
| Abstract | 第8-9页 |
| 第一章 绪论 | 第9-18页 |
| ·研究背景及意义 | 第9页 |
| ·密码协议形式化分析方法 | 第9-12页 |
| ·符号方法 | 第9-12页 |
| ·计算方法 | 第12页 |
| ·计算可靠性研究现状 | 第12-16页 |
| ·逻辑方法与模拟方法 | 第12-15页 |
| ·LMMS:概率多项式时间下进程演算方法 | 第15页 |
| ·符号方法的密码学扩充 | 第15页 |
| ·总结 | 第15-16页 |
| ·论文主要内容 | 第16-18页 |
| 第二章 Micciancio-Warinschi方法的分析与研究 | 第18-27页 |
| ·公钥加密方案的安全性 | 第18-19页 |
| ·双方协议 | 第19-22页 |
| ·协议语法 | 第19页 |
| ·协议执行模型—符号模型与计算模型 | 第19-22页 |
| ·符号模型的计算可靠性 | 第22-25页 |
| ·本章小结 | 第25-27页 |
| 第三章 扩展 Micciancio-Warinschi方法 | 第27-60页 |
| ·扩展协议语法 | 第27-29页 |
| ·标记 | 第27-28页 |
| ·标记消息 | 第28-29页 |
| ·标记角色 | 第29页 |
| ·扩展标记符号模型 | 第29-35页 |
| ·消息项 | 第29-30页 |
| ·攻击者模型 | 第30-31页 |
| ·协议描述 | 第31-33页 |
| ·符号安全性建模 | 第33-35页 |
| ·扩展计算模型 | 第35-48页 |
| ·密码方案的安全定义 | 第35-45页 |
| ·计算语义 | 第45-47页 |
| ·计算安全性建模 | 第47-48页 |
| ·计算可靠性论证 | 第48-53页 |
| ·联系计算迹与符号迹 | 第48-52页 |
| ·联系符号安全性质与计算安全性质 | 第52-53页 |
| ·实例分析 | 第53-59页 |
| ·NS公钥协议实例分析 | 第53-56页 |
| ·NSL公钥协议实例分析 | 第56-58页 |
| ·结果分析 | 第58-59页 |
| ·本章小结 | 第59-60页 |
| 第四章 扩展标记符号模型的随机变换 | 第60-70页 |
| ·随机变换 | 第60-62页 |
| ·协议规范建模 | 第60页 |
| ·攻击者建模 | 第60-61页 |
| ·安全性质建模 | 第61-62页 |
| ·随机变换规则 | 第62-64页 |
| ·随机变换的正确性证明 | 第64-69页 |
| ·本章小结 | 第69-70页 |
| 第五章 扩展标记符号模型的计算可靠性验证 | 第70-88页 |
| ·ProVerif | 第71-73页 |
| ·ProVerif的基本结构 | 第71-72页 |
| ·Horn语句 | 第72-73页 |
| ·CryptoVerif | 第73-76页 |
| ·语法 | 第73-75页 |
| ·安全特性 | 第75页 |
| ·CryptoVerif输入语法 | 第75-76页 |
| ·计算可靠性验证的结构及工作流程 | 第76-78页 |
| ·计算可靠性验证的实现 | 第78-84页 |
| ·输入部分 | 第78页 |
| ·核心处理部分 | 第78-84页 |
| ·结果输出部分 | 第84页 |
| ·实验结果与分析 | 第84-87页 |
| ·本章小结 | 第87-88页 |
| 第六章 结束语 | 第88-90页 |
| ·论文工作总结 | 第88-89页 |
| ·工作展望 | 第89-90页 |
| 参考文献 | 第90-95页 |
| 作者简历 攻读硕士学位期间完成的主要工作 | 第95-96页 |
| 致谢 | 第96页 |