满足隐私需求的服务组合信息流控制方法研究*

姜家鑫，黄志球，马薇薇

1.南京航空航天大学 计算机科学与技术学院，南京 210016 2.软件新技术与产业化协同创新中心，南京 210016

1 引言

面向服务的计算（service-oriented computing，SOC）是一种基于互联网的全新计算模式，它是以Web服务作为基本元素，在传统的面向对象技术和分布式技术基础上提出的一种新的软件开发、部署和集成的模式[1]。Web服务是一种自描述、自包含、与平台无关的自治计算单元，使用标准的Web技术与其他服务进行交互。随着Web服务技术的迅速发展，越来越多的Web服务发布到互联网中，但是单个服务可能很难满足用户多个功能请求，因此有必要将多个已存在的Web服务按照功能、逻辑关系组合起来，以满足用户的功能性需求，组合起来的新服务被称作组合服务，服务的组合过程称为服务组合[2]。

用户在享受组合服务带来便利的同时，也需要将一些个人隐私信息发送给服务中，来满足相应的功能性需求，而隐私信息一旦被收集，用户很难控制服务如何使用和暴露这些信息[3]。随着用户隐私信息被侵犯的案例不断增加，隐私保护问题越来越受到关注，特别是在服务组合的过程中，由于用户与成员服务之间缺少相关的协议约束，难以保证隐私信息是否按照用户的需求进行使用和暴露[4]。因此，如何在满足用户功能性需求的前提下，最大可能地减少用户的隐私信息暴露是实现安全Web服务组合的一个关键性问题[5]。

为了加强服务组合的安全性，有必要在系统的设计阶段对服务组合的隐私需求进行分析和验证。目前，服务组合隐私保护的研究工作主要聚焦于提供隐私保护的服务组合访问控制方法。然而，在组合服务中，原始隐私数据可能在成员服务之间发送和接收消息时发生改变。成员服务发送和接收的消息，可能是从原始的隐私数据中计算出来的，这种信息流也会造成隐私信息的泄漏。考虑如下例子，假设一个组合服务中有3个成员服务S1、S2、S3，其中S1向S2发送了数据D1，S2向S3发送了数据D2，数据D2是从S2接收到的数据D1中计算而来的，如果D1被认为是不允许被发送到服务S3中的隐私敏感数据，而D2包含D1中的部分信息，在传送到S3时，有可能造成D1中的数据泄漏。而现有的Web服务安全性模型不支持这种成员服务在交互过程中产生的间接隐私数据的泄漏。

本文的主要贡献有：

（1）提出一种基于信任度的Web服务组合隐私信息流控制模型。该模型利用信任度作为服务访问隐私权限的条件，在此基础上提出隐私数据项依赖模型，检测服务组合中产生的间接隐私数据项。

（2）提出一种带隐私语义的Petri网模型对服务组合的行为进行建模。提出隐私授权认证算法，根据该算法检测Petri网中存在的隐私策略违背的现象，从而验证服务组合是否满足用户的隐私需求。

本文组织结构如下：第2章从访问控制和信息流控制两方面对服务组合隐私保护的相关工作进行讨论；第3章提出一种基于信任度的服务组合信息流控制模型，对服务的隐私策略进行建模；第4章对服务组合的行为进行建模和验证，检测服务组合中是否存在隐私信息泄露问题；第5章通过实验证明本文方法的有效性；第6章总结全文，并对未来工作进行展望。

2 相关工作

本章从访问控制和信息流控制两方面对Web服务组合的安全性与隐私保护方法进行讨论。

Web服务组合访问控制方法主要包括自主访问控制（discretionary access control，DAC）和强制访问控制（mandatory access control，MAC）两方面。DAC策略允许系统中信息的拥有者按照自己的意愿指定系统中其他主体对信息的访问权。文献[6]提出着色Petri网（color Petri net，CPN）框架用于验证基于角色的访问控制策略的一致性；文献[7]将上述框架用于面向服务的业务流程权限管理；文献[8]使用CPN建模与分析职责约束分离的工作流。MAC策略由系统管理部门按照严格的规则制定一些访问规则，使系统中的每个主体和客体都被赋予了相应的安全属性，这些安全属性是不能改变的。现有的MAC策略大多是基于多级安全策略模型[9]。文献[10]提出基于任务的访问控制模型，并使用Petri网进行验证。

Web服务组合信息流控制方法是一个新的研究领域。文献[11]将服务的组合简化为若干个服务链，通过三阶段组合协议对服务组合进行信息流控制。文献[12]使用CPN描述服务组合的业务流程，使用结构化的干扰性来判断服务组合中的信息泄漏。文献[13]对存在信息泄漏但认为是安全的信息流节点进行降级处理，使其能在系统中正常运行。文献[14]给出信息流的干扰性与因果模型中有效性之间的关系，提出一种黑盒的信息流分析方法。

通过信息流干扰性来判断信息泄露的方法过于严格，因为服务组合在满足用户功能性需求的同时会收集或者暴露用户的隐私数据，如果隐私数据的泄漏在用户可接受的范围内，则认为满足用户的隐私需求，所以对隐私保护定量的信息流控制方法是有必要的。

3 基于信任度的服务组合信息流控制模型

3.1 服务信任度

在服务组合的过程中，成员服务一般来自于不同的组织，相互之间缺乏必要的信任关系。它们中存在一些诚实的服务，在收集用户的隐私服务后，不会暴露给未经授权的服务或组织，但是同时也存在一些恶意的服务，为了获取个人的利益，可能将用户的隐私数据暴露给第三方。因此，当用户在暴露隐私数据给服务之前，需要服务具有一定的信任度。用户根据服务的信任度，有选择性地暴露个人的隐私，服务的信任度越高，可获得的隐私数据就越多。

定义1（信任度）信任度是度量服务可信程度的指标。设S是一组有穷的服务集，对于任何一个服务s∈S，函数f(s)∈[0,1]用于获取服务s的信任度，其中0代表服务不可信，1代表十分可信，值越大说明可信程度越高。

服务的信任度由用户来评价，用户在使用服务后，根据服务对用户隐私数据的危害程度来进行判断。目前已经有一些网站存在用户对服务的信任度评价机制，比如seekda（http://seekda.com）和WebService-List（http://webservicelist.com）。

3.2 隐私数据项依赖模型

用户在隐私需求中定义了直接隐私数据，而在组合服务的运行中，会根据直接隐私数据产生一些间接的隐私数据[15]，为了描述这些间接的隐私数据，构造了隐私数据项依赖模型。

定义2（直接隐私数据项）用户为完成功能性需求提供给组合服务的涉及隐私信息的数据项。

定义3（间接隐私数据项）在服务组合过程中，通过直接隐私数据项的计算而产生的能够间接地暴露用户隐私信息的数据项。

定义4（隐私数据项依赖关系）一个隐私数据项依赖关系（privacy data item dependency relation，PDIDR）是一个三元组E=＜D,d,F＞。其中：

（1）D={d1,d2,…,dn}是隐私数据项的集合。

（2）d是间接隐私数据项。

（3）F={f1,f2,…,fn}是依赖因子的集合，其中fi(1≤i≤n)表示隐私数据项d对di的依赖程度。依赖因子fi的取值范围见表1，fi的值越大，说明数据项d对di的依赖程度越大。为了简化，可以将依赖关系写为

定义5（隐私数据项依赖图）一个隐私数据项依赖图（privacy data item dependency graph，PDIDG）是一个三元组PDIDG=＜V,E,F＞，其中V是隐私数据项的集合，包括直接隐私数据项和间接隐私数据项；E是边的集合，表示隐私数据项之间的依赖关系；F是边的权值，表示隐私数据项之间的依赖程度，取值范围如表1所示。在隐私数据项依赖图中，出度为0的节点为直接隐私数据项，出度不为0的节点为间接隐私数据项。

Table 1 Value of dependency factor表1依赖因子的取值

图1是一个隐私数据项依赖图的实例，其中节点d、h、i出度为0，是直接隐私数据项，而a、b、c、e、f、g是间接隐私数据项，且存在如下的依赖关系：

Fig.1 Privacy data item dependency graph图1 隐私数据项依赖图

设用户要求访问直接隐私数据项d1、d2的服务信任度分别不低于T1、T2，若存在一个服务需要访问间接隐私数据项d且存在依赖关系则该服务对d1访问的信任度不低于fT1且对d2访问的信任度不低于fT2。

直接隐私数据项由用户在隐私需求中指定，服务组合的隐私分析人员根据用户提供的直接隐私数据项，分析服务组合中数据输入输出的依赖关系及具体应用的语义分析，指定间接隐私数据项，构造隐私数据项依赖图。

3.3 服务组合隐私信息流控制模型

在服务组合中，每一个成员服务都包含一组操作，用于收集或者暴露用户的隐私数据，用户希望最大程度地控制隐私信息的泄漏。为了满足用户的需求，本文采用隐私策略来规约成员服务在执行收集和暴露操作时对一组隐私数据的访问权限。

定义6（隐私策略）设S是一个有穷的服务集合，代表组合服务中的所有服务；OP是一个有穷的操作集，代表服务组合中成员服务之间发送和接受消息的操作。D是一组有穷的直接隐私数据项集，表示根据用户隐私需求定义的一系列隐私数据项。I是一组有穷的间接隐私数据项集，表示在服务交互过程中新产生的一系列依赖于直接隐私数据项的间接隐私数据项。T是一组有穷的隐私权限类型集，本文中的隐私权限包括收集隐私数据权限和暴露隐私数据权限。一个隐私策略是一个四元组，plcy=＜s,op,ftp,pm＞。其中：

（1）s∈S是组合服务中的一个成员服务。

（2）op代表服务执行的某一个操作。

（3）ftp是一个转换函数，通过隐私数据项依赖图，将对间接隐私数据项访问的信任度转化为对直接隐私数据项访问的信任度。

（4）pm是一个策略矩阵，由T行D列组成，矩阵元素pm[i,j]∈[0,1](0≤i≤T,0≤j≤D)是一个信任度阈值，表示服务s在访问数据对象j的i类隐私权限时所需要的信任度阈值。其中，0表示可以将该权限授予给任何服务，1表示不授予。

定义7（隐私信息流控制模型）一个服务组合的隐私信息流控制模型（privacy information flow control model，PIFCM）定义为五元组PIFCM= ＜S,OP,PM,PLCY,Fpm＞，其中：

（1）S是一个有穷的服务集，代表服务组合中的所有服务。

（2）OP是一组有穷的操作。

（3）PM是一组有穷的策略矩阵集。

（4）PLCY⊆S×OP×PM是一组有穷的隐私策略集，对任意策略plcy∈PLCY，它规约服务s在执行op操作时的一组隐私权限。

（5）Fpm是(S,OP)→PM的映射函数，用于获取服务s的操作op所对应的策略矩阵pm，其中s∈S，op∈OP，pm∈PM。

4 服务组合隐私行为建模与验证

4.1 服务组合隐私行为建模

为了实现一个Web服务组合系统，需要选取一组具体的服务来完成指定的功能，虽然服务的组合能够满足用户的功能性需求，但可能不满足用户的非功能性需求，比如隐私的授权约束[16]。因此为了确保服务的安全性与正确性，需要在服务组合的设计阶段对其进行隐私需求的建模与验证。

BPEL（business process execution language）已经成为事实上的Web服务组合标准语言，本文针对BPEL中可能存在的隐私泄漏问题进行隐私建模与验证。因为Petri网有严格的数学定义和直观的图形表示，又有丰富的系统描述能力和系统行为分析能力，所以国内外很多研究者通过将BPEL转化为Petri网来验证服务组合中的各种性质。

BPEL2oWFN是一个开源的BPEL分析工具，可以将BPEL转换到标准的Petri网，通过模型检测工具分析死锁等Petri网属性或者系统完备性以及时序逻辑；也可以转化为开放工作流网（open workflow net，OWFN），使用Fiona工具分析OWFN的可控性，从而分析BPEL的交互过程。图2是对“BPEL2oWFN（http://www.gnu.org/software/bpel2owfn/index.html）”工具链的一个概述。

Fig.2 BPEL2oWFN tool chain图2BPEL2oWFN工具链

OWFN是一种特殊的Petri网，在原有的Petri网的基础上引入了与外界交互的消息库所，因此便于研究者分析系统与外界交互的行为。文献[17]详细给出了将BPEL转化为OWFN的方法，将BPEL中的活动转换为OWFN中的变迁，将内部控制逻辑转化为内部消息库所，将与外部的交互过程转化为外部消息库所。

图3是一个简单的OWFN的实例。其中，虚线的矩形边框代表一个服务的边界，p1是起始库所，p3是终止库所，p4、p5库所代表服务与外界的交互过程，p4表示输入消息库所，p5表示输出消息库所。

Fig.3 An example of OWFN图3 一个OWFN的例子

为了能够分析BPEL中隐私数据的使用情况，本文提出一种支持隐私数据检测的隐私开放工作流网（privacy open workflow net，POWFN）。

定义8（隐私开放工作流网）一个隐私开放工作流网定义为五元组POWFN=＜P,T,F,M0,RMd＞，其中：

（1）P是库所的集合。P=Pi∪Po∪P′并且Pi∩Po∩P′=∅，其中Pi是输入消息库所的集合，Po是输出消息库所的集合，P′是服务内部消息库所的集合。

（2）T是变迁的集合。T=Ti∪To并且Ti∩To=∅，其中Ti是内部变迁的集合，其前置库所和后置库所都属于P′；To是外部变迁的集合，其前置库所和后置库所至少有一个不属于P′。

（3）F是有向边的集合，代表流关系，F=(P×T)∪(T×P)。

（4）M0是初始标识。

（5）RMd=＜ftr,RM＞是一个二元组，代表对直接隐私数据项隐私权限请求矩阵的集合。其中ftr是一个转换函数，通过隐私数据项依赖图，将对间接隐私数据项访问的请求转化为对直接隐私数据项访问的请求；RM是服务的隐私权限请求矩阵，其中既包括对用户直接隐私数据项的请求，又包括对服务组合过程中产生的间接隐私数据项的请求。每一个外部变迁To对应于一个RMd，对于每一个请求矩阵rmd∈RMd由T行D列组成，其中T代表一组有穷的隐私权限类型，D代表一组有穷的隐私数据对象，矩阵元素rmd[i,j]∈{0,1}(0≤i≤T,0≤j≤D)，1表示服务请求数据对象j类型为i的权限，0表示不请求这种权限。

4.2 服务组合隐私授权验证算法

要检验一个Web服务组合是否满足用户的隐私需求，实际上检验各成员服务的信任度水平是否满足用户所提供的直接隐私数据项的最小信任度要求。用户提供的信任度通过服务组合信息流控制模型规约为成员服务的隐私策略矩阵，成员服务的交互行为通过POWFN规约为隐私权限请求矩阵。

算法服务组合隐私需求验证算法

输入：隐私信息流控制模型PIFCM=＜S,OP,PM,PLCY,Fpm＞；隐私开放工作流网POWFN=＜P,T,F,M0,RMd＞。

输出：ture（满足隐私需求）或者false（不满足隐私需求）。

1.根据PIFCM和POWFN提取出每个服务s的隐私策略矩阵pm和隐私权限请求矩阵rmd（pm与rmd等行等列）；

2.创建一个初始值为0且与rmd等行等列的授权矩阵dm;

服务组合隐私需求算法中，首先获取每个服务的隐私策略矩阵pm和隐私权限请求矩阵rm，并构建一个初始化为0的授权矩阵dm，用于判断是否接受服务的授权请求；其次，对策略矩阵中的每个元素与该服务的信任度进行比较，如果服务的信任度大于等于策略矩阵的信任度，则将授权矩阵的对应项设置为1，若不满足则置为0；然后，查看该服务是否请求了对应的隐私数据项，如果服务既不满足隐私数据的信任度需求，又请求了该隐私数据，则将该项置为-1；最后查看服务的授权矩阵中是否存在值为-1的元素，若存在，则返回false，不存在则返回true。

5 案例分析

一个购物代理（Shopping Agent，SA）服务组合中包括代理服务（Agent）、售货服务（Seller）、支付服务（Pay）、快递服务（Shipper），这4个服务组合在一起完成用户购买物品、支付、货物运输的一站式服务。图4给出了用户通过服务组合成功完成在线购物的场景。

Fig.4 Scenario of successful reservation in SA service composition图4 SA服务组合完成用户订单请求的场景

用户首先登录到Agent服务中，当需要购物时送订单请求消息（OrdReq）到Seller服务；Seller服务在接收到OrdReq后，向Pay服务发送货物支付请求消息(PayReq）；如果用户银行卡的可用额度能够支付订单，则Pay服务返回支付成功消息（PayOK）到Seller服务中；若支付成功，则Seller服务向Shipper服务发送货物配送请求（ShipReq）；若运送货物成功则返回配送成功消息（ShipOK）到Seller服务中；随后Seller服务返回OrderOK消息到Agent服务中，完成用户购物流程。

在线购物服务组合的隐私分析人员根据所有用户提供的直接隐私数据项以及服务组合的业务流程构造隐私数据项依赖图，如图5所示。

Fig.5 PDIDG of service composition图5 服务组合的隐私数据项依赖图

某一特定用户的隐私需求是服务组合中所有用户隐私需求的子集，因此其隐私数据项依赖图也应该是整个服务组合的隐私数据项依赖图的子集。例如，某一用户给出隐私需求的直接隐私数据项包括用户姓名（name）、手机号（phone）、信用卡号（credit-Card）、地址（address），所对应的隐私数据项依赖图如图6所示。

Fig.6 PDIDG of a single user图6 针对某一用户的隐私数据项依赖图

在线购物服务组合中的成员服务在完成用户购买商品、支付、货物运输过程中，有如下的消息传递涉及用户的隐私信息泄漏。

（1）订单请求（OrdReq）：Agent服务通过收集用户的姓名（name）、手机号（phone）、银行卡（credit-Card）、地址（address）等直接隐私数据项进行处理，产生间接隐私数据项OrderId，发送给Seller服务，Seller服务只有对OrderId依赖的所有直接隐私数据项都具有收集权限，才能接收OrdReq请求。

（2）支付请求（PayReq）：Seller服务通过收集用户的直接隐私数据项，产生间接隐私数据项PayID，并试图发送给Pay服务，服务Pay只有对PayID依赖的所有直接隐私数据项都具有收集权限，才能接收PayID。

（3）货物运输请求（ShipReq）：Seller服务通过收集用户的直接隐私数据项，产生间接隐私数据项ShipID，并试图发送给Shipper服务，服务Shipper只有对ShipID依赖的所有直接隐私数据项有收集权限，才能接收ShipReq。

利用隐私开放工作流网对服务组合的行为进行建模，本文关注于服务之间的交互过程，因此忽略服务内部的消息库所，只关注于服务之间的外部消息库所，所形成的隐私开放工作流网如图7所示。

Fig.7 POWFN of online shopping service composition图7 在线购物服务组合的隐私开放工作流网

在该案例中，假设用户对Agent、Seller、Pay、Shipper服务的信任度分别为0.8、0.8、0.7、0.7，而用户希望自己的隐私数据（直接隐私数据项）name、phone、credit-Card、address被信任度大于0.6、0.7、0.8、0.6的服务所访问。

表2～表5分别代表服务组合中各成员服务的操作和相应的策略矩阵。其中后缀“？”表示服务是消息的接收者，后缀“！”表示服务是消息的发送者，矩阵的行向量分别代表收集和暴露操作，矩阵的列向量分别代表用户的直接隐私数据项name、phone、creditCard、address。Agent服务发送了OrderReq消息到Seller服务中，并接收来自Seller服务的OrderOK消息；Seller服务向Agent服务发送了OrderOK消息并接收OrderReq消息，向Pay服务发送PayReq消息并接收PayOK消息，向Shipper服务发送ShipReq消息并接收ShipOK消息；Pay服务接收了来自Seller服务的PayReq消息，并向Seller服务发送了PayOK消息；Shipper服务接收来自Seller服务的ShipReq消息，并发送ShipOK消息到Seller服务。发送的数据为间接隐私数据，根据隐私数据项依赖图中的关系，可以计算出相应的信任度。

Table 2 Operations and policy matrixes ofAgent表2 Agent服务的操作和策略矩阵

Table 3 Operations and policy matrixes of Seller表3 Seller服务的操作和策略矩阵

Table 4 Operations and policy matrixes of Pay表4 Pay服务的操作和策略矩阵

Table 5 Operations and policy matrixes of Shipper表5 Shipper服务的操作和策略矩阵

表6～表9代表服务组合中各成员服务运行过程中的操作和相应的请求矩阵。矩阵中1代表成员服务需要收集（或暴露）隐私数据，0代表不收集（或暴露）数据。

Table 6 Operations and request matrixes ofAgent表6 Agent服务的操作和请求矩阵

Table 7 Operations and request matrixes of Seller表7 Seller服务的操作和请求矩阵

Table 8 Operations and request matrixes of Pay表8 Pay服务的操作和请求矩阵

Table 9 Operations and request matrixes of Shipper表9 Shipper服务的操作和请求矩阵

基于以上表格，对SA服务组合进行隐私权限的验证。通过4.2节给出的隐私需求验证算法，可以得到Pay服务的授权矩阵，见表10。

从表10可知，服务Pay的操作PayReq通过间接隐私数据项PayID请求了隐私数据creditCard，然而Pay的信任度为0.7，小于creditCard所要求的信任度0.8，因此该服务不满足隐私策略约束。

Table 10 Operations and delegation matrixes of Pay表10 Pay服务的操作和授权矩阵

6 总结与展望

本文针对服务组合中的隐私保护问题，使用隐私策略矩阵规约服务的隐私权限，并使用隐私数据项依赖图规约间接隐私数据项与直接隐私数据项的依赖关系，提出了服务组合的信息流控制模型；同时采用隐私开放工作流网对服务组合的行为建模，给出了服务组合隐私需求验证算法，验证服务的信任度是否满足用户提出隐私数据的信任度需求。

下一步的研究工作包括：提出一种服务组合隐私协商机制，当服务组合不满足用户隐私需求时，对用户隐私需求和服务组合的隐私策略进行协商。此外，本文主要是针对服务组合收集和暴露用户隐私数据两种行为进行验证，今后需要对现有的模型进行扩充，使其支持隐私数据时间属性的验证。

[1]Ameller D,Burgués X,Collell O,et al.Development of serviceoriented architectures using model-driven development:a mapping study[J].Information and Software Technology,2015,62(1):42-66.

[2]Papazoglou M P,Pohl K,Parkin M,et al.Service research challenges and solutions for the future internet[M].Berlin,Heidelberg:Springer,2010.

[3]Liu Linyuan.Research on privacy analysis and verification of Web service composition[D].Nanjing:Nanjing University ofAeronautics andAstronautics,2011.

[4]Meziane H,Benbernou S.A dynamic privacy model for Web services[J].Computer Standards&Interfaces,2010,32(5/6):288-304.

[5]Barth A,Rubinstein B I P,Sundararajan M,et al.A learningbased approach to reactive security[J].IEEE Transactions on Dependable and Secure Computing,2012,9(4):482-493.

[6]Shafiq B,Masood A,Joshi J,et al.A role-based access control policy verification framework for real-time systems[C]//Proceedings of the 10th International Workshop on Object-Oriented Real-Time Dependable Systems,Sedona,Feb 2-4,2005.Washington:IEEE Computer Society,2005:13-20.

[7]Sun Haiyang,Wang Xin,Yang Jian,et al.Authorization policy based business collaboration reliability verification[C]//LNCS 5364:Proceedings of the 6th International Conference on Service-Oriented Computing,Sydney,Dec 1-5,2008.Berlin,Heidelberg:Springer,2008:579-584.

[8]Lu Yahui,Zhang Li,Sun Jiaguang.Using colored Petri nets to model and analyze workflow with separation of duty constraints[J].The International Journal of Advanced Manufacturing Technology,2009,40(1/2):179-192.

[9]Bell D E,La Padula L J.Secure computer system:unified exposition and multics interpretation[R].Bedford:The MITRE Corporation,1976.

[10]Röhrig S,Knorr K.Security analysis of electronic business processes[J].Electronic Commerce Research,2004,4(1/2):59-81.

[11]She Wei,Yen I L,Thuraisingham B,et al.Security-aware service composition with fine-grained information flow control[J].IEEE Transactions on Services Computing,2013,6(3):330-343.

[12]Accorsi R,Wonnemann C,Dochow S.SWAT:a security workflow analysis toolkit for reliably secure process-aware information systems[C]//Proceedings of the 6th International Conference on Availability,Reliability and Security,Vienna,Aug 22-26,2011.Washington:IEEE Computer Society,2011:692-697.

[13]Accorsi R,Lehmann A,Lohmann N.Information leak detection in business process models:theory,application,and tool support[J].Information Systems,2015,47:244-257.

[14]Tschantz M C,Datta A,Datta A,et al.A methodology for information flow experiments[C]//Proceedings of the 28th Computer Security Foundations Symposium,Verona,Jul 13-17,2015.Washington:IEEE Computer Society,2015:554-568.

[15]Peng Huanfeng,Huang Zhiqiu,Fan Dajuan,et al.Specification and verification of user privacy requirements for service composition[J].Journal of Software,2016,27(8):1948-1963.

[16]Lu Jiajun,Huang Zhiqiu,Ke Changbo.Verification of behavior-aware privacy requirements in Web services composition[J].Journal of Software,2014,9(4):944-951.

[17]Lohmann N,Massuthe P,Stahl C,et al.Analyzing interacting WS-BPEL processes using flexible model generation[J].Data&Knowledge Engineering,2008,64(1):38-54.

附中文参考文献：

[3]刘林源.Web服务组合隐私分析与验证研究[D].南京:南京航空航天大学，2011.

[15]彭焕峰,黄志球,范大娟,等.面向服务组合的用户隐私需求规约与验证方法[J].软件学报,2016,27(8):1948-1963.