| 摘要 | 第1-9页 |
| ABSTRACT | 第9-13页 |
| 符号说明和缩略词 | 第13-14页 |
| 第一章 绪论 | 第14-27页 |
| ·、安全协议的一些基本概念 | 第14-17页 |
| ·、网络协议及会话 | 第14-15页 |
| ·、安全协议及分类 | 第15-16页 |
| ·、安全协议的服务 | 第16-17页 |
| ·、密码学的相关内容 | 第17-20页 |
| ·、常用的密码体制 | 第17-18页 |
| ·、常用的密码要素 | 第18-20页 |
| ·、针对安全协议的攻击 | 第20-24页 |
| ·、消息重放攻击 | 第20-22页 |
| ·、平行会话攻击 | 第22-23页 |
| ·、密码学缺陷攻击 | 第23-24页 |
| ·、本文工作的背景及意义 | 第24页 |
| ·、研究工作概要及论文安排 | 第24-27页 |
| 第二章 安全协议的形式化分析方法 | 第27-39页 |
| ·、符号理论 | 第27-33页 |
| ·、基于推理结构的方法 | 第27-29页 |
| ·、基于攻击结构的方法 | 第29-30页 |
| ·、基于证明结构的方法 | 第30-31页 |
| ·、符号理论的缺陷 | 第31-33页 |
| ·、计算理论 | 第33-35页 |
| ·、模式方法 | 第33-34页 |
| ·、计算理论的缺陷 | 第34-35页 |
| ·、安全协议形式化方法的新发展 | 第35-37页 |
| ·、Abadi和Rowaway的可调和性思想 | 第35-37页 |
| ·本章小结 | 第37-39页 |
| 第三章 对CS逻辑的改进与扩展 | 第39-52页 |
| ·、CS逻辑的介绍 | 第39-42页 |
| ·、基本介绍 | 第39页 |
| ·、CS逻辑的符号 | 第39-40页 |
| ·、CS逻辑的推理系统 | 第40-42页 |
| ·、CS逻辑及已有扩展的缺陷 | 第42-43页 |
| ·、CS逻辑的缺陷 | 第42-43页 |
| ·、已有扩展的缺陷 | 第43页 |
| ·、我们对CS逻辑的扩展 | 第43-47页 |
| ·、增加的符号 | 第43-44页 |
| ·、对已有逻辑公理的改进和扩展 | 第44-46页 |
| ·、新添加的公理 | 第46-47页 |
| ·、实例分析 | 第47-50页 |
| ·、一种对称密钥交换协议的分析实例 | 第47-48页 |
| ·、协议分析 | 第48-50页 |
| ·、本章小结 | 第50-52页 |
| 第四章 MBL逻辑 | 第52-70页 |
| ·、BAN类逻辑的缺陷 | 第52-54页 |
| ·、MBL逻辑 | 第54-64页 |
| ·、MBL逻辑对安全协议设计的要求 | 第54-55页 |
| ·、MBL逻辑的符号 | 第55页 |
| ·、MBL逻辑的敌手模型 | 第55-57页 |
| ·、MBL逻辑的语义模型 | 第57-60页 |
| ·、推理规则 | 第60-61页 |
| ·、推理规则的正确性证明 | 第61-64页 |
| ·、分析举例 | 第64-67页 |
| ·、MBL逻辑的可扩展性 | 第67-68页 |
| ·、本章小结 | 第68-70页 |
| 第五章 MBL逻辑的自动化分析 | 第70-79页 |
| ·、有关自动化的已有工作 | 第70-71页 |
| ·、基于MBL逻辑的自动化分析法 | 第71-78页 |
| ·、MBL逻辑符号到Prolog语言的转化 | 第72-73页 |
| ·、协议信息在Prolog语言的存储 | 第73页 |
| ·、推理的实现 | 第73-76页 |
| ·、实例分析 | 第76-78页 |
| ·、本章小结 | 第78-79页 |
| 第六章 设计安全的认证密钥交换协议 | 第79-90页 |
| ·、加密体制的安全性 | 第79-84页 |
| ·、不可区分的选择明文攻击 | 第80-81页 |
| ·、不可区分的选择密文攻击 | 第81-82页 |
| ·、不可区分适应性选择密文攻击 | 第82-83页 |
| ·、加密体制的选取 | 第83-84页 |
| ·、一个协议及其攻击 | 第84-85页 |
| ·、安全因素 | 第85-87页 |
| ·、认证性 | 第85-86页 |
| ·、正确的密码学保护 | 第86-87页 |
| ·、对YAHALOM协议的改进 | 第87-88页 |
| ·、对NEEDHAM-SCHREODER公钥认证协议的改进 | 第88页 |
| ·、本章小结 | 第88-90页 |
| 第七章 计算理论下认证密钥交换协议的安全性 | 第90-97页 |
| ·、基本概念 | 第90页 |
| ·、消息驱动的认证密钥交换协议 | 第90页 |
| ·、匹配对话 | 第90页 |
| ·、认证密钥交换协议的安全性 | 第90-95页 |
| ·分析协议的认证性 | 第91-94页 |
| ·保密性的讨论 | 第94-95页 |
| ·、本章小结 | 第95-97页 |
| 第八章 符号理论和计算理论相结合的分析法 | 第97-106页 |
| ·、通信的形式化 | 第97-98页 |
| ·、完全性与正确性 | 第98-99页 |
| ·、对MBL逻辑的修改和扩展 | 第99-100页 |
| ·、改进YAHALOM协议的安全性分析 | 第100-105页 |
| ·、协议及其安全目标的描述 | 第100-101页 |
| ·、形式化分析 | 第101-105页 |
| ·、本章小结 | 第105-106页 |
| 第九章 总结 | 第106-108页 |
| 参考文献 | 第108-117页 |
| 感谢 | 第117-118页 |
| 博士学习期间发表的论文情况 | 第118-119页 |
| 在读期间参与科研项目情况 | 第119-120页 |
| 学位论文评阅及答辩情况表 | 第120页 |