| 摘要 | 第1-21页 |
| ABSTRACT | 第21-23页 |
| 第一章 绪论 | 第23-28页 |
| §1.1 课题背景 | 第25-26页 |
| §1.2 我们的工作与本文的组织结构 | 第26-28页 |
| §1.2.1 主要工作 | 第26页 |
| §1.2.2 本文的组织结构 | 第26-28页 |
| 第二章 电子商务协议 | 第28-44页 |
| §2.1 密码协议 | 第28-35页 |
| ·密码协议基本概念 | 第28-29页 |
| ·密码协议分类 | 第29-31页 |
| ·密码协议的安全性 | 第31-32页 |
| ·密码协议的设计规范 | 第32-33页 |
| ·密码协议的形式化分析 | 第33-35页 |
| §2.2 电子商务协议介绍 | 第35-40页 |
| ·电子商务协议基本概念 | 第35-36页 |
| ·电子商务协议的主要性质 | 第36-38页 |
| ·SSL协议 | 第38页 |
| ·SET协议 | 第38-39页 |
| ·SET与SSL协议的比较 | 第39-40页 |
| §2.3 电子商务协议形式化分析方法 | 第40-43页 |
| §2.4 小结 | 第43-44页 |
| 第三章 电子商务协议的逻辑分析方法及其在公平非否认协议中的应用 | 第44-70页 |
| §3.1 一阶逻辑 | 第44-47页 |
| ·简要介绍 | 第45-46页 |
| ·语法 | 第46页 |
| ·语义 | 第46-47页 |
| §3.2 BAN逻辑 | 第47-57页 |
| ·BAN逻辑产生背景 | 第47页 |
| ·BAN逻辑简介 | 第47-48页 |
| ·BAN逻辑系统中的构造子 | 第48-49页 |
| ·BAN逻辑系统中的基本推理规则 | 第49-52页 |
| ·基于BAN逻辑的认证协议分析 | 第52-54页 |
| ·一个新的认证协议及其形式化分析 | 第54-57页 |
| §3.3 GNY逻辑 | 第57-58页 |
| ·GNY逻辑基本思想 | 第57页 |
| ·GNY逻辑评价 | 第57-58页 |
| §3.4 SVO逻辑 | 第58-59页 |
| ·SVO逻辑的基本集合 | 第58页 |
| ·SVO逻辑的推理法则 | 第58-59页 |
| §3.5 KAILAR逻辑 | 第59-61页 |
| §3.6 周—卿方法 | 第61-65页 |
| ·方法简介 | 第61-63页 |
| ·推理规则 | 第63-65页 |
| §3.7 一种新的公平可追究协议及其形式化分析 | 第65-69页 |
| ·NCP协议及其分析 | 第65-66页 |
| ·NCP′描述 | 第66页 |
| ·NCP′协议的形式化分析 | 第66-68页 |
| ·NCP′协议与相关工作的比较 | 第68-69页 |
| §3.8 小结 | 第69-70页 |
| 第四章 电子商务协议的模型检测技术 | 第70-87页 |
| §4.1 时序逻辑与CTL | 第71-77页 |
| ·时序逻辑 | 第71-73页 |
| ·分枝时序逻辑 | 第73-74页 |
| ·CTL语法 | 第74-75页 |
| ·CTL语义 | 第75-77页 |
| §4.2 SMV与NUSMV | 第77-82页 |
| ·模型检测概述 | 第77-79页 |
| ·符号模型检测工具SMV | 第79-81页 |
| ·模型检测新工具——NUSMV | 第81-82页 |
| §4.3 基于CTL与SMV的电子商务协议的模型检测方法 | 第82-86页 |
| ·ISI协议及其重要性质 | 第82-83页 |
| ·ISI协议分析与验证 | 第83-86页 |
| §4.4 小结 | 第86-87页 |
| 第五章 一种新的基于博弈的逻辑——ATL | 第87-98页 |
| §5.1 博弈逻辑 | 第87-88页 |
| ·博弈逻辑的概念与研究对象 | 第87-88页 |
| ·基本内容 | 第88页 |
| §5.2 交替转换系统ATS | 第88-92页 |
| §5.3 时间交替时序逻辑ATL | 第92-95页 |
| ·ATL的语法 | 第92页 |
| ·ATL的语义 | 第92-94页 |
| ·ATL的公平性约束 | 第94-95页 |
| §5.4 基于ATL的模型检测 | 第95-97页 |
| ·ATL的模型检测算法 | 第95-96页 |
| ·保护命令语言 | 第96页 |
| ·MOCHA | 第96-97页 |
| §5.5 小结 | 第97-98页 |
| 第六章 基于ATL的电子商务协议形式化分析 | 第98-115页 |
| §6.1 电子商务协议的建模与描述 | 第98-99页 |
| ·基本假设 | 第98-99页 |
| §6.2 ZDB协议的分析 | 第99-105页 |
| ·ZDB协议简介 | 第99-101页 |
| ·ZDB协议的建模 | 第101-103页 |
| ·ZDB协议性质的ATL描述与分析 | 第103-105页 |
| §6.3 FNORP协议的分析 | 第105-111页 |
| ·FNORP协议及其变种 | 第105-109页 |
| ·FNORP协议的建模 | 第109页 |
| ·FNORP协议性质的ATL描述与分析 | 第109-111页 |
| §6.4 ZHOU-GOLLMANN协议的分析 | 第111-114页 |
| ·Zhou-Gollmann协议 | 第111-112页 |
| ·Zhou-Gollmann协议的建模 | 第112页 |
| ·Zhou-Gollmann协议性质的ATL描述与分析 | 第112-114页 |
| §6.5 小结 | 第114-115页 |
| 第七章 结束语 | 第115-117页 |
| §7.1 主要研究工作 | 第115-116页 |
| §7.2 下一步工作 | 第116-117页 |
| 主要参考文献 | 第117-124页 |
| 附录A：攻读博士期间主要成果 | 第124-125页 |
| 攻读博士期间的主要学术论文(第1作者或独立) | 第124页 |
| 主持课题 | 第124-125页 |
| 致谢 | 第125-126页 |
| 原创;性声明 | 第126页 |
| 关于学位论文使用授权的声明 | 第126页 |
