SET协议支付过程分析及模型检测
| 摘要 | 第1-21页 |
| Abstract | 第21-23页 |
| 前言 | 第23-24页 |
| 第1章 安全协议的检验方法 | 第24-28页 |
| ·非形式化方法 | 第24页 |
| ·形式化方法 | 第24-28页 |
| ·形式化方法概述 | 第25页 |
| ·形式化方法的分类 | 第25-28页 |
| 第2章 模型检测 | 第28-31页 |
| ·模型检测简介 | 第28-29页 |
| ·模型检测工具 | 第29-30页 |
| ·模型检测技术分析密码协议的方法研究 | 第30页 |
| ·模型检测的现状及问题 | 第30-31页 |
| 第3章 SMV符号模型检验系统 | 第31-40页 |
| ·SMV系统简介 | 第31页 |
| ·SMV系统的原理框图 | 第31-32页 |
| ·SMV语言 | 第32-35页 |
| ·SMV语言程序语法定义 | 第32-34页 |
| ·一个SMV实例 | 第34-35页 |
| ·与SMV系统相关的几个概念 | 第35-37页 |
| ·应用SMV系统进行协议分析 | 第37-39页 |
| ·使用SMV时应该注意的问题 | 第39-40页 |
| 第4章 SET协议及其支付过程分析 | 第40-48页 |
| ·SET安全协议 | 第40-42页 |
| ·SET要达到的最主要的目标 | 第40页 |
| ·SET协议中的参与者 | 第40页 |
| ·SET协议的工作原理 | 第40-41页 |
| ·SET协议中所采用的加密技术 | 第41-42页 |
| ·支付过程分析 | 第42-48页 |
| ·购买请求 | 第42-44页 |
| ·支付授权 | 第44-45页 |
| ·支付获得 | 第45-48页 |
| 第5章 SET协议支付过程的模型检测 | 第48-58页 |
| ·SET协议支付过程的抽象模型 | 第48-49页 |
| ·协议主体的状态转换图 | 第49-52页 |
| ·基于CTL的安全属性描述 | 第52-53页 |
| ·SET协议支付过程的编程说明 | 第53-55页 |
| ·SET支付协议安全属性的验证 | 第55-57页 |
| ·结论与进一步构想 | 第57-58页 |
| 致谢 | 第58-59页 |
| 参考文献 | 第59-62页 |
| 附录 | 第62-63页 |
| 原创性声明 | 第63页 |
| 关于学位论文使用授权的声明 | 第63页 |
