| 独创性声明 | 第1-5页 |
| 摘要 | 第5-6页 |
| ABSTRACT | 第6-9页 |
| 第一章 前言 | 第9-12页 |
| 1．1 研究背景 | 第9-10页 |
| 1．2 研究总结 | 第10-12页 |
| 第二章 电子商务协议的原子性 | 第12-22页 |
| 2．1 简介 | 第12-17页 |
| 2．1．1 电子商务的定义 | 第12页 |
| 2．1．2 电子商务协议的分类 | 第12-14页 |
| 2．1．3 电子商务协议的性质 | 第14-17页 |
| 2．2 原子性的由来 | 第17-19页 |
| 2．2．1 钱的原子性(Money Atomicity) | 第18页 |
| 2．2．2 商品的原子性(Goods Atomicity) | 第18页 |
| 2．2．3 可确认发送的原子性(Certified Delivery) | 第18页 |
| 2．2．4 原子性的层次结构 | 第18-19页 |
| 2．3 NET-Bill协议的原子性分析 | 第19-22页 |
| 2．3．1 NET-Bill协议的参与主体 | 第19页 |
| 2．3．2 NET-Bill协议的步骤 | 第19-20页 |
| 2．3．3 NET-Bill协议的原子性分析 | 第20-22页 |
| 第三章 电子商务协议形式化分析方法 | 第22-41页 |
| 3．1 形式化分析介绍 | 第22-27页 |
| 3．1．1 形式化分析的概念 | 第22页 |
| 3．1．2 有限状态机 | 第22-24页 |
| 3．1．3 Petri网 | 第24-26页 |
| 3．1．4 时态逻辑 | 第26-27页 |
| 3．2 形式化分析的现状 | 第27-29页 |
| 3．3 形式化分析的方法 | 第29-41页 |
| 3．3．1 信任逻辑方法 | 第30-32页 |
| 3．3．2 定理证明法 | 第32-36页 |
| 3．3．3 模型检验法 | 第36-39页 |
| 3．3．4 其它方法 | 第39-41页 |
| 第四章 SMV符号模型检验系统 | 第41-49页 |
| 4．1 SMV符号模型检验系统 | 第41-46页 |
| 4．1．1 SMV(symbolic model verifier)系统简介 | 第41-42页 |
| 4．1．2 与SMV系统相关的几个概念 | 第42页 |
| 4．1．3 SMV输入语言介绍 | 第42-46页 |
| 4．2 SMV系统工具 | 第46-47页 |
| 4．2．1 SMV系统原理框图 | 第46页 |
| 4．2．2 使用SMV注意的几个问题 | 第46-47页 |
| 4．3 应用SMV系统进行协议分析 | 第47-49页 |
| 4．3．1 建立系统模型 | 第47-48页 |
| 4．3．2 给出所要验证的状态迁移系统的命题描述 | 第48页 |
| 4．3．3 系统状态遍历 | 第48-49页 |
| 第五章 SET协议原子性检验 | 第49-68页 |
| 5．1 SET协议的分析建模 | 第49-53页 |
| 5．1．1 SET协议的支付模型 | 第49页 |
| 5．1．2 SET协议的支付协议的数据结构 | 第49-50页 |
| 5．1．3 SET协议的支付协议的有限状态模型 | 第50-53页 |
| 5．2 SET协议的系统说明 | 第53-54页 |
| 5．3 SET协议的原子性系统属性描述 | 第54-55页 |
| 5．3．1 钱的原子性的CTL描述 | 第55页 |
| 5．3．2 商品的原子性描述 | 第55页 |
| 5．4 SET协议的原子性检验结果 | 第55-56页 |
| 5．5 SET协议的原子性检验结果分析 | 第56-57页 |
| 5．6 SET协议的一个改进版本的分析验证 | 第57-68页 |
| 5．6．1 SET协议的分析建模 | 第57-63页 |
| 5．6．2 改进后SET协议的系统说明 | 第63-65页 |
| 5．6．3 改进后SET协议的原子性系统属性描述 | 第65-68页 |
| 第六章 结束语 | 第68-69页 |
| 参考文献 | 第69-72页 |
| 致谢 | 第72页 |
