颜色Petri网的电子商务协议攻击分析方法

司亚利，刘文远，卢 贝

（1.燕山大学 里仁学院，河北 秦皇岛066004；2.燕山大学 信息科学与工程学院，河北 秦皇岛066004）

0 引 言

安全协议是实现网络安全的关键技术之一，许多安全协议在设计或实现后，由于漏洞的存在而受到攻击［1］，所以协议的安全性认证至关重要。在采用形式化方法分析安全协议方面，Petri网技术是一个重要研究内容。文献［2－7］针对不同的安全协议，从不同角度提出了基于颜色Petri网（CPN）的形式化建模与分析方法。进而，针对一种常见并且危害性最大的重放攻击形式，相关形式化分析成果也陆续提出。Aurn等设计并提出一种分析协议优势和缺陷的重放攻击分析方法［8］；张卫华等提出更加简便高效的CPN 规划识别及多步骤攻击检测方法［9］；Fan Kai等利用并发签名和可信第三方来阻止恶意支付，以保证电子商务交易协议的安全性和公平性［10］，但是缺少形式化分析方法的认证。

电子商务协议属于一种特殊的安全协议，除了继承安全协议的性质，还有自身特殊的性质，如公平性、可追究性、原子性和时限性等。目前在电子商务协议的形式化分析中，多数侧重于研究协议的特殊性质，而极少关注电子商务协议的安全属性，缺少关于攻击的形式化分析方法。因此，针对电子商务协议中的重复攻击问题，提出一种基于颜色Petri网的攻击形式化建模方法，并利用逆向状态分析和CPN Tools两种方法分析CMP1协议中不安全状态的可达性，从而得到攻击结果。

1 CPN 的电子商务协议攻击分析方法

目前，关于电子商务协议的攻击分析研究较少，并缺乏形式化工具的应用分析。本节提出一种针对电子商务协议攻击的颜色Petri网建模方法，然后采用理论和实验两种方法分析所定义的不安全状态是否可达，如果可达表明存在被攻击的漏洞，反之则说明协议是安全的。在对电子商务协议的攻击建模和分析过程中，遵循的操作步骤是：首先建立电子商务协议正常执行的模型；其次加入攻击者模型；再次定义协议的不安全状态；最后是协议的攻击结果分析。具体阐述如下。

1.1 建立协议正常执行的模型

一个颜色Petri网可以表示成一个七元组：CPN＝｛P，T，F，C，I＋，I－，M0｝。其中P 表示库所的有限集合，T是变迁的有限集合，P ∪T ≠，P ∩T ≠。F ∈（P×T）∪（T×P）是有向弧集合，它建立库所颜色和变迁的每种颜色之间的对应关系。C 是定义在P ∪T 上的颜色集，I＋和I－分别称为P×T 的输入函数和输出函数，M0是初始标识。利用CPN ML（machine language）语法声明模型中的颜色集、变量、常量和函数，建立分层颜色Petri网模型，把每个实体定义成一个替代变迁。

（1）协议消息与CPN 元素的对应关系。建模的基础准备是对电子商务协议进行形式化语义描述，而已有的规范语义大多针对特定的协议进行设计，通用性不强，如果分析其它协议就需要对原有语义加以扩展。本文为了把通用的协议消息说明和CPN 方法相结合，抽象出通用协议的基本要素，并在此基础上建立与颜色Petri网元素的对应关系：

原子消息，即私钥、公钥、会话密钥、明文等不可拆分的消息，对应简单颜色集（unit类型）。如：colset SK＝with ska｜skb｜skc；颜色集SK 声明了3个会话密钥集。

复合消息，是原子消息经过若干运算操作（加密、哈希运算、拼接、签名等）后形成的消息，对应复合颜色集（product类型）。例如用公钥加密的消息｛m｝pk 可声明为colset MES ＝product M＊PK 。

各主体之间传递的复杂消息，对应CPN 中的联合颜色集（union类型）。

电子商务协议的整个执行过程，对应颜色Petri网仿真（CPN Simulation）。

（2）根据上一步骤的对应关系，建立协议在正常执行状态下的CPN 模型。

首先，对各主体的公钥、私钥和会话密钥等建立对应的公钥颜色集、私钥颜色集、会话密钥集及各自的颜色变量。

其次，把协议中的每条消息抽象成原子消息或复合消息，定义相应的简单颜色集、复合颜色集、颜色变量，同时建立协议的不可否认证据。

再次，建立主体之间传输的复杂消息颜色集。根据协议的执行语句，如果是多个复合消息的拼接，则建立一个union类型的颜色集来表示整个协议主体间交换消息的集合。

最后，建立颜色Petri网。对于比较复杂的电子商务协议，采用层次清晰的分层结构。在顶层建立协议的完整执行流程模型，把每一个实体定义成一个替代变迁。为了体现主体功能的独立集中性，主体处理的消息在底层模型实现。同时，按照协议的需求为变迁和输出弧进行程序判定，来达到最完善的协议建模。

1.2 加入攻击者的模型

分析攻击者的攻击流程，并把攻击者模型加入到第1.1节建立的模型中。具体方法是先分析并写出协议可能遭受的攻击及其流程，画出带有攻击者的协议流程图。然后，采用第1.1节的建模方法建立攻击者模型，最后将攻击者模型加入到正常执行的模型中，即在分层CPN 模型的顶层加入攻击者替代变迁，形成完整的带有攻击者的CPN 模型。

1.3 定义协议的不安全状态

安全协议认证的攻击者目标比较简单，一般是通过攻击协议以获取会话密钥，并冒充他人身份进行会话以实现欺诈等非法活动。然而，电子商务协议比安全协议复杂，不同协议主体的交换消息又大不相同，难以定义攻击目标。因此，如何定义电子商务协议的不安全状态成为关键问题。

经过深入研究发现，为了分析电子商务协议的可追究性和公平性，在协议的具体步骤设计时都已经定义了发方不可否认证据EOO（evidence of origin）和收方不可否认证据EOR（evidence of recipt），这是参与方相互交换消息的重要组成部分，同时也是保证自身利益的不可否认证据。利用这个特性，本文提出在分析重放攻击时，把电子商务协议的攻击目标定义成EOO 和EOR 中最为敏感的重要信息，如电子现金、用户信息、交易货物等。这种方法既准确，又能保证不同协议的不安全状态定义有据可依。以CMP1协议为例，EOO 是｛m｝SKa，EOR 是｛h（m）｝SKb，用本方法提取出的攻击目标是发送方发出的原始消息m。

1.4 分析协议的攻击结果

Petri网中分析网模型的方法有很多，其中状态方程分析协议模型准确，CPN Tools对模型进行分析和仿真方便快捷。因此，本文在提出新的建模方法后，先利用Petri网的逆向分析方法进行理论分析，然后利用颜色Petri网的CPN Tools仿真工具对模型进行仿真分析，从而得出结论。

（1）理论分析。逆向状态分析方法，也就是求解网的状态方程，体现了倒推的思想。设CPN＝｛P，T，F，M0｝是一个有界Petri网，P ＝｛p1，p2，…，pm｝，T ＝｛t1，t2，…，tn｝，则CPN 的结构可以用一个n 行m 列的关联矩阵（incidence matrix）C ＝ cijn×m来表示［11］，其中aij＝－，i（｛1，2， …，n｝，j（｛1，2， …，m｝，＝

CPN 的标识（即不安全状态）能够用一个非负整数向量M＝［M（p1），M（p2），…，M（pm）］T来表示，得到状态方程M＝M0＋CTX。最后，分析协议的安全性通过解状态方程实现，如果无解说明该状态是安全的；反之有解则说明不安全，并给出变迁发生序列（也就是攻击剧情）。

（2）实验分析。建立协议的CPN 模型后，利用CPN Tools工具进行仿真分析，检验所提方法的正确性和有效性。CPN Tools具有交互性好和时效性强等优点，并且有自动化分析过程。运行CPN Tools中的状态空间，利用ML查询函数判断定义的不安全状态是否可达。如果可达，则该协议存在漏洞，肯定是不安全的。如果不可达，则说明该协议是安全的。

2 实例分析

以经典的CMP1（certified electronic mail）电子商务协议为例，利用提出的方法对其进行建模分析。

2.1 协议的描述

CMP1协议正常执行的具体描述如下：

EOO：｛m｝SKaEOR：｛h（m）｝SKb；

（1）A →B：h（m），｛K｝Kttp，｛｛m｝SKa｝K；

（2）B →T：｛h（m）｝SKb，｛K｝Kttp，｛｛m｝SKa｝K；

（3）T →B：｛｛m｝SKa｝SKt；

（4）T →A：｛｛h（m）｝SKb，（B，m）｝SKt。

第（1）步表示参与方A 选择一个会话密钥K，把消息m的摘要h（m）、用K 对签名｛m｝SKa加密所生成的密文｛｛m｝SKa｝K、加密后的会话密钥｛K｝Kttp发送给B。第（2）步，B签名摘要h（m）生成｛h（m）｝SKb，和A 发送消息的后两部分转发给可信第三方T。T 解密后获取｛m｝SKa来检验A 的签名，通过｛h（m）｝SKb验证B的签名；对｛｛m｝SKa｝K获得的消息m 计算摘要h（m），和从｛h（m）｝SKb获得的h（m）进行比较，如果相同，则协议顺利执行第（3）步，把｛m｝SKa用T 的私钥签名后发给B；若不一致则终止协议。第（4）步，T 用私钥对B 签名后的摘要和（B，m）进行签名，并发送给A。

2.2 带有攻击者的CMP1协议流程

第1步：A →B：h（m），｛K｝Kttp，｛｛m｝SKa｝K；

第2步：B →T：｛h（m）｝SKb，｛K｝Kttp，｛｛m｝SKa｝K；

攻击者：I（B）→T：｛h（m）｝SKb，｛K｝Kttp，｛｛m｝SKa｝K；

第3步：T →B：｛｛m｝SKa｝SKt；

攻击者：T →I（B）：｛｛m｝SKa｝SKt；

第4步：T →A：｛｛h（m）｝SKb，（B，m）｝SKt；

攻击者：T →I（A）：｛｛h（m）｝SKb，（B，m）｝SKt。

上面给出的是带有攻击者的协议流程。攻击者I在第1步截获A 发送给B的消息，并在第2步冒充B给T 转发消息，T 正常执行比较消息摘要和验证签名的操作，如果通过验证，继续执行第3、4步，给A 和B 发送T 签过名的消息。攻击者在此过程中可冒充A 或B的身份接收从T 反馈的消息。

2.3 带有攻击者的CPN 模型

colset ID＝with A｜B｜T｜I；

colset M＝with ml；

colset PK＝with pka｜pkb｜pkt；

colset SK＝with ska｜skb｜skt；

colset EOO＝product M＊SK；

colset EOR＝product H＊SK；

colset EOO＿K＝product EOO＊KEY；

colset EOO＿S＝product EOO＊SK；

colset MSG ＝union s：H ＋k ＿e：K ＿E ＋keoo：EOO＿K＋eor：EOR＋seoo：EOO＿S＋bm：BM＋skey：SK；

首先给出的是带有攻击者的CPN 模型中部分颜色集声明。ID 定义了主体A 和B、可信第三方和攻击者这4个参与协议的主体身份；M 是主体发出的原始消息，PK 和SK分别是主体的公钥和私钥。EOO 和EOR 是product类型的颜色集，定义协议中的发方和收方不可否认证据。颜色集MSG 是union类型，表示每个主体间发送的消息，它组合了几个独立而又相关的颜色集。然后，定义各个颜色集的颜色变量，定义功能函数VeriSig（sk：SK，pk：PK），用于检验主体的签名信息。

根据2.1节和2.2节的协议流程，采用自顶而下的分层建模方法，首先建立协议的Top层模型，然后分别建立各主体的模型。

图1是带有攻击者的CMP1协议颜色Petri网的顶层模型。模型中，A、B、T 和I是替代变迁，分别对应相应的变迁子页，用于实现各主体的具体内部消息转换。T2A、A2B、Ib2T、Ia2B等库所表示主体之间发送消息，T2A 表示T 发送信息给A，Ib2T 表示攻击者I冒充主体B发送了一条消息给T。

图1 TOP层模型

图2是主体A 的模型。具体的执行流程是：A 签名消息m，提取出发方不可否认证据eoo，再用密钥K 加密eoo生成keo，作为第一部分消息。用Hash函数对消息m 进行运算，生成消息摘要h（m），作为第二部分消息。用可信第三方T 的公钥对密钥K 加密，作为第三部分的消息。然后，组合三部分消息发送给接收方B。在协议的第4 步A收到T 发送的消息后，对其解密，从而得到收方不可否认证据eor。

图2 主体A 的模型

图3为攻击者I的模型。攻击者有很多攻击手段，模型中，I截获A 给B发送的消息，然后冒充A 直接给B 转发消息；类似的，I截获B 给T 发送的消息，并冒充B 给T转发消息。针对协议第3步和第4步，I截获从T 发送出来的消息，利用T 的公钥解密消息，最终I获得从A 发送出的原始消息m，以达到攻击目标。

图3 攻击者的模型

接下来建立带有攻击者的CMP1协议的主体B 模型。攻击者冒充主体A 给B发送消息m，B收到消息后对h（m）进行签名，并与另外两部分消息组合起来转发给T。B 在收到T 反馈的消息后，解密获得发方不可否认证据。

图4是可信第三方T 的模型。T 分解B 发送的消息，得到eoo以验证A 的签名，对eor验证B的签名。T 对eoo解密得到的消息m 计算摘要h（m），对比eor中的摘要，如果二者相同，则可信第三方公布消息，为各主体获取使用。在这里，攻击者具有冒充A 或B提取消息的可能。

图4 可信第三方T 的模型

2.4 带有攻击者的CPN 模型分析

方法一：理论分析。根据建立好的CPN 模型，利用逆向状态分析方法对模型进行分析，具体过程按照第1.4节的理论分析部分进行。

建立CMP1协议的关联矩阵，包括协议关联矩阵的A模型子矩阵C1（见表1）、I模型的子矩阵C2（见表2）、B模型的子矩阵C3和T 模型的子矩阵C4（略）。

协议的初始状态是MT0＝［0，0，0，0，0，0，SK，M，HASH，KEY，PK，0，0，0，…，0］。此时只有A、B和I拥有知识集，例如主体的公私钥等。

表1 关联矩阵的子矩阵C1

表2 关联矩阵的子矩阵C2

不安全状态是MT＝［0，0，0，0，0，0，SK，M，HASH，KEY，PK，0，…，M，0，…，EOO，EOR］，即攻击者成功截获了A 给B发送的消息m。A 和B均取得对方的不可否认证据，但是没有发现他人窃取了消息。

得到并求解状态方程M＝M0＋CTX。利用线性函数的有解判定式可知方程有解，并且找到了一个可执行的变迁序列：σ＝sa，hs，keo，ek，g1，stb，get，sb，g2，stt，get，dek，deo，dem，com，reh，g3，deh，geoo，dem。

因此得出，攻击者能够窃取关键信息m，CMP1 协议存在不安全状态。

方法二：利用工具分析。先将已经建立好的CMP1协议的颜色Petri网模型根据第1节提出的方法录入到CPN Tools中，接下来运行状态空间分析和ML查询函数。

在仿真工具CPN Tools中单击EnterStateSpace tool，对模型所有可能的连通状态、状态空间和强连通分量状态图进行计算并保存。得到的状态空间报告如下所示，报告显示出整个模型共生成220 个结点和751 条弧，共产生3个死结点，即218，219，220。

接下来分析协议的可追究性，查询结果如图5 所示，攻击者I成功地获得了A 给B 发送的消息。因此，CMP1协议存在重放攻击的危险。

图5 查询结果

至此，采用两种方法分析得出的结论是一致的，能够说明本文提出方法是正确、有效的。

3 结束语

本文提出了一种基于颜色Petri网的电子商务协议攻击分析的建模方法，从协议的不可否认证据中提取不安全信息，定义成不安全状态，并给出了具体的建模和分析过程。继而以CMP1 协议为例，用所提方法建立协议的CPN 模型，经过理论分析和实验仿真后得出CMP1协议存在漏洞的结论，同时说明了所提出方法的有效性。本方法具有很好的通用性，能够对其它电子商务协议进行攻击建模和分析。

［1］Fan Yutao，Su Guiping，He Liu，et al.Study on a CPN－based auto－analysis tool for security protocols ［C］／／Proceedings of the 4th International Symposium on Information Science and Engineering，2012：179－182.

［2］Yang Xu，Xie Xiaoyao.Modeling and analysis of security protocols using colored Petri nets ［J］.Journal of Computers，2011，6 （1）：19－27.

［3］Zhao Jianjie，Gu Dawu，Zhang Lei.Security analysis and enhancement for three－party password－based authenticated key exchange protocol［J］.Security and Communication Networks，2012，5 （3）：273－278.

［4］Kenneth G Paterson，Gaven J Watson.Authenticated－encryption with padding：A formal security treatment［G］.Lecture Notes in Computer Science 6805：Cryptography and Security：From Theory to Applications2012：83－107.

［5］SU Guiping，SUN Sha.Formal analysis of non－repudiation protocol based on colored Petri net model［J］.China Information Security，2011，9 （8）：54－55 （in Chinese）. ［苏桂平，孙沙.基于CPN 模型的不可否认协议分析 ［J］.信息安全与通信保密，2011，9 （8）：54－55.］

［6］Alessandro Armando，Giancarlo Pellegrino，Roberto Carbone，et al.From model－checking to automated testing of security protocols：Bridging the gap ［G］.Lecture Notes in Computer Science 7305：Tests and Proofs，2012：3－18.

［7］Huang Hejiao，Zhou Qiang.Petri－net－based modeling and resolving of black hole attack in WMN ［C］／／Proceedings of the International Computer Software and Applications Conference，2012：409－414.

［8］Aurn Kumar Singh，Arun K Misra.Analysis of cryptographically replay attacks and its mitigation mechanism ［J］.Advances in Intelligent and Soft Computing，2012，132：787－794.

［9］ZHANG Weihua，FAN Zhihua.Method of plan recognition and multi－step attack detecting based on CPN ［J］.Computer Engineering and Design，2007，28 （11）：2516－2520 （in Chinese）.［张卫华，范植华.基于CPN 的规划识别及多步骤攻击检测方法 ［J］.计算机工程与设计，2007，28 （11）：2516－2520.］

［10］Fan Kai，Wang Yue，Li Hui.Fairness electronic payment protocol［J］.International Journal of Grid and Utility Computing，2012，3 （1）：53－58.

［11］Yu Yuedua，Yu Huininga，Liang Qia.Reachability analysis of logic Petri nets using incidence matrix ［J］.Enterprise Information Systems，2013：1－18.