基于符号模型检验的电子商务协议原子性的研究与实现

摘要

目前对电子商务协议的检验手段主要有:直观的分析,实际攻击测试和形式化的检验分析技术.由于形式化分析借助于形式化分析方法和工具完成,具有逻辑严密和断言普遍的优点,但是形式化分析中的逻辑验证需要初始假设的非形式化过程,以及对协议进行理想化等缺陷.Gavin Lowe首先使用CSP和模型检验技术对密码协议进行分析,它克服了逻辑验证的上述缺陷.模型检验在电子商务协议安全性分析验证方面得到了广泛的应用.本文应用符号模型检验器(SMV)对电子商务协议的原子性进行分析,在对SET协议进行形式化描述的基础上,对SET协议进行分析和检验,指出了协议的缺陷.同时对该协议进行改进,又对改进后的协议的进行分析和检验,表明应用符号模型检验器对电子商务协议分析检验的可行性.

目录

文摘

英文文摘

独创性声明及学位论文版权使用授权书

第一章前言

1.1研究背景

1.2研究总结

第二章电子商务协议的原子性

2.1简介

2.1.1电子商务的定义

2.1.2电子商务协议的分类

2.1.3电子商务协议的性质

2.2原子性的由来

2.2.1钱的原子性(Money Atomicity)

2.2.2商品的原子性(Goods Atomicity)

2.2.3可确认发送的原子性(Certified Delivery)

2.2.4原子性的层次结构

2.3 NET-BILL协议的原子性分析

2.3.1 NET-Bill协议的参与主体

2.3.2 NET-Bill协议的步骤

2.3.3 NET-Bi1l协议的原子性分析

第三章电子商务协议形式化分析方法

3.1形式化分析介绍

3.1.1形式化分析的概念

3.1.2有限状态机

3.1.3 Petri网

3.1.4时态逻辑

3.2形式化分析的现状

3.3形式化分析的方法

3.3.1信任逻辑方法

3.3.2定理证明法

3.3.3模型检验法

3.3.4其它方法

第四章SMV符号模型检验系统

4.1 SMV符号模型检验系统

4.1.1 SMV(symbolic model verifier)系统简介

4.1.2与SMV系统相关的几个概念

4.1.3 SMV输入语言介绍

4.2 SMV系统工具

4.2.1 SMV系统原理框图

4.2.2使用SMV注意的几个问题

4.3应用SMV系统进行协议分析

4.3.1建立系统模型

4.3.2给出所要验证的状态迁移系统的命题描述

4.3.3系统状态遍历

第五章SET协议原子性检验

5.1 SET协议的分析建模

5.1.1 SET协议的支付模型

5.1.2 SET协议的支付协议的数据结构

5.1.3 SET协议的支付协议的有限状态模型

5.2 SET协议的系统说明

5.3 SET协议的原子性系统属性描述

5.3.1钱的原子性的CTL描述

5.3.2商品的原子性描述

5.4 SET协议的原子性检验结果

5.5 SET协议的原子性检验结果分析

5.6 SET协议的一个改进版本的分析验证

5.6.1 SET协议的分析建模

5.6.2改进后SET协议的系统说明

5.6.3改进后SET协议的原子性系统属性描述

第六章结束语

参考文献

致谢