电子商务协议的形式化分析与漏洞检测

论文摘要

电子商务安全协议,为电子商务活动提供一系列的安全保护工作,是整个系统安全体系的核心。电子商务安全协议除需要提供保密性、认证性等一般安全性质外,通常还需要满足原子性、匿名性以及不可否认性等多种特性。因此,电子商务安全协议的设计与安全检测是目前的研究热点与难点。研究某种方法能准确高效的发现协议中的安全问题,并对检测出的漏洞进行有效的分析和修复,对于电子商务协议的安全运行至关重要。本文围绕电子商务安全协议的形式化分析与协议漏洞检测开展研究工作,主要工作与创新点为：1.在介绍基于CSP的模型检测工具FDR以及建模工具Casper的基础上,对Caper/FDR中攻击者的能力以及系统中产生的攻击者模型进行了描述和分析；2.将Casper/FDR2模型检测方法运用到电子商务领域的研究分析中,找到了多个电子商务协议的漏洞,并提出了具体的改进方案；3.在给出电子商务协议原子性的两个扩展特性的基础上,提出了运用CSP建模方式对交易协议的扩展原子性进行形式化分析方法,建立了非常规状态的系统模型,并运用FDR对建立的CSP模型进行检测,对于实验中发现的协议漏洞,提出了改进方案；4.在基于CSP的安全协议匿名性理论基础上,提出了一套对于电子商务协议匿名性的形式化分析方法,给出了适用于CSP/FDR模型检测技术的建模框架,并通过对一个电子商务协议进行实验描述了具体的建模分析过程。本文研究成果表明：以CSP理论框架为基础,运用相应的模型检测工具Casper和FDR2,通过有限自动机结构对电子商务协议中的所有状态集合进行检测,可有效测试与发现电子商务协议中保密性、认证性和匿名性等重要特性的满足情况,对保障电子商务系统的安全高效运行具有重要意义。

论文目录

• 中文摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景与意义
• 1.1.1 电子商务发展现状
• 1.1.2 对电子商务协议分析的意义
• 1.1.3 国内外研究现状
• 1.2 主要工作
• 1.3 本文章节安排
• 1.4 小结
• 第二章 电子商务协议简介
• 2.1 安全电子商务协议概述
• 2.1.1 电子商务协议运行环境中的主要角色
• 2.1.2 安全电子商务协议的主要特性
• 2.1.3 Digicash电子商务协议
• 2.2 安全电子商务协议的缺陷
• 2.2.1 常见攻击手段
• 2.2.2 利用协议设计漏洞的攻击
• 2.3 新的潜在安全威胁
• 2.4 小结
• 第三章 基于CSP方法的模型检测技术
• 3.1 安全协议的形式化分析基础
• 3.1.1 模态逻辑技术
• 3.1.2 模型检测技术
• 3.1.3 定理证明技术
• 3.2 CSP简介
• 3.2.1 CSP中常用操作符
• 3.2.2 进程
• 3.2.3 CSP中的迹模型
• 3.2.4 一个简单的CSP系统模型
• 3.3 基于CSP的模型检测工具
• 3.3.1 FDR
• 3.3.2 Casper
• 3.4 Casper/FDR中的攻击者模型
• 3.4.1 攻击者能力分析
• 3.4.2 具有攻击者的系统模型
• 3.4.3 入侵者建模
• 3.5 小结
• 第四章 基于CASPER/FDR2的电子商务协议形式化分析研究
• 4.1 协议背景
• 4.2 注册协议建模和分析
• 4.2.1 注册协议
• 4.2.2 注册协议的Casper建模
• 4.2.3 检测结果及分析
• 4.3 对注册协议的改进
• 4.4 小结
• 第五章 电子商务协议扩展原子性的分析验证
• 5.1 电子商务协议原子性的扩展
• 5.1.1 接收验证原子性
• 5.1.2 撤销交易原子性
• 5.2 建立协议的CSP模型
• 5.2.1 交易协议
• 5.2.2 定义协议的运行环境
• 5.2.3 定义协议数据、通信信道和进程
• 5.2.4 对交易实体及系统整体进行建模
• 5.2.5 建立协议目标声明
• 5.2.6 协议的非常规状态模型
• 5.3 FDR模型检测
• 5.3.1 FDR检测
• 5.3.2 检测结果调试
• 5.4 协议原子性目标分析
• 5.4.1 接收验证原子性分析
• 5.4.2 撤销交易原子性分析
• 5.5 协议改进
• 5.6 小结
• 第六章 电子商务协议强匿名性分析验证
• 6.1 基于CSP模型的协议匿名性分析理论基础
• 6.1.1 匿名性定义
• 6.1.2 观察者模型
• 6.2 改进的电子商务协议匿名性形式化分析框架
• 6.2.1 电子商务协议匿名性要求
• 6.2.2 电子商务协议匿名性模型框架
• 6.3 电子商务协议的匿名性模型建立
• 6.3.1 协议环境建模
• 6.3.2 参与实体建模
• 6.3.3 匿名性目标建模
• 6.4 结果验证和分析
• 6.4.1 协议观察者
• 6.4.2 模型检测结果和分析
• 6.4.3 内部观察者模型检测和分析
• 6.5 小结
• 第七章 总结和展望
• 7.1 总结
• 7.2 展望
• 参考文献
• 致谢
• 个人简历、在读期间研究成果以及发表的学术论文