轻量级移动支付协议公平性分析

李 茜，王 峥，马建芬，李 娜

1.太原理工大学 计算机科学与技术学院，太原 030024

2.国网山西省电力公司，太原 030024

1 引言

移动支付（Mobile Payment）作为移动电子商务的重要应用之一[1]，是依托其移动终端（一般为手机），通过无线网络购买货物或服务的一种新型支付方式[2]。移动互联网络的发展和无线设备的普及，使移动支付给人们的生活带来极大便利。与此同时，其安全问题和支付效率问题也逐渐成为人们关注的热点[3]。为保证移动支付安全、顺利进行，在通信以及传输数据时，必须采用安全高效的移动支付协议。因此，对现有轻量级移动支付协议的形式化分析和研究已经成为信息安全领域中的一个重要课题[4]。

2004年，Kungpisdan等人提出一个适用于无线网络的安全的基于帐户的移动支付协议[5]，协议采用了对称加密算法，无需对主体公钥加解密计算，减轻移动终端的计算负荷，提高协议执行效率。Tan等人基于文献[5]进一步提出安全的轻量级对称密钥移动支付协议[6]，他们认为公钥体制计算量大，不适用于移动终端的支付活动。针对全连接场景未考虑到客户和商家不能直接通信的情况，承接Kungpisdan等与Tan等人的设计思想，Isaac和Zeadally于2012年提出PCMS（secure Payment Centric Model using Symmetric cryptography protocol）[7]协议，该协议以支付网关为中心，采用轻量级对称加密技术，适用于计算能力差，存储资源有限的移动设备和无线信道带宽低，不可靠的移动环境。同时，用临时身份代替客户的真实身份，保护客户隐私，并在2014年继续对PCMS协议进行了设计实现和性能分析[8]。结果表明，PCMS协议需要更少的计算量和存储空间，可以部署在计算资源有限的移动设备上，使支付交易在无线网络上有效地执行。2017年，吴格格等人用UPPAAL模型检测工具对PCMS协议形式化分析，证明其满足无死锁、钱原子性、有效性和时效性[9]。

本文在前人研究基础上，进一步分析该协议的隐私性、机密性、认证性和完整性等，并基于串空间理论和认证测试方法，研究分析PCMS协议的公平性，针对协议不满足的安全属性做出改进，用模型检测工具SPIN（Simple Promela Interpreter）[10]对改进后的协议进行验证分析。

2 PCMS协议

PCMS协议分为商家注册子协议和支付子协议两部分。商家注册子协议在客户和商家之间进行，主要用于交换主密钥，并通过主密钥生成一套新的会话密钥。本文主要对支付子协议进行形式化分析研究，其执行顺序如图1所示。

图1 PCMS支付子协议执行顺序图

协议描述符号说明如表1所示。

协议描述如下：

（1）C→PG→M：NIDC,i,TIDReq。

（2）M→PG→C：{TID,IDM}KSC-Mi。

客户将自己的昵称、指数i（用来生成客户和商家之间的会话密钥）和TID请求通过支付网关发送给商家，商家将自己的身份标识和交易特性用i生成的会话密钥加密，通过支付网关发送给客户，客户和商家通过支付网关交换必要的信息。

表1 协议描述符号说明表

（3）C→PG→M：PRequest；PRequest={OI,Price,NIDC,IDI,TSTC,z,h(KSC-Iz),VSRequest}KSC-Mi,MAC[(OI,Price,NIDC,IDI,TSTC,z,h(KSC-Iz),KSC-Mi+1]；VSRequest=(MAC[(Price,h(OI),TSTC,TC,IDM),KSC-Iz],TC,TSTC。

客户通过支付网关向商家发送支付请求，其中包含有扣款请求（可选择使用借记卡或信用卡支付）和C生成的时间戳，用客户和商家的共享密钥加密。商家收到支付请求后，通过时间戳验证支付请求的有效性。若有效，则将解密得到的扣款请求和M生成的时间戳发送给支付网关；若无效，则通知支付网关取消交易。

（5.1）PG→I：NIDC,IDM,VSRequest,TID,h(OI),z,Price,h(KSC-Iz)；

（5.2）PG→A：Price,IDM；

（5.3）I,A→PG：VSResponse,Stt,h(Stt,h(OI),,h(KSC-Iz))；VSResponse={Stt,h(OI),KSM-PGk+1}KSC-Iz。

支付网关解密得到转账请求后，通过M的时间戳验证转账请求的有效性。若有效，则向I、A发送信息，完成转账操作；若无效，则通知客户和商家取消交易。I在验证了扣款请求和客户账户的有效性后，将款项从客户账户转移到商家账户，并将包含交易状态的扣款响应发送给支付网关。这部分交易均在银行专有网络内进行，安全性暂不做考虑。

（6）PG →M：VCResponse；VCResponse={Stt,h(Stt,

支付网关将转账响应和支付响应分别发送给商家和客户。至此，商家账户已经收到款项，客户确定商家将发送货物或提供服务。

3 协议的形式化分析

3.1 相关知识

3.1.1 串空间

设两个互不相交的原子项集合：A为原子消息集合，其中的元素用a表示；K为密钥集合，其中的元素用k表示。设T为协议运行中，协议各主体之间相互交换传递的消息集合，其中的元素用t表示，及消息项。

定义1（串空间）带符号的二元组＜σ,t＞表示一个事件。其中，σ∈{+,-}，“+”表示协议主体发送一条消息，“-”表示协议主体接收到一条消息；t∈T，表示协议中所有的消息项。±T表示串空间中所有事件的集合；是所有带符号项的有限序列集合，其元素为 (＜σ1,a1＞,＜σ2,a2＞,…,＜σn,an＞)，n表示序列长度，term(n)=σt。一个串表示一个主体对消息的所有发送和接收行为。串到带符号项的有限序列集合的一个映射tr称为串的迹映射，通常把串的迹称为串。二元组＜Σ,tr＞表示一个串空间。其中，Σ表示串的集合[11]。

3.1.2 认证测试

认证测试方法以串空间理论为基础，是一种基于挑战-应答机制，用于证明安全协议认证属性的方法，串空间模型中的所有定义和性质都适用于认证测试[12]。

定义2（主动测试）如果t为a在n中的测试组件，且K∉P，那么，接收节点（负节点）n是项t={h}k关于值a的主动测试。

定理1设C=＜NC,EC＞是T上的丛，n∈NC，n是项t={h}k关于值a的主动测试，可得：必然存在一个常规正节点包含t为组件[13]。

定理2设C=＜NC,EC＞是T上的丛，n∈NC，且n不是串空间的源节点，如果节点n的符号为正，且t⊂term(n)，那么必然存在一个包含t的发送边[14]。

2000年，主动测试概念由Guttman等人首次提出，定理1是认证测试的一个推理，定理2是串空间理论的一个扩展，详细证明见文献[13]和[14]。

3.2 串空间建模

串空间是形式化分析方法中定理证明的一种[19]。综合定理证明技术和协议迹分析技术的优势，可以用消息串的代数表示法描述协议的执行，也可以用串空间图的形式刻画协议的执行过程。串空间中每一个丛就是协议的一个并发运行，协议的安全性通过丛保持的性质来证明，模型简洁易懂。

PCMS协议执行过程中，客户完全信任于发卡银行，相信其不会把自己的隐私透露给商家或支付网关，客户的昵称由发卡银行分配。给出PCMS协议的串空间模型[15]，如图2所示。

图2 PCMS支付子协议串空间模型图

其中，客户的目标在于，确定交易成功，款项以正确数额转给正确的商家账户，商家承诺向其发送货物或提供服务。客户目标通过支付网关发送给客户的支付响应来实现，支付响应中包含的Stt表明交易的成功与否。同时，客户可以将自己的OI做哈希运算，与解密得到的h(OI)比对，验证交易信息的正确性。商家的目标在于，收到准确数额的款项，确定交易成功。商家目标通过支付网关发送给商家的转账响应来实现。支付网关的目的是在客户和商家之间传递消息，通知客户和商家交易成功。因此，只要保证客户和商家的目标可以实现，支付网关的目标即实现。

由此可见，保证协议公平性的关键在于，C收到支付响应，当且仅当P收到支付请求；M收到转账响应，当且仅当P收到转账请求。协议（1）、（2）步，只是客户和商家通过支付网关交换必要的信息，不涉及各主体的切身利益。给出PCMS协议部分串空间模型图[16]，如图3所示。

定义3设Init[PRequest,PResponse]是客户串的集合，其轨迹(trace)＜+PRequest,-PResponse＞。

定义4设Resp[PRequest,VCRequest,IDM,z,KSC-Iz,k,VCResponse]是商家串的集合，其轨迹为＜-PResponse,

图3 PCMS协议部分串空间模型图

定义5设Gateway[PRequest,VCRequest,k,VCResponse]是支付网关串的集合，其轨迹为-PResponse＞。

3.3 安全目标分析

客户用昵称NIDC代替其真实IDC，无论是商家还是支付网关都无法通过客户的昵称查找到其真实ID，可以有效保护客户账户、密码等隐私信息。同时，该协议采用对称密钥加密，根据完美密钥假设，其不会被泄漏，是安全可靠的，用主密钥生成新的会话密钥，可有效防止密钥猜测攻击，同时对称加密保证了主体之间的认证性。PCMS协议通过采用MAC技术，保证了所传递信息的源发性和完整性，使发送方的消息不可抵赖、不能伪造。

分析表明，PCMS协议满足隐私性、机密性、认证性和完整性。

PCMS协议的公平性通过M与P之间的公平性和C与P之间的公平性分别证明。

执行过程中M与P之间是公平的，如果M收到转账响应，当且仅当P收到转账请求。首先，证明如果M收到转账响应，那么P一定能够收到转账请求。用串空间理论形式化描述如下：

命题1假设C为PCMS协议串空间Σ中的一个丛，如果 S,SPϵΣ,SϵResp[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse],C-height(S)=3，则C中必然存在正常串：Sp∈Gateway[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(SP)≥3。

证明由假设可知SϵResp[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，则S在C上的迹为由于uns_term＜S,3＞=VCResponse，节点＜S,3＞是符号为负的常规节点，构成项VCResponse的主动测试。由主动测试定理可得，丛C中必定存在一个常规节点n1，使得该项属于uns_term(n1)，而该项是P传递的转账响应，故节点n1只能在串SP上。

对串SP的迹分析可知，n1=＜SP,4＞，所以＜S,3＞唯一起源于＜SP,4＞，C-height(SP)=4，满足命题中C-height(SP)≥3的条件。得出结论：当M收到转账响应时，P一定能够收到转账请求。这对于M和P来说都是公平的。

接着，证明如果P能收到转账请求，那么M一定能够收到转账响应。用串空间理论形式化描述如下：

命题2假设C为PCMS协议串空间Σ中的一个丛，如果 S,SMϵΣ,SϵGateway[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，则C 中必然存在正常串：SM∈Resp[PRequest,VCRequest,IDM,z,KSC-Iz,k,VCResponse]，且C-height(SM)≥3。

证明由假设可知SϵGateway[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，则S在C上的迹为：由于，节点＜S,3＞是符号为负的常规节点，构成项{VCRequest||IDM||z||h(KSC-Iz)}KSM-PGk||k||MAC[(VCRequest||IDM||z||h(KSC-Iz)||KSM-PGk+1]，的主动测试。由主动测试定理可得，丛C中必定存在一个常规节点n2，使得该项属于term(n2)。而该项是M传递的转账请求，故节点n2只能在串SM上。

对串SM的迹分析可知，n2=＜SM,2＞，所以＜S,3＞唯一起源于＜SM,2＞，即C-height(SM)=2，不满足命题中 C-height(SM)≥3的条件。在串 S中，当C-height(S)=3时，S已经收到了M发送的转账请求，但若此时协议中断，就不能保证VCResponse的产生，也无法确定M是否收到过P向其发送的转账响应。得出结论：当P收到转账请求时，M不一定能够收到转账响应。这对于M来说是不公平的。此时，M已经得到付款，但由于未收到转账响应，不会向C发送货物或提供服务，间接影响到了C的利益。

同理，定义PCMS协议执行过程中C与P之间是公平的，如果C收到支付响应，当且仅当P收到支付请求。用串空间理论建模和认证测试方法形式化证明，得到结论：如果C收到支付响应，那么P一定能够收到支付请求；但如果P收到支付请求，C不一定能够收到支付响应。这对于C来说是不公平的。但是，此时由于M已经收到货款和转账响应，并且向C发送货物或提供服务，只是C未收到支付响应，没有一方的切身利益受到损害。

综上所述，PCMS协议不满足公平性。由于对C的不公平并不会使任何主体利益受损，因此，只针对M和P之间的不公平情况做出改进。

4 协议改进及验证

4.1 协议改进

由上述可知，在协议执行到第（6）步，当P为不诚实主体或因网络导致通信中断时，P收到了M的转账请求，但M未收到相应的转账响应，M和P之间不满足安全协议的公平性，使C的利益间接受损。针对以上情况，本文通过增加一个P的时间戳来保证M对转账响应的接收情况，在消息无效的情况下，通过退款子协议来完成后续步骤，保证C的利益。

对原协议第（6）步修改如下：

（6）PG→M：VCResponse;VCResponse={Stt,TSTP,

增加退款子协议如下：

（2）PG→A：NIDC,IDM,Price,TC,TID；

（3）PG→I：Price,NIDC；

（4）I,A→PG：Yes/No；

协议执行的第（6）步，若M 在P时间戳规定的时间内未收到转账响应，则执行退款子协议，向P发送消息终止交易。P与I和A沟通，再次将款项转移，并通知M交易取消成功。

4.2 SPIN模型检测工具验证

SPIN模型检测工具支持设计和验证系统，可作为一个模拟器，快速对建立的系统模型进行随意、引导性的或交互的仿真。使用Promela语言编程建模直观、明白地描述系统设计，用线性时序逻辑LTL有力、简明地描述系统需求，并通过有效算法验证系统是否满足需求[15]。

对改进后的协议，用Promela语言描述系统进行模拟分析，保证模型建立的正确性，通过simulate模拟协议中各主体的交易行为，如图4所示。图4中，从左至右分别代表客户、商家、支付网关和银行的交互过程，所示图可成功模拟协议的执行顺序，与设计一致。

图4 主体交易行为模拟图

协议属性验证输出结果如图5所示，此时SPIN产生一个分析器，其被编译和执行，并将结果显示在Verifiction Output窗口中。图的第一部分表示：所用模型检测工具的版本为Spin Version 6.4.6-2016.12.2，默认使用偏序简约运算法则。第二部分表示：SPIN平台按照实验设计运行，默认在全部状态空间搜索，整个检测过程以正常状态结束，无死锁。由图5第三部分第8行可知，描述该全局系统状态使用68字节的内存空间，检测运行过程中最长深度优先搜索路径包含63个状态转移，查找过程中未检测到错误，若有错误检测会自动停止并报错。有110个不同的全局系统状态存储在状态空间中，每个状态需要68个字节进行有效描述，遇到34曾遍历过的状态，总工作量为144个状态搜索遍历，用默认Hash算法函数存储状态时，无冲突产生。第四部分显示数据使用的内存空间所占字节量。

图5 验证输出结果图

结果分析表明，通过对协议的改进可实现协议的公平性[16]。

5 结束语

本文形式化分析了轻量级移动支付协议PCMS的安全性，并基于串空间理论的认证测试方法，对其公平性进行形式化分析。原协议不满足公平性存在漏洞，改进方案增加支付网关的时间戳来保证商家对转账响应信息的接收，增加退款子协议完成后续退款流程。改进方案使商家除了收到准确数额的款项，确定交易成功以外，还对客户的利益负有责任。用模型检测工具SPIN分析验证，结果表明，改进后的协议设计合理，满足公平性。下一步工作，将继续对轻量级移动支付协议安全属性进行深入研究分析，在保证安全属性的前提下，简化子协议。