淺析電子商務(wù)支付協(xié)議認(rèn)證性的SVO邏輯驗(yàn)證

劉麗峰

(山西金融職業(yè)學(xué)院,030008)

淺析電子商務(wù)支付協(xié)議認(rèn)證性的SVO邏輯驗(yàn)證

劉麗峰

(山西金融職業(yè)學(xué)院,030008)

當(dāng)前，高效、安全的支付方式已成為移動電子商務(wù)發(fā)展的首要問題。但目前移動電子商務(wù)研究中對移動支付協(xié)議的設(shè)計(jì)尚不健全，如何對移動支付協(xié)議認(rèn)證備受關(guān)注。本文淺析電死商務(wù)協(xié)議認(rèn)證中SVO邏輯驗(yàn)證的應(yīng)用。

電子商務(wù)；支付協(xié)議認(rèn)證；SVO邏輯

網(wǎng)絡(luò)及信息技術(shù)的快速發(fā)展，致使電子商務(wù)愈發(fā)熱門，且增長趨勢明顯。作為其中最關(guān)鍵的電子支付環(huán)節(jié)，其支付協(xié)議的安全和高效直接影響著電子商務(wù)的健康、持續(xù)發(fā)展。本研究從形式化理論和工具驗(yàn)證結(jié)合的方式，對BNA邏輯在驗(yàn)證Netbill協(xié)議推理認(rèn)證中進(jìn)行了分析和闡釋。

1 驗(yàn)證SVO邏輯形式化的方法

在對形式化的安全協(xié)議進(jìn)行分析時(shí)，安全協(xié)議驗(yàn)證屬于重要的邏輯方法。而BNA邏輯則是邏輯方法的鼻祖。一些類似BNA邏輯的分析方法在這之后也陸續(xù)的出現(xiàn)。在1994年，Paul C.van Oorschot與Paul Syverson在BAN邏輯的基礎(chǔ)上，對 AT邏輯和VO邏輯以及GNY邏輯等進(jìn)行總結(jié)時(shí)，提出了SOV邏輯。

SVO邏輯的擴(kuò)展公理以及語法。SVO邏輯定義的公式語言跟消息語言是在原子項(xiàng)集合的基礎(chǔ)上進(jìn)行的。若用K跟X分別用密匙跟消息進(jìn)行表達(dá)，協(xié)議的主體用a跟b來表示，那么N元函數(shù)f（X1，X2,…，Xn）在消息語言中表示消息。如果密匙在加密后得到消息，那么用{X}k表示。私匙k在對x進(jìn)行簽名后得到的消息，用[X]k表示。不能識別但是還能讓主體接收到消息，用*表示。公式SharedKey（K，A，B）在語言公式中表示A跟B的良好共享秘鑰的主體是K。公式：A says X、A said X、A sees X、resh（X）跟A received表達(dá)的意思是，消息x跟主體a之間的一些關(guān)系。A says X表示的是如果a這次開始會話后發(fā)送了x。而A said X表示的是以前發(fā)送的。公式A controls ψ與A believes ψ分別表示A作為主體時(shí)，相信并控制公式ψ。另外，├ψ表示ψ這個(gè)公式屬于一個(gè)定理。

SOV邏輯的規(guī)則有兩條，但是公理達(dá)到20條。主要包括必要性規(guī)則Nec、源關(guān)聯(lián)公理Ax3、相信公里Ax1、接收公理Ax7-9、說過公理Ax14-15、看見公理Ax10、仲裁公理Ax16、Nonce驗(yàn)證公理x19和新鮮性公理Ax17等。在SVO邏輯下，協(xié)議的分析方法中SVO邏輯對安全協(xié)議做出多種認(rèn)證目標(biāo)，具體目標(biāo)如下：（1）G1 存活確認(rèn)：A believes B says X ；（2）G2身份認(rèn)證：A believes B says (X,Na)；（3）G3 建立安全密鑰：A believes SharedKey （K-，A,B）；（4）G4 密鑰的確認(rèn)：A believes SharedKey （K+，A,B）；（5）G5 密鑰的新鮮性：A believes fresh (K)；（6）G6 彼此確認(rèn)密鑰： A believes B says SharedKey （K-，B，A）。分析Netbill協(xié)議涉及到只由單方的主體掌握對稱密匙。為了方便協(xié)議的證明，還根據(jù)a*3導(dǎo)出a*3.1。K－表示的是密匙K還沒有得到確認(rèn)。

2 描述形式化的Netbill協(xié)議

Netbill協(xié)議的步驟。在1996年，Carnegie Mellon大學(xué)的J.D.Tygar教授提出了Netbill 協(xié)議。這個(gè)電子商務(wù)微支付協(xié)議是針對數(shù)字商品提出的。這個(gè)協(xié)議涉及到了三個(gè)方面：Netbill服務(wù)器跟商戶以及顧客。該協(xié)議在三個(gè)方面上都有涉及：（1）在協(xié)商價(jià)格的階段。當(dāng)客戶要向要向商戶了解一些某數(shù)字產(chǎn)品的價(jià)格時(shí)，商戶要把報(bào)價(jià)告訴給客戶；（2）進(jìn)行遞送商品的階段。當(dāng)商家被告知客戶接受了商品的報(bào)價(jià)，商戶在發(fā)送該數(shù)字產(chǎn)品給客戶時(shí)，要用對稱密匙K進(jìn)行加密；（3）在支付款項(xiàng)階段?？蛻粢o商戶發(fā)送一份電子支付訂單的數(shù)字簽名，對該商品的訂單，商戶要跟密匙K進(jìn)行簽名加密，并且要把這兩個(gè)發(fā)給Netbill服務(wù)器。Netbill服務(wù)器要驗(yàn)證收到的簽字消息，要有效的進(jìn)行支付跟檢驗(yàn)顧客賬號的支付信息，然后要給商戶返還里面包含K的簽名收據(jù)，進(jìn)一步的結(jié)果需要商戶再返還給客戶。之后客戶要在Msg4中把加密的商品進(jìn)行解密。

3 SVO形式化驗(yàn)證Netbill協(xié)議簡化模型及未來的發(fā)展

通過對目標(biāo)的驗(yàn)證，來分析SVO邏輯協(xié)議的簡化模型。在Netbill協(xié)議中存在的子協(xié)議，主體的身份認(rèn)證由Kerberos協(xié)議進(jìn)行負(fù)責(zé)。因此，密匙建立協(xié)議跟Netbill 協(xié)議是同一樣的。商戶M獨(dú)立的生成，是K的m次方對商品進(jìn)行加密。不需要對K的m平方進(jìn)行相互的確認(rèn)，其他的主體也只是被動的接受。例如：C believes M said Goods。根據(jù)公式的分析，可以知道認(rèn)證目標(biāo)能夠被Netbill協(xié)議滿足。就是密匙K的m次方能夠安全的建立在M于C之間。能得到C的確定，并且是新鮮的密匙。雖然G沒有滿足協(xié)議，主要是因?yàn)閷Ξa(chǎn)品Goods的新鮮性沒有推到出來。形式化的分析了邏輯推理過程跟協(xié)議簡化的方法。對認(rèn)證其他電子商務(wù)支付協(xié)議起到了一定程度的借鑒作用。Netbill協(xié)議的認(rèn)證性得到了滿足，但是商家時(shí)序的責(zé)任問題還是存在協(xié)議中的。由于在SOV推理時(shí)對時(shí)序的缺乏重視，沒有辦法在這個(gè)角度進(jìn)行協(xié)議的分析。所以，要考慮時(shí)態(tài)算子要加入到SVO邏輯中，語言能力有所增加后，對認(rèn)證電子商務(wù)支付協(xié)議有更多的目標(biāo)。

4 總結(jié)

電子商務(wù)的發(fā)展已勢不可擋，如何確保其健康、持續(xù)、快速的發(fā)展，電子商務(wù)支付的安全高效的重要性不言而喻。通過本文對SVO的邏輯推理方法的擴(kuò)展來看，其Netbill微支付協(xié)議的認(rèn)證性是安全、可靠且高效的。值得同行借鑒參考，相信隨著互聯(lián)網(wǎng)網(wǎng)絡(luò)信息技術(shù)的快速發(fā)展，定能使之更加完善，已安全高速的現(xiàn)代化形象為電子商務(wù)的發(fā)展奠定堅(jiān)實(shí)基礎(chǔ)。

[1] 肖茵茵,蘇開樂.電子商務(wù)支付協(xié)議認(rèn)證性的SVO邏輯驗(yàn)證[J].計(jì)算機(jī)工程與應(yīng)用,2014,(08):6-10.

[2] 肖仕成,李開,甘早斌.基于四方的安全電子商務(wù)支付協(xié)議分析與驗(yàn)證[J].計(jì)算機(jī)科學(xué),2012,39(3):75-78.

[3] 陳莉,袁開銀.滿足多種安全屬性的復(fù)合型支付協(xié)議及其邏輯分析[J].計(jì)算機(jī)應(yīng)用研究,2012,(7):2672-2677.

[4] 馬生.有窮機(jī)和邏輯結(jié)合的電子商務(wù)協(xié)議分析方法[J].小型微型計(jì)算機(jī)系統(tǒng),2013,34(3):492-497.

[5] 黃珍.淺析電子商務(wù)中移動支付[J].科技與創(chuàng)新,2015,(9):36-37.

劉麗峰，女，（1970—），山西金融職業(yè)學(xué)院副教授，山西大學(xué)碩士學(xué)歷。研究方向:電子商務(wù)。

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