简易付款验证

　　简易付款验证是指在电子商务消费过程中由消费者(customer )、商家(mer2chant)和银行(bank)及所信任的第三方认证机构(CA)之间的信息流、资金流的交易验证。在电子商务模型中，各个主体(消费者、商家、银行等) 进行交互必须遵循一定的规则，以保证各方的利益和安全，并且能控制交易风险，这就是协议的模式。安全的电子商务协议是保证电子商务活动正常开展的前提。我们可以用形式化的方法来描述与验证网络协议，从而发现协议中潜在的错误。

　　简介

　　电子商务由消费者( customer )、商家( mer2chant)和银行( bank)及所信任的第三方认证机构(CA)之间的信息流、资金流和物流的交互关系，各方通过遍及全球的、开放的但不安全的Internet相互联系。在电子商务模型中，各个主体(消费者、商家、银行等) 进行交互必须遵循一定的规则，以保证各方的利益和安全，并且能控制交易风险，这就是协议的模式。安全的电子商务协议是保证电子商务活动正常开展的前提。我们可以用形式化的方法来描述与验证网络协议，从而发现协议中潜在的错误。已经开发出多种基于时间自动机的网络协议验证工具，UPPAAL就是很好的工具之一。

　　简单网络支付协议(SNPP)是由MIT计算机科学实验室的Semyon Dukach提出的。该协议使用UDP 数据报传输，DES 对称加密技术，HOLD技术和相互独立机制为不信任的双方实现安全支付交易。对SNPP 协议进行过分析和检验，但是他们仅仅给出了简化的SNPP 协议模型，并且在给出的银行模型上还存在一些不足之处1。

　　简单网络支付协议

　　消费者首先选择信任的银行开户存入现金，得到相应的银行账号和采用对称加密产生的密钥。银行记录每个账户的现金类别和数量、现金预留表，密钥，最近交易号码和所有的历史交易号码列表的信息，通过账号来索引。HOLD信息包含账户，账号/银行身份匹配认证以及超时约束。当消费者发送HOLD信息给商家时，协议开始运行，然后商家把信息转送到自己的银行，若商家和消费者不属于同一个银行，则把HOLD信息转送到消费者银行。

　　若消费者账户的资金足够，银行先将预留信息添加到消费者账户的现金预留列表，再返回一个确认信息给商家银行，否则整个HOLD将被拒绝。商家在收到自己的银行的通知后，将商品发送给消费者。

　　同时，消费者收到商品后发送PAY信息确认付款，商家把该信息转送到商家银行，商家银行再把该信息转送到消费者银行，消费者银行通过外部程序把资金送到商家银行，商家银行将要求的资金数量转入商家账号，交易完成2。

　　协议形式化建模及验证

　　1.建立模型

　　对协议中的4个进程超时约束别分设为单位时间15，20，20，20。若消费者在收到商家的发货信息15个单位时间之后，仍未发送付款消息则发送超时消息；若商家在发送确认发货消息之后20个单位时间内未收到消费者的付款信息则发送超时信息；若商家银行在发送确认消息给商家20个单位时间之后没有收到付款消息则发送超时信息；若消费者银行在发送已预留资金20个单位时间之后未收到付款消息则认为是超时，发送超时消息。超时计时器在接收到以上进程的超时信息后，立即发送消息给外部仲裁程序。

　　建立模型时，假设消费者与商家的银行是不同银行。此外，在不影响协议关键性质检测的前提下，假设银行支付过程为理想过程，即不存在网络通信及其它设备故障的情况。

　　定义5个进程模块:消费者进程，商家进程，消费者银行进程，商家银行进程，超时计时器进程。其中消费者进程只与商家进程进行通讯，商家进程只与商家银行进程进行通讯，商家银行只与消费者银行进行通讯，超时计时器只负责接收来自以上进程的超时信息。

　　2.模型验证

　　应用UPPAAL工具，先对协议原模型进行验证，即验证由消费者、商家、银行进程构成的协议模型，再验证本文建立的模型。结果表明，原模型满足货币原子性，但是会存在消费者收到了商品而未付款的情况。而由协议的符号描述可知，若消费者收到了商品或服务，却对此不满意，则不会进行下一步骤。新模型验证结果满足该性质，表示消费者和商家等待信任第三方的仲裁，而银行将预留资金冻结等待信任第三方的通知。这说明通过仲裁状态可达性，使得协议的新模型满足了商品原子性。

　　总结

　　从货币原子性和商品原子性这两个角度对简单网络支付协议进行了分析，通过UPPAAL 检测发现该协议原模型满足货币原子性，但在商品原子性上存在缺陷，可能产生消费者收到了商品而未付款的情况。所以在原模型的基础上，我们增加了对不同银行间交易行为和交易中超时行为的分析，设计了超时计时器模块，提出了用仲裁状态可达性来通知外部仲裁程序解决交易纠纷，从而使新模型满足了商品原子性3。

　　本词条内容贡献者为:

　　王海侠 - 副教授 - 南京理工大学