肖茵茵 ，蘇開樂

XIAOYinyin1，2,SU Kaile2，3

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

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

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

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

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

安全協(xié)議驗(yàn)證邏輯是安全協(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)建立了合理的理論模型。由于篇幅所限，對(duì)于SVO邏輯，這里只對(duì)本文協(xié)議驗(yàn)證所需的部分做簡單介紹，其他詳見文獻(xiàn)[10]。

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

SVO邏輯在原子項(xiàng)集合的基礎(chǔ)上定義了消息語言和公式語言。若以X和K分別表示消息和密鑰，以A和B表示協(xié)議主體，則在消息語言中，n元函數(shù)F（X1，X2，…，Xn）是消息，如{X}K是用密鑰K對(duì)X加密后得到的消息；[X]K是用私鑰K對(duì)X簽名后得到的消息。*表示主體所收到但不可識(shí)別的消息。在公式語言中，公式“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在本次會(huì)話開始后發(fā)送了X，而“A said X”是以前發(fā)送的；公式“A believes ψ”和“A controlsψ”分別表示主體A相信和控制公式ψ。另外，┐ 、∧ 、? 、? 分別表示“非”、“與”、“蘊(yùn)含”和“推理”；├ψ表示公式ψ是一個(gè)定理。

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

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

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

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

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

3.1 協(xié)議步驟

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

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

3.2 消息簡化

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

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

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

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

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

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

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

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

4.1 驗(yàn)證目標(biāo)

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

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

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

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

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

4.3 推理過程

下面，用SVO邏輯的推理規(guī)則和公理對(duì)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 驗(yàn)證結(jié)果

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

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

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

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

5 結(jié)束語

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

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

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

[2]繆力，譚志華，張大方.基于SPIN的網(wǎng)絡(luò)認(rèn)證協(xié)議高效模型檢測[J].計(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é)議驗(yàn)證及改進(jìn)[J].華中科技大學(xué)學(xué)報(bào)，2013，41（7）：97-102.

[6]肖茵茵，蘇開樂，岳偉亞，等.SET證書申請(qǐng)協(xié)議在SPV下的自動(dòng)化驗(yàn)證及改進(jìn)[J].計(jì)算機(jī)學(xué)報(bào)，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é)報(bào)，2004，30（3）：102-105.

[9]彭勛，董榮勝，郭云川，等.在Netbill交易協(xié)議中引入對(duì)商家的時(shí)限責(zé)任的追究[J].計(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.