基于模型检测的电子商务交易协议形式化分析与验证

发布时间：2017-11-19 20:19

  本文关键词：基于模型检测的电子商务交易协议形式化分析与验证

  更多相关文章： 形式化方法 Spin 模型检测 电子商务交易协议 Promela

【摘要】：根据CNNIC(China Internet Network Information Center,中国互联网络信息中心)发布的“第37次中国互联网络发展状况统计报告”,2015年,42.7%的网民遭遇过网络安全问题。随着网络购物群体的不断增大,电子商务安全问题引起了消费者的广泛关注。2015年,我国网络购物用户规模达到4.13亿,同时,16.4%的消费者在网购过程中遭遇到过网络消费欺诈。由此可见,网络安全问题和交易安全问题是保证电子商务进一步发展的关键之所在。交易协议是交易安全问题的核心。本文从网络交易安全问题出发,选取主流电子商务B2C模式作为研究对象,通过模型检测方法对基于第三方支付平台的交易协议进行了形式化建模、分析和验证,以保证买家和商户之间完成安全、可靠的交易活动。其主要内容如下：1.介绍了课题背景、相关理论基础和采用形式化方法分析安全协议的发展过程以及研究现状。2.对B2C模式涉及到的电子商务交易协议进行了简要的分析,使用Promela语言形式化地描述了电子商务交易协议中涉及到的四个实体：买家、商户网站、第三方支付平台和银行。3.使用模型检测方法对B2C模式交易协议进行形式化验证,对交易协议进行抽象化建模,描述了电子商务交易协议的LTL性质,使用Spin的图形界面工具XSpin得到交易协议的运行轨迹,在此基础上分析目前B2C模式交易协议存在的潜在安全隐患。4.针对分析结果,提出了一种基于B2C模式的改进模型,增加了物流方和第三方隐私服务器两个实体,用于规范交易流程和保护买家隐私。
【学位授予单位】：宁夏大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：F724.6;TP393.08

【相似文献】

中国期刊全文数据库 前10条

1 戎玫;张广泉;;模型检测新技术研究[J];计算机科学;2003年05期

2 肖健宇;张德运;郑卫斌;;过程提取用于改善程序模型检测的可伸缩性[J];西安交通大学学报;2006年06期

3 袁志斌;徐正权;王能超;;软件模型检测中的抽象[J];计算机科学;2006年07期

4 刘吉锋;孙吉贵;;基于抽象-验证-细化范例的软件模型检测[J];计算机科学;2006年12期

5 化志章;吴传孙;揭安全;薛锦云;;软件模型检测新技术研究[J];微计算机信息;2007年36期

6 王飞明;胡元闯;董荣胜;;模型检测研究进展[J];广西科学院学报;2008年04期

7 邝宏斌;罗贵明;;并行软件模型检测[J];计算机工程;2008年19期

8 何恺铎;顾明;宋晓宇;李力;李江;;面向源代码的软件模型检测及其实现[J];计算机科学;2009年01期

9 林璇;;模型检测方法在入侵检测中的应用研究[J];现代计算机(专业版);2009年02期

10 顾滨兵;;一种软件模型检测方法及其原型系统[J];微计算机应用;2010年11期

中国重要会议论文全文数据库 前5条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

中国博士学位论文全文数据库 前10条

1 奚琪;基于模型检测的二进制代码恶意行为识别技术研究[D];解放军信息工程大学;2014年

2 黄镇谨;基于模型检测的时空性能分析若干问题研究[D];合肥工业大学;2016年

3 江华;界程演算模型检测[D];贵州大学;2008年

4 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

5 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

6 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

7 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

8 尹良泽;基于SAT的组合迁移系统模型检测技术研究[D];清华大学;2014年

9 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

10 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

中国硕士学位论文全文数据库 前10条

1 黄延凯;基于图转换的关联属性规约模型检测及其支撑平台研究[D];南京航空航天大学;2015年

2 余鹏;基于模型检测的网络传播干预策略问题研究[D];南京航空航天大学;2015年

3 程贝;基于抽象和学习的统计模型检测研究[D];华东师范大学;2016年

4 何佳;面向复杂随机系统的贝叶斯统计模型检测方法[D];华东师范大学;2016年

5 王云云;基于分组压缩算法的并行程序模型检测[D];中国科学技术大学;2016年

6 段廷银;基于云计算平台的时态逻辑模型检测算法研究与实现[D];郑州大学;2016年

7 许鹏涛;基于模型检测的入侵检测基准测试平台研究[D];郑州大学;2016年

8 李婉璐;基于模型检测的电子商务交易协议形式化分析与验证[D];宁夏大学;2016年

9 张衍志;符号化模型检测算法的研究[D];吉林大学;2009年

10 黎吾平;模型检测在软件方面的应用[D];吉林大学;2008年

，

本文编号：1204789