| 摘要 | 第1-5页 |
| ABSTRACT | 第5-8页 |
| 第一章 绪论 | 第8-13页 |
| ·密码协议相关的密码技术 | 第8-9页 |
| ·密码协议简介 | 第9-10页 |
| ·密码协议的概念 | 第9页 |
| ·密码协议的历史 | 第9页 |
| ·对于密码协议的直观描述 | 第9-10页 |
| ·国内外研究现状 | 第10-11页 |
| ·论文主要工作、创新点及组织结构 | 第11-13页 |
| ·论文主要工作和创新点 | 第11页 |
| ·论文组织结构 | 第11-13页 |
| 第二章 密码协议的常见缺陷以及相应的攻击 | 第13-23页 |
| ·攻击者的模型 | 第13-14页 |
| ·分析密码协议的主要困难 | 第14页 |
| ·对于密码协议的常见攻击 | 第14-22页 |
| ·重放攻击 | 第15-18页 |
| ·中间人攻击 | 第18-20页 |
| ·平行会话攻击 | 第20-21页 |
| ·类型攻击 | 第21-22页 |
| ·攻击方法难以穷尽 | 第22页 |
| ·本章小结 | 第22-23页 |
| 第三章 密码协议形式化分析方法 | 第23-35页 |
| ·计算观点 | 第23-26页 |
| ·相互认证的目标：匹配对话 | 第23页 |
| ·相互认证成功的定义 | 第23-24页 |
| ·MAP1 协议以及其安全性证明 | 第24-26页 |
| ·对计算观点的分析 | 第26页 |
| ·逻辑符号观点 | 第26-33页 |
| ·BAN 逻辑 | 第26-27页 |
| ·BAN 逻辑框架介绍 | 第27-29页 |
| ·BAN 逻辑分析举例 | 第29-32页 |
| ·BAN 逻辑的缺陷以及提出新的形式化方法的必要性 | 第32-33页 |
| ·状态探查观点 | 第33页 |
| ·对这三种观点的理解 | 第33-34页 |
| ·本章小结 | 第34-35页 |
| 第四章 一种新的密码协议形式化分析方法 | 第35-56页 |
| ·对密码协议的非形式化分析方法 | 第35-39页 |
| ·非形式化分析方法简介 | 第35-37页 |
| ·提出非形式化分析方法的原因 | 第37页 |
| ·非形式化分析方法的作用 | 第37-39页 |
| ·形式化分析方法的基本框架 | 第39页 |
| ·系统各子模块的功能说明 | 第39-55页 |
| ·模块1：对协议进行符号化 | 第39-40页 |
| ·模块2：对消息本身进行的源认证 | 第40-42页 |
| ·模块3：新鲜性标识符对于各个主体的关联验证 | 第42-44页 |
| ·模块4：进行Wenbo Mao 规则检验 | 第44-46页 |
| ·模块5：对协议进行安全性证明 | 第46-55页 |
| ·本章小结 | 第55-56页 |
| 第五章 新形式化分析方法的实践应用 | 第56-71页 |
| ·形式化分析方法的应用 | 第56页 |
| ·对SSH 协议的分析 | 第56-59页 |
| ·SSH 协议简介 | 第56页 |
| ·SSH 协议的整体架构 | 第56-57页 |
| ·SSH 传输层协议 | 第57-58页 |
| ·对SSH 传输层协议的安全性进行安全性分析 | 第58-59页 |
| ·对Kerberos 协议的分析 | 第59-63页 |
| ·Kerberos 协议简介 | 第59页 |
| ·Kerberos 协议的总体结构 | 第59-60页 |
| ·认证服务交换 | 第60页 |
| ·与TGS 运行协议 | 第60-61页 |
| ·与应用服务器运行协议 | 第61页 |
| ·对Kerberos 协议的安全性进行形式化分析 | 第61-63页 |
| ·对工作站-工作站（STS）协议的分析 | 第63-69页 |
| ·STS 协议简介 | 第63-65页 |
| ·对STS 协议的安全性进行形式化分析 | 第65-69页 |
| ·本文提出的形式化方法的优缺点 | 第69-70页 |
| ·本章小结 | 第70-71页 |
| 第六章 总结和展望 | 第71-72页 |
| 致谢 | 第72-73页 |
| 参考文献 | 第73-76页 |