安全移动商务协议分析与研究

论文摘要

在移动通信技术和网络迅速发展的今天，移动商务成为一个必然趋势。安全公平的移动交易成为学者们研究的焦点，而移动商务协议作为移动商务安全技术的应用服务层，安全性越来越引起人们的关注。着色Petri网(CPN)是一种高级的Petri网成功应用于通信协议和工作流的分析，目前使用CPN对移动商务协议进行属性分析的报道比较少。本文提出一种基于CPN的移动商务协议建模和安全属性分析的新方法，基于分析获得的安全移动商务协议特性设计了一个满足安全属性的新移动商务协议，并模拟实现了该协议，通过攻击验证了协议的安全性。本文首先介绍了移动商务协议研究现状和基本安全属性，以及目前分析方法中存在的问题。然后详细介绍了协议分析工具—着色Petri网及其仿真工具CPN Tools和分析方法。其次，本文提出了一个利用着色Petri网对移动商务协议进行建模的新方法，以典型的移动商务协议KSL为例，详细介绍了利用着色Petri网对协议安全属性的形式化分析方法，证明了方法的可行性和正确性，并发现了基于逻辑的形式化方法未能发现的可追究性上的缺陷。之后，通过逻辑分析验证了CPN方法能够发现成功新的协议漏洞，并总结概括出一般移动商务协议满足安全属性的必要条件。最后，基于上文的安全移动商务协议必要条件，提出新的移动商务协议，包括双向身份认证和移动宏支付协议两部分。并设计了一个移动商务系统实现该协议，经过仿真模拟攻击验证了协议满足认证性、完整性、私密性、不可否认性、可追究性和公平性，而且不会影响系统的传输速度。

论文目录

• 摘要
• Abstract
• 1 绪论
• 1.1 课题背景
• 1.2 移动商务的特点
• 1.3 移动商务协议发展现状
• 1.3.1 移动身份认证协议现状
• 1.3.2 移动支付协议现状
• 1.4 移动商务协议分析现状
• 1.5 本文研究的主要内容
• 2 移动商务协议基本理论
• 2.1 移动商务协议的安全属性
• 2.1.1 认证性
• 2.1.2 完整性
• 2.1.3 私密性
• 2.1.4 不可否认性
• 2.1.5 可追究性
• 2.1.6 公平性
• 2.2 电子商务协议分析方法
• 2.2.1 逻辑方法
• 2.2.2 LPC方法
• 2.2.3 过程演算方法
• 2.2.4 Petri网等通用形式方法
• 3 着色Petri网及其分析工具CPN Tools
• 3.1 着色Petri网基本理论
• 3.1.1 Petri网基本概念
• 3.1.2 着色Petri网的基本概念
• 3.1.3 有色Petri网的动态特性
• 3.2 分层着色Petri网
• 3.2.1 变迁代替
• 3.2.2 位置联合
• 3.3 时延着色Petri网
• 3.4 CPN Tools工具
• 3.4.1 CPN Tools仿真
• 3.4.2 状态空间报告
• 4 基于CPN的移动商务协议分析
• 4.1 CPN协议分析的一般步骤
• 4.1.1 分层建立协议模型
• 4.1.2 模型状态空间分析
• 4.2 KSL移动商务协议简介
• 4.2.1 KSL协议描述中用到的符号说明
• 4.2.2 KSL协议的具体描述
• 4.3 KSL协议的CPN模型
• 4.3.1 顶层模块结构
• 4.3.2 子模块结构
• 4.4 基于CPN的KSL协议属性分析
• 4.4.1 认证性分析
• 4.4.2 私密性分析
• 4.4.3 完整性分析
• 4.4.4 不可否认性分析
• 4.4.5 可追究性分析
• 4.5 基于时延CPN的改进KSL协议公平性分析
• 4.5.1 改进的KSL协议
• 4.5.2 改进的KSL协议公平性分析
• 4.6 逻辑分析KSL协议安全属性
• 4.6.1 BAN逻辑分析认证性
• 4.6.2 SVO逻辑分析不可否认性
• 4.6.3 Kaila逻辑分析可追究性
• 4.7 移动商务协议满足安全属性的条件
• 5 一种新的移动商务协议
• 5.1 协议描述中用到的符号
• 5.2 移动身份认证协议
• 5.2.1 身份认证协议描述
• 5.2.2 身份认证协议分析
• 5.3 移动宏支付协议
• 5.3.1 移动宏支付协议描述
• 5.3.2 移动宏支付协议属性分析
• 5.4 新移动商务协议的实现
• 5.4.1 实现环境
• 5.4.2 系统框架流程
• 5.4.3 消费者界面
• 5.4.4 系统测试
• 5.4.5 系统评价
• 结论
• 参考文献
• 附录A 新移动宏支付协议CPN分析
• 攻读硕士学位期间发表学术论文情况
• 致谢