1.一种设计阶段网络交易业务交互过程的逻辑漏洞分析方法具体包括如下步骤：S100：利用颜色petri网对网络交易业务交互过程进行建模，构建交互业务流程融合网络IBPF；

S200：提出所述网络交易业务交互过程中的交易逻辑一致性和交易处理完成状态两个基本安全属性；

S300：基于用于发现网络交易业务交互过程中逻辑漏洞的算法，结合交互业务流程融合网络IBPF和所述两个基本安全属性，对设计阶段网络交易业务交互过程进行漏洞分析和验证。

2.根据权利要求1所述的方法，所述S100步骤中的颜色petri网具体定义为：颜色Petri网是一个九元组CPN＝(P，T，A，∑，V，C，G，E，I)，其中，优选的：

1)P是一组有限的库所集，用圆圈来表示；

2)T是一组有限的变迁集T，使得 用矩形来表示；

3) 是一组有向弧集，用有向弧来表示；

4)∑是一组有限的非空颜色集；

5)V是一组有限的类型变量，使得Type[v]∈∑对所有变量v∈V；

6)C：P→∑是一个为每个库所指定颜色集的函数；

7)G：T→EXPRV是一种判定函数，它为每个变迁t指定一个布尔表达式，使Type[G(t)]＝Bool；

8)E：A→EXPRV是一个弧表达式函数，它将弧表达式赋给每个弧a，使得Type[E(a)]＝C(p)MS，其中p是连接到弧a的库所，MS表示多重集；

9)I： 是一个标识初始化函数，使Type[I(p)]＝C(p)MS，其中MS表示多重集。

3.根据权利要求1所述的方法，所述S100步骤中的交互业务流程融合网络IBPF描述了基于颜色petri网的分布式、多主体和多会话的网络交易业务交互过程，其具体定义为：逻辑业务流程LBP＝(P，T，A，∑，V，C，G，E，I)，其中：LBP有三个特殊的库所α，β和γ，其中α∈P称为初始库所，β∈P称为终止库所，γ∈P称为存储库所，一个具有通道的逻辑业务流程LBPC＝(P∪PIN∪PO，T，A∪AIN∪AO，∑，V，C′，G，E′，I′)，LBPC是从LBP扩展而来的，它集成了一些交互库所(通道)，用来描述不同主体之间交易参数的通信通道，其中：

1) PI N 是 一 组 输 入 通 道 库所 ，P O 是 一 组 输 出 通 道库 所 ，

2)

3)

4)C′：(PIN∪PO)→∑，如果p∈P，那么C′(p)＝C(p)；

5)E′：(AIN∪AO)→EXPRV，如果a∈A，那么E′(a)＝E(a)；

6)I′：(PIN∪PO)→EXPRφ，如果p∈P，那么I′(p)＝I(p)；

两个网的融合运算Φ为LBPC1ΦLBPC2＝LBPC＝(P∪PIN∪PO，T，A，∑，V，C，G，E，I)，其中P＝P1∪P2，T＝T1∪T2，A＝A1∪A2，∑＝∑1∪∑2，V＝V1∪V2，(p∈Pn)→(C(p)＝Cn(p))∧(I(p)＝In(p))，(a∈An)→(A(a)＝An(a))，(t∈Tn)→(G(t)＝Gn(t))；

交互业务流程融合网络IBPF＝(P∪PIN∪PO，T，A，∑，V，C，G，E，I)＝LBPC1ΦLBPC2Φ...ΦLBPCm，一个IBPF是m(m≥2)个LBPC的融合。

4.根据权利要求1所述的方法，所述步骤S200中的交易逻辑一致性定义为：在初始标识M0下，m∈N，每个交易结束状态M需要满足以下条件：

1)对于每个参数v， vBOOL＝true；

2)对于表示参与者或交易的每个变量ρ， 和 它只有一个值；

其中，βm表示终止库所，γm表示存储库所，m≥2，N是自然数集。

5.根据权利要求1所述的方法，所述步骤S200中的交易处理完成状态定义为：在初始标识M0下，m∈N，σ是IBPF的可执行变迁序列，并且需要满足以下两个条件：

1)

2)

其中，βm表示终止库所，γm表示存储库所，m≥2，N是自然数集。

6.根据权利要求1所述的方法，所述步骤S300具体为：根据逻辑漏洞构造初始配置，利用用于发现网络交易业务交互过程中逻辑漏洞的算法获得一个终止状态，并分析相应的逻辑漏洞，最后再通过构造新的初始配置来验证其他逻辑漏洞。

7.根据权利要求1所述的方法，所述步骤S300的用于发现网络交易业务交互过程中逻辑漏洞的算法，具体为：步骤1：标识集 ∏＝{M0}；其中，M0是初始标识；

步骤2：设M0为根节点，并标记为“中间状态”；

步骤3：当存在“中间状态”节点时，选择任意一个“中间状态”节点作为M；

步骤3.1：如果M是交易完成状态，但不满足交易逻辑一致性，则Ω＝Ω∪{M}，重复步骤

3，否则进行下一步；

步骤3.2：如果 M在t下都不发生，则∏＝∏∪{M}，重复步骤3，否则进行下一步；

步骤3.3：如果上述都不满足，那么对于在M下都有发生权的t(t∈T)来说，如果存在则将M’标记为“中间状态”，∏＝∏∪{M’}，重复步骤3；

步骤3.4：去除标记为“中间状态”的M，重复步骤3。