浅析电子商务支付协议认证性的SVO逻辑验证

刘丽峰

(山西金融职业学院,030008)

浅析电子商务支付协议认证性的SVO逻辑验证

刘丽峰

(山西金融职业学院,030008)

当前，高效、安全的支付方式已成为移动电子商务发展的首要问题。但目前移动电子商务研究中对移动支付协议的设计尚不健全，如何对移动支付协议认证备受关注。本文浅析电死商务协议认证中SVO逻辑验证的应用。

电子商务；支付协议认证；SVO逻辑

网络及信息技术的快速发展，致使电子商务愈发热门，且增长趋势明显。作为其中最关键的电子支付环节，其支付协议的安全和高效直接影响着电子商务的健康、持续发展。本研究从形式化理论和工具验证结合的方式，对BNA逻辑在验证Netbill协议推理认证中进行了分析和阐释。

1 验证SVO逻辑形式化的方法

在对形式化的安全协议进行分析时，安全协议验证属于重要的逻辑方法。而BNA逻辑则是逻辑方法的鼻祖。一些类似BNA逻辑的分析方法在这之后也陆续的出现。在1994年，Paul C.van Oorschot与Paul Syverson在BAN逻辑的基础上，对 AT逻辑和VO逻辑以及GNY逻辑等进行总结时，提出了SOV逻辑。

SVO逻辑的扩展公理以及语法。SVO逻辑定义的公式语言跟消息语言是在原子项集合的基础上进行的。若用K跟X分别用密匙跟消息进行表达，协议的主体用a跟b来表示，那么N元函数f（X1，X2,…，Xn）在消息语言中表示消息。如果密匙在加密后得到消息，那么用{X}k表示。私匙k在对x进行签名后得到的消息，用[X]k表示。不能识别但是还能让主体接收到消息，用*表示。公式SharedKey（K，A，B）在语言公式中表示A跟B的良好共享秘钥的主体是K。公式：A says X、A said X、A sees X、resh（X）跟A received表达的意思是，消息x跟主体a之间的一些关系。A says X表示的是如果a这次开始会话后发送了x。而A said X表示的是以前发送的。公式A controls ψ与A believes ψ分别表示A作为主体时，相信并控制公式ψ。另外，├ψ表示ψ这个公式属于一个定理。

SOV逻辑的规则有两条，但是公理达到20条。主要包括必要性规则Nec、源关联公理Ax3、相信公里Ax1、接收公理Ax7-9、说过公理Ax14-15、看见公理Ax10、仲裁公理Ax16、Nonce验证公理x19和新鲜性公理Ax17等。在SVO逻辑下，协议的分析方法中SVO逻辑对安全协议做出多种认证目标，具体目标如下：（1）G1 存活确认：A believes B says X ；（2）G2身份认证：A believes B says (X,Na)；（3）G3 建立安全密钥：A believes SharedKey （K-，A,B）；（4）G4 密钥的确认：A believes SharedKey （K+，A,B）；（5）G5 密钥的新鲜性：A believes fresh (K)；（6）G6 彼此确认密钥： A believes B says SharedKey （K-，B，A）。分析Netbill协议涉及到只由单方的主体掌握对称密匙。为了方便协议的证明，还根据a*3导出a*3.1。K－表示的是密匙K还没有得到确认。

2 描述形式化的Netbill协议

Netbill协议的步骤。在1996年，Carnegie Mellon大学的J.D.Tygar教授提出了Netbill 协议。这个电子商务微支付协议是针对数字商品提出的。这个协议涉及到了三个方面：Netbill服务器跟商户以及顾客。该协议在三个方面上都有涉及：（1）在协商价格的阶段。当客户要向要向商户了解一些某数字产品的价格时，商户要把报价告诉给客户；（2）进行递送商品的阶段。当商家被告知客户接受了商品的报价，商户在发送该数字产品给客户时，要用对称密匙K进行加密；（3）在支付款项阶段。客户要给商户发送一份电子支付订单的数字签名，对该商品的订单，商户要跟密匙K进行签名加密，并且要把这两个发给Netbill服务器。Netbill服务器要验证收到的签字消息，要有效的进行支付跟检验顾客账号的支付信息，然后要给商户返还里面包含K的签名收据，进一步的结果需要商户再返还给客户。之后客户要在Msg4中把加密的商品进行解密。

3 SVO形式化验证Netbill协议简化模型及未来的发展

通过对目标的验证，来分析SVO逻辑协议的简化模型。在Netbill协议中存在的子协议，主体的身份认证由Kerberos协议进行负责。因此，密匙建立协议跟Netbill 协议是同一样的。商户M独立的生成，是K的m次方对商品进行加密。不需要对K的m平方进行相互的确认，其他的主体也只是被动的接受。例如：C believes M said Goods。根据公式的分析，可以知道认证目标能够被Netbill协议满足。就是密匙K的m次方能够安全的建立在M于C之间。能得到C的确定，并且是新鲜的密匙。虽然G没有满足协议，主要是因为对产品Goods的新鲜性没有推到出来。形式化的分析了逻辑推理过程跟协议简化的方法。对认证其他电子商务支付协议起到了一定程度的借鉴作用。Netbill协议的认证性得到了满足，但是商家时序的责任问题还是存在协议中的。由于在SOV推理时对时序的缺乏重视，没有办法在这个角度进行协议的分析。所以，要考虑时态算子要加入到SVO逻辑中，语言能力有所增加后，对认证电子商务支付协议有更多的目标。

4 总结

电子商务的发展已势不可挡，如何确保其健康、持续、快速的发展，电子商务支付的安全高效的重要性不言而喻。通过本文对SVO的逻辑推理方法的扩展来看，其Netbill微支付协议的认证性是安全、可靠且高效的。值得同行借鉴参考，相信随着互联网网络信息技术的快速发展，定能使之更加完善，已安全高速的现代化形象为电子商务的发展奠定坚实基础。

[1] 肖茵茵,苏开乐.电子商务支付协议认证性的SVO逻辑验证[J].计算机工程与应用,2014,(08):6-10.

[2] 肖仕成,李开,甘早斌.基于四方的安全电子商务支付协议分析与验证[J].计算机科学,2012,39(3):75-78.

[3] 陈莉,袁开银.满足多种安全属性的复合型支付协议及其逻辑分析[J].计算机应用研究,2012,(7):2672-2677.

[4] 马生.有穷机和逻辑结合的电子商务协议分析方法[J].小型微型计算机系统,2013,34(3):492-497.

[5] 黄珍.浅析电子商务中移动支付[J].科技与创新,2015,(9):36-37.

刘丽峰，女，（1970—），山西金融职业学院副教授，山西大学硕士学历。研究方向:电子商务。

SVO logic verification of authentication of electronic commerce payment protocol

Liu Lifeng
(Shanxi Professional College of Finance,030008)

At present,efficient and secure payment has become the primary problem of the development of mobile electronic commerce.But at present,the design of mobile payment protocol is not perfect,how to pay attention to the mobile payment protocol authentication. Application of SVO logic verification in the authentication of electronic commerce protocol.

electronic commerce;payment protocol authentication;SVO logic