基于UPPAAL的电子商务协议安全性分析

论文摘要

随着网络的迅速发展,电子商务正逐渐得到大规模的应用。但电子商务的安全问题也越来越突出,已成为网上购物者的主要顾虑,没有安全就没有可被人们接受的电子商务。安全的电子商务协议是保证电子商务活动正常开展的基础,但一个貌似安全的协议往往存在安全上的漏洞。因此,一个电子商务协议在设计出来之后,需要从多方面对其各种性质进行分析,协议验证是揭示电子商务协议是否存在缺陷的重要途径。模型检测是一种常见的形式化分析方法,已被广泛的用于分析各种各样的协议,近年来也被用于电子商务协议。UPPAAL是一个基于模型检测理论的自动化验证工具,通常用于分析通信协议,但很少被用于安全协议的分析和验证。本文证明UPPAAL可用于分析电子商务协议的常见的安全协议。并利用UPPAAL分析了几个重要的电子商务协议的安全性质。验证结果表明,UPPAAL可以分析电子商务协议的一些安全性质,尤其适于不可靠环境下协议的执行,且可以利用生成的消息序列对协议进行改进。基于此,我们利用UPPAAL分析了一个重要的电子商务协议匿名可恢复的公平交换协议,第一次形式化验证了该协议满足有效性、公平性、时效性等基本的安全性质。此外,我们还发现,一个安全的电子商务协议在不可靠环境下执行时,有可能不再满足安全性质;当安全性质违背时,可借助模型检测工具UPPAAL生成的消息序列对协议进行改进。

论文目录

• 图目录
• 摘要
• ABSTRACT
• 第一章 引言
• 1.1 研究背景
• 1.2 研究现状
• 1.3 研究内容
• 1.3.1 本文的主要任务
• 1.3.2 本文需要解决的问题和难点
• 1.3.3 本文主要研究内容
• 1.4 本文结构
• 第二章 预备知识
• 2.1 电子商务协议的基本概念
• 2.2 电子商务协议所基于的基础结构
• 2.2.1 公开密钥基础结构
• 2.2.2 对称加密
• 2.2.3 数字签名
• 2.3 常见的电子商务协议的安全性质
• 2.4 电子商务协议的分析前提和设计准则
• 2.5 电子商务协议分析方法简介
• 2.5.1 协议的形式化
• 2.5.2 协议的验证
• 2.5.3 模型检测简介
• 2.5.4 协议的分析过程
• 2.6 模型检测理论中一些重要的研究方法
• 2.7 基于时间自动机的自动验证工具 UPPAAL
• 2.8 小结
• 第三章 基于UPPAAL 的电子商务协议的安全性质验证
• 3.1 协议描述
• 3.2 可靠环境下单轮协议验证
• 3.2.1 协议参与者建模
• 3.2.2 协议模拟
• 3.2.3 用UPPAAL 验证
• 3.3 对协议的改进
• 3.4 小结
• 第四章 基于UPPAAL 的匿名可恢复的公平交换协议性质验证
• 4.1 匿名可恢复的公平交换协议描述
• 4.2 基本协议的安全性质验证与分析
• 4.2.1 为基本协议的各参与者建模
• 4.2.2 协议模拟
• 4.2.3 安全性质验证
• 4.3 完整协议的安全性质验证
• 4.3.1 建立模型
• 4.3.2 协议模拟
• 4.3.3 安全性质验证
• 4.4 小结
• 第五章 基于UPPAAL 的不可靠环境下单轮FR 协议验证
• 5.1 协议描述
• 5.2 不可靠环境下单轮FR 协议验证
• 5.3 小结
• 第六章 总结与展望
• 致谢
• 参考文献