对于形式化颜色Petri网电子商务协议形式化策略

论文导读：的颜色Petri网模型，经过逆向状态浅析，验证了该协议满足可追究性、公平性和时限性。其次，探讨了电子商务协议中有着的不安全状态。提出以电子商务协议的发送方非否认证据EOO(EvidenceOfOrigin)和接收方非否认证据EOR(EvidenceOfRecipt)中提取不安全状态并定义不安全状态的策略，解决了不同电子商务协议不安全状态难以确定的
摘要：随着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论文
本论文由www.7ctime.com,需要论文可以联系人员哦。摘要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.1 颜色 Petri 网的基本定义18

2.2 颜色 Petri 网的特点及引发规则18-19

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.1 协议的描述28

3.2 协议的建模28-31

3.3 协议的浅析31-33

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 协论文导读：1协议404.4.2带有攻击者的CMP1协议流程40-414.4.3带有攻击者的CMP1协议的颜色Petri网模型41-444.4.4带有攻击者的CMP1协议的颜色Petri网模型的浅析44-464.5本章小结46-47第5章实验浅析47-545.1实验工具47-495.1.1CPNTools中的ML语法47-485.1.2CPNTools中颜色Petri网的编辑及运转48-495.2实验验证
议的不安全状态的定义39-40

4.

3.4 协议的攻击的结果浅析40

4 实例浅析40-46

4.1 CMP1 协议40

4.2 带有攻击者的 CMP1 协议流程40-41

4.3 带有攻击者的 CMP1 协议的颜色 Petri 网模型41-44

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