基于UPPAAL在线支付系统的安全性验证

摘要：随着电子商务的不断发展，消费者对于在线支付系统的服务质量要求越来越高，支付系统不仅要高速完成每笔交易，更要保证支付过程的安全性。在线支付是电子商务的核心功能模块，而这个核心模块又由各个地理位置上分离的各个子模块组成，在该文中会对四个主要子模块进行建模，分析各模块之间的依赖关系及超时的扩散效应，通过UPPAAL对建模后的系统进行模型检测。经实验验证，所设计的支付系统模型可以在产生某个模块的超时后依然能满足安全性。

关键词：电子商务；支付系统；UPPAAL；模型检测

中图分类号：TP393 文献标识码：A 文章编号：1009-3044（2014）34-8341-02

在线支付是电子商务[1]的一个核心模块，是比传统的先下支付更快捷，更方便的一种交易方式。在线支付的出现极大的降低了交易的额外成本，加快了交易速度，使得市场经济下的自由贸易更为兴盛。在线支付改变了人们传统的支付方式，使得消费者可以在有网络的任意地方进行购物消费或者办理转账业务。

目前，安全的在线支付方式是通过通信方式和密码技术实现的，主要有以下3种：1） 帐号直接传输方式；2） SET方式；3） 专用协议方式。

1 时间自动机的基本概念

时间自动机可以表示成一个多元组 [Λi=（Li，l0i，Ti，Ci，Ii，Ei）] ，其中i表示不同的自动机，不同的自动机对应于不同的模版。其中[Li]是自动机的有限状态集合；[l0i]是自动机的初始状态；[Ti]是自动机所有动作（action）的集合；[Ci]是一个有限时钟集合，[Ii]是一种映射关系，指明每个状态上有加的时间约束，所以表示为[Ii=Ii（x）]；[Ei?Li × Ti × B（Ci） × 2Ci × Li]是所有迁移的集合，如迁移[（l，g，a，x，l'）]

表示从状态[l]出发的迁移在有约束条件g的作用下，执行一个动作a， 最后转换成状态[l'] ，其中x为所在自动机的始终变量。

2 在线支付系统在UPPAAL[3]中的建模

在线支付系统的模型含有三个4个模版类（Template）：消费者模型（Consumer），商家模型（Merchant），

支付网关模型（Payment Gateway），银行模型（Bank）。

1） Consumer 模版类（如图1所示），主要有7个状态：Start，Wait1，ToPay，Wait2，Reset，Success

其中初始状态是Start 状态，因此在这个状态时，没有任何变量。Consumer模版类发送一个BUY信号给商家的模版类Merchant，之后Consumer会进入等待状态Wait。

当Consumer收到enough信号后，会进入ToPay状态，当消费者付款之后，将进入另一个等待状态Wait2，等待商家回复一个确认信号complete，之后进入Success状态；

2） Merchant 模版类（如图2所示），主要有7个状态：Start，Check，Wait1，Wait2，Wait3，Reset，Success

Merchant 模版类初始状态为Start，收到Consumer发送的BUY信号，Merchant会进入短暂的Check状态后，发送request信号给支付网关（Payment Gateway），Merchant 发送charge信号给Payment Gateway请求对消费者账户进行扣款，当Payment Gateway返回received信号后表示已经扣款成功，最后Merchant复位到Start状态。

3） PaymentGateway模版（如图3所示）主要有8个状态： Start，ToCheck，Wait1，Checking，Wait2，Wait3，Reset，Success

PaymentGateway模版类的结构和Merchant 模版类类似，PaymentGateway相当与整个支付系统的Controller，其负责接收来自商家的消费者账户验证请求，以及接收扣款请求。但是真正负责验证消费者账户和执行扣款的操作是由Bank模版类处理，PaymentGateway起到的是转发请求和第三方认证的作用。

4） Bank模版类（如图4所示），主要有7个状态：Start，Checking，YES，NO，Wait，Reset，Success

Bank是真正负责执行账户验证和支付操作的模版类，Checking状态是银行进行验证账户时的状态，Bank会把验证的结果（no信号或yes信号）返回给支付网关PaymentGateway，之后Bank会进入NO 或YES状态，如能收到transaction则会进入等待状态Wait，当Bank完成扣款后，则回复deal消息给PaymentGateway，且自身进入Success状态，并最后回到初始状态。

3 各模版的时间自动机定义

1） 消费者自动机模型定义

2） 商家自动机模型定义

3） 支付网关模型定义

4） 银行模型定义

4 对于在线支付系统中的超时问题的分析与解决

为了保证在线支付系统操作的原子性，当底层模块Bank 产生了超时，就必须把其上层的所有模块重置到初始状态。在图4中，Bank模块的超时发生在两处状态：YES 和Wait，超时时间分别设定为5T 和6T。超时时Bank都会进入Reset状态，且之后会发送reset_PG信号给上层模块PaymentGateway。

如果在PaymentGateway模块中的Wait2，ToTrans，Wait3 时接到Bank模块的回复信息是reset_PG，表明Bank模块已超时或者说已失效，PaymentGateway就会进入Reset状态，并且在恢复到初始状态之前会发送reset_M信号给上层模块Merchant。

与PaymentGateway模块相似，Merchant模块可能会收到reset_M信号的等待状态是Wait2， ToCharge， Wait3三个状态。同样在收到reset_M后都会进入Reset状态，恢复到初始化状态前发送reset_C给Consumer。

同样，Consumer如果在ToPay和Wait2状态时收到reset_C信号，Consumer就会恢复到初始状态Start。

5 使用UPPAAL对模型进行验证

先使用UPPAAL软件对上述四个模版类建立模型，模型建立之后要对系统的性质进行验证。为避免系统发生死锁，需要验证 A[] not deadlock 这一属性。为了验证最终支付操作能顺利完成，需要验证下列三个属性：

6 结束语

本课题通过形式化方法模型检测语言并采用UPPAAL建模工具进行在线支付系统支付过程的建模及结果验证，最终的验证结果是各个模版类最终都能达到理想状态，即时是在Bank模型出现超时的情况下。实验中如果底层模型出现超时，上层模型必须重置其状态，重置的过程是自底向上依次重置。设计中并为考虑多个模型出现超时的情况，但处理方法也可类似设计。 本文的侧重点是要满足系统的安全性，关于快速性，即超时问题将在后续的研究中得到改进。

参考文献：

[1] 肖修林，吴朝晖.可信用电子商务系统体系架构研究[J].计算机集成制造系统，CIMS.2003.

[2] Lu，Shiyong，Model checking the secure electronic transaction （SET） protocol[D].Univ of New York at Stony Brook， Stony Brook， United States，1999.

[3] Gerd Behrmann， Alexandre David， Kim G Larsen.A Tutorial on Uppaal[D].Aalborg University， Denmark，Updated 17th November 2004.

[4] 刘如娟，戴桂兰，胡长军，等.Web服务的模型检测技术探讨[J].小型微型计算机系统，2007（11）.

（下转第8346页）

（上接第8342页）

[5] 官尚元，伍卫国，董小社，等.自动信任协商的形式化描述与验证研究[J].通信学报，2011（2）.

[6] 郭华， 庄雷，张习勇.UPPAAL――一种适合自动验证实时系统的工具[D].西安：西安理工大学，2006.

[7] 梁少华.网上银行电子商务支付的实现[D].长春：吉林大学，2013.

[8] 付雄，程文青，郎为民，等.安全电子支付系统研究[J].计算机科学，2005（1）.

[9] 张传武，彭启琮，沈野樵，等.安全支付网关技术研究与系统实现[J].系统工程与电子技术，2002（3）.

[10] 袁姗姗.基于SET的支付网关的研究与设计[D].武汉：华中科技大学，2006.