数据起源请求协议的安全性分析与验证

张 森， 王凤英

(山东理工大学 计算机科学与技术学院， 山东 淄博255091)

随着信息技术的发展，数据的传播与交流日益频繁.人们越来越多地遇到这样的问题：这些数据是怎么来的，它们从哪里来.这些问题对于数据的可靠性和数据的质量有着重要的意义.而Web的兴起使这个问题更加突出，Web极大地改变了数据流动的方式[1]：首先，数据流动的速度加快了；其次，数据的质量难以控制；另外Web上的数据本身是在不断演化的，这给数据的验证带来了很多不便.数据起源给我们解决了这个问题，数据起源记录数据的来源，有助于人们在日后方便地审计数据的使用情况，使我们可以通过对起源的查询、分析，了解源数据的发展过程，对保护数据的完整性、保密性、不可否认性以及有效性有着重要意义.数据起源广泛用于档案、艺术、考古学、医学、天文学、物理学等领域[2],在科学计算及科学流程中扮演着越来越重要的角色.文献[3]提出了基于起源的安全审计模型，各实体之间的通信按照不同的协议进行.文献[4]中采用UMLSec的顺序图对协议进行了安全性的分析，UMLSec模型[4]是对UML的扩展，类似于非形式化的标记，标记需要细心解释，繁琐复杂.它是半形式化的，其语法结构虽然采用形式化的规约，但其语义部分是由自然语言描述，缺乏准确的语义，逻辑性不强，不易发现系统描述不一致等方面的问题.本文采用BAN逻辑方法形式化地验证，更加简单、方便、高效.

1 数据起源

1.1 数据起源概述

越来越多的情况表明，掌握和理解数据的产生、转换、更新过程的信息不仅是有意义的，而且是必需的，例如医院的电子病历记录着病人病情的诊断过程，病历上信息的变化对病人以后的复诊有很大影响.另外如果发生医疗纠纷，人们可以通过审计病历信息进行相应的责任认定.这些关于数据来源产生过程的信息就是数据起源.数据起源研究数据的来源以及从来源到目前状态的过程中所发生的一切变化，包括任何人对其采取的任何操作.数据起源应记录哪些内容，文献[5]中介绍了7W模型，即数据起源信息应包括who、when、 where、what、which、why、how这7部分.其核心是what，即记录该数据生命周期内各种事件来描述该数据发生了什么以及该数据现在是什么;其他六项都是围绕what描述它的信息，描述该数据的归属权、什么时候在哪儿怎么发生了什么处理过程，处理过程是怎样进行的，这个过程都有哪些要素、哪些主体参与，导致数据成为现在的状态的原因.文献[6]中将数据起源定义为：给定数据集D={d1，d2，…，dn}和操作op，d′=op(D)表示对D进行op操作的结果，d′的起源prov(d′)是一个三元组.根据此定义，数据起源包括三方面的信息：源数据D、源数据的起源prov(D)和本次操作op.

1.2 数据起源安全

前面介绍了数据起源的基本概念，我们可以利用数据起源了解源数据经历了哪些操作变成现在的状态，或者说我们看到的数据有哪些人对它做了哪些操作.通过对数据的审计，我们就可以判断数据的使用情况.然而，数据起源可能会受到如下方面的安全威胁[7]：起源在传输过程中部分或完全丢失；恶意用户会截获起源信息；恶意用户会掩盖或者篡改数据起源；恶意用户拒绝承认他曾发送或接受过某信息.数据起源信息与数据哪个更重要？文献[8]中职业业绩评价的例子告诉我们，数据起源信息比数据更敏感，要求更高的安全性.第2节介绍的可审计起源系统在数据起源的记录、存储、查询和分析等各个阶段提供安全保证.

2 可审计起源系统

文献[3]介绍的可审计起源系统的信息流包括4个阶段：记录阶段、存储阶段、查询阶段和分析阶段.用户要访问数据，要额外记录一些附加的信息，这些信息用来描述他们的执行过程，称之为过程文档.这些过程文档有一系列的声明组成，这些声明由系统产生，包括操作的所有步骤和参与的数据.最后要存储在起源仓库中，通过查询这些过程文档可以获取数据的起源信息.最后通过对起源信息的分析，从而验证数据是否被非法使用.

2.1 基于起源的审计结构

审计结构包括数据控制者(DC)、数据对象(DS)、数据处理者(DP)、审计员(Auditor)和起源仓库(PS).数据控制者可以由个人或者组织充当，他确定私人信息的处理目标和方式.数据对象的信息由数据控制者控制，他可以是个人也可以是组织.起源仓库存放数据起源信息.数据处理者代表数据控制者处理信息.审计员通过查询起源来评估数据对象信息的使用情况.审计员可以由个人和组织充当.

上面所介绍的每个实体之间的通讯依赖于三个协议：数据请求协议、任务请求协议和查询请求协议.数据请求协议作用于数据控制者和数据对象之间，任务请求协议作用于数据控制者和数据处理者之间，查询请求协议作用于审计员和起源仓库之间.基于起源的审计结构[3]如图1所示.

图1 基于起源的审计结构

2.2 数据请求协议

数据请求协议[3]是数据控制者向数据对象发出数据请求，数据对象响应并返回数据.其过程如下：DC向DS由于特定的目的请求个人信息，这个目的限定了数据使用的方式，DS先对DC进行认证，认证成功后，DS将数据返回给DC.DC收到数据后，DC确认他的接收.同时，DS和DC将整个过程记录在起源仓库中.

DS、DC和PS之间共交换交换六条消息：

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

声明A1由发送者DC产生，先将A1的哈希值发送给DS，在将A1发送至起源存储器.

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由发送者DS产生，先将A2的哈希值发送给DC，再将A2发送至起源存储器.

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表示数据的使用目的，data表示DS返回的请求数据，ok表示确认数据的接收，hash()为哈希函数，表示一个哈希值，signk-1DC表示使用DC的私钥签名，signk-1DS表示DS使用其私钥进行签名，‖表示数据的级联，rel表示消息之间的关系，声明A2中的rel表示A2是由于请求而产生,A3中的rel表示A3因回复确认产生.

3 数据请求协议的安全性分析

前面介绍了基于起源的审计结构要满足的基本安全属性为：机密性、完整性、认证性和不可否认性，文献[3]中利用UMLSec对数据请求协议的安全性进行了分析，构造了一个安全起源图并设计了一个算法检查起源图的完整性，证明协议满足对完整性的要求.本节从机密性、认证性这两个方面进行分析.

3.1 机密性分析

本文2.2节中给出的消息交换过程中，消息M1、M2、M3使用的加密密钥为对称密钥，该对称密钥由安全传输层(TLS)协议产生[3].安全传输层协议(TLS)用于在两个通信应用程序之间提供保密性和数据完整性.然而，TLS标准并没有规定应用程序如何在 TLS上增加安全性；它把如何启动 TLS握手协议以及如何解释交换的认证证书的决定权留给协议的设计者和实施者来判断.因此，对于数据请求协议来说，它的机密性建立在安全传输层协议安全的基础之上.另外，协议未能实现完美向前保密(PFS)，一旦当前对称密钥泄露，会对已经传输的信息造成威胁.多数情况下，尤其是在数据起源中，完美向前保密是非常重要的，因为数据起源信息对“历史消息”很敏感.

在DC和DS将声明A1、A2、A3发送到PS的过程中，传输的消息ID、数据、和关系都是明文发送，没有经过加密处理.这就可能被攻击者截获导致泄密.攻击者通过监听公共信道获取此消息，如果明文传送，攻击者就能够知道起源信息.因此将该消息进行加密处理，即使用对称密钥将声明中的消息进行加密后发送给PS，可避免信息泄露.

3.2 认证性分析

TLS协议同样为实体进行身份认证，文献[9-10]对TLS协议的分析证明其身份认证是完整的，安全的.数据请求协议中的实体包括DS、DC和PS，按照协议的描述，实体之间的认证依靠数字签名来保证.第一阶段，DC发送请求给DS，首先计算请求数据的哈希值形成摘要，使用DC的私钥签名发送给DS，DS接收到请求消息后，使用DC的公钥进行验证.任何人都无法冒充系统中的实体签名，各实体都保存其他实体的公钥用来验证签名，其私钥必须保密.DC和DS将声明发送到PS时，PS也要验证它们的签名.但此审计结构中，DS和DC向PS发送消息时，DS和DC并没有验证PS的身份，即该结构只实现了单项身份认证.

4 协议的形式化验证

4.1 BAN逻辑[11]

BAN逻辑方法是一种基于模态逻辑技术的安全协议分析方法，是最早出现的形式化分析方法，它是基于信仰的逻辑分析方法，通过对协议运行过程中消息发送与接收的认证，从最初的知识发展为协议运行所要达到的目的，即主体的最终信仰.基于知识和信仰的模态逻辑方法,由于其简单、实用、抽象度高,可以揭示安全协议中的安全缺陷和冗余性,在安全协议验证方面获得了广泛应用.基于模态逻辑的协议验证是一个演绎推理的过程，在此之前应先定义逻辑推理规则和公理.

4.1.1 BAN逻辑语法

BAN逻辑处理的对象包括主体、密钥和公式.一般来说，P、Q等表示主体变量，K表示密钥变量，X表示公式变量.BAN逻辑包含联接词，用逗号表示；除此之外还定义了一下语法结构：

P|≡X: P相信X，即主体P相信X是正确的.

P ◁X: P看到X，即主体P收到了包含X的消息，能读出并能重复.

P|～X : P曾经说过X，即曾发送过一条包含X的消息，并且在发送时是相信X的.

P| ⟹X: P对X有仲裁权，即P对命题X有权威性，其他主体都信服.

以网络教学为辅助的课堂教学模式是指在课堂教学中部分教学内容及其过程以网络教学方式进行的教学模式。部分融入的网络教学内容包括网络教学展示、网络习题测评、网络教学互动，等等。在网络教学部分融入课堂教学过程中，网络教学融入的比例不大，一般不超过30%，最多也不超过50%，非网络教学的传统课堂教学仍占课堂教学内容及其过程的大部分。在网络教学为辅助的课堂教学模式中，教师对教学过程的把控往往相对容易，因为这种模式的大部分时间仍然处于传统课堂教学模式之中，教师可以按照过去的经验式、当面人对人管理方式管理教学课堂。

#(X): X是新鲜的.

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

4.1.2 推理规则

BAN逻辑的推理规则如下：

(1)消息意义规则

(2)随机数验证规则

如果P相信X是新鲜的，且P相信Q曾经发送过X，那么P相信Q相信X.

(3)信仰规则

(4)消息新鲜性规则

如果P相信X是新鲜的，那么P相信与X级联的消息都是新鲜的.

(5)消息接收规则

(6)仲裁规则

如果P相信Q对X有仲裁权，并且P相信Q相信X，那么P也相信X.

4.2 协议的形式化分析

4.2.1 协议的形式化描述

根据BAN逻辑对协议分析的一般方法，明文省略，不将其形式化.因此，数据请求协议形式化描述如下：

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 协议初始化假设

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

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

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

4.2.3 协议目标形式化描述

要证明协议的认证性和保密性，安全目标为

(G1) DS|≡DC|～purpose DS相信DC发送过purpose.

(G2) DC|≡DS|～data DC相信DS发送过data.

(G3) DS|≡DC|～ok DS相信DC发送过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分别表示接收数据的实体相信他所接受的数据的正确性.

4.2.4 协议分析

由协议的形式化描述可知，

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

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

根据消息接受规则R9和初始化假设A4，可以得出：

DS◁purpose,DS◁ok

根据消息接收规则和初始化假设A2，得出：

DS◁hash(M1),DS◁hash(M2)

由消息意义规则R2，可得协议目标G1和G3.

同理，由于DC◁{k′{(data‖id2‖hash(A2)},signk-1DS(hash(M2)}，根据消息接受规则可初始化假设A3和A1可推出DC◁data和DC◁hash(M3)，由消息意义规则推出协议目标G2.

由初始化假设A8和协议目标G2，根据随机数验证规则R2，可得DC|≡DS|≡data，即协议目标G5.

同理由初始化假设A9和协议目标G1和G3，根据随机数验证规则可得协议目标G4和G6.

由DS|⟹data，DC|≡DS|≡data，DC|≡DS|～data，DS |≡#(data)可以推出DC|≡DS|⟹data，根据仲裁规则可得 DC|≡data.

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

至此，4.2.3节的协议的所有安全目标都能够实现，就说明协议满足对认证性和机密性的要求.

经过以上分析过程可以看出，BAN逻辑简单、易掌握，且逻辑性强，结构清晰.与UMLSec模型相比我们可以很容易对协议进行形式化的分析，不必构造复杂的模型.

5 结束语

数据起源概括地来说是指记录数据的来源以及随后数据转化过程的所有处理步骤，反映了数据在某一状态的静态信息和数据在转化过程中的动态特征.数据起源可以更方便地对数据进行审计追踪，从而可以检查数据是否被滥用.基于起源的审计系统就是为这一目的而设计，它应满足对机密性和认证性的要求.本文从这两个方面对基于起源的的审计结构中的数据请求协议进行了形式化的分析，利用BAN逻辑证明该协议满足对机密性和认证性的要求.下一步工作将继续对起源安全协议进行研究，保证数据起源的安全.

[1]刘喜平,万常选. 数据起源研究综述[J]. 科技广场，2005(1): 47-52.

[2] 陈颖. 一种基于DNA双螺旋结构的数据起源模型[J]. 现代图书情报技术，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安全系统开发[M]. 沈晴霓, 译. 北京：清华大学出版社, 2009.

[5] 戴超凡,王涛,张鹏程. 数据起源技术发展研究综述[J]. 计算机应用研究, 2010, 27(9): 3215-3221.

[6] 刘喜平,万常选. 带起源的数据:模型与存储[C]//中国计算机学会数据库专业委员会.第二十五届中国数据库学术会议论文集(一). 北京: 《计算机科学》杂志社, 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协议及其BAN逻辑分析[J]. 计算机工程，2011,37(1): 142-144,148.

[10] 马英杰,肖丽萍,何文才,等. 用BAN逻辑方法分析TLS协议[J]. 微处理机，2006(1): 20-23.

[11] 李建华. 网络安全协议的形式化分析与验证[M]. 北京：机械工业出版社，2010.