Formal Enforcement of Security Policies on Choreographed Services Mahjoub Langar and Karim Dahmani LIP2 Research Laboratory, Facult◆e des Sciences de Tunis, Tunisia Abstract. Web services are software systems that support distributed applications composed of independent processes which communicate by message passing. To realize the full potential of web services, we need to compose existent web services in order to get more functionalities. However the composition of web services should be secure. In this paper we propose an automatic formal approach to monitor the execution of a choreography of web services and we prove its correctness. We introduce the syntax and semantic rules of a new operator which takes as input a choreography and a security policy and produces as output a secure version of this choreography which behaves like the original one and does not violate the security policy. Keywords: Choreographed services, web service security, formal veri cation, runtime veri cation 1 Introduction With the explosive growth of the Internet, intranet and electronic commerce, the concept of web services has emerged in the world to be exploited by most cross-organizational boundaries. In fact, web services provide a suitable techni- cal foundation for making business processes accessible within and across en- terprises. Moreover web services are software systems that support distributed applications composed of independent processes which communicate by message passing. But for an appropriate exploitation of web services, we need to com- pose them. Indeed, individual web services often o↵er limited capabilities. In some situations, a client's request cannot be satis ed by a single web service. However, when composed with other web services, they can satisfy the client demand. To realize the full potential of web services, we need to compose exis- tent web services in order to get more functionalities. Web service composition rules deal with how di↵erent services are composed into a coherent global ser- vice. In particular, they specify the order in which services are invoked, and the conditions under which a certain service may or may not be invoked. Among the approaches investigated in service composition, we distinguish orchestra- tion and choreography. The orchestration composes available services and adds a central coordinator (the orchestrater) which is responsible for invoking and composing the single sub-activities. However the second one, referred to as web service choreography, does not assume the exploitation of a central coordinator but it de nes complex tasks via the de nition of the conversation that should be undertaken by each participant. While several proposals exist for orchestration languages (e.g. Business Process Execution Language (BPEL)[1], Web Services Flow Language (WSFL)[2]), choreography languages are still in a preliminary stage of de nition. A proposal, Web Service Choreography Description Language (WS-CDL)[3], was issued by the World Wide Web Consortium (W3C) in De- cember 2004. The need of secure web service composition has led to a great interest from researchers of the last decade. However most of the works focus on how to guar- antee desired properties such as correctness, deadlock avoidance, etc. In our work, in addition to these properties, we introduce an automatic approach to monitor a choreography by specifying and enforcing security policies on web ser- vices and we prove its correctness using formal methods. Some works such as [4,5] have enforced security policies on concurrent systems using process alge- bra. Formal methods are mathematical techniques that are well-suited to address the aforementioned issues. A variety of proposals to formally describe, compose and verify web service compositions using the formal methods exists. In [6], a Petri-net based design and veri cation framework for web service composition is proposed. In [7], the authors introduce a Petri-net based algebra to compose web services based on control ows. In [8], authors use Milner's process algebra CCS to specify and compose web services as processes, and the Concurrency Workbench to validate properties such as correct web service composition. In [9], the authors provide an encoding of BPEL processes into web service timed state transition systems, a formalism that is closely related to timed automata and discuss a framework in which timed assumptions can be model checked. In this paper, we propose an enforcement of security policies over web ser- vices using formal methods. We present an automated approach for monitoring the behavior of a service in a choreography. More precisely, we de ne an operator ⌦ that takes as input a process P and a security policy P and generates a new process P 0 = P ⌦ P which respects the following conditions : ✏ P 0 js P ; i.e. P 0 satis es the security policy P : ✏ P 0 v P; i.e. behaviors of P 0 are also behaviors of P: ✏ 8Q : ((Q js P ) and (Q v P )) =) Q v P 0 , i.e. all good behaviors of P are also behaviors of P 0 : P P ⌦ P0 = P ⌦ P The rest of the paper is structured as follows. In section 2, we brie y describe the global calculus. Section 3 presents the formalism used to specify security poli- cies. Section 4 illustrates the formalism used to specify choreographed services. In section 5, we present our security framework for monitoring a choreography. In section 6, we discuss some related works while conclusions are in section 7. 2 Global Calculus The global calculus [10] is distilled from WS-CDL. It describes the global ow of interactions between the participants. The syntax of the global calculus is given by the standard BNF. 2.1 Syntax of the Global Calculus I ::= A ! B : ch(⌫ s~):I (Init) j A ! B : shop; e; yi:I (Comm) j x@A := e:I (Assign) j if e@A then I1 else I2 (If T henElse) j I1 + I2 (Sum) j I1 jI2 (P ar) j (⌫s)I (N ew) j XA (recV ar) j rec X A :I (Rec) j0 (Inaction) The rst rule (Init) says that the participant A invokes a service ch located at B and initiates new freshly generated session channels s~: The second rule (Comm) expresses the sending action by A whose message consists of a selected operator op and an expression e to the participant B which will store the value of e at the variable y: (Assign) is a local construct which updates the variable x located at A with e: (P ar) and (Sum) are respectively the parallel composition and the non-deterministic choice of interactions. (If T henElse) is the standard conditional operation, while (recV ar) and (Rec) are used to express recursive behavior of interactions. 0 is the inactive interaction. 2.2 Semantics of the Global Calculus The formal semantics of the global calculus is de ned in terms of con gurations ( ; I): The notation ( ; I) ! ( 0 ; I 0 ) says that the global description I at a state (which is the collection of all local states of the participants) will reduce to I 0 at a new state 0 : Samples of reduction rules are presented here while the overall operational semantic is detailed in [10]. (Init) ( ; A ! B : ch(⌫ s~):I) ! ( ; (⌫ s~)I) ` e@A + v (Comm) ( ; A ! B : shop; e; xi:I) ! ( [x@B 7! v]; I) ` e@A + v ( ; I1 ) ! ( 0 ; I10 ) (Assign) (P ar) ( ; x@A := e:I) ! ( [x@A 7! v]; I) ( ; I1 jI2 ) ! ( 0 ; I10 jI2 ) ( ; I1 ) ! ( 0 ; I10 ) ( ; I[rec X A :I=X A ]) ! ( 0 ; I 0 ) (Sum) 0 (Rec) ( ; I 1 + I 2 ) ! ( 0 ; I1 ) ( ; rec X A :I) ! ( 0 ; I 0 ) The rst rule is for initiation : A invokes a service located at B and initiates session channels s~ which will be shared locally by A and B: The second rule is for communication. The notation ` e + v is an evaluation judgment : evaluates the expression e to the value v: [x@B 7! v] is the resulting state of updating the local variable x at B by v: The evaluation judgment is also used in the assignment rule. The fourth rule is for parallelism. The (Sum) rule describes the behavior of a non-deterministic choice. The (Rec) rule says that if the unfolding of rec X A :I under reduces to I 0 then rec X A :I under will reach ( 0 ; I 0 ): Example 1. This example shows a communication between a buyer and a seller. These participants share new freshly generated session channels B2Sch and S2Bch: Through S2Bch; the seller o↵ers a quote to the buyer. Through B2Sch; the buyer selects one of the two options o↵ered by the seller, QuoteAccept and QuoteReject. If the rst option is selected, the buyer sends the quote "100" which will be stored in x by Seller and continues with the interaction I1 : In the other case, the seller sends the abort number stored in the variable xAbortN o which will be stored in y by the Seller and terminates. Buyer ! Seller : ch(⌫B2Sch; S2Bch): Seller ! Buyer : S2Bchhquote; 100; yi: if y@Buyer  1000 then f Buyer ! Seller : B2SchhquoteAccept; 100; xi:I1 g else f Buyer ! Seller : B2SchhquoteReject; xabortN o ; xi:0 g 3 Security Policy Speci cation The language that we will use for the speci cation of security policies is EP C which is a subset of EP C (End-point calculus). The End-Point Calculus pre- cisely identi es a local behavior of each participant in a web service. End-Point Calculus is inspired from the ⇡-calculus. It is an applied variant of ⇡-calculus augmented with the notion of participants and their local states. In [10], au- thors have established a projection from the global calculus into the end-point calculus. So descriptions of participants behaviors in end-point calculus are not extracted directly from the choreography, but projected from the global calculus. Details of this theory of end-point projection are presented in [10]. Since in the proposed enforcement approach we transform the security policy to a monitor, we reach immediately this goal by choosing EP C since it is a subset of EP C: 3.1 Syntax of EP C We show the syntax of EP C ; where s denote session channels, e an expression which can be an atomic value (such as a natural number or a boolean value) or a function (such as arithmetic functions and boolean operators) or a variable. op1 ; op2 ; ::: range over operations. x is a variable. The rst construct is a receiving action, it is the invocation of one of the operators opi and reception of an expres- sion which will be evaluated and stored in xi : The second construct is a sending action, it is the invocation of operator op with expression e: Furthermore, the operator " " represents the alternative composition. Finally, recursion is used for representing unbounded repetition. For representing recursive behaviors, we use term variables X; Y; : : : The operator used for recursion is rec X:P: Each occurrence of X in P denotes a recurring point. rec X:P behaves as P until an occurrence of X is found in the execution of P; then it will return to rec X:P: s B ⌃ opi (xi ):Pi ; s C ophei:P; P1 P2 ; X; rec X:P; 0 i 3.2 Semantics of EP C Note that processes do not evolve alone. A process is located in a participant which synchronize with another one to evolve. A participant A with its behavior P at a local state is called a network and denoted by A[P ] : Syntax of networks is given by the following grammar : N ::= A[P ] (Participant) j N jM (Parallel-NW) j (⌫s)N (Res-NW) j ✏ (Inaction-NW) where A[P ] is a participant with its behavior as shown in the rst construct. Two communicating participants are represented by two networks combined by parallel composition. When two participants initiate a session channel for com- munication, this session channel must be restricted to these two participants, this is given by (Res-NW): ✏ denote the lack of networks. Reduction rules of networks are given by : M ⌘ M0 M0 ! N0 N0 ⌘ N Struct-NW M !N M ! M0 M ! M0 Par-NW Res-NW M jN ! M 0 jN (⌫s)M ! (⌫s)M 0 Semantics of EP C is then given by : 2 `e+v A[s C opj hei:P ] 1 jB[s B ⌃ opi (xi ):Qi ] 2 ! A[P ] 1 jB[Qj ] 2 [xj 7!v] i A[P1 ] ! A[P10 ] 0 A[P [rec X:P=X]] ! A[P 0 ] 0 A[P1 P2 ] ! A[P10 ] 0 A[rec X:P ] ! A[P 0 ] 0 Security policies are usually speci ed in logic-based languages. Such languages employ mainly three operators to compose properties : and, or and not: The or operator is given here by : The not operator is de ned here as follows : assume we have two participants A and B communicating and we want to apply the property "A should not send op1 to participant B", then we write it using EP C as follows : P = rec X:(sB C opi hei i:X sB B ⌃ opi (xi ):X) i6=1 i Example 2. Assume we have a client wanting to check its account details within a bank. The bank should not send him back his account details if he is not yet authenticated. A client is said to be authenticated if he has received from the bank an acceptance for his authentication's attempt using the operation accept: The bank answers the client for his account request through the operation resAccount: The security property will then be written as follows : P = rec X:(s B ⌃ opi (xi ):X i sC opi hei:X opi 2faccept;resAccountg = s C accept:rec Y:(s C opi hei i:Y s B ⌃ opi (xi ):Y )) i i The security property is expressed using the recursion operator. In the recursion block, we have 3 behaviors combined with the internal choice which we denote by P 1 ; P 2 and P 3 where P 1 = s B ⌃ opi (xi ):X i P 2 =sC opi hei:X opi 2faccept;resAccountg = P 3 = s C accept:rec Y:(s C opi hei i:Y s B ⌃ opi (xi ):Y ) i i The block P 1 expresses the fact that the property allows all receiving actions. The block P 2 inhibits sending accept or resAccount to the client. The block P 3 intercepts the accept sending action and then no more restrictions are imposed since the authentication of the client is accepted. So, an intruder who wants to check an account's details without authentication cannot achieve its goal since the resAccount is only permitted in the block following the accept sending action. 4 Choreography Speci cation The technique used in this paper for describing the composition of web services is the choreography. The WS-CDL is based on two engineering principles : Service Channel Principle corresponds to the repeated availability of service channels. Session Principle is a basic principle in many communication-centred programs which says a sequence of conversations belonging to a protocol should not be confused with other concurrent runs of this or other protocols by the participants. As a speci cation of the choreography description language WS-CDL, we introduce a modi ed version of the end-point calculus which is a formalism presented in [10]. The end-point calculus describes the behavior of a participant in a choreography from its end-point view. 4.1 Secured End-Point Calculus The secured end-point calculus EP CS is a variant of EP C (End-Point Calculus)[10]. EP CS has the particularity of explicitly handling the monitoring concept through its operator @P : For instance, the process @P (P ) can execute only actions that could be executed by both the controller P and the process P: We describe hereafter the formal syntax and dynamic semantics of the secured end-point calculus. Syntax of EP CS Since EP C is a subset of EP C and EP CS is an extension of EP C; a part of the syntax of EP CS is presented in the last section. So in this section we will present the overall syntax of EP CS but we will describe only constructs that have not been described before. P ::= !ch(~ s):P j ch(⌫ s~):Q j s B ⌃ opi (xi ):Pi i j s C ophei:Q j x := e:P j if e then P else Q j P Q j P jQ j (⌫s)P j X j rec X:P j 0 j @P (P ) The two rst constructs represent session initiation. !ch(~ s):P is used for input and ch(⌫ s~):Q for output. !ch(~ s) says that the service channel ch; which is avail- able to public, is ready to receive an unbounded number of invocations, o↵ering a communication via its freshly generated session channels s 2 s~: ch(⌫ s~) is an invocation of a service located at the service channel ch and an initiation of a communication session which will occur through session channels s~: After a ses- sion has been initiated between two participants and freshly generated session channels have been shared between them, they can communicate using the com- munication constructs. The assignment operator is x := e:P . if e then P else Q is a choice based on the evaluation of the expression e: The parallel composi- tion is given by P jQ: The restriction construct (⌫s)P indicates that the session channel s is local to P: 0 denotes the lack of actions. Finally, @P (P ) is the en- forcement operator which controls the execution of P by allowing it to evolve if P is satis ed. Semantics of EP CS Initiation/Communication simulation Let P be a process stipulating the local behavior of a participant A in a web service. We observe in the end-point cal- culus reduction rules that processes always evolve without an external factor unless in initiation and communication. In fact, a participant initiating a com- munication or communicating with an another participant needs to synchronize with him to realize the interaction . Therefore, for enforcing security policies on a participant's behavior, we need to have a totally local description of its interactions. So we need to de ne a simulation relation for the initiation and the communication of processes so that we can simulate the evolution of a process locally, i.e. without synchronizing with an another participant . We will de ne the normal form of a process then introduce the simulation relation. De nition 1 (Normal form of a process). Every process representing the local behavior of a participant in a web service can be written as an internal sum of processes, which we call the normal form of a process : 8P 2 P; P = a i Pi i where P denotes the set of processes, ai range over atomic actions and Pi range over processes in P: De nition 2 (Simulation Relation). We de ne a simulation relation over a networks, denoted by A[P ] A[P 0 ] 0 ; which says that process P in A at the state is able to execute the action a and reduce to P 0 with a new local state 0 : The simulation relation is de ned following this rule P = a i Pi 9i 2 f1; : : : ; ng : a = ai i a A[P ] A[Pi ] This rule says that when P is written in its normal form and one of the constituting processes is able to do an action a then A[P ] is also able to do it. Semantics of EP CS : Init s):P j P 0 ] A j B[ch(⌫ s~):Q j Q0 ] B ! (⌫ s~)(A[!ch(~ A[!ch(~ s):P jP jP 0 ] A j B[QjQ0 ] B ) A `e+v Assign A[x := e:P jP 0 ] A ! A[P jP 0 ] A [x7!v] A ` e + tt IfTrue A[if e then P1 else P2 jP 0 ] A ! A[P1 jP 0 ] A A ` e + ff IfFalse A[if e then P1 else P2 jP 0 ] A ! A[P2 jP 0 ] A A[P1 jR] A ! A[P10 jR] A0 A[P ] A ! A[P 0 ] A0 Par Res A[P1 jP2 jR] A ! A[P10 jP2 jR] A0 A[(⌫s)P ] A ! A[(⌫s)P 0 ] A0 Init-In-Sec s):P )] A jB[ch(⌫ s~):QjR] B ! (⌫ s~)(A[@P (P )j@P (!ch(~ A[@P (!ch(~ s):P )] A jB[QjR]) Init-Out-Sec A[@P (ch(⌫ s~):P )] A jB[!ch(~ s):QjR] B ! (⌫ s~)(A[@P (P )] A jB[!ch(~ s):QjQjR] B ) sBop(x) sBop(x) A[P ] A A[P 0 ] A A[P ] A A[P 0 ] A A `e+v Comm-In-Sec A[@P (P )] A jB[s C ophei:QjR] B ! A[@P 0 (P 0 )] A [x7!v] jB[QjR] B Comm-Out-Sec sCopj hei sCopj hei A[P ] A A[P 0 ] A A[P ] A A[P 0 ] A B `e+v A[@P (P )] A jB[s B ⌃ opi (xi ):Qi jR] B ! A[@P 0 (P )] A jB[Qj jR] B [xj 7!v] 0 i A `e+v Assign-Sec A[@P (x := e:P )] A ! A[@P (P )] A [x7!v] A[@P (P1 )] ! A[@P 0 (P10 )] 0 Par-Sec A[@P (P1 jP2 )] ! A[@P 0 (P10 jP2 )] 0 ` e + tt IfTrue-Sec A[@P (P jif e then P1 else P2 )] ! A[@P (P jP1 )] ` e + ff IfFalse-Sec A[@P (P jif e then P1 else P2 )] ! A[@P (P jP2 )] A[@P (P )] ! A[@P 0 (P 0 )] 0 Res-Sec A[(⌫ s~)(@P (P ))] ! A[(⌫ s~)(@P 0 (P 0 )] 0 ) The Init-rule shows how two participants initiate a session by sharing new freshly generated session channels s~: These session channels are restricted to par- ticipants A and B by the binding operator (⌫): Assignment is a local construct. Assign-rule evaluates an expression e and assigns the result of this evaluation to the variable x in A; then A behaves as P: The Res-rule restricts the use of session channels s~ to the process P in A: Init-In-Sec and Init-Out-Sec are the rules for communication initiation. We do not control session initiations but we control communication messages between the participants. Communication rules say if P and P are able to send or receive through the same session channel the same operation and become respectively P 0 and P 0 then @P (P ) do this ac- tion and becomes @P 0 (P 0 ): Secured assignment rule says that assignment is not considered by enforcement. The secured parallel composition rule says that the security operator applied to P1 jP2 can evolve into (@P 0 (P10 jP2 )) if P1 can evolve simultaneously with the policy security P into respectively P10 and P 0 : For the restriction rule, binding session channels does not a↵ect the enforcement. Finally, the conditional rules say that enforcement is not a↵ected by conditionals. 5 Choreography Monitoring The goal of this research is to enforce security policies over a choreography. Some of the important features of the enforcement operator is that it allows us to enforce only concerned participants by the security policies. In this in-lined monitoring framework, we do not modify the original behaviors of participants in a choreography. But if the security policy is not veri ed the evolution of the choreography will stop. In this section, we prove the correctness of our theory by de ning rst some notions such as the partial order over processes and satis- faction notions. De nition 3 (Partial Order over Processes). Let A[P1 ] ; A[P2 ] be two networks. We say A[P1 ] v A[P2 ] if the following condition hold : a a A[P1 ] A[P10 ] =) A[P2 ] A[P20 ] and A[P10 ] v A[P20 ] : De nition 4 (Satisfaction Notions). Let P be a security policy and ⇠ a trace. Symbols ✏ and js are de ned as follows : { We say that ⇠ satis es P ; denoted by ⇠ ✏ P ; if ⇠ 2 JP K where JP K denotes the set of traces of P : { We say that ⇠ could satisfy P ; denoted by ⇠ js P ; if it exists a trace ⇠ 0 such that ⇠:⇠ 0 ✏ P : Theorem 1. Let P be a process and P a policy security. The following prop- erties hold : 1. @P (P ) js P ; 2. A[@P (P )] v A[P ] ; 3. 8P 0 : ((P 0 js P ) and (A[P 0 ] v A[P ] )) =) A[P 0 ] v A[@P (P )] : Proof. 1. The process @P (P ) is de ned so that it can evolve into another pro- cess only if the security policy P is satis ed. 2. As well as the rst property, the proof is obtained directly from the reduction rules of the security operator and the de nition of the partial order. 3. Consider a process P 0 2 P such that P 0 js P and A[P 0 ] v A[P ] : Suppose a A[P 0 ] A[P10 ] 0 : Since A[P 0 ] v A[P ] 0 ; we conclude directly from the a de nition of v that A[P ] A[P1 ] 0 : Since P 0 js P ; we can also conclude a from the de nition of js; that a js P : Finally, as A[P ] A[P1 ] 0 and a a js P so A[@P (P )] A[@P 0 (P1 )] 0 and then A[P 0 ] v A[@P (P )] : Example 3 (Buyer-Seller Protocol). The buyer initiates a communication with the seller and requests for a quote. The seller sends back the quote. If the buyer rejects it then the protocol terminates. Otherwise, the seller sends to the buyer an order con rmation and the buyer con rms his command. In this case, the seller contacts the shipper and asks for delivery details which he transfer to the buyer and the protocol terminates. The security property that we want to ap- ply in this protocol is : "the seller should communicate with the shipper only if the buyer con rms his command". As a consequence, the seller won't send to buyer the delivery details if he has not con rmed his command. The protocol is depicted in Fig.1. Critical actions that we have to supervise are in dark grey in Fig.1. The choreography's description in global calculus is the following : Buyer ! Seller : B2SCh(s): Seller ! Buyer : shackSessioni: Buyer ! Seller : shreqQuotei: Seller ! Buyer : shrespQuote; vquote ; xquote i: if resonable(xquote )@Buyer then Buyer ! Seller : shquoteAccepti: Seller ! Buyer : shorderConf irmi: Buyer ! Seller : shackConf irmi: Seller ! Shipper : B2SHCh(s0 ): Shipper ! Seller : s0 hackSessioni: Seller ! Shipper : s0 hreqDelivDeti: Shipper ! Seller : s0 hdelivDet; vdelivDet ; xdelivDet i: Seller ! Buyer : shdelivDet; xdelivDet ; xdelivDet i:0 else Buyer ! Seller : shquoteRejecti:0 The end-point projection gives the end-point behaviors. The buyer's behavior is the following : Buyer[B2SCh(⌫s):s B ackSession:s C reqQuote:s B respQuote(xquote ) ackSession reqQuote respQuote quoteAcc Buyer Seller quoteRej orderCon rm ackCon rm delivDet n sio es kS et ac D iv el D q et re D liv de Shipper Fig. 1. Buyer Seller Protocol :if reasonable(vquote ) then s C quoteAcc:s B orderConf irm:s C ackConf irm :s B delivDet(xdelivDet ):0 else s C quoteRej:0] The seller's behavior is the following : Seller[B2SCh(s):s C ackSession:s B reqQuote:s C respQuotehequote i: (s B quoteAcc:s C orderConf irm:s B ackConf irm: B2SHCh(⌫s0 ):s0 B ackSession:s0 C reqDelivDethebuyer i:s0 B delivDet(xdelivDet ) :s C delivDet(xdelivDet ):0 ) + (s B quoteRej:0)] The shipper's behavior is the following : Shipper[B2SHCh(s0 ):s0 C ackSession:s0 B reqDelivDet(xbuyer ) :s0 C delivDethedelivDet i:0] The security property has the following behavior : P = rec X:( s C opi hei:X op6=delivDet sB ⌃ opi (xi ):X op6=ackConf irm s B ackConf irm:rec Y:(s0 C opi hei:Y s0 B ⌃ opi (xi ):Y i i sC opi hei:Y ) i ) The security property P is written using the recursion operator. In the recursion block, there are 3 processes combined with the internal choice. The rst process is : sC opi hei:X which says that, through the session channel s (shared op6=delivDet between the buyer and the seller), the buyer can execute any sending action un- less delivery details which should be done after the seller has received a con r- mation from the buyer. The second process is : sB ⌃ opi (xi ):X which op6=ackConf irm says that the seller can receive any operation other than ackConf irm. This ac- tion is intercepted in the third process s B ackConf irm:rec Y:(s0 C opi hei:Y i s0 B ⌃ opi (xi ):Y s C opi hei:Y ): In this process, after the seller has received a i i con rmation from the buyer, he can communicate with the shipper through the session channel s0 without any restriction and he has also no restriction on his sending actions to the buyer, so he can send him the delivery details. 6 Related Works Web services veri cation have been a subject of interest of several research ef- forts. Some of the relevant contributions in this domain are cited in this section. Most of formal approaches introduced a monitor which does not stop the pro- gram when a violation is detected. Moreover, these contributions implement a monitor as a web service in addition to other web services. The originality of our work is the introduction of the monitor within concerned participants processes. In [11], a run-time event-based approach to deal with the problem of monitoring conformance of interaction sequences is presented. When a violation is detected, the program shows errors in dashboards. In [12], authors introduce an approach to verify the conformance of a web service implementation against a behavioral speci cation, through the application of testing. The Stream X-machines are used as an intuitive modeling formalism for constructing the behavioral speci - cation of a stateful web service and a method for deriving test cases from that speci cation in an automated way. The test generation method produces com- plete sets of test cases that, under certain assumptions, are guaranteed to reveal all non-conformance faults in a service implementation under test. However, this approach only returns non-conformance faults and does not react dynamically against these errors. While, in [13], authors propose a monitoring framework of a choreographed service which supports the early detection of faults and decide whether it is still possible to continue the service. Authors in [?] have proposed service automata as a framework for enforcing security policies in distributed systems. They encapsulate the program in a service automaton composed of the monitored program, an interceptor, an enforcer, a coordinator and a local policy. The interceptor intercepts critical actions and passes them to the coor- dinator that determines whether the action complies the security policy or not and decides upon possible countermeasures then the enforcer implements these decisions. However the authors do not precise how to detect critical actions. 7 Conclusion In this paper, we have introduced a formal approach allowing to automatically enforce a security policy on choreographed services. Indeed, we introduced a new calculus with an enforcement operator @P : The semantics of the proposed calculus insure that choreographed services can evolve only if it does not violate the enforced security policy. The originality of our work consists on the fact that we do not add a new web service as a monitor but rather we wrap the security policy inside the choreographed services. Future work will focus on the de nition of a complete mapping between WS- CDL and global calculus. Moreover, we will seek means to optimize the enforced choreographed services so that we reduce as much as we can the overhead due to the enforcement operator. References 1. Corporation, I.: Business process execution language for web services bpel-4ws. http://www.ibm.com/developerworks/library/ws-bpel/ (2002) 2. F.Leymann: Web services ow language (ws ) version 1.0. Technical Report, International Business Machines Corporation (IBM) (May 2001) 3. Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y.: Web services choreography description language version 1.0. W3C Working Draft (December 2004) 4. Langar, M., Mejri, M., Adi, K.: Formal enforcement of security policies on con- current systems. J. Symb. Comput. 46(9) (2011) 997{1016 5. Khoury, R., Tawbi, N.: Corrective enforcement: A new paradigm of security policy enforcement by monitors. ACM Trans. Inf. Syst. Secur. 15(2) (2012) 10 6. Yi, X., Kochut, K.: A cp-nets-based design and veri cation framework for web services composition. In: ICWS. (2004) 756{760 7. Hamadi, R., Benatallah, B.: A petri net-based model for web service composition. In: ADC. (2003) 191{200 8. Sala un, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: ICWS. (2004) 43{ 9. Kazhamiakin, R., Pandya, P.K., Pistore, M.: Timed modelling and analysis in web service compositions. In: ARES. (2006) 840{846 10. Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred pro- gramming for web services. In: ESOP. (2007) 2{17 11. Baouab, A., Perrin, O., Godart, C.: An optimized derivation of event queries to monitor choreography violations. In: ICSOC. (2012) 222{236 12. Dranidis, D., Ramollari, E., Kourtesis, D.: Run-time veri cation of behavioural conformance for conversational web services. In: ECOWS. (2009) 139{147 13. Ardissono, L., Furnari, R., Goy, A., Petrone, G., Segnan, M.: Monitoring chore- ographed services. In: Innovations and Advanced Techniques in Computer and Information Sciences and Engineering. (2007) 283{288 14. Fu, X., Bultan, T., Su, J.: Analysis of interacting bpel web services. In: WWW. (2004) 621{630