一种新的复合型电子支付协议及其形式化分析
2018-07-05汪学明贵州大学计算机科学与技术学院贵州贵阳550025
丁 月 汪学明(贵州大学计算机科学与技术学院 贵州 贵阳 550025)
0 引 言
随着计算机技术和互联网络技术飞跃发展，电子商务[1]活动日益活跃，如何保障电子商务的安全是当前亟需解决和处理的一大难题。电子商务中买卖双方都是在网上进行交易，而电子支付协议是保障网络安全交易的关键和基础，只有安全有效的电子支付协议才能保证电子商务交易的顺利进行。
为此，近些年来海内外专家对电子支付协议和身份认证协议进行了深入研究。文献[2]根据电子支付协议ISI创建出FSM模型,并且使用符号检验工具SMV验证得出ISI协议不满足公平性。刘义春等[3]利用串空间逻辑对ISI协议进行验证,同样也分析出其不具有公平性。文献[4]通过引入FTP防止协议中断，并用Kailar逻辑进行分析，虽然满足了公平性，但是并不能防止商家的恶意欺骗。文献[5]描述了远程身份认证和密钥协商协议，利用随机数，防止了重放攻击并且利用Hash函数提高了完整性。文献[6]利用公钥基础设施技术和CRAM技术,构造出动态身份认证系统。文献[7]描述了新的适用于分布式网络的单点登录协议，实现了用户和应用服务器双方之间的相互认证。
目前，多数支付协议的结构都比较单一，比如:脱机小额支付协议[8]、电子现金支付协议[9]等。本文提出了一种新的复合型电子支付协议。该协议由保证安全支付基础的身份认证子协议和支付子协议两部分组成。该协议利用令牌[13]认证技术使用户和服务供应商之间完成双向身份认证[14]并完成了密钥的协商；在支付子协议中利用Hash函数，对部分信息进行了双重加密，提高了协议的完整性。同时在交易过程中为了防止存在欺诈行为，把部分信息交予第三方进行转发，以维护交易环境的安全。最后使用SVO逻辑和改进后的Kailar逻辑对新的复合型安全支付协议进行形化分析，验证其是否具有双向认证性、可追究性和公平性。
1 AECPP协议及其缺陷
1.1 协议描述
AECPP协议是一种具有多种安全属性的复合型支付协议，参与实体如下：用户MU、互联网信息服务供应商SP、攻击者I以及MU和SP都信任的货币服务方CS与仲裁方ADJ。协议具体约定及说明参考文献[10]。
基于令牌的认证子协议TAKEP描述如下：
(1) MU→SP:IDMU，SP，TokenMUn-2，{TS，TokenMUn-1，{KMU_SP}KMAC1}KCS，MAC1；
(2) SP→CS:IDMU，SP，TokenMUn-2，{TS，TokenMUn-1，{KMU_SP}KMAC1}KCS，MAC2；
(3) CS→SP:IDMU，SP，{TS，SUCC，{KMU_SP}KMAC1}KSP_CS_1，MAC3；
(4) SP→MU:IDMU，SP，{TS，SUCC}KMU_SP，MAC4。
支付子协议即ISI的改进法方案描述如下：
(1) SP→MU:{{kSP，SP}KTTP-1}KMU_SP；
(2) MU→SP:{{coins}KCS-1，SKMU，K_SES，S_ID}KSP；
(3) SP→CS:{{coins}KCS-1，SKSP，transaction，IDMU}KCS，{{amount，Tid，date}KSP-1}SKMU；
(4) SP→CS:{{new_coins}KCS-1}SKSP；
(5) MU→CS:{{amount，Tid，date}KSP-1}SKMU。
1.2 协议存在的问题
令牌认证子协议TAKEP利用Hash链完成了服务商对用户的单向认证，并且实现了双方交易会话密钥的协商，验证材料集合是由Hash链中的节点构成的，每次移动用户登录网络信息服务供应商网站，就出示一个令牌。虽然Hash[11]函数具有很高的软件执行效率，但其只能对持有令牌的用户实现单向验证，无法实现双向认证，容易遭到匿名攻击。
此外，该协议的支付子协议是对ISI[12]协议进行改进后形成的。在交易进行时，有可能发生交易的双方对交易信息恶意删除或改动作伪，无法确保交易内容是否准确完整。
2 新的复合型电子支付协议
新的复合电子支付协议是由基于令牌的双向认证子协议和匿名电子支付子协议构成。认证子协议利用令牌完成了用户和第三方彼此身份信息的识别确认，同时达成了交易会话密钥的协商；支付子协议可以保证用户向服务商匿名付款，服务商获得电子现金支付。参与新复合型电子支付协议的实体如下：移动用户A，互联网服务供应商B，A、B双方都信任的货币服务第三方TTP。
2.1 新的基于令牌认证子协议
2.1.1 符号定义
为了完成移动用户和互联网服务供应商之间的相互认证和会话密钥的协商，协议所使用的符号定义如下：
certA、certB、certT：移动用户A、互联网服务供应商B、可信第三方TTP的公钥证书；
IDA：用户A的匿名身份标识符，用于实现用户的匿名支付；
Kca、Kca-1：证书机构授予的公钥和私钥；
KA、KB、KT：移动用户A、互联网服务供应商B、可信第三方TTP的公钥；
KA-1、KB-1、KT-1：移动用户A、互联网服务供应商B、可信第三方TTP的私钥；
K：TTP的对称密钥；
{M}K：用密钥K加密消息M;
KR：随机的临时对称密钥；
KAB：A和B之间的会话密钥、KAT：A和TTP之间的会话密钥；
TokenA：TTP授予A的服务令牌
(TokenA={IDA，TTP，KAT，Tt，lifetime}K)；
Tt：TTP生成的时间戳；lifetime：TokenA的生存时间；
NA、NA＇； NB、NB＇； NT、NT＇：A、B、TTP生成的一次性随机数。
2.1.2 令牌认证协议描述
M1:A→TTP:IDA；
M2:TTP→A:certT，{NT，IDA}KT-1；
M3:A→TTP:{certA，{NT+1，NA，KR，IDA}KA-1}KT；
M4:TTP→A:TokenA，{NA+1，IDA，TTP，KAT}KR；
M5:A→B:TokenA，IDA，NA＇；
M6:B→TTP:certB，{TokenA，IDA，NA＇，B}KB-1；
M7:TTP→B:{certT，{{NA＇-1，IDA，KAB}KAT，IDA，NB+1，KAB}KT-1}KB；
M8:B→A:{NA＇-1，IDA，B，KAB}KAT，{NA＇+1，B，IDA，NB＇}KAB；
M9:A→B:{NB＇+1}KAB。
协议说明如下：
消息M1-M4实现了移动用户与可信第三方之间相互认证，并且在此期间用户得到了服务令牌TokenA。消息M5-M7完成了对移动用户的TokenA的检验，若检验通过，则可以与互联网服务供应商进行联机。消息M8-M9用来验证互联网服务供应商的身份。
M1:用户A发出认证请求。
M2：用户A收到TTP的公钥证书及用其私钥加密的随机数NT和A的身份，A可以用TTP的公开密钥解密。
M3:为了保证信息的安全性，该信息只能让第三方看到，用移动用户A的私钥对消息进行签名认证，然后用可信第三方的公钥再进行加密。
M4:TTP利用A产生的一次性密钥对用户发送的应答消息实施加密。响应的消息中包含与A之间的会话密钥，并且给A颁发服务令牌。
M5: 移动用户A向互联网服务供应商B提出服务请求。
M6: 可信第三方对用户的服务令牌进行校验，如果校验失败，则协议终止，如果成功，则执行第7步协议。
M7: 可信第三方生成用户与服务供应商之间的会话密钥，并发送给B。
M8: B将由TTP发送的消息转发给A，A用其与TTP之间的共享密钥解密得到KAB。
2.2 改进的支付子协议
2.2.1 协议所使用的符号
KA、KB、KT：移动用户A、互联网服务供应商B、可信第三方TTP的公钥；
KA-1、KB-1、KT-1：移动用户A、互联网服务供应商B、可信第三方TTP的私钥；
SKA、SKB：移动用户A、互联网服务供应商B对称会话密钥；
KAB：A和B之间的会话密钥；
S_id：服务的标识符；K_ses：密钥；
Transactiont：具体事务处理；
Tid，date：B收到电子货币的时间和日期；
KMAC1：A与B共享的用于加密Hash函数的密钥；
KMAC2：A与TTP共享的用于加密Hash函数的密钥；
KMAC3：B与TTP共享的用于加密Hash函数的密钥。
消息完整性验证码如下：
MAC1：HMAC({{KB，B}KT-1} KAB，KMAC1)；
MAC2：HMAC({{{coins}KT-1，SKA，K_ses,S_id}KA-1}KT，KMAC2)；
MAC3：HMAC({{coins}KT-1，{SKA，K_ses,S_id}KMAC1}KB，KMAC3)；
MAC4：HMAC({{coins}KT-1，{SKB, transaction，IDA}KMAC3}KT，{{amount，Tid，date}KB-1}SKA，KMAC3)；
MAC5：HMAC({{new_coins}KT-1}SKB，KMAC3)；
MAC6：HMAC({amount，Tid，date}KB-1}SKA，KMAC2)。
2.2.2 改进的支付子协议描述
M1:B→A:{{KB，B}KT-1}KAB，MAC1；
M2:A→TTP:{{{coins}KT-1，SKA，K_ses，S_id}KMAC2}KT，MAC2；
M3:TTP→B:{{coins}KT-1，{SKA，K_ses，S_id}KMAC3}KB，MAC3；
M4:B→TTP:{{coins}KT-1，{SKB，transaction，IDA}KMAC3}KT，{{amount，Tid，date}KB-1}SKA，MAC4；
M5:B↔TTP:{{new_coins}KT-1}SKB，MAC5；
M6:A↔TTP:{{amount，Tid，date}KB-1}SKA，MAC6。
协议说明如下：
M1: 服务方向用户提供由第三方签名并用公钥证书来验证身份，同时A得到了B的公开密钥。
M2: 用户将向服务方提供的信息发送到第三方，由第三方进行转发。
M3: 第三方将用户的电子货币、私钥、希望得到的服务标识和密钥转发给B。
M4: B将收到的电子货币转发给TTP,并且把付款收据发送给第三方。
M5: 若TTP确认这笔付款存在，则把这笔付款交给B。
M6: 由于传输信道的不安全性，为了保证协议中断时双方处于对等状态，采用FTP传送方式，使得用户A获得支付收据。
3 新协议的形式化分析
下面使用SVO逻辑和Kailar逻辑对复合型电子支付协议的属性进行形式化分析。因篇幅有限，分析方法不在此赘述。
3.1 双向认证性
3.1.1 认证目标
使用SVO逻辑分析该子协议证明的目标如下：
G1：A believes shared(A，KAB，B);
G2：B believes shared(A，KAB，B);
G3：A believes B believes shared(A，KAB，B);
G4：B believes A believes shared(A，KAB，B)。
3.1.2 协议理想化
对协议语句理解如下：
M1:A→TTP:IDA；
M2:TTP→A:{PK(TTP，KT)}Kca-1，{NT}KT-1，{IDA}KT-1；
M3:A→TTP:{{PK(A，KA)}Kca-1，{NT+1，NA，shared(A，KR，TTP)，IDA、TTP}KA-1}KT；
M4:TTP→A:TokenA，{NA+1，IDA，TTP，shared(A，KAT，TTP)}KR；
M5:A→B:TokenA，IDA，NA＇；
M6:B→TTP:{PK(B，KB)}Kca-1，{TokenA，IDA，NA＇，B}KB-1；
M7:TTP→B:{{PK(TTP，KT)}Kca-1，{{NA＇-1，IDA，B，shared(A，KAB，B)}KAT，IDA，B，NB+1，shared(A，KAB，B)}KT-1}KB；
M8:B→A:{NA＇-1，IDA，B，shared(A，KAB，B)}KAT，{NA＇+1，B，IDA，NB＇，shared(A，KAB，B)}KAB；
M9:A→B:{NB＇+1，shared(A，KAB，B)}KAB。
3.1.3 初始化假设
A1:A，B，TTP believes PK(CA，Kca)；
A2:B，A believes CA controls PK(TTP，KT)；
A3:TTP believes CA controls PK(B，KB)；
A4:TTP believes CA controls PK(A，KA)；
A5:A，TTP believes shared(A，KR，TTP)；
A6:TTP believes PK(TTP，KT)；
A7:B believes PK(B，KB)；
A8:TTP believes A controls shared(A，KR，TTP)；
A9:A believes TTP controls shared(A，KAT，TTP)；
A10:A，B believes TTP controls shared(A，KAB，B)；
A11:A，B believes fresh PK(TTP，KT)；
A12:TTP believes fresh PK(A，KA)；
A13:TTP believes fresh PK(B，KB)；
A14:TTP believes fresh(NT)；
A15:A believes fresh(NA)；A believes fresh (NA＇)；
A16:B believes fresh(NB)；B believes fresh (NB＇)。
3.1.4 逻辑推理
分析所用到的SVO逻辑公理如下：
R1：P believes Ψ∧ P believes(Ψ⊃φ)⊃ P believes φ；
R2：shared(P，K，Q)∧ R received {XQ}K⊃Q said X；
R3：PK(Q，K)∧ R received{X}K-1⊃Q said X；
R4：P received(X1，…，Xn)⊃P received Xi；
R5：P received{X}K∧P has K-1⊃P received X；
R6：P said(X1，…，Xn)⊃P said Xi∧P sees Xi；
R7：P controls Ψ ∧ P said Ψ⊃Ψ；
R8：fresh(Xi)⊃fresh(X1，…，Xn)。
根据推理过程需要合理拓展公理如下：
R9：P believes fresh(X)∧ P believes Q said X⊃ P believes Q believes X；
R10：P believes Q believes(X，Y)⊃P believes Q believes X。
推理过程如下：
由M2，R4可得：
(a) A received{PK(TTP，KT)}Kca-1。
由(a)、A1和R3可得：
(b) A believes CA said PK(TTP，KT)。
由(b)、A2和R7可得：
(c) A believes PK(TTP，KT)。
由M3、R4、A6和R5可得：
(d) TTP received{PK(A，KA)}Kca-1，TTP received{NT+1，NA，shared(A，KR，TTP)，A、TTP}KA-1。
由(d)和A1可得：
(e) TTP believes CA said PK(A，KA)。
由(e)、A12、A4、R7和R9可得：
(f) TTP believes PK(A，KA)。
由(d)、(f)、R3可得：
(g) TTP believes A said{NT+1，NA，shared(A，KR，TTP)}。
由A15和R8、R7可得：
(h) TTP believes shared(A，KR，TTP)。
由R6和M4可得：
(i) A received {NA+1，shared(A，KAT，TTP)}KR。
由(i)、A5、A9、A15、R2、R9、R8、R7、R10可得：
(j) A believes shared(A,KAT,TTP)。
由M6和R4可得：
(k) TTP received {PK(B，KB)}Kca-1。
由A1、A3、A13、R7、R9、R3、(k)可得：
(l) TTP believes PK(B，KB)。
由M7、A7、R5和R4可得：
(m) B received{PK(TTP，KT)}Kca-1；
(n) B received {NA＇，{shared(A，KAB，B)}KAT，NB+1，shared(A，KAB，B)}KT-1。
由A1、A11、A2、R3、R9、R7、(m)可得：
(o) B believes PK(TTP，KT)；(G2)。
由A16、A10、R3、R9、R7、R8、R6、R10、(n)、(o)可得：
(p) B believes shared(A，KAB，B)；(G1)。
由M8和R4可得：
(q) A received{NA＇-1，shared(A，KAB，B)}KAT；
(r) A received{NA＇+1，NB＇，shared(A，KAB，B)}KAB。
由(q)、(j)、A15、A10、R2、R8、R9、R10、R7可得：
(s) A believes shared(A，KAB，B)；(G3)。
由A15、R2、R8、R9、R10、(r)、(s)可得：
(t) A believes B believes shared(A，KAB，B)。
由M9、(p)、A16、R2、R9、R8、R10可得：
(u) B believes A believes shared(A，KAB，B)；(G4)。
因此得到结论(s)、(p)、(t)、(u)与认证目标G1、G2、G3、G4一致。由此可见，该协议的认证令牌子协议满足可双向认证性。
3.2 可追究性
3.2.1 认证目标
因为支付子协议是令牌认证子协议基础上的一个匿名的协议，所以用户A和服务供应商B已经进行了密钥的协商。若要满足支付方A的可追究性，只需验证收款证明对于收款方是有效的即可；若要满足提供服务方B的可追究性，则需证明用户A受收到了B曾经发送过的收据证明。因此，采用Kailar逻辑分析该子协议要达到的目标如下：
G1：B≻TTP→new_coins;
G2：A≻B→{amount，Tid，date}KB-1。
3.2.2 初始拥有集合
P1：OA0={KT，KAB，KMAC1，KMAC2};
P2：OB0={KT，KAB，KMAC1，KMAC3};
3.2.3 EOO和EOR
发放非否认证据EOO ={new_cions}KT-1；
收方非否认证据EOR ={amount，Tid，date}KB-1。
3.2.4 逻辑推理
分析所用到的改进后的Kailar逻辑如下：
假设EOO∈OB成立，即{new_cions}KT-1∈OB成立，也就是：
(a){new_cions}KT-1∈B成立。
由(a)、P4和R1可得：
(b) B≻TTP→new_coins。(G1)。
假设EOR∈OA成立，即{amount，Tid，date}KB-1∈OA，也就是：
(c) {amount，Tid，date}KB-1∈A成立。
由于KAB∈OA0∈OA，并且 {{KB，B}KT-1} KAB∈OA1∈OA，那么{{KB，B}KT-1}∈OA1∈OA。
(d) {KB，B}KT-1∈A。
由(d)、P3、(R1)可得：
(e) A≻TTP→{KB,B}。
再由(e)和R2可得：
最后根据(f)、(c)和R1可得：
(g) A≻B→{amount，Tid，date}KB-1；(G2)
因此得到结论(b)、(g)与认证目标G1、G2一致。
可见，支付子协议满足可追究性。
3.3 公平性
3.3.1 认证目标
G2：协议异常终止时，通信双方都处于同等地位，任何一方都不占优势。
3.3.2 逻辑推理
分析OA：
OA6=OA5∪{{{amount，Tid，date}KB-1}SKA}
(h) {{{amount，Tid，date}KB-1}SKA}? OA；
由 (i) OA1={KAB，KB，KT，KMAC2}，OA6=OA2=OA1∪{{{{coins}KT-1，SKA，K_ses,S_id}KMAC2}KT}得
(j) SKA∈OA6。
根据(h)、(i)、(j)得
(k) {amount，Tid，date}KB-1∈OA。
分析OB：
OB5=OB4∪{{{new_coins}KT-1}SKB}，OB4=OB3∪{{ coins}KT-1，{SKB，transaction,IDA}KMAC3}，根据P2得SKB∈OB5，因此
(l){new_cions}KT-1∈OB。
因此当协议正常结束时证明结果(k)、(l)满足G1。
在协议的1～4步中，若产生中断，双方都不占优势；在协议的第5、6步时，由于协议采用的FTP传输方式，出现异常后语句不会中断。因此满足G2。
可见，支付子协议满足公平性。
4 协议对比
本文所提出的新的复合型安全协议不仅具有可追究性和公平性，相比原有的协议在认证的安全性、保密性等方面也有了进一步的提升。原有协议与新复合协议对比如表1所示。
表1 原有协议与新复合协议对比
5 结 语
本文提出了一种新的复合型电子支付协议，该协议使得移动用户和互联网服务提供方之间的身份得到了确认并且达成了密钥协商，同时支付子协议的完整性得到了提高。接着利用形式化分析语言SVO逻辑和Kailar逻辑对新的复合协议进行分析，结果表明新协议具有双向认证性、可追究性和公平性。该协议安全可靠，可以在实际电子商务交易中进行运用，用来保证交易的安全，并且用户的个人信息也不会遭到泄露。
尽管本文对原有协议进行了改进，但是新复合电子支付协议的实现步骤较多，如何提高该协议的运行效率需要进一步研究。
[1] 周景春. 基于SSL协议的电子商务支付系统的设计与实现[J]. 现代电子技术,2017,40(2):167- 170.
[2] 文静华, 张梅, 李祥. ISI协议的符号模型检验分析[J]. 电讯技术,2005,45(6):80- 83.
[3] 郭华,李舟军,庄雷,等. 一种新的电子商务协议分析方法[J]. 计算机科学,2010,37(8):56- 60.
[4] 徐洋,汪学明,谢晓尧. 一个新的电子支付协议及其形式化分析[J]. 计算机应用与软件,2008,25(9):93- 94,124.
[5] 张利华,章丽萍,张有光,等. 基于口令的远程身份认证及密钥协商协议[J]. 计算机应用,2009,29(4):924- 927.
[6] 张秋余,梁爽,王怀江. 一种新的基于PKI的动态身份认证系统的设计[J].计算机应用研究,2006,23(10):116- 118.
[7] 杨荣华. 基于SOA的单点登录系统研究与设计[D].中南大学,2008.
[8] San A M, Sathitwiriyawong C. Efficient offline micropayment protocol for multi-vendor[C]// 2016 International Computer Science and Engineering Conference (ICSEC), Chiang Mai, 2016:1- 4.
[9] Dreier J, Kassem A, Lafourcade P. Formal Analysis of E-Cash Protocols[C]// International Conference on Security and Cryptography. 2015:65- 75.
[10] 陈莉,袁开银. 满足多种安全属性的复合型支付协议及其逻辑分析[J]. 计算机应用研究,2012,29(7):2672- 2677.
[11] 王勇,蔡国永. 基于随机函数的哈希函数[J]. 计算机工程与设计,2015,36(10):2679- 2683.
[12] Medvinsky G, Neuman C. NetCash: a design for practical electronic currency on the Internet[C]// ACM Conference on Computer and Communications Security. ACM, 1993:102- 106.
[13] 杨箫.面向支付的Tokenization系统的关键技术研究与实现[D].电子科技大学,2016.
[14] 陶源,周喜,马玉鹏,等. 基于Hash函数的移动双向认证协议[J]. 计算机应用,2016,36(3):657- 660.
[15] ISO/IEC 3rd CD 13888-1.Information technology-Security techniques,Part 1:General model.ISO/IEC JTC11/SC24 N1274[S]. 1996.
