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

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

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

所述步骤S200中的交易逻辑一致性定义为：在初始标识M0下，m∈N，其中，M0是一个集合，其代表的是petri网的初始标识，即当前库所中含有的令牌状态的集合；每个交易结束状态需要满足以下条件：

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

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

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

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

1)

2)

E(t，βm)是从变迁t到库所βm的输入弧上的弧表达式；M(βm)表示库所βm中的标识；

表示所有属于库所βm前置变迁的累加和；

E(t，γm)是从变迁t到库所γm的输入弧上的弧表达式；M(γm)表示库所γm中的标识；

表示所有属于库所γm前置变迁的累加和。

2.根据权利要求1所述的方法，所述S100步骤中的交互业务流程融合网络IBPF描述了基于颜色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表示多重集；

逻辑业务流程LBP＝所述九元组CPN＝(P，T，A，∑，V，G，G，E，I)，其中：LBP有三个特殊的库所α，β和γ，其中α∈P称为初始库所，β∈P称为终止库所，γ· ·

∈P称为存储库所， 其中，点 在前面表示前置变迁集，点 在后面的表示后置变迁集；

一个具有通道的逻辑业务流程LBPC是从LBP扩展而来的，它集成了多个交互库所，用来描述不同主体之间交易参数的通信通道：LBPC＝(P∪PIN∪P0，T，A∪AIN∪A0，∑，V，C’，G，E’，I’)，其中：

1) P I N 是 一 组 输 入 通 道 库 所 ，P 0 是 一组 输出 通 道 库所 ，

2)

3)

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

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

6) 如果p∈P，那么I’(p)＝I(p)；

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

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

4.根据权利要求1所述的方法，所述步骤S300的用于发现网络交易业务交互过程中逻辑漏洞的算法，具体为：

步骤1：标识集 Π＝{M0}；其中，Ω是库所对应的令牌集合，M0是初始标识；

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

步骤3：当存在“中间状态”节点时，选择任意一个“中间状态”节点作为M；步骤3.1：如果节点M是交易完成状态，但不满足交易逻辑一致性，则Ω＝Ω∪{M}，重复步骤3，否则进行下一步；

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

步骤3.3：如果上述步骤3.1、3.2的判断前提都不满足，那么对于在M下都有发生权的t，t∈T来说，如果存在其他节点 则将M’标记为“中间状态”，Π＝Π∪{M’}，重复步骤3；

步骤3.4：如果上述步骤3.1、3.2、3.3的判断前提都不满足，去除标记为“中间状态”的M，重复步骤3。