淺析電子商務支付協議認證性的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