數(shù)據(jù)起源請求協(xié)議的安全性分析與驗證

張 森， 王鳳英

(山東理工大學 計算機科學與技術(shù)學院， 山東 淄博255091)

隨著信息技術(shù)的發(fā)展，數(shù)據(jù)的傳播與交流日益頻繁.人們越來越多地遇到這樣的問題：這些數(shù)據(jù)是怎么來的，它們從哪里來.這些問題對于數(shù)據(jù)的可靠性和數(shù)據(jù)的質(zhì)量有著重要的意義.而Web的興起使這個問題更加突出，Web極大地改變了數(shù)據(jù)流動的方式[1]：首先，數(shù)據(jù)流動的速度加快了；其次，數(shù)據(jù)的質(zhì)量難以控制；另外Web上的數(shù)據(jù)本身是在不斷演化的，這給數(shù)據(jù)的驗證帶來了很多不便.數(shù)據(jù)起源給我們解決了這個問題，數(shù)據(jù)起源記錄數(shù)據(jù)的來源，有助于人們在日后方便地審計數(shù)據(jù)的使用情況，使我們可以通過對起源的查詢、分析，了解源數(shù)據(jù)的發(fā)展過程，對保護數(shù)據(jù)的完整性、保密性、不可否認性以及有效性有著重要意義.數(shù)據(jù)起源廣泛用于檔案、藝術(shù)、考古學、醫(yī)學、天文學、物理學等領(lǐng)域[2],在科學計算及科學流程中扮演著越來越重要的角色.文獻[3]提出了基于起源的安全審計模型，各實體之間的通信按照不同的協(xié)議進行.文獻[4]中采用UMLSec的順序圖對協(xié)議進行了安全性的分析，UMLSec模型[4]是對UML的擴展，類似于非形式化的標記，標記需要細心解釋，繁瑣復(fù)雜.它是半形式化的，其語法結(jié)構(gòu)雖然采用形式化的規(guī)約，但其語義部分是由自然語言描述，缺乏準確的語義，邏輯性不強，不易發(fā)現(xiàn)系統(tǒng)描述不一致等方面的問題.本文采用BAN邏輯方法形式化地驗證，更加簡單、方便、高效.

1 數(shù)據(jù)起源

1.1 數(shù)據(jù)起源概述

越來越多的情況表明，掌握和理解數(shù)據(jù)的產(chǎn)生、轉(zhuǎn)換、更新過程的信息不僅是有意義的，而且是必需的，例如醫(yī)院的電子病歷記錄著病人病情的診斷過程，病歷上信息的變化對病人以后的復(fù)診有很大影響.另外如果發(fā)生醫(yī)療糾紛，人們可以通過審計病歷信息進行相應(yīng)的責任認定.這些關(guān)于數(shù)據(jù)來源產(chǎn)生過程的信息就是數(shù)據(jù)起源.數(shù)據(jù)起源研究數(shù)據(jù)的來源以及從來源到目前狀態(tài)的過程中所發(fā)生的一切變化，包括任何人對其采取的任何操作.數(shù)據(jù)起源應(yīng)記錄哪些內(nèi)容，文獻[5]中介紹了7W模型，即數(shù)據(jù)起源信息應(yīng)包括who、when、 where、what、which、why、how這7部分.其核心是what，即記錄該數(shù)據(jù)生命周期內(nèi)各種事件來描述該數(shù)據(jù)發(fā)生了什么以及該數(shù)據(jù)現(xiàn)在是什么;其他六項都是圍繞what描述它的信息，描述該數(shù)據(jù)的歸屬權(quán)、什么時候在哪兒怎么發(fā)生了什么處理過程，處理過程是怎樣進行的，這個過程都有哪些要素、哪些主體參與，導(dǎo)致數(shù)據(jù)成為現(xiàn)在的狀態(tài)的原因.文獻[6]中將數(shù)據(jù)起源定義為：給定數(shù)據(jù)集D={d1，d2，…，dn}和操作op，d′=op(D)表示對D進行op操作的結(jié)果，d′的起源prov(d′)是一個三元組.根據(jù)此定義，數(shù)據(jù)起源包括三方面的信息：源數(shù)據(jù)D、源數(shù)據(jù)的起源prov(D)和本次操作op.

1.2 數(shù)據(jù)起源安全

前面介紹了數(shù)據(jù)起源的基本概念，我們可以利用數(shù)據(jù)起源了解源數(shù)據(jù)經(jīng)歷了哪些操作變成現(xiàn)在的狀態(tài)，或者說我們看到的數(shù)據(jù)有哪些人對它做了哪些操作.通過對數(shù)據(jù)的審計，我們就可以判斷數(shù)據(jù)的使用情況.然而，數(shù)據(jù)起源可能會受到如下方面的安全威脅[7]：起源在傳輸過程中部分或完全丟失；惡意用戶會截獲起源信息；惡意用戶會掩蓋或者篡改數(shù)據(jù)起源；惡意用戶拒絕承認他曾發(fā)送或接受過某信息.數(shù)據(jù)起源信息與數(shù)據(jù)哪個更重要？文獻[8]中職業(yè)業(yè)績評價的例子告訴我們，數(shù)據(jù)起源信息比數(shù)據(jù)更敏感，要求更高的安全性.第2節(jié)介紹的可審計起源系統(tǒng)在數(shù)據(jù)起源的記錄、存儲、查詢和分析等各個階段提供安全保證.

2 可審計起源系統(tǒng)

文獻[3]介紹的可審計起源系統(tǒng)的信息流包括4個階段：記錄階段、存儲階段、查詢階段和分析階段.用戶要訪問數(shù)據(jù)，要額外記錄一些附加的信息，這些信息用來描述他們的執(zhí)行過程，稱之為過程文檔.這些過程文檔有一系列的聲明組成，這些聲明由系統(tǒng)產(chǎn)生，包括操作的所有步驟和參與的數(shù)據(jù).最后要存儲在起源倉庫中，通過查詢這些過程文檔可以獲取數(shù)據(jù)的起源信息.最后通過對起源信息的分析，從而驗證數(shù)據(jù)是否被非法使用.

2.1 基于起源的審計結(jié)構(gòu)

審計結(jié)構(gòu)包括數(shù)據(jù)控制者(DC)、數(shù)據(jù)對象(DS)、數(shù)據(jù)處理者(DP)、審計員(Auditor)和起源倉庫(PS).數(shù)據(jù)控制者可以由個人或者組織充當，他確定私人信息的處理目標和方式.數(shù)據(jù)對象的信息由數(shù)據(jù)控制者控制，他可以是個人也可以是組織.起源倉庫存放數(shù)據(jù)起源信息.數(shù)據(jù)處理者代表數(shù)據(jù)控制者處理信息.審計員通過查詢起源來評估數(shù)據(jù)對象信息的使用情況.審計員可以由個人和組織充當.

上面所介紹的每個實體之間的通訊依賴于三個協(xié)議：數(shù)據(jù)請求協(xié)議、任務(wù)請求協(xié)議和查詢請求協(xié)議.數(shù)據(jù)請求協(xié)議作用于數(shù)據(jù)控制者和數(shù)據(jù)對象之間，任務(wù)請求協(xié)議作用于數(shù)據(jù)控制者和數(shù)據(jù)處理者之間，查詢請求協(xié)議作用于審計員和起源倉庫之間.基于起源的審計結(jié)構(gòu)[3]如圖1所示.

圖1 基于起源的審計結(jié)構(gòu)

2.2 數(shù)據(jù)請求協(xié)議

數(shù)據(jù)請求協(xié)議[3]是數(shù)據(jù)控制者向數(shù)據(jù)對象發(fā)出數(shù)據(jù)請求，數(shù)據(jù)對象響應(yīng)并返回數(shù)據(jù).其過程如下：DC向DS由于特定的目的請求個人信息，這個目的限定了數(shù)據(jù)使用的方式，DS先對DC進行認證，認證成功后，DS將數(shù)據(jù)返回給DC.DC收到數(shù)據(jù)后，DC確認他的接收.同時，DS和DC將整個過程記錄在起源倉庫中.

DS、DC和PS之間共交換交換六條消息：

M1′: DC→PS: {signk-1DC(hash(id1‖purpose))}；

聲明A1由發(fā)送者DC產(chǎn)生，先將A1的哈希值發(fā)送給DS，在將A1發(fā)送至起源存儲器.

M2: DS→DC: {k′(data‖idA2‖hash(A2)),signk-1DS(hash(M2))}，

M2′: DS→PS: {idA2‖data‖rel‖idA1,hash(data‖rel‖hash(M2)),signk-1DS(A2))}；

聲明A2由發(fā)送者DS產(chǎn)生，先將A2的哈希值發(fā)送給DC，再將A2發(fā)送至起源存儲器.

M3: DC→DS: {k′(idA2‖ok‖hash(A2)),signk-1DC′(hash(M3))}，

M3′: DC→PS: {idA3‖ok‖rel‖idA2,hash(data‖rel‖hash(M3)),signk-1DC(A3)}.

其中，idM1表示消息的標識，idA2表示聲明標識，k′表示對稱密鑰，用來加密消息.purpose表示數(shù)據(jù)的使用目的，data表示DS返回的請求數(shù)據(jù)，ok表示確認數(shù)據(jù)的接收，hash()為哈希函數(shù)，表示一個哈希值，signk-1DC表示使用DC的私鑰簽名，signk-1DS表示DS使用其私鑰進行簽名，‖表示數(shù)據(jù)的級聯(lián)，rel表示消息之間的關(guān)系，聲明A2中的rel表示A2是由于請求而產(chǎn)生,A3中的rel表示A3因回復(fù)確認產(chǎn)生.

3 數(shù)據(jù)請求協(xié)議的安全性分析

前面介紹了基于起源的審計結(jié)構(gòu)要滿足的基本安全屬性為：機密性、完整性、認證性和不可否認性，文獻[3]中利用UMLSec對數(shù)據(jù)請求協(xié)議的安全性進行了分析，構(gòu)造了一個安全起源圖并設(shè)計了一個算法檢查起源圖的完整性，證明協(xié)議滿足對完整性的要求.本節(jié)從機密性、認證性這兩個方面進行分析.

3.1 機密性分析

本文2.2節(jié)中給出的消息交換過程中，消息M1、M2、M3使用的加密密鑰為對稱密鑰，該對稱密鑰由安全傳輸層(TLS)協(xié)議產(chǎn)生[3].安全傳輸層協(xié)議(TLS)用于在兩個通信應(yīng)用程序之間提供保密性和數(shù)據(jù)完整性.然而，TLS標準并沒有規(guī)定應(yīng)用程序如何在 TLS上增加安全性；它把如何啟動 TLS握手協(xié)議以及如何解釋交換的認證證書的決定權(quán)留給協(xié)議的設(shè)計者和實施者來判斷.因此，對于數(shù)據(jù)請求協(xié)議來說，它的機密性建立在安全傳輸層協(xié)議安全的基礎(chǔ)之上.另外，協(xié)議未能實現(xiàn)完美向前保密(PFS)，一旦當前對稱密鑰泄露，會對已經(jīng)傳輸?shù)男畔⒃斐赏{.多數(shù)情況下，尤其是在數(shù)據(jù)起源中，完美向前保密是非常重要的，因為數(shù)據(jù)起源信息對“歷史消息”很敏感.

在DC和DS將聲明A1、A2、A3發(fā)送到PS的過程中，傳輸?shù)南D、數(shù)據(jù)、和關(guān)系都是明文發(fā)送，沒有經(jīng)過加密處理.這就可能被攻擊者截獲導(dǎo)致泄密.攻擊者通過監(jiān)聽公共信道獲取此消息，如果明文傳送，攻擊者就能夠知道起源信息.因此將該消息進行加密處理，即使用對稱密鑰將聲明中的消息進行加密后發(fā)送給PS，可避免信息泄露.

3.2 認證性分析

TLS協(xié)議同樣為實體進行身份認證，文獻[9-10]對TLS協(xié)議的分析證明其身份認證是完整的，安全的.數(shù)據(jù)請求協(xié)議中的實體包括DS、DC和PS，按照協(xié)議的描述，實體之間的認證依靠數(shù)字簽名來保證.第一階段，DC發(fā)送請求給DS，首先計算請求數(shù)據(jù)的哈希值形成摘要，使用DC的私鑰簽名發(fā)送給DS，DS接收到請求消息后，使用DC的公鑰進行驗證.任何人都無法冒充系統(tǒng)中的實體簽名，各實體都保存其他實體的公鑰用來驗證簽名，其私鑰必須保密.DC和DS將聲明發(fā)送到PS時，PS也要驗證它們的簽名.但此審計結(jié)構(gòu)中，DS和DC向PS發(fā)送消息時，DS和DC并沒有驗證PS的身份，即該結(jié)構(gòu)只實現(xiàn)了單項身份認證.

4 協(xié)議的形式化驗證

4.1 BAN邏輯[11]

BAN邏輯方法是一種基于模態(tài)邏輯技術(shù)的安全協(xié)議分析方法，是最早出現(xiàn)的形式化分析方法，它是基于信仰的邏輯分析方法，通過對協(xié)議運行過程中消息發(fā)送與接收的認證，從最初的知識發(fā)展為協(xié)議運行所要達到的目的，即主體的最終信仰.基于知識和信仰的模態(tài)邏輯方法,由于其簡單、實用、抽象度高,可以揭示安全協(xié)議中的安全缺陷和冗余性,在安全協(xié)議驗證方面獲得了廣泛應(yīng)用.基于模態(tài)邏輯的協(xié)議驗證是一個演繹推理的過程，在此之前應(yīng)先定義邏輯推理規(guī)則和公理.

4.1.1 BAN邏輯語法

BAN邏輯處理的對象包括主體、密鑰和公式.一般來說，P、Q等表示主體變量，K表示密鑰變量，X表示公式變量.BAN邏輯包含聯(lián)接詞，用逗號表示；除此之外還定義了一下語法結(jié)構(gòu)：

P|≡X: P相信X，即主體P相信X是正確的.

P ?X: P看到X，即主體P收到了包含X的消息，能讀出并能重復(fù).

P|～X : P曾經(jīng)說過X，即曾發(fā)送過一條包含X的消息，并且在發(fā)送時是相信X的.

P| ?X: P對X有仲裁權(quán)，即P對命題X有權(quán)威性，其他主體都信服.

以網(wǎng)絡(luò)教學為輔助的課堂教學模式是指在課堂教學中部分教學內(nèi)容及其過程以網(wǎng)絡(luò)教學方式進行的教學模式。部分融入的網(wǎng)絡(luò)教學內(nèi)容包括網(wǎng)絡(luò)教學展示、網(wǎng)絡(luò)習題測評、網(wǎng)絡(luò)教學互動，等等。在網(wǎng)絡(luò)教學部分融入課堂教學過程中，網(wǎng)絡(luò)教學融入的比例不大，一般不超過30%，最多也不超過50%，非網(wǎng)絡(luò)教學的傳統(tǒng)課堂教學仍占課堂教學內(nèi)容及其過程的大部分。在網(wǎng)絡(luò)教學為輔助的課堂教學模式中，教師對教學過程的把控往往相對容易，因為這種模式的大部分時間仍然處于傳統(tǒng)課堂教學模式之中，教師可以按照過去的經(jīng)驗式、當面人對人管理方式管理教學課堂。

#(X): X是新鮮的.

K{X}:用密鑰K加密X得到的密文.

4.1.2 推理規(guī)則

BAN邏輯的推理規(guī)則如下：

(1)消息意義規(guī)則

(2)隨機數(shù)驗證規(guī)則

如果P相信X是新鮮的，且P相信Q曾經(jīng)發(fā)送過X，那么P相信Q相信X.

(3)信仰規(guī)則

(4)消息新鮮性規(guī)則

如果P相信X是新鮮的，那么P相信與X級聯(lián)的消息都是新鮮的.

(5)消息接收規(guī)則

(6)仲裁規(guī)則

如果P相信Q對X有仲裁權(quán)，并且P相信Q相信X，那么P也相信X.

4.2 協(xié)議的形式化分析

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

根據(jù)BAN邏輯對協(xié)議分析的一般方法，明文省略，不將其形式化.因此，數(shù)據(jù)請求協(xié)議形式化描述如下：

DS ?{k′{(idM1‖purpose‖hash(A1)},signk-1DC(hash(M1)}

DC?{k′{(data‖id2‖hash(A2)},signk-1DS(hash(M2)}

DS ?{k′{(idA2‖ok‖hash(A2)},signk-1DC’(hash(M3))}

4.2.2 協(xié)議初始化假設(shè)

(A5)DC|?purpose (A6)DC|?ok

(A7) DS|?data (A8)DS |≡#(data)

(A9)DC|≡#(purpose,ok)

4.2.3 協(xié)議目標形式化描述

要證明協(xié)議的認證性和保密性，安全目標為

(G1) DS|≡DC|～purpose DS相信DC發(fā)送過purpose.

(G2) DC|≡DS|～data DC相信DS發(fā)送過data.

(G3) DS|≡DC|～ok DS相信DC發(fā)送過ok.

(G4) DS|≡DC|≡purpose

(G5) DS|≡DC|≡ok DS相信DC相信purpose和ok的正確性.

(G6) DC|≡DS|≡data DC相信DS相信data的正確性.

(G7) DS|≡purpose (G8) DC|≡data

(G9) DS|≡ok

G7，G8，G9分別表示接收數(shù)據(jù)的實體相信他所接受的數(shù)據(jù)的正確性.

4.2.4 協(xié)議分析

由協(xié)議的形式化描述可知，

DS ?{k′{(idM1‖purpose‖hash(A1)},signk-1DC(hash(M1)},

DS ?{k′{(idM1‖ok‖hash(A1)},signk-1DC(hash(M3)}.

根據(jù)消息接受規(guī)則R9和初始化假設(shè)A4，可以得出：

DS?purpose,DS?ok

根據(jù)消息接收規(guī)則和初始化假設(shè)A2，得出：

DS?hash(M1),DS?hash(M2)

由消息意義規(guī)則R2，可得協(xié)議目標G1和G3.

同理，由于DC?{k′{(data‖id2‖hash(A2)},signk-1DS(hash(M2)}，根據(jù)消息接受規(guī)則可初始化假設(shè)A3和A1可推出DC?data和DC?hash(M3)，由消息意義規(guī)則推出協(xié)議目標G2.

由初始化假設(shè)A8和協(xié)議目標G2，根據(jù)隨機數(shù)驗證規(guī)則R2，可得DC|≡DS|≡data，即協(xié)議目標G5.

同理由初始化假設(shè)A9和協(xié)議目標G1和G3，根據(jù)隨機數(shù)驗證規(guī)則可得協(xié)議目標G4和G6.

由DS|?data，DC|≡DS|≡data，DC|≡DS|～data，DS |≡#(data)可以推出DC|≡DS|?data，根據(jù)仲裁規(guī)則可得 DC|≡data.

同理可得DS|≡purpose，DS|≡ok.

至此，4.2.3節(jié)的協(xié)議的所有安全目標都能夠?qū)崿F(xiàn)，就說明協(xié)議滿足對認證性和機密性的要求.

經(jīng)過以上分析過程可以看出，BAN邏輯簡單、易掌握，且邏輯性強，結(jié)構(gòu)清晰.與UMLSec模型相比我們可以很容易對協(xié)議進行形式化的分析，不必構(gòu)造復(fù)雜的模型.

5 結(jié)束語

數(shù)據(jù)起源概括地來說是指記錄數(shù)據(jù)的來源以及隨后數(shù)據(jù)轉(zhuǎn)化過程的所有處理步驟，反映了數(shù)據(jù)在某一狀態(tài)的靜態(tài)信息和數(shù)據(jù)在轉(zhuǎn)化過程中的動態(tài)特征.數(shù)據(jù)起源可以更方便地對數(shù)據(jù)進行審計追蹤，從而可以檢查數(shù)據(jù)是否被濫用.基于起源的審計系統(tǒng)就是為這一目的而設(shè)計，它應(yīng)滿足對機密性和認證性的要求.本文從這兩個方面對基于起源的的審計結(jié)構(gòu)中的數(shù)據(jù)請求協(xié)議進行了形式化的分析，利用BAN邏輯證明該協(xié)議滿足對機密性和認證性的要求.下一步工作將繼續(xù)對起源安全協(xié)議進行研究，保證數(shù)據(jù)起源的安全.

[1]劉喜平,萬常選. 數(shù)據(jù)起源研究綜述[J]. 科技廣場，2005(1): 47-52.

[2] 陳穎. 一種基于DNA雙螺旋結(jié)構(gòu)的數(shù)據(jù)起源模型[J]. 現(xiàn)代圖書情報技術(shù)，2008(10)：11-1.

[3] Perez A R, Moreau L. Securing provenance-based audits [M]//Provenance and Annotation of Data and Processes. Berlin Heidelberg: Springer, 2010: 148-164.

[4] 朱爾金斯J. UML安全系統(tǒng)開發(fā)[M]. 沈晴霓, 譯. 北京：清華大學出版社, 2009.

[5] 戴超凡,王濤,張鵬程. 數(shù)據(jù)起源技術(shù)發(fā)展研究綜述[J]. 計算機應(yīng)用研究, 2010, 27(9): 3215-3221.

[6] 劉喜平,萬常選. 帶起源的數(shù)據(jù):模型與存儲[C]//中國計算機學會數(shù)據(jù)庫專業(yè)委員會.第二十五屆中國數(shù)據(jù)庫學術(shù)會議論文集(一). 北京: 《計算機科學》雜志社, 2008：195-199.

[7] Jung I Y, Yeom H Y. Provenance security guarantee from origin up to now in the e-Science environment [J]. Journal of Systems Architecture, 2011, 57(4): 425-440.

[8] Braun U, Shinnar A, Seltzer M. Securing Provenance[C]// Provos N. Proceedings of the 3rd conference on Hot topics in security. Berkeley: USENIX Association, 2008: 1-5.

[9] 于代榮,楊揚,馬炳先,等. 基于身份的TLS協(xié)議及其BAN邏輯分析[J]. 計算機工程，2011,37(1): 142-144,148.

[10] 馬英杰,肖麗萍,何文才,等. 用BAN邏輯方法分析TLS協(xié)議[J]. 微處理機，2006(1): 20-23.

[11] 李建華. 網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗證[M]. 北京：機械工業(yè)出版社，2010.