电子商务协议形式化方法及模型检测技术的研究与应用

论文摘要

电子商务协议形式化分析是电子商务研究的一个重要方面，电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础，其基本属性包括安全性、保密性、完整性、可认证性、非否认性及公平性等。进行电子商务协议的形式化分析研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术保障。 目前国内外对电子商务协议的分析验证手段主要有以下几种： (1)实际攻击验证方法； (2)从表面上进行直观检测； (3)形式化逻辑分析方法。 前两种方法存在较多缺点，如：属于事后检测，需在协议建立实施之后才能进行检测、检测手段不够严密等。而形式化逻辑分析方法可以在协议实施之前就用严格可靠的方法对其进行分析验证，是一个最有前途的研究方法。目前在各种电子商务协议形式化分析方法研究中，有影响的方法主要有BAN逻辑方法、Kailar逻辑方法、串空间方法、进程代数方法及基于时序逻辑的方法等。其中，时序逻辑方法能够通过建立数学模型来描述协议系统，可提供相应的模型检测工具对协议性质进行自动验证，对状态空间有限的并发协议系统分析尤为成功，已成为对电子商务协议进行形式化分析的主要工具之一。 本文主要对基于逻辑的形式化方法与模型检测技术及其在电子商务协议形式化分析中的应用进行了系统研究，重点对ATL逻辑方法及其在电子商务协议并形式化分析中的应用进行了研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术，其工作主要有以下几个方面： 1．对电子商务协议的基本理论和基本性质进行了分析和讨论，包括：安全性、保密性、完整性、可认证性、非否认性、公平性、时效性等，并对其中一些重要性质做新的定义，提出电子商务协议设计的基本准则。 2．对当前流行的基于逻辑的电子商务协议形式化分析方法进行重点研究，包括BAN逻辑、Kailar逻辑及周一卿方法。采用这些较新的形式化分析方法对几个典型协议进行分析，找出设计缺陷并提出新的公平非否认性协议。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• §1.1 课题背景
• §1.2 我们的工作与本文的组织结构
• §1.2.1 主要工作
• §1.2.2 本文的组织结构
• 第二章 电子商务协议
• §2.1 密码协议
• 2.1.1 密码协议基本概念
• 2.1.2 密码协议分类
• 2.1.2 密码协议的安全性
• 2.1.3 密码协议的设计规范
• 2.1.4 密码协议的形式化分析
• §2.2 电子商务协议介绍
• 2.2.1 电子商务协议基本概念
• 2.2.2 电子商务协议的主要性质
• 2.2.3 SSL协议
• 2.2.4 SET协议
• 2.2.5 SET与SSL协议的比较
• §2.3 电子商务协议形式化分析方法
• §2.4 小结
• 第三章 电子商务协议的逻辑分析方法及其在公平非否认协议中的应用
• §3.1 一阶逻辑
• 3.1.1 简要介绍
• 3.1.2 语法
• 3.1.3 语义
• §3.2 BAN逻辑
• 3.2.1 BAN逻辑产生背景
• 3.2.2 BAN逻辑简介
• 3.2.3 BAN逻辑系统中的构造子
• 3.2.4 BAN逻辑系统中的基本推理规则
• 3.2.5 基于BAN逻辑的认证协议分析
• 3.2.6 一个新的认证协议及其形式化分析
• §3.3 GNY逻辑
• 3.3.1 GNY逻辑基本思想
• 3.3.2 GNY逻辑评价
• §3.4 SVO逻辑
• 3.4.1 SVO逻辑的基本集合
• 3.4.2 SVO逻辑的推理法则
• §3.5 KAILAR逻辑
• §3.6 周—卿方法
• 3.6.1 方法简介
• 3.6.2 推理规则
• §3.7 一种新的公平可追究协议及其形式化分析
• 3.7.1 NCP协议及其分析
• 3.7.2 NCP′描述
• 3.7.3 NCP′协议的形式化分析
• 3.7.4 NCP′协议与相关工作的比较
• §3.8 小结
• 第四章 电子商务协议的模型检测技术
• §4.1 时序逻辑与CTL
• 4.1.1 时序逻辑
• 4.1.2 分枝时序逻辑
• 4.1.3 CTL语法
• 4.1.4 CTL语义
• §4.2 SMV与NUSMV
• 4.2.1 模型检测概述
• 4.2.2 符号模型检测工具SMV
• 4.2.3 模型检测新工具——NUSMV
• §4.3 基于CTL与SMV的电子商务协议的模型检测方法
• 4.3.1 ISI协议及其重要性质
• 4.3.2 ISI协议分析与验证
• §4.4 小结
• 第五章 一种新的基于博弈的逻辑——ATL
• §5.1 博弈逻辑
• 5.1.1 博弈逻辑的概念与研究对象
• 5.1.2 基本内容
• §5.2 交替转换系统ATS
• §5.3 时间交替时序逻辑ATL
• 5.3.1 ATL的语法
• 5.3.2 ATL的语义
• 5.3.3 ATL的公平性约束
• §5.4 基于ATL的模型检测
• 5.4.1 ATL的模型检测算法
• 5.4.2 保护命令语言
• 5.4.3 MOCHA
• §5.5 小结
• 第六章 基于ATL的电子商务协议形式化分析
• §6.1 电子商务协议的建模与描述
• 6.1.1 基本假设
• §6.2 ZDB协议的分析
• 6.2.1 ZDB协议简介
• 6.2.2 ZDB协议的建模
• 6.2.3 ZDB协议性质的ATL描述与分析
• §6.3 FNORP协议的分析
• 6.3.1 FNORP协议及其变种
• 6.3.2 FNORP协议的建模
• 6.3.3 FNORP协议性质的ATL描述与分析
• §6.4 ZHOU-GOLLMANN协议的分析
• 6.4.1 Zhou-Gollmann协议
• 6.4.2 Zhou-Gollmann协议的建模
• 6.4.3 Zhou-Gollmann协议性质的ATL描述与分析
• §6.5 小结
• 第七章 结束语
• §7.1 主要研究工作
• §7.2 下一步工作
• 主要参考文献
• 附录A：攻读博士期间主要成果
• 攻读博士期间的主要学术论文（第1作者或独立）
• 主持课题
• 致谢
• 原创;性声明
• 关于学位论文使用授权的声明