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