颜色Petri网的电子商务协议形式化分析方法研究

发布时间：2017-04-20 12:00

  本文关键词：颜色Petri网的电子商务协议形式化分析方法研究，由笔耕文化传播整理发布。

【摘要】：随着Internet的迅猛发展，电子商务已经深入到了社会的各个角落。如何确定电子商务交易的安全可靠，成为了一门重要的研究课题。电子商务协议是一种保证电子商务交易正常展开的协议，在满足安全协议的性质的同时，还要保证满足可追究性、公平性和时限性等特殊性质。对电子商务协议的形式化分析，是发现电子商务协议缺陷的有效工具。本文使用颜色Petri网形式化分析工具，提出了可追究性、公平性和时限性三者兼顾的形式化建模方法，并对电子商务协议中存在的攻击进行了建模分析。 首先，在高级网颜色Petri网的基础上，提出一种对电子商务协议的可追究性、公平性和时限性建模的颜色Petri网方法。在协议的可追究性和公平性Petri网模型基础上，加入了复杂多变的时限性因素，形成了三者兼顾的模型。利用Petri网中逆向状态分析方法对该模型进行分析，验证协议是否满足三个性质。以改进的ZG协议KZG协议为例，，用所提建模方法建立了KZG协议的颜色Petri网模型，经过逆向状态分析，验证了该协议满足可追究性、公平性和时限性。 其次，研究了电子商务协议中存在的不安全状态。提出从电子商务协议的发送方非否认证据EOO(Evidence Of Origin)和接收方非否认证据EOR(Evidence Of Recipt)中提取不安全状态并定义不安全状态的方法，解决了不同电子商务协议不安全状态难以确定的难题。提出了建立带攻击者的颜色Petri网建模方法并利用逆向分析方法分析不安全状态是否可达。以CMP1为例，建立了带攻击者的CMP1颜色Petri网模型，进过分析发现该协议存在的不安全状态可达，该协议存在漏洞。 最后，利用颜色Petri网的仿真工具CPN Tools对所建立的KZG协议以及CMP1协议的颜色Petri网模型进行了仿真实验。运行状态空间分析工具，建立ML查询函数，查询协议的相关性质是否满足，进一步验证所提方法的正确有效。
【关键词】：电子商务协议 形式化分析 颜色Petri网 CPN Tools KZG CMP1
【学位授予单位】：燕山大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：TP301.1;TP393.04
【目录】：

• 摘要5-6
• Abstract6-9
• 第1章 绪论9-15
• 1.1 研究背景和意义9-10
• 1.2 国内外研究现状10-12
• 1.2.1 Petri 网的研究现状及分析10-11
• 1.2.2 高级网颜色 Petri 网的研究现状及分析11-12
• 1.2.3 国内外研究现状的总结12
• 1.3 本文主要内容12-13
• 1.4 本文组织结构13-15
• 第2章 电子商务协议及颜色 Petri 网分析方法15-23
• 2.1 电子商务协议的相关概念15-17
• 2.1.1 电子商务协议的语义15-16
• 2.1.2 电子商务协议的安全性质16-17
• 2.2 颜色 Petri 网的相关知识17-20
• 2.2.1 颜色 Petri 网的基本定义18
• 2.2.2 颜色 Petri 网的特征及引发规则18-19
• 2.2.3 颜色 Petri 网的性质19-20
• 2.3 颜色 Petri 网的主要分析方法和工具20-22
• 2.4 颜色 Petri 网的方法的总结22
• 2.5 本章小结22-23
• 第3章 一种颜色 Petri 网的电子商务协议建模方法23-35
• 3.1 引言23
• 3.2 一种颜色 Petri 网的电子商务协议建模方法23-27
• 3.2.1 电子商务协议消息的抽象24
• 3.2.2 具体建模步骤24-26
• 3.2.3 协议的分析26-27
• 3.3 实例分析27-34
• 3.3.1 协议的描述28
• 3.3.2 协议的建模28-31
• 3.3.3 协议的分析31-33
• 3.3.4 本文方法与相关方法的比较33-34
• 3.4 本章小结34-35
• 第4章 一种颜色 Petri 网的电子商务协议攻击建模方法35-47
• 4.1 引言35-36
• 4.2 攻击者模型及攻击目标和手段36-37
• 4.2.1 Dolev-Yao 模型36
• 4.2.2 安全协议中的攻击目标和手段36-37
• 4.3 一种颜色 Petri 网的电子商务协议攻击建模方法37-40
• 4.3.1 协议的建模及分析过程37-38
• 4.3.2 协议的建模步骤38-39
• 4.3.3 协议的不安全状态的定义39-40
• 4.3.4 协议的攻击的结果分析40
• 4.4 实例分析40-46
• 4.4.1 CMP1 协议40
• 4.4.2 带有攻击者的 CMP1 协议流程40-41
• 4.4.3 带有攻击者的 CMP1 协议的颜色 Petri 网模型41-44
• 4.4.4 带有攻击者的 CMP1 协议的颜色 Petri 网模型的分析44-46
• 4.5 本章小结46-47
• 第5章 实验分析47-54
• 5.1 实验工具47-49
• 5.1.1 CPN Tools 中的 ML 语法47-48
• 5.1.2 CPN Tools 中颜色 Petri 网的编辑及运行48-49
• 5.2 实验验证49-53
• 5.2.1 KZG 协议的验证49-52
• 5.2.2 CMP1 协议的验证52-53
• 5.3 本章小结53-54
• 结论54-55
• 参考文献55-59
• 攻读硕士学位期间承担的科研任务与主要成果59-60
• 致谢60-61
• 作者简介61

【参考文献】

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

1 王志强;;着色Petri网应用研究[J];电脑与信息技术;2010年05期

2 刘道斌,郭莉,白硕;基于Petri网的安全协议形式化分析[J];电子学报;2004年11期

3 刘文琦;顾宏;;基于分层时间有色Petri网的支付协议公平性分析[J];电子与信息学报;2009年06期

4 刘道斌,郭莉,白硕;一种新的安全协议验证方法[J];计算机研究与发展;2003年10期

5 黎波涛,罗军舟;不可否认协议的Petri网建模与分析[J];计算机研究与发展;2005年09期

6 刘雪艳;吴慧欣;张强;王彩芬;;基于面向对象时间Petri网的密码协议分析[J];计算机工程;2009年13期

7 王剑;唐朝京;张权;张森强;;基于Petri网的密码协议分析[J];计算机工程与科学;2006年02期

8 龙士工,李祥;基于着色Petri网仿真模型的安全协议分析[J];计算机仿真;2005年06期

9 周典萃,卿斯汉,周展飞;Kailar逻辑的缺陷[J];软件学报;1999年12期

10 王贵林,卿斯汉,周展飞;认证协议的一些新攻击方法[J];软件学报;2001年06期

  本文关键词：颜色Petri网的电子商务协议形式化分析方法研究，由笔耕文化传播整理发布。

本文编号：318596