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

肖茵茵 ，苏开乐

XIAOYinyin1，2,SU Kaile2，3

1.广东技术师范学院 计算机学院，广州 510665

2.中山大学 信息科学与技术学院 广东省信息安全重点实验室，广州 510275

3.北京大学 信息科学技术学院 教育部高可信软件技术重点实验室，北京100871

1.School of Computer Science,Guangdong Polytechnic Normal University,Guangzhou 510665,China

2.Guangdong Key Lab of Information Security Technology,School of Information Science and Technology,Sun Yat-sen University,Guangzhou 510275,China

3.Key Lab of High Confidence Software Technologies,Ministry of Education,School of Electronics Engineering and Computer Science,Peking University,Beijing 100871,China

1 引言

随着电子商务的普及和发展，SSL、SET、Netbill等电子商务支付协议的地位越来越重要。安全协议的手工分析十分困难，容易出错，特别是对复杂的电子商务支付协议来说，采用形式化的理论和工具验证其安全性十分必要[1]。在现有的电子商务协议安全性研究中，多采用有限模型检测法寻找协议的漏洞和潜在攻击的路径（证伪法）[2-4]，这类方法具有自动化工具（SMV、SPIN等），使用方便，但检测的状态空间有限，即使检测不出攻击，也无法保证协议在任意会话中的正确性。另一类方法采用定理证明和逻辑推理，可验证协议能否满足特定的安全性质以及证明协议的正确性（证真法）[5-7]，这类方法准确度高，但验证过程繁杂，验证复杂协议时难度较大，如文献[5]用实例化空间逻辑验证了SET协议的秘密性和认证性，但文中并未说明其具体推理过程；文献[8-9]展示了使用类BAN逻辑验证Netbill协议的推理过程，但文中主要关注的是协议的原子性和时限责任等问题，而未讨论其认证性。

本文使用SVO逻辑方法[10]，选取Netbill协议[11]，对其认证性进行形式化分析：首先对SVO逻辑的公理集进行扩展，然后在不影响Netbill协议安全性的前提下，为其建立简化模型，之后针对协议特点，修正和补充了其验证目标，最后给出了具体的推理过程和验证结果以及相关工作的比较。随着人们对网络知识产权保护意识的提高，用于数字产品交易的Netbill微支付协议重新受到了人们的重视，因此本文的研究是有现实意义的。更重要的是，文中展示的协议简化方法和逻辑推理过程也适用于分析其他电子商务支付协议的认证性。

2 SVO逻辑形式化验证方法

安全协议验证逻辑是安全协议形式化分析中的一类重要方法，而BAN逻辑[12]是这类方法的鼻祖。在此之后，又有一系列类BAN逻辑分析方法相继出现。1994年，Paul Syverson和Paul C.van Oorschot在总结BAN逻辑和GNY逻辑、AT逻辑及VO逻辑等类BAN逻辑的基础上提出了SVO逻辑[10]。SVO逻辑修补了其他类BAN逻辑的缺陷和不足，具有十分简洁的推理规则和公理。它的出现标志着BAN逻辑及类BAN逻辑的成熟，为逻辑系统建立了合理的理论模型。由于篇幅所限，对于SVO逻辑，这里只对本文协议验证所需的部分做简单介绍，其他详见文献[10]。

2.1 SVO逻辑语法及扩展公理

SVO逻辑在原子项集合的基础上定义了消息语言和公式语言。若以X和K分别表示消息和密钥，以A和B表示协议主体，则在消息语言中，n元函数F（X1，X2，…，Xn）是消息，如{X}K是用密钥K对X加密后得到的消息；[X]K是用私钥K对X签名后得到的消息。*表示主体所收到但不可识别的消息。在公式语言中，公式“SharedKey（K，A，B）”表示“K是主体A与B的良好共享密钥”；公式“A sees X”，“A says X”，“A said X”，“A received X”和“fresh（X）”表示主体A与消息X的各种关系，如“A says X”表示A在本次会话开始后发送了X，而“A said X”是以前发送的；公式“A believes ψ”和“A controlsψ”分别表示主体A相信和控制公式ψ。另外，┐ 、∧ 、⊃ 、⇒ 分别表示“非”、“与”、“蕴含”和“推理”；├ψ表示公式ψ是一个定理。

SVO逻辑的规则有2条，公理有20条，本文协议验证过程中用到的有必要性规则Nec（Necessitation）、相信公理Ax1、源关联公理Ax3、接收公理Ax7~Ax9、看见公理Ax10、说过公理Ax14~Ax15、仲裁公理Ax16、新鲜性公理Ax17、Nonce验证公理Ax19，具体如下（XB表示消息X来自于主体B）：

2.2 SVO逻辑下的协议分析方法

其中，K－表明密钥K还未得到确认；K+表明密钥K已经得到确认，即从B发的消息中，得知B知道K。

用SVO逻辑分析安全协议，即验证协议是否满足上述认证目标，其步骤和BAN逻辑类似。不同的是，SVO逻辑并不“理想化”协议，而是对协议进行假设。SVO假设有4类：第1类是初始假设，即那些在协议运行开始时被认为成立的公式，如主体相信自己产生的随机数的新鲜性、主体和可信第三方之间密钥的良好性、可信第三方产生的密钥的新鲜性、良好性等；第2类反映了消息的接收，这可直接由协议消息而得；第3类假设反映了主体对接收到消息的理解；第4类假设用来反映消息接收者对消息的解释。

3 Netbill协议的形式化描述

3.1 协议步骤

Netbill协议是Carnegie Mellon大学的J.D.Tygar教授于1996年提出的一个针对数字商品（例如一个软件或一首歌曲）的电子商务微支付协议[11]。该协议涉及到三方参与者：顾客、商户及Netbill服务器，客户持有的Netbill账号等价于一个虚拟电子信用卡账号。Netbill协议的主要步骤如图1所示。

该协议分为三个阶段：在价格协商阶段，顾客向商户查询某数字商品价格，商户向该顾客报价；在商品递送阶段，顾客告知商户他接受报价，商户将该数字商品用对称密钥K加密后发送给顾客；在支付阶段，顾客准备一份电子支付订单的数字签名值发送给商户，商户对该订单和密钥K签名加密，并将此二者发送给Netbill服务器。Netbill服务器解密并验证收到的签名消息，对顾客账号等支付信息的有效性进行检验和支付授权，然后将包含K的签名收据返回给商户，由商户将结果进一步转送给顾客，最后顾客将Msg4中的加密信息商品解密。

3.2 消息简化

验证复杂协议的首要步骤是在不影响协议验证目标的前提下合理简化协议。在不影响Netbill协议认证性的基础上，在形式化描述该协议时，对协议消息做了如下简化：

（1）去除了状态标识、顾客的起拍价、顾客及商户的备忘域、等可选的部分消息。

（2）SVO逻辑基于Dolev-Yao符号化模型对协议进行推理，其消息操作是作用在消息集合上的抽象函数/密码原语，因此，也不对Netbill协议使用的具体密码算法进行区分，只以加密、签名等抽象函数表示密码学运算：

TAB（Identity）：一个Kerberos许可证，用于向B证明A是用Identity命名的，并在他们之间建立一个共享的会话密钥KAB。

3.3 协议简化模型的形式化描述

根据3.2节中的分析，简化后的Netbill协议如下：

其中，C、M和N分别代表顾客、商户和Netbill服务器；PRD（Product Request Data）是商品请求数据；TID是交易ID；ProductID是商品ID；Price是商户的报价；Goods是具体商品内容；CAcct、MAcct分别是顾客和商户的账号；EPO（Electronic Purchase Order）是电子支付订单，其明文部分包括商户和Netbill服务器可读的交易信息（如商品描述、客户认证等），其加密部分包括只有Netbill服务器可读的支付指令（如顾客账号等）；EPOID是电子支付的ID，是全局唯一的标识符，将被用在NetBill数据库中唯一地确认这次交易；Receipt是Netbill服务器返回的收据，其中包含是否接受本次支付的结果Result和对商品进行加/解密的密钥KM。

4 Netbill协议简化模型的SVO形式化验证

4.1 验证目标

基于SVO逻辑的协议分析，其目的是验证协议是否满足第2章中的SVO认证目标。Netbill协议的子协议中，由Kerberos协议负责其主体的身份认证，通信主体能被Kerberos协议赋予身份票据进行会话，这说明SVO目标G1、G2已被Kerberos协议满足，验证过程可见文献[13]，因此，G1、G2也被Netbill协议满足；另外，Netbill协议属于密钥建立协议，其中对商品进行加密的密钥KM由商户M独立生成，其他主体只是被动的接受，无需对KM进行相互确认，即并没有G6这样的目标。因此，省略了G1、G2、G6目标的验证。与普通的密钥建立协议不同，Netbill协议仅涉及到单方主体掌握对称密钥KM，不适合用Sharedkey相关公式描述其性质，因此，在SVO逻辑认证目标的基础上进行了一些改动，总结出要验证的Netbill协议认证目标：

Netbill协议的最终目的是顾客C付款之后能从商户M处获得密钥KM，对之前收到的加密产品进行解密，获得商品Goods。因此，除了SVO认证目标外，还制定了以下验证目标：

4.2 协议假设

基于SVO逻辑的协议分析，其目的是验证协议是否满足进行推理前，应对Netbill协议制定SVO逻辑假设。因篇幅所限，下面只列出与推理过程相关的假设。

首先是初始假设：

4.3 推理过程

下面，用SVO逻辑的推理规则和公理对Netbill协议进行推导：

由（13）、（15）可知，顾客C在收到密钥KM之后，能收到由商户M发来的产品Goods。由于Goods不由新鲜随机数生成，所以无法继续推导出Goods的新鲜性，无法得知M是否在本次运行中说过Goods，即目标G'不成立。但由（12）可知，加密后的产品确实是在本次运行中发送的，即顾客C收到的加密产品仍是新鲜的。

4.4 验证结果

由上文的分析，可知Netbill协议能够满足认证目标G3'、G4'、G5'，即密钥 KM能够在 C 和 M 之间安全地建立，并受到C的确认，而且该密钥是新鲜的；虽然目标G'未被协议满足，但这只是因为无法推导出产品Goods的新鲜性所致，顾客C收到的加密产品仍是新鲜的，且若收到密钥KM，还是能收到由M发来的产品Goods。这一验证结果表明，Netbill协议的认证性是有保障的。

4.5 相关工作比较

与本文相关的研究工作有文献[5，8-9]，其具体的比较可见表1。从表中可知，本文的工作着重对Netbill协议的认证性进行了验证，而文献[8-9]主要关注的是该协议的原子性和时限责任等问题；文献[5]验证了另一电子商务协议——SET协议的认证性和秘密性，但文中并未说明其具体推理过程，而本文的逻辑推理过程具体完整，这是使用逻辑方法对安全协议进行验证的重要环节。另外，由于文中所使用的SVO逻辑具有清晰的语义和合理的理论模型，因此本文给出的协议假设也比上述研究工作更加完整合理。

表1 与本文相关的研究工作比较

5 结束语

使用扩展的SVO逻辑推理方法，对Netbill微支付协议的认证性进行形式化分析。针对协议特点，对SVO逻辑的公理集进行扩展，修正和补充了协议的验证目标，建立了不影响既有安全性的协议简化模型，给出了合理的协议假设和具体完整的逻辑推理过程，验证结果表明Netbill协议的认证性是有保障的。最后对相关研究工作进行了比较。这一协议简化方法和逻辑推理过程对其他电子商务支付协议认证性的形式化分析起到了一定的借鉴作用。

本文未来研究工作的方向如下：虽然Netbill协议满足认证性，但该协议还存在商家时限责任[9]等问题，由于SVO逻辑缺乏对时序的推理，无法从这一角度分析协议。因此，可考虑对SVO逻辑加入时态算子，增强其语言能力后再对更多电子商务支付协议进行更多目标的验证。

[1]薛锐，冯登国.安全协议的形式化分析技术与方法[J].计算机学报，2006，29（1）：1-20.

[2]缪力，谭志华，张大方.基于SPIN的网络认证协议高效模型检测[J].计算机工程与应用，2012，48（21）：62-67.

[3]Lu S M，Zhang J L，Luo L M.The automatic verification and improvement of SET protocol model with SMV[C]//Proceedings of the International Symposium on Information Engineering and Electronic Commerce（IEEC’09），Ternopil，2009：433-436.

[4]Panti M，Spalazzi L，Tacconi S，et al.Automatic verification of security in payment protocols for electronic commerce[C]//Proceedings of the 4th International Conference on Enterprise Information Systems，2002：968-974.

[5]肖茵茵，苏开乐，马震远，等.实例化空间逻辑下的SET支付协议验证及改进[J].华中科技大学学报，2013，41（7）：97-102.

[6]肖茵茵，苏开乐，岳伟亚，等.SET证书申请协议在SPV下的自动化验证及改进[J].计算机学报，2008，31（6）：1035-1045.

[7]Giampaolo B，Fabio M，Paulson L C.An overview of the verification of SET[J].International Journal of Information Security，2005，4（1/2）：17-28.

[8]冯涛，余冬梅，边培泉.Netbill协议的形式化描述及分析[J].兰州理工大学学报，2004，30（3）：102-105.

[9]彭勋，董荣胜，郭云川，等.在Netbill交易协议中引入对商家的时限责任的追究[J].计算机科学，2004，31（10）：79-83.

[10]Syverson P F，Vanoorscho P C.An unified cryptographic protocol logic[R].Washington：Naval Research Lab，1996.

[11]Cox B，Tygar J D.Netbill security and transaction protocol[C]//Proceedings of the 1st USENIX Workshop on Electronic Commerce，1995：77-88.

[12]Burrows M，Abadi M，Needham R.A logic of authentication[J].ACM Transactions on Computer Systems，1990，8（1）：18-36.

[13]党继胜.基于SVO逻辑的电子商务协议形式化分析与研究[D].贵阳：贵州大学，2007.