学位论文 > 优秀研究生学位论文题录展示

电子商务协议的形式化分析

作　者: 王章凯
导　师: 傅育熙
学　校: 上海交通大学
专　业: 计算机软件与理论
关键词: 电子商务交换协议形式化方法模型检测协议验证公平性
分类号: F713.36
类　型: 硕士论文
年　份: 2010年
下　载: 80次
引　用: 1次
阅　读: 论文下载

内容摘要

由于互联网的普及,随之而兴起的电子商务已经成为一个新的商业交易模式,而相应的电子商务协议则是这一新型的交易模式顺利进行的保证。网络环境下协议的安全、原子、隐私与匿名这些属性的有效解决则是电子商务广泛应用关键。而严格的形式化描述和分析是刻画电子商务协议并验证它们相应属性的有效方法.电子商务协议作为安全协议当中的一类重要协议,除了具有一般的安全协议所应当具备的性质以外,还有其一些专有的独特性质。本文首先介绍了安全协议形式化分析的研究现状和主要方法,并且重点讨论了其中的模型检测方法。还对电子商务协议的研究状况做了简要介绍。概括了电子商务协议的分类并且对原子性、不可否认性、公平性等主要的安全性质归纳讨论。最后以一个具体的电子商务协议为例,使用CSP为建模语言刻画了该协议和并以电子商务协议中公平性作为需要验证的属性,以基于CSP的FDR为相应的模型验证工具,用有限自动机结构对模型所有状态集合进行检验,检测该协议是否特定的一些公平性(即金钱原子性,货币原子性和有效接受性),并且在模型中引入网络环境下很容易出现的两大故障(即断线和网站故障),观察引入故障后相应的性质能否保持并分析其原因。并且提出一些可能的修改意见对协议加以完善。

全文目录

摘要  5-6
ABSTRACT  6-9
第一章绪论  9-14
  1.1 研究背景及意义  9-10
  1.2 安全协议形式化方法概述  10-12
    1.2.1 安全协议的定义及分类  10-11
    1.2.2 形式化分析的意义  11-12
    1.2.3 主要的几种形式化方法  12
  1.3 研究内容  12-13
  1.4 本文结构  13-14
第二章电子商务协议概述  14-21
  2.1 电子商务协议背景  14-15
  2.2 电子商务协议的结构  15
  2.3 电子商务协议的运行环境  15
  2.4 电子商务协议分类  15-16
  2.5 电子商务协议性质分析  16-19
  2.6 电子商务协议的设计原则  19-20
  2.7 电子商务协议分析方法简介  20
  2.8 本章小结  20-21
第三章模型检测技术  21-25
  3.1 模型检测简介  21-22
  3.2 模型检测与其他形式化方法的比较  22-23
  3.3 模型检测工具  23-24
  3.4 模型检测的现状及问题  24-25
第四章基于CSP的电子商务协议的模型检测  25-42
  4.1 CSP与FDR模型验证框架介绍  25-29
    4.1.1 CSP介绍  25-26
      4.1.1.1 基本概念  25
      4.1.1.2 CSP的语法  25-26
    4.1.2 模型检测工具FDR介绍  26-29
  4.2 用CSP建模安全协议  29-32
    4.2.1 对协议建模  29-31
    4.2.2 对性质建模  31-32
  4.3 在CSP和FDR框架下验证电子商务协议  32-40
    4.3.1 协议介绍  32-35
    4.3.2 对协议进行建模  35-39
      4.3.2.1 对顾客进程进行建模  35-36
      4.3.2.2 对商家进程建模  36-37
      4.3.2.3 对银行进程建模  37
      4.3.2.4 对顾客、商家、银行之间的通讯进行建模  37-38
      4.3.2.5 对三个公平性进行建模  38
      4.3.2.6 对每个性质相对应的系统建模  38-39
    4.3.3 在不可靠环境下验证相应的性质  39
      4.3.3.1 对通讯失败建模  39
      4.3.3.2 对顾客、商家和银行站点故障建模  39
      4.3.3.3 不可靠环境下模型检测的结果  39
    4.3.4 实验结果分析  39-40
  4.4 本章小结  40-42
第五章总结和展望  42-45
  5.1 总结  42-43
  5.2 展望  43-45
参考文献  45-50
致谢  50-51
在学期间的研究成果及发表的论文  51-53

电子商务协议的形式化分析

内容摘要

全文目录

相似论文