基于Petri网的银行软件身份验证流程建模与分析

张 顺，方 欢

（安徽理工大学 数学与大数据学院，安徽 淮南 232001）

现如今大多数行业都有各自的业务流程，而一个良好的业务流程可以提高效率，节约成本。通过对业务流程建模可以发现业务流程结构存在的问题并且对该模型进行优化。目前针对业务流程建模提出的建模语言有BPM、BPEL、EPCs 和YAWL[1-2]等。而Petri 网建立在一定的数学理论基础上，可以用来分析比较复杂的系统，有理论依据。所以使用基于Petri网的建模与分析的学者越来越多。文献[3]针对微博网络信息传播过程，结合颜色Petri网和时延Petri网建立的Petri网模型可以更加真实地模拟信息传播情况。文献[4]基于Petri 网对银行贷款流程进行建模，并使用关联矩阵和不变量性质对其进行分析，使得银行贷款流程更加安全高效。文献[5]将技术系统中的一些元素与有色Petri 网结合起来，为系统动作时序的改进提供了方向与优化模型。文献[6]使用Petri 网对AlexNet 和DenseNet-BC 建模并且通过所建模型优化了网络结构和参数。文献[7]针对在前台挂号时用户的不良行为，使用含测试弧的Petri 网对该流程进行建模优化，优化后的系统有效地约束了用户的不良行为，提高了前台的工作效率。

银行软件掌握着人们的财产安全。而软件开发者也考虑到了该软件的重要性，在使用该软件时需要进行身份验证，所以需要对该身份验证流程进行分析，防止身份冒用，降低风险。本文根据该银行软件的身份验证流程，构建符合银行软件身份验证流程的Petri网模型，并使用基于Petri网的一些理论知识分析所建立系统的可达性、有界性和活性，来帮助用户实现身份认证，降低身份冒用的风险。

定义1[8]（网的概念）模型Petri 网N=(S,T;F)是一个三元组满足以下条件：

（Ⅰ）S⋂T=∅,S⋃T≠∅；

（Ⅱ）F⊆(S×T)⋃(T×S)；

（Ⅲ）dom(F)⋃cod(F)=S⋃T。

其中dom(F)={x∈S⋃T|∃y∈S⋃T:(x,y)∈F}；
cod(F)={x∈S⋃T|∃y∈S⋃T:(y,x)∈F}。

定义2[8]（关联矩阵）设Σ=(S,T;F,M)为一个Petri 网，S={s1,s2,…,sm}，T={t1,t2,…,tn}，则Petri网N的结构(S,T;F) 可以用一个n行m列矩阵A=|aij|n×m来表示，其中

其中i∈{1,2,…,n},j∈{1,2,…,m} 。则称A为网N=(S,T;F)的关联矩阵。

定义3[8]（唯一可达向量网）设N=(S,T;F)为一个Petri 网Σ=(N,M0)。如果对∀M∈R(M0)，状态方程

都有唯一的一个解向量X，则称Σ为一个唯一可达向量网系统。若对任意初始标识M0，Σ都是一个唯一可达向量网系统，则称N为唯一可达向量网。它有以下推论：

推论1网N=(S,T;F)是唯一可达向量网，当且仅当N的关联矩阵A是一个行满秩矩阵，即R(A)=|T|。

推论2若Σ=(S,T;F,M0)为一个行满秩Petri网，那么对任意m(m=|S|) 维向量M，方程M=M0+ATX有唯一解，其中A是Σ的关联矩阵。

定义4[8]（可达性）设N=(S,T;F,M) 为Petri网，如果存在t∈T，使M[t＞M′，则称M′为从M直接可达的。其中，M[t＞M′表示从标识M发生变迁t得到一个新的标识M′。如果存在变迁序列t1，t2，…，tk和标识序列M1，M2，…，Mk使 得M[t1＞M1[t2＞M2…Mk-1[tk＞Mk，则称Mk是从M可达的。从M可达的一切标识的集合记为R（M）。

构建Petri网模型来模拟身份验证行为流程。该软件的身份验证流程主要包括3个部分：软件登录、身份信息填写和人脸识别。其中软件登录部分使用的是选择结构，这表明用户只能选择一种方式进行登录；
在身份信息填写部分使用的是交叉结构，这表明用户必须填写真实姓名和身份证件号才能进行下一步；
而人脸识别部分则使用了选择和循环结构，这表明如果用户通过人脸识别验证则能正常使用该软件，否则就要重新进行登录。该流程的具体描述如下：当用户要使用该软件时，首先要打开它进行登录t0，登录分别为两种方式，一种是使用短信登录t1，另一种是使用微信登录t2。当登录成功之后开始进行身份信息验证t3，分别填写用户姓名t4和身份证号码t5，都填写完成之后，提交验证信息t6。如果身份信息验证失败t10，则重新进行身份信息验证。如果身份信息验证成功，则进行人脸识别验证t7，若面部识别验证成功，可以正常使用该软件，否则需要重新登录验证。根据该流程构建的Petri 网模型如图1 所示，该模型中各个变迁的含义描述如表1所示。

图1 某银行软件身份验证流程Petri网结构图Σ1

表1 模型各变迁含义

本节是根据Petri网的一些理论性质来分析该模型的可达性、有界性、安全性以及活性。可达性可以保证身份验证模型的任意状态都是可达的，不存在孤立的状态。有界性可以保证该模型不会过分地消耗系统资源。而安全性则保证了该模型的任意状态只需满足一个条件即可执行。

通过直接使用状态方程求解作为判断起始状态标识到终止状态标识是否可达性的基本方法，它的一般流程如下：

Step1首先给出与Petri 网对应的起始标识M0和终止标识M，然后求出状态方程M=M0+ATX的非负整数解。如果不存在非负整数解，那么M不是从M0可达的；
如果存在非负整数解，则执行Step2。

Step2对状态方程的非负整数解Xj（j=1，2，…），检查是否存在合法变迁序列σ∈T*使得M0[σ＞且∀i∈{1,2,…,|T|}:#(ti/σ)=Xj(i) 。当对某个Xj找出一个合法序列时，说明M0到M可达，即，M∈R(M0)；
否则要检查所有的解向量，如果找不到相应的合法序列，说明M0到M不可达，即M∉R(M0)。

按照这个方法对一般的Petri 网作可达性判定，需要遍历所有解向量，直到找到符合网结构的序列，所涉及到的计算量大。为了使可达性的判定更加方便，本文使用唯一可达向量网的方法来判断任意两个标识之间的可达性，本文给出该方法的判定流程如表2。

表2 本文判断可述性算法

本文算法1 的第2 步到第9 步表示，先判断网Σ的关联矩阵是不是行满秩矩阵，根据推论1，如果R(A)!=|T|，则矩阵A不是行满秩矩阵，即网Σ不是唯一可达向量网。第3步表示对网Σ进行满秩平凡拓展得到唯一可达向量网Σ1，然后计算出网Σ1的关联矩阵，构造与网Σ对应的新的起始表示和终止标识。第11步是根据推论2使用第10步计算好的右逆阵B来求唯一的解向量X。第12步到第13步是判断解向量X是否是大于等于零的，也就是说解向量里的每个元素都是非负的，其次还要判断在网中是否有一条合法的序列满足解向量X，该序列中某个活动出现的次数也要与解向量中对应的数字相同。如果同时满足这两个条件则可以判定初始标识到终止标识是可达的。

使用唯一可达向量网的方法来判断网Σ=(S,T;F,M)中从初始标识M0到M1标识是否可达的算法流程如算法1所示。

输入参数：网Σ，网Σ的关联矩阵A，初始标识M0和终止标识M1。

输出结果：True表示初始标识M0到终止标识M1可达，False表示初始标识M0到终止标识M1不可达。

该系统网Σ1的初始标识M0={1，0，0，0，0，0，0，0，0，0}。我们判断状态标识M′={1，0，0，0，0，0，0，0，0，0}是否从M0可达。该系统网的关联矩阵A为

对矩阵A进行初等变换，通过计算得到R(A)=8 ＜11。矩阵A11×10是非行满秩矩阵，网Σ1是非满秩Petri 网。需要对该Petri 网Σ1进行满秩平凡拓展转换成唯一可达向量网。因为R(A)=8，并且t2、t5、t7对应的行向量能够被其他向量表示，所以在网中额外加入三个库所S10、S11、S12，并添加流关系，F′={(t2,S10),(t5,S11),(t7,S12)}，这3 个库所只充当计数器的作用，它们包含的标识数表示对应变迁的发生次数，对整个网结构的性质没有影响。拓展后的满秩Petri网如图2所示。

图2 平凡拓展后的满秩Petri网Σ2

经过平凡拓展后的网系统Σ2的关联矩阵A2为

矩阵A2初等变换得出R(A2)=11，为行满秩矩阵，系统网Σ2为满秩Petri网。

可以通过式（3）求出关联矩阵A2的右逆阵为

由Σ1中的标识M′可以得出在Σ2中对应的标识为

其中k，m，n分别表示当库所S9有一个标识的情况下（网Σ2运行结束时），库所S10、S11、S12中的标识数。

可以求出解向量

若取k=0，n=1，m=1，则得到

为状态方程的非负整数解。所以X1也是Σ2的状态方程的一个解。通过Σ2的运行可以验证，存在变迁序列σ1=t0t1t3t4t5t6t7t8满足M0[σ1＞且#(ti/σ1)=X(i)(i=0,1,2,…,10) 。所以，M′是从M0可达的。

然后，我们通过关联矩阵与状态标识来判断系统网Σ1中的变迁是否存在可以触发的可能。该模型的初始标识为

通过变迁运行规则计算方法，使用关联矩阵，可以对在M0标识状态下网的运行情况进行分析。我们首先对标识M0下变迁t0的使能状态进行分析。

最后，通过使用状态方程来计算系统网Σ1中的状态标识的变化情况，以此来分析该系统网的有界性。分析该模型可知，在初始状态下，只有起始库所有标识，其他变迁都因为缺少标识而没有发生权，只有变迁t0有发生权，根据状态方程可以计算出在标识M0下变迁t0发生后的标识M1。

触发t0变迁得到的新标识M1表示用户打开软件进行登录。在M1标识下，t2变迁处于使能状态可以发生，同理可以根据状态方程求出M2，其他标识也可以通过该方法计算得出。通过计算可以得知网系统Σ1在运行状态下，各个库所的最大标识数都为1，因此该网系统是一个有界网，并且是一个安全网。

使用PIPE 软件对上面的分析进行验证，首先使用PIPE对该模型的Petri网结构进行建模，然后我们使用它的分析功能，运行网Σ1的其中一条发生序列和状态空间分析结果见图3。

图3 使用PIPE工具得到的运行结果

通过它的运行结果可以看出，该模型的Petri 网是有界的、安全的，并且它的其中一个执行序列为t0t2t3t4t5t6t7t8，如果我们求出的解向量

其中k，m，n分别取1，则该向量为{1，0，1，1，1，1，1，1，1，0，0}，在网Σ1中满足该向量的一条序列为t0t2t3t4t5t6t7t8，与使用PIPE仿真验证的结果一致。因此本文针对该软件的身份验证流程模型分析是合理的，可以使用该模型对身份验证流程进行优化。

银行软件掌握着用户的财产安全，为了降低身份冒用风险，本文对该软件的身份验证流程建立了Petri网模型，并使用Petri网相关的一些理论知识，如唯一可达向量网、状态方程和关联矩阵，来分析Petri网模型的可达性、有界性和活性。本文使用唯一可达向量网的方法来求解系统网的可达性，与直接使用状态方程的方式相比减少了工作量。最后使用仿真工具PIPE 进行验证，验证结果表明，本文所建立的模型是有界的、安全的。