| 目录 | 第1-8页 |
| 中文摘要 | 第8-12页 |
| ABSTRACT | 第12-17页 |
| 本文所用的符号 | 第17-18页 |
| 第一章 引言 | 第18-23页 |
| ·安全协议的概念及分类 | 第18-19页 |
| ·安全协议的安全性质 | 第19页 |
| ·对安全协议进行形式化分析的意义 | 第19-20页 |
| ·我们的研究内容 | 第20-21页 |
| ·本文的结构 | 第21-23页 |
| 第二章 安全协议的形式化分析方法介绍 | 第23-32页 |
| ·基于推理的方法 | 第23-26页 |
| ·BAN逻辑 | 第23-24页 |
| ·GNY逻辑 | 第24-25页 |
| ·AT逻辑 | 第25页 |
| ·SVO逻辑 | 第25-26页 |
| ·基于攻击的自动化工具 | 第26-28页 |
| ·基于CSP的模型检测工具FDR | 第26-27页 |
| ·Mur φ验证系统 | 第27页 |
| ·Interrogator | 第27-28页 |
| ·NRL协议分析器 | 第28页 |
| ·基于证明的方法 | 第28-31页 |
| ·humanreadable证明法 | 第28-29页 |
| ·Paulson归纳法 | 第29页 |
| ·Schneider秩函数 | 第29页 |
| ·串空间 | 第29-30页 |
| ·Attacks限定法 | 第30-31页 |
| ·总结 | 第31-32页 |
| 第三章 公平交换协议及其形式化分析方法 | 第32-38页 |
| ·公平交换协议的演变 | 第32-34页 |
| ·逐步交换协议 | 第32-33页 |
| ·使用在线可信第三方(TTP)的公平交换协议 | 第33页 |
| ·使用离线可信第三方的公平交换协议 | 第33-34页 |
| ·公平交换协议要满足的特性 | 第34-35页 |
| ·已有公平交换协议形式化分析方法介绍 | 第35-37页 |
| ·CSP工具 | 第35-36页 |
| ·归纳方法 | 第36页 |
| ·Possum animation工具 | 第36页 |
| ·Mur φ | 第36-37页 |
| ·Mocha | 第37页 |
| ·OFMC | 第37页 |
| ·总结 | 第37-38页 |
| 第四章 一种分析公平交换协议的新方法 | 第38-51页 |
| ·对协议的目标及协议中传递的消息进行形式化描述 | 第38-41页 |
| ·对协议的目标及协议中传递的消息进行形式化描述的方法 | 第39页 |
| ·消息验证 | 第39-40页 |
| ·对协议的目标及协议中传递的消息进行形式化描述的意义 | 第40-41页 |
| ·协议结构 | 第41-42页 |
| ·丛的搜索 | 第42-48页 |
| ·丛的约简 | 第43-46页 |
| ·寻找可能存在的丛的步骤 | 第46-48页 |
| ·可行性分析 | 第48-49页 |
| ·丛的公平性分析 | 第49-50页 |
| ·适时中止性 | 第50页 |
| ·总结 | 第50-51页 |
| 第五章 对两个挂号电子邮件协议的分析 | 第51-74页 |
| ·对ASW挂号电子邮件协议的分析 | 第51-62页 |
| ·协议简介 | 第51-52页 |
| ·协议传递消息和协议目标的形式化描述 | 第52-54页 |
| ·寻找所有可能存在的丛 | 第54-60页 |
| ·协议的可行性分析 | 第60页 |
| ·丛的公平性分析 | 第60-61页 |
| ·适时中止性分析 | 第61页 |
| ·关于检测效率 | 第61页 |
| ·与已有分析结果的比较 | 第61-62页 |
| ·ZDB协议的形式化分析 | 第62-73页 |
| ·协议简介 | 第62-64页 |
| ·协议传递消息及交易方目标的形式化描述 | 第64-66页 |
| ·协议传递消息的形式化描述 | 第64-66页 |
| ·交易方目标的形式化描述 | 第66页 |
| ·搜索可能存在的丛 | 第66-71页 |
| ·几点讨论 | 第71-72页 |
| ·修改 | 第72-73页 |
| ·总结 | 第73-74页 |
| 第六章 对两个合同签订协议的分析 | 第74-84页 |
| ·MICALI协议的形式化分析 | 第74-79页 |
| ·协议简介 | 第74-75页 |
| ·协议传递消息和交易方目标的形式化描述 | 第75-76页 |
| ·搜索可能存在的丛 | 第76-78页 |
| ·丛的公平性分析 | 第78-79页 |
| ·可行性分析 | 第79页 |
| ·适时中止性分析 | 第79页 |
| ·结论 | 第79页 |
| ·BWZZ协议的形式化分析 | 第79-83页 |
| ·协议简介 | 第79-80页 |
| ·协议传递消息及交易方目标的形式化描述 | 第80-81页 |
| ·搜索可能存在的丛 | 第81页 |
| ·丛的公平性分析 | 第81-82页 |
| ·可行性分析 | 第82页 |
| ·适时中止性分析 | 第82页 |
| ·结论 | 第82-83页 |
| ·总结 | 第83-84页 |
| 第七章 自动分析算法 | 第84-93页 |
| ·自动分析算法的思路 | 第84页 |
| ·自动分析算法的初始输入 | 第84-85页 |
| ·关键算法描述 | 第85-93页 |
| 第八章 公平交换协议的可追究性分析 | 第93-102页 |
| ·方法介绍 | 第93-96页 |
| ·逻辑构件： | 第94页 |
| ·公理系统 | 第94-96页 |
| ·改进与扩展 | 第96-97页 |
| ·可追究性分析之例 | 第97-101页 |
| ·ASW协议的可追究性分析 | 第97-99页 |
| ·ZDB协议的可追究性分析 | 第99-101页 |
| ·总结 | 第101-102页 |
| 第九章 基于串空间模型的公平交换协议的形式化分析 | 第102-118页 |
| ·基于串空间模型的公平交换协议形式化分析 | 第103-105页 |
| ·串空间基本概念介绍 | 第103-104页 |
| ·串空间方法扩展及交换协议公平性的形式化描述 | 第104-105页 |
| ·ASOKAN-SHOUP-WAIDNER协议公平性的形式化分析 | 第105-110页 |
| ·协议的目的 | 第105-106页 |
| ·ASW协议的串空间模型 | 第106-107页 |
| ·ASW协议的形式化分析 | 第107-110页 |
| ·小结 | 第110页 |
| ·RSA-CEMD协议分析及基于串空间模型的形式化证明 | 第110-117页 |
| ·RSA-CEMD协议介绍 | 第111-112页 |
| ·对RSA-CEMD协议的分析 | 第112-113页 |
| ·对RSA-CEMD协议的修改 | 第113-114页 |
| ·修改后RSA-CEMD协议的公平性分析 | 第114-117页 |
| ·小结 | 第117页 |
| ·总结 | 第117-118页 |
| 第十章 总结 | 第118-120页 |
| ·本论文所做工作总结 | 第118页 |
| ·将来的研究方向 | 第118-120页 |
| 参考文献 | 第120-130页 |
| 致谢 | 第130-131页 |
| 攻读学位期间完成的论文 | 第131页 |
| 博士期间参加科研项目情况 | 第131-132页 |
| 学位论文评阅及答辩情况表 | 第132页 |
