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

肖茵茵 ，蘇開樂

XIAOYinyin1，2,SU Kaile2，3

1.廣東技術(shù)師范學(xué)院 計算機(jī)學(xué)院，廣州 510665

2.中山大學(xué) 信息科學(xué)與技術(shù)學(xué)院 廣東省信息安全重點(diǎn)實(shí)驗室，廣州 510275

3.北京大學(xué) 信息科學(xué)技術(shù)學(xué)院 教育部高可信軟件技術(shù)重點(diǎn)實(shí)驗室，北京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 引言

隨著電子商務(wù)的普及和發(fā)展，SSL、SET、Netbill等電子商務(wù)支付協(xié)議的地位越來越重要。安全協(xié)議的手工分析十分困難，容易出錯，特別是對復(fù)雜的電子商務(wù)支付協(xié)議來說，采用形式化的理論和工具驗證其安全性十分必要[1]。在現(xiàn)有的電子商務(wù)協(xié)議安全性研究中，多采用有限模型檢測法尋找協(xié)議的漏洞和潛在攻擊的路徑（證偽法）[2-4]，這類方法具有自動化工具（SMV、SPIN等），使用方便，但檢測的狀態(tài)空間有限，即使檢測不出攻擊，也無法保證協(xié)議在任意會話中的正確性。另一類方法采用定理證明和邏輯推理，可驗證協(xié)議能否滿足特定的安全性質(zhì)以及證明協(xié)議的正確性（證真法）[5-7]，這類方法準(zhǔn)確度高，但驗證過程繁雜，驗證復(fù)雜協(xié)議時難度較大，如文獻(xiàn)[5]用實(shí)例化空間邏輯驗證了SET協(xié)議的秘密性和認(rèn)證性，但文中并未說明其具體推理過程；文獻(xiàn)[8-9]展示了使用類BAN邏輯驗證Netbill協(xié)議的推理過程，但文中主要關(guān)注的是協(xié)議的原子性和時限責(zé)任等問題，而未討論其認(rèn)證性。

本文使用SVO邏輯方法[10]，選取Netbill協(xié)議[11]，對其認(rèn)證性進(jìn)行形式化分析：首先對SVO邏輯的公理集進(jìn)行擴(kuò)展，然后在不影響Netbill協(xié)議安全性的前提下，為其建立簡化模型，之后針對協(xié)議特點(diǎn)，修正和補(bǔ)充了其驗證目標(biāo)，最后給出了具體的推理過程和驗證結(jié)果以及相關(guān)工作的比較。隨著人們對網(wǎng)絡(luò)知識產(chǎn)權(quán)保護(hù)意識的提高，用于數(shù)字產(chǎn)品交易的Netbill微支付協(xié)議重新受到了人們的重視，因此本文的研究是有現(xiàn)實(shí)意義的。更重要的是，文中展示的協(xié)議簡化方法和邏輯推理過程也適用于分析其他電子商務(wù)支付協(xié)議的認(rèn)證性。

2 SVO邏輯形式化驗證方法

安全協(xié)議驗證邏輯是安全協(xié)議形式化分析中的一類重要方法，而BAN邏輯[12]是這類方法的鼻祖。在此之后，又有一系列類BAN邏輯分析方法相繼出現(xiàn)。1994年，Paul Syverson和Paul C.van Oorschot在總結(jié)BAN邏輯和GNY邏輯、AT邏輯及VO邏輯等類BAN邏輯的基礎(chǔ)上提出了SVO邏輯[10]。SVO邏輯修補(bǔ)了其他類BAN邏輯的缺陷和不足，具有十分簡潔的推理規(guī)則和公理。它的出現(xiàn)標(biāo)志著BAN邏輯及類BAN邏輯的成熟，為邏輯系統(tǒng)建立了合理的理論模型。由于篇幅所限，對于SVO邏輯，這里只對本文協(xié)議驗證所需的部分做簡單介紹，其他詳見文獻(xiàn)[10]。

2.1 SVO邏輯語法及擴(kuò)展公理

SVO邏輯在原子項集合的基礎(chǔ)上定義了消息語言和公式語言。若以X和K分別表示消息和密鑰，以A和B表示協(xié)議主體，則在消息語言中，n元函數(shù)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的各種關(guān)系，如“A says X”表示A在本次會話開始后發(fā)送了X，而“A said X”是以前發(fā)送的；公式“A believes ψ”和“A controlsψ”分別表示主體A相信和控制公式ψ。另外，┐ 、∧ 、? 、? 分別表示“非”、“與”、“蘊(yùn)含”和“推理”；├ψ表示公式ψ是一個定理。

SVO邏輯的規(guī)則有2條，公理有20條，本文協(xié)議驗證過程中用到的有必要性規(guī)則Nec（Necessitation）、相信公理Ax1、源關(guān)聯(lián)公理Ax3、接收公理Ax7~Ax9、看見公理Ax10、說過公理Ax14~Ax15、仲裁公理Ax16、新鮮性公理Ax17、Nonce驗證公理Ax19，具體如下（XB表示消息X來自于主體B）：

2.2 SVO邏輯下的協(xié)議分析方法

其中，K－表明密鑰K還未得到確認(rèn)；K+表明密鑰K已經(jīng)得到確認(rèn)，即從B發(fā)的消息中，得知B知道K。

用SVO邏輯分析安全協(xié)議，即驗證協(xié)議是否滿足上述認(rèn)證目標(biāo)，其步驟和BAN邏輯類似。不同的是，SVO邏輯并不“理想化”協(xié)議，而是對協(xié)議進(jìn)行假設(shè)。SVO假設(shè)有4類：第1類是初始假設(shè)，即那些在協(xié)議運(yùn)行開始時被認(rèn)為成立的公式，如主體相信自己產(chǎn)生的隨機(jī)數(shù)的新鮮性、主體和可信第三方之間密鑰的良好性、可信第三方產(chǎn)生的密鑰的新鮮性、良好性等；第2類反映了消息的接收，這可直接由協(xié)議消息而得；第3類假設(shè)反映了主體對接收到消息的理解；第4類假設(shè)用來反映消息接收者對消息的解釋。

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

3.1 協(xié)議步驟

Netbill協(xié)議是Carnegie Mellon大學(xué)的J.D.Tygar教授于1996年提出的一個針對數(shù)字商品（例如一個軟件或一首歌曲）的電子商務(wù)微支付協(xié)議[11]。該協(xié)議涉及到三方參與者：顧客、商戶及Netbill服務(wù)器，客戶持有的Netbill賬號等價于一個虛擬電子信用卡賬號。Netbill協(xié)議的主要步驟如圖1所示。

該協(xié)議分為三個階段：在價格協(xié)商階段，顧客向商戶查詢某數(shù)字商品價格，商戶向該顧客報價；在商品遞送階段，顧客告知商戶他接受報價，商戶將該數(shù)字商品用對稱密鑰K加密后發(fā)送給顧客；在支付階段，顧客準(zhǔn)備一份電子支付訂單的數(shù)字簽名值發(fā)送給商戶，商戶對該訂單和密鑰K簽名加密，并將此二者發(fā)送給Netbill服務(wù)器。Netbill服務(wù)器解密并驗證收到的簽名消息，對顧客賬號等支付信息的有效性進(jìn)行檢驗和支付授權(quán)，然后將包含K的簽名收據(jù)返回給商戶，由商戶將結(jié)果進(jìn)一步轉(zhuǎn)送給顧客，最后顧客將Msg4中的加密信息商品解密。

3.2 消息簡化

驗證復(fù)雜協(xié)議的首要步驟是在不影響協(xié)議驗證目標(biāo)的前提下合理簡化協(xié)議。在不影響Netbill協(xié)議認(rèn)證性的基礎(chǔ)上，在形式化描述該協(xié)議時，對協(xié)議消息做了如下簡化：

（1）去除了狀態(tài)標(biāo)識、顧客的起拍價、顧客及商戶的備忘域、等可選的部分消息。

（2）SVO邏輯基于Dolev-Yao符號化模型對協(xié)議進(jìn)行推理，其消息操作是作用在消息集合上的抽象函數(shù)/密碼原語，因此，也不對Netbill協(xié)議使用的具體密碼算法進(jìn)行區(qū)分，只以加密、簽名等抽象函數(shù)表示密碼學(xué)運(yùn)算：

TAB（Identity）：一個Kerberos許可證，用于向B證明A是用Identity命名的，并在他們之間建立一個共享的會話密鑰KAB。

3.3 協(xié)議簡化模型的形式化描述

根據(jù)3.2節(jié)中的分析，簡化后的Netbill協(xié)議如下：

其中，C、M和N分別代表顧客、商戶和Netbill服務(wù)器；PRD（Product Request Data）是商品請求數(shù)據(jù)；TID是交易ID；ProductID是商品ID；Price是商戶的報價；Goods是具體商品內(nèi)容；CAcct、MAcct分別是顧客和商戶的賬號；EPO（Electronic Purchase Order）是電子支付訂單，其明文部分包括商戶和Netbill服務(wù)器可讀的交易信息（如商品描述、客戶認(rèn)證等），其加密部分包括只有Netbill服務(wù)器可讀的支付指令（如顧客賬號等）；EPOID是電子支付的ID，是全局唯一的標(biāo)識符，將被用在NetBill數(shù)據(jù)庫中唯一地確認(rèn)這次交易；Receipt是Netbill服務(wù)器返回的收據(jù)，其中包含是否接受本次支付的結(jié)果Result和對商品進(jìn)行加/解密的密鑰KM。

4 Netbill協(xié)議簡化模型的SVO形式化驗證

4.1 驗證目標(biāo)

基于SVO邏輯的協(xié)議分析，其目的是驗證協(xié)議是否滿足第2章中的SVO認(rèn)證目標(biāo)。Netbill協(xié)議的子協(xié)議中，由Kerberos協(xié)議負(fù)責(zé)其主體的身份認(rèn)證，通信主體能被Kerberos協(xié)議賦予身份票據(jù)進(jìn)行會話，這說明SVO目標(biāo)G1、G2已被Kerberos協(xié)議滿足，驗證過程可見文獻(xiàn)[13]，因此，G1、G2也被Netbill協(xié)議滿足；另外，Netbill協(xié)議屬于密鑰建立協(xié)議，其中對商品進(jìn)行加密的密鑰KM由商戶M獨(dú)立生成，其他主體只是被動的接受，無需對KM進(jìn)行相互確認(rèn)，即并沒有G6這樣的目標(biāo)。因此，省略了G1、G2、G6目標(biāo)的驗證。與普通的密鑰建立協(xié)議不同，Netbill協(xié)議僅涉及到單方主體掌握對稱密鑰KM，不適合用Sharedkey相關(guān)公式描述其性質(zhì)，因此，在SVO邏輯認(rèn)證目標(biāo)的基礎(chǔ)上進(jìn)行了一些改動，總結(jié)出要驗證的Netbill協(xié)議認(rèn)證目標(biāo)：

Netbill協(xié)議的最終目的是顧客C付款之后能從商戶M處獲得密鑰KM，對之前收到的加密產(chǎn)品進(jìn)行解密，獲得商品Goods。因此，除了SVO認(rèn)證目標(biāo)外，還制定了以下驗證目標(biāo)：

4.2 協(xié)議假設(shè)

基于SVO邏輯的協(xié)議分析，其目的是驗證協(xié)議是否滿足進(jìn)行推理前，應(yīng)對Netbill協(xié)議制定SVO邏輯假設(shè)。因篇幅所限，下面只列出與推理過程相關(guān)的假設(shè)。

首先是初始假設(shè)：

4.3 推理過程

下面，用SVO邏輯的推理規(guī)則和公理對Netbill協(xié)議進(jìn)行推導(dǎo)：

由（13）、（15）可知，顧客C在收到密鑰KM之后，能收到由商戶M發(fā)來的產(chǎn)品Goods。由于Goods不由新鮮隨機(jī)數(shù)生成，所以無法繼續(xù)推導(dǎo)出Goods的新鮮性，無法得知M是否在本次運(yùn)行中說過Goods，即目標(biāo)G'不成立。但由（12）可知，加密后的產(chǎn)品確實(shí)是在本次運(yùn)行中發(fā)送的，即顧客C收到的加密產(chǎn)品仍是新鮮的。

4.4 驗證結(jié)果

由上文的分析，可知Netbill協(xié)議能夠滿足認(rèn)證目標(biāo)G3'、G4'、G5'，即密鑰 KM能夠在 C 和 M 之間安全地建立，并受到C的確認(rèn)，而且該密鑰是新鮮的；雖然目標(biāo)G'未被協(xié)議滿足，但這只是因為無法推導(dǎo)出產(chǎn)品Goods的新鮮性所致，顧客C收到的加密產(chǎn)品仍是新鮮的，且若收到密鑰KM，還是能收到由M發(fā)來的產(chǎn)品Goods。這一驗證結(jié)果表明，Netbill協(xié)議的認(rèn)證性是有保障的。

4.5 相關(guān)工作比較

與本文相關(guān)的研究工作有文獻(xiàn)[5，8-9]，其具體的比較可見表1。從表中可知，本文的工作著重對Netbill協(xié)議的認(rèn)證性進(jìn)行了驗證，而文獻(xiàn)[8-9]主要關(guān)注的是該協(xié)議的原子性和時限責(zé)任等問題；文獻(xiàn)[5]驗證了另一電子商務(wù)協(xié)議——SET協(xié)議的認(rèn)證性和秘密性，但文中并未說明其具體推理過程，而本文的邏輯推理過程具體完整，這是使用邏輯方法對安全協(xié)議進(jìn)行驗證的重要環(huán)節(jié)。另外，由于文中所使用的SVO邏輯具有清晰的語義和合理的理論模型，因此本文給出的協(xié)議假設(shè)也比上述研究工作更加完整合理。

表1 與本文相關(guān)的研究工作比較

5 結(jié)束語

使用擴(kuò)展的SVO邏輯推理方法，對Netbill微支付協(xié)議的認(rèn)證性進(jìn)行形式化分析。針對協(xié)議特點(diǎn)，對SVO邏輯的公理集進(jìn)行擴(kuò)展，修正和補(bǔ)充了協(xié)議的驗證目標(biāo)，建立了不影響既有安全性的協(xié)議簡化模型，給出了合理的協(xié)議假設(shè)和具體完整的邏輯推理過程，驗證結(jié)果表明Netbill協(xié)議的認(rèn)證性是有保障的。最后對相關(guān)研究工作進(jìn)行了比較。這一協(xié)議簡化方法和邏輯推理過程對其他電子商務(wù)支付協(xié)議認(rèn)證性的形式化分析起到了一定的借鑒作用。

本文未來研究工作的方向如下：雖然Netbill協(xié)議滿足認(rèn)證性，但該協(xié)議還存在商家時限責(zé)任[9]等問題，由于SVO邏輯缺乏對時序的推理，無法從這一角度分析協(xié)議。因此，可考慮對SVO邏輯加入時態(tài)算子，增強(qiáng)其語言能力后再對更多電子商務(wù)支付協(xié)議進(jìn)行更多目標(biāo)的驗證。

[1]薛銳，馮登國.安全協(xié)議的形式化分析技術(shù)與方法[J].計算機(jī)學(xué)報，2006，29（1）：1-20.

[2]繆力，譚志華，張大方.基于SPIN的網(wǎng)絡(luò)認(rèn)證協(xié)議高效模型檢測[J].計算機(jī)工程與應(yīng)用，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]肖茵茵，蘇開樂，馬震遠(yuǎn)，等.實(shí)例化空間邏輯下的SET支付協(xié)議驗證及改進(jìn)[J].華中科技大學(xué)學(xué)報，2013，41（7）：97-102.

[6]肖茵茵，蘇開樂，岳偉亞，等.SET證書申請協(xié)議在SPV下的自動化驗證及改進(jìn)[J].計算機(jī)學(xué)報，2008，31（6）：1035-1045.

[7]Giampaolo B，F(xiàn)abio 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協(xié)議的形式化描述及分析[J].蘭州理工大學(xué)學(xué)報，2004，30（3）：102-105.

[9]彭勛，董榮勝，郭云川，等.在Netbill交易協(xié)議中引入對商家的時限責(zé)任的追究[J].計算機(jī)科學(xué)，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邏輯的電子商務(wù)協(xié)議形式化分析與研究[D].貴陽：貴州大學(xué)，2007.