Keywords: vérification, protocoles de sécurité, composition

Composition de protocoles de sécurité

Résumé : Les protocoles de sécurité sont des petits programmes qui s'exécutent dans un environnement hostile. De nombreux résultats permettent de réaliser une analyse formelle de ces protocoles en présence d'un intrus actif qui peut bloquer, intercepter et envoyer de nouveaux messages. Cependant ces résultats ne fournissent aucune garantie de sécurité dans le cas où le protocole est exécuté dans un environnement où d'autres protocoles, partageant éventuellement des clefs, interviennent.

Dans ce papier, nous montrons que la sécurité des protocoles se composent. Plus précisément, nous montrons que lorsqu'un protocole est sûr, il le reste même lorsque d'autres protocoles sont exécutés, pourvu que chaque message chiffré du protocole contienne un identifiant, comme par exemple le nom du protocole.

Introduction

Security protocols are small programs that aim at securing communications over a public network like the Internet. Considering the increasing size of networks and their dependence on cryptographic protocols, a high level of assurance is needed in the correctness of such protocols. The design of such protocols is difficult and error-prone; many attacks have been discovered even several years after the publication of a protocol. Consequently, there has been a growing interest in applying formal methods for validating cryptographic protocols and many results have been obtained. The main advantage of the formal approach is its relative simplicity which makes it amenable to automated analysis. For example, the secrecy preservation is co-NP-complete for a bounded number of sessions [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions and composed keys is NP-complete[END_REF], and decidable for an unbounded number of sessions under some additional restrictions (e.g. [2,[START_REF] Blanchet | Verification of cryptographic protocols: Tagging enforces termination[END_REF][START_REF] Seidl | Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying[END_REF]). Many tools have also been developed to automatically verify cryptographic protocols like [START_REF] Lowe | Casper: A compiler for the analysis of security protocols[END_REF][START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prolog rules[END_REF].

However even when a protocol has been proved secure for an unbounded number of sessions, against a fully active adversary that can intercept, block and send new messages, there is absolutely no guarantee if the protocol is executed in an environment where other protocols, possibly sharing some common identities and keys like public keys or long-term symmetric keys, are executed. This is however very likely to happen since a user connected to the Internet for example, usually uses simultaneously several protocols with the same identity. The interaction with the other protocols may dramatically damage the security of a protocol. Consider for example the two following naive protocols.

P 1 : A → B : {s} pub(B) P 2 : A → B : {N a } pub(B) B → A : N a
In protocol P 1 , the agent A simply sends a secret s encrypted under B's public key. In protocol P 2 , the agent sends some fresh nonce to B encrypted under B's public key. The agent B acknowledges A's message by forwarding A's nonce. While P 1 executed alone easily guarantees the secrecy of s, even against an active adversary, the secrecy of s is no more guaranteed when the protocol P 2 is executed. Indeed, an adversary may use the protocol P 2 as an oracle to decrypt any message. More realistic examples illustrating interactions between protocols can be found in e.g. [START_REF] Kelsey | Protocol interactions and the chosen protocol attack[END_REF]. The purpose of this paper is to investigate sufficient and rather tight conditions for a protocol to be safely used in an environment where other protocols may be executed as well. Our main contribution is to show that whenever a protocol is proved secure when it is executed alone, its security is not compromised by the interactions with any other protocol, provided each protocol is given an identifier (e.g. the protocol's name) that should appear in any encrypted message. Continuing our example, let us consider the two slightly modified protocols.

P ′

1 : A → B : {1, s} pub(B)

P ′ 2 : A → B : {2, N a } pub(B) B → A : N a
Applying our result, we immediately deduce that P ′ 1 can be safely executed together with P ′ 2 , without compromising the secrecy of s.

The idea of adding an identifier in encrypted messages is not novel. This rule is in the same spirit as those proposed in the paper of Abadi and Needham on prudent engineering practice for cryptographic protocols [START_REF] Abadi | Prudent engineering practice for cryptographic protocols[END_REF] (principle 10). The use of unique protocol identifiers is also recommended in [START_REF] Kelsey | Protocol interactions and the chosen protocol attack[END_REF][START_REF] Canetti | Environmental requirements for authentication protocols[END_REF] and has also been used in the design of fail-stop protocols [START_REF] Gong | Fail-stop protocols: An approach to designing secure protocols[END_REF]. However, to the best of our knowledge, it has never been proved that it is sufficient for securely executing several protocols in the same environment. Note that some other results also use tags for different purposes. For instance, Blanchet uses tags to exhibit a decidable class [START_REF] Blanchet | Verification of cryptographic protocols: Tagging enforces termination[END_REF] but his tagging policy is stronger since any two encrypted subterm in a protocol have to contain different tags.

The result the most closely related to ours is the one of Guttman and Thayer [START_REF] Guttman | Protocol independence through disjoint encryption[END_REF]. They show that two protocols can be safely executed together without damaging interactions, as soon as the protocols are "independent". The independence hypothesis requires in particular that the set of encrypted messages that the two protocols handle should be different. As in our case, this can be ensured by giving each protocol a distinguishing value that should be included in the set of encrypted messages that the protocol handles. However, the major difference with our result is that this hypothesis has to hold on any valid execution of the protocol. In particular, considering again the protocol P ′ 2 , an agent should not accept a message of the form {2, {1, m} k } pub(B) while he might not be able to decrypt the inside encryption and detect that it contains the wrong identifier. In particular, their result do not allow to conclude when no typing hypothesis is assumed (that is, when agents are not required to check the type of each component of a message) or for protocols with cyphertext forwarding, that is, when agents have to forward unknown message components.

Datta et al. [START_REF] Datta | A derivation system and compositional logic for security protocols[END_REF][START_REF] Datta | Protocol composition logic (PCL)[END_REF] have also studied secure protocol composition in a more broader sense: protocols can be composed in parallel, sequentially or protocols may use other protocols as components. However, they do not provide any syntactic conditions for a protocol P to be safely executed in parallel with other protocols. For any protocol P ′ that might be executed in parallel, they have to prove that the two protocols P and P ′ satisfy each other invariants. Their approach is thus rather designed for component-based design of protocols.

2 Models for security protocols

t ::= term | x variable x | a name a | f (a) application of symbol f ∈ {pub, priv} on a name | f (t 1 , t 2 ) application of symbol f ∈ {enc, enca, sign, }
As usual, we write vars(t) (resp. names(t)) for the set of variables (resp. names) occurring in t. A term is ground or closed if and only if it has no variables. We write St (t) for the set of subterms of a term t. This notion is extended as expected to sets of terms. Extended names are names or terms of the form pub(a), priv(a). The set of extended names of a term t, denoted by n(t), is n(t) = names(t) ∪ {pub(t), priv(t) | pub(t) or priv(t) ∈ St(t)}. For example, we have that n(enc(a, pub(b))) = {a, b, pub(b), priv(b)}. Substitutions are written σ = {x 1 → t 1 , . . . , x n → t n } with dom(σ) = {x 1 , . . . , x n }. The substitution σ is closed if and only if all the t i are closed. The application of a substitution σ to a term t is written σ(t) or tσ.

Intruder capabilities

The ability of the intruder is modelled by a deduction system described in Figure 1 and corresponds to the usual Dolev-Yao rules. The first line describes the composition rules. We call these deduction rules pairing, symmetric and asymmetric encryption and signature respectively. The two last lines describe the decomposition rules and the axiom. We call these rules first and second projection, symmetric and asymmetric decryption respectively. Intuitively, these deduction rules say that an intruder can compose messages by pairing, encrypting and signing messages provided he has the corresponding keys. Conversely, it can decompose messages by projecting or decrypting provided it has the decryption keys. For signatures, the intruder is also able to verify whether a signature sign(m, k) and a message m match (provided she has the verification key), but this does not give her any new message. That is why this capability is not represented in the deduction system. We also consider an optional rule T ⊢ sign(u, priv(v)) T ⊢ u that expresses that an intruder can retrieve the whole message from its signature. This property may or may not hold depending on the signature scheme, and that is why this rule is optional. Our results hold in both cases (that is, when the deduction relation ⊢ is defined with or without this rule).

A term u is deducible from a set of terms T , denoted by T ⊢ u if there exists a proof i.e. a tree such that the root is T ⊢ u, the leaves are of the form T ⊢ v with v ∈ T (axiom rule) and every intermediate node is an instance of one of the rules of the deduction system.

T ⊢ u T ⊢ v T ⊢ u, v T ⊢ u T ⊢ v T ⊢ enc(u, v) T ⊢ u T ⊢ v T ⊢ enca(u, v) T ⊢ u T ⊢ v T ⊢ sign(u, v) T ⊢ u, v T ⊢ u T ⊢ u, v T ⊢ v T ⊢ enc(u, v) T ⊢ v T ⊢ u T ⊢ enca(u, pub(v)) T ⊢ priv(v) T ⊢ u T ⊢ sign(u, priv(v)) (optional) T ⊢ u u ∈ T T ⊢ u Figure 1: Intruder deduction system. Example 1 The term k 1 , k 2 is deducible from the set T 1 = {enc(k 1 , k 2 ), k 2 }. A proof of T 1 ⊢ k 1 , k 2 is: T 1 ⊢ enc(k 1 , k 2 ) T 1 ⊢ k 2 T 1 ⊢ k 1 T 1 ⊢ k 2 T 1 ⊢ k 1 , k 2 2.

Protocols

We consider protocols specified in a language similar to the one of [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions and composed keys is NP-complete[END_REF] allowing parties to exchange messages built from identities and randomly generated nonces using public key, symmetric encryption and digital signatures. The individual behavior of each protocol participant is defined by a role describing a sequence of message receptions/transmissions, and a k-party protocol is given by k such roles.

Definition 1 (Roles and protocols) The set Roles of roles for protocol participants is the set of sequences of the form (rcv 1 , N 1 , snd 1 ) • • • (rcv ℓ , N ℓ , snd ℓ ) where each element, called rule, satisfies (rcv i , N i , snd i ) ∈ Terms × 2 X × Terms, and for any variable, x ∈ vars(snd i ) implies x ∈ 1≤j≤i N j ∪ vars(rcv j ).

The length of a role is the number of elements in its sequence. A k-party protocol is a mapping Π : [k] → Roles, where [k] = {1, 2, . . . , k}.

The last condition ensures that each variable which appears in a sent term is either a nonce or has been introduced in a previously received message. The set of variables, names or extended names of a protocol is defined as expected, considering all the terms occurring in the role's specification.

The j th role of a protocol Π is denoted by (rcv

j 1 N j 1 → snd j 1 ) • • • (rcv j k j N j k j
→ snd j k j ). It specifies the messages to be sent/received by the party executing the role: at step i, the j th party expects to receive a message conformed to rcv j i , instantiate the variables of N j i with fresh

INRIA

names and returns the message snd j i . We assume the sets N j i to be pairwise disjoint. The special constants init and stop will be used to specify that no message is expected or sent.

The composition of two protocols Π 1 and Π 2 , denoted by Π 1 | Π 2 is the protocol obtained by the union of the roles of Π 1 and Π

2 . If Π 1 : [k 1 ] → Roles and Π 2 : [k 2 ] → Roles, then Π = Π 1 | Π 2 : [k 1 + k 2 ] → Roles with Π(i) = Π 1 (i) for any 1 ≤ i ≤ k 1 and Π(k 1 + i) = Π 2 (i) for any 1 ≤ i ≤ k 2 .
Example 2 Consider the famous Needham-Schroeder asymmetric key authentication protocol [START_REF] Needham | Using encryption for authentication in large networks of computers[END_REF] designed for mutual authentication.

A → B : {N a , A} pub(B) B → A : {N a , N b } pub(A) A → B : {N b } pub(B)
The agent A sends to B his name and a fresh nonce (a randomly generated value) encrypted with the public key of B. The agent B answers by copying A's nonce and adds a fresh nonce N B , encrypted by A's public key. The agent A acknowledges by forwarding B's nonce encrypted by B's public key. For instance, let a, b, and c be three agent names. The role Π(1) corresponding to the first participant played by a talking to c is:

(init {X} → enca( X, a , pub(c))), (enca( X, x , pub(a)) ∅ → enca(x, pub(c)))
The role Π(2) corresponding to the second participant played by b with a is:

(enca( y, a , pub(b))

{Y }

→ enca( y, Y , pub(a))), (enca(Y, pub(b))

∅ → stop)
Note that there is also a role corresponding to the first participant played by a talking to b for example. If more agent identities need to be considered, then the corresponding roles should be added to the protocol. It has been shown however that two agents are sufficient (one honest and one dishonest) for proving security properties [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF].

Clearly, not all protocols written using the syntax above are meaningful. In particular, some of them might not be executable. A precise definition of executability is not relevant for our result. We use instead a weaker hypothesis (see Section 3). In particular, our combination result also holds for non executable protocols that satisfy our hypothesis.

Constraint systems

Constraint systems are quite common (see e.g. [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions and composed keys is NP-complete[END_REF][START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF][START_REF] Cortier | Deciding key cycles for security protocols[END_REF]) in modeling security protocols. They are used to specify secrecy preservation of security protocols under a particular, finite scenario. We recall here their formalism and we show in the next section that the secrecy preservation problem for an unbounded number of sessions can be specified using (infinite) families of constraint systems.

Definition 2 (constraint system) A constraint system C is either ⊥ or a finite set of expressions T u, called constraints, where T is a non empty set of terms, called the lefthand side of the constraint and u is a term, called the right-hand side of the constraint, such that: the left-hand sides of all constraints are totally order by inclusion;

if x ∈ vars(T ) for some (T u) ∈ C then T x def = min{T ′ | (T ′ u ′ ) ∈ C and x ∈ vars(u ′ )} exists and T x T .
A solution of C is a closed substitution θ such that for every (T u) ∈ C, we have that T θ ⊢ uθ. The empty constraint system is always satisfiable whereas ⊥ denotes an unsatisfiable system.

A constraint system C is usually denoted as a conjunction of constraints C = 1≤i≤n (T i u i ) with T i ⊆ T i+1 , for all 1 ≤ i < n. The second condition in Definition 2 says that if x ∈ vars(T i ) then ∃j < i such that T j = T x and T j T i . In other words, each time a variable occurs first in some right-hand side, it must not have occurred before in some left-hand side. The left-hand side of a constraint system usually represents the messages sent on the network.

Secrecy

We define the general secrecy preservation problem for an unbounded number of sessions, using infinite families of constraint systems. A role may be executed in several sessions, using different nonces at each session. Moreover, since the adversary may block, redirect and send new messages, all the sessions might be interleaved in many ways. This is captured by the notion of scenario.

Definition 3 (scenario) A scenario for a protocol Π : [k] → Roles is a sequence of the form (r 1 , s 1 ) • • • (r n , s n ) such that 1 ≤ r i ≤ k, s i ∈ N,
the number of identical occurrences of a pair (r, s) is smaller than the length of the role r, and whenever s i = s j then r i = r j .

The numbers r i and s i represent respectively the involved role and the session number. The last condition ensures that a session number is not reused on other roles. Given a scenario sc, we say that (r, s) ∈ sc if (r, s) is an element of the sequence sc. Let Π = Π 1 | Π 2 be a protocol obtained by composition of Π 1 and Π 2 and let sc be a scenario for Π. The scenario sc| Π 1 is simply the sequence obtained from sc by removing any element (r, s) where r is a role of Π 2 . Given a scenario, we can define a sequence of rules that corresponds to the sequence of expected and sent messages.

Definition 4 Given a scenario sc = (r 1 , s 1 ) • • • (r n , s n ) for a k-party protocol Π, the se- quence of rules (u 1 , v 1 ) • • • (u n , v n ) associated to sc is defined as follows. Let Π(j) = (rcv j 1 N j 1 → snd j 1 ) • • • (rcv j k j N j k j → snd j k j ) for 1 ≤ j ≤ k. INRIA Let p i = #{(r j , s j ) ∈ sc | j ≤ i, r j = r i }, i.e.
the number of previous occurrences in sc of the role r i . We have

p i ≤ k r i and (u i , v i ) = (rcv r i p i σ r i ,s i , snd r i p i σ r i ,s i ),
where

dom(σ r,s ) = 1≤i≤k r (N r i ∪ vars(rcv r i )), i.e. variables occurring in Π(r), σ r,s (x) = n x,s if x ∈ 1≤i≤k r N r
i , where n x,s is a name. σ r,s (x) = x s otherwise, where x s is a variable.

We assume that names (resp. variables) with different indexes are pairwise different and also different from the names (resp. variables) occurring in Π, We say that a protocol preserves the secrecy of a data if it preserves its secrecy for any scenario. In particular, the secrecy of the data must be preserved for any possible instances of its fresh values (e.g. nonces and keys).

Definition 5 (secrecy) A protocol Π preserves the secrecy of a term m for the initial knowledge T 0 if for any scenario sc for Π, for any role number 1 ≤ i ≤ k, for any session number s i ∈ N that either corresponds to role i, that is (i, s i ) ∈ sc or does not appear in the scenario, that is ∀j, (j, s i ) / ∈ sc, the following constraint system is not satisfiable

T ′ 0 u 1 ∧ 1≤i<n (T ′ 0 ∪ {v 1 , . . . , v i } u i+1 ) ∧ (T ′ 0 ∪ {v 1 , . . . , v n } mσ 1,s 1 • • • σ k,s k )
where

T ′ 0 = T 0 ∪{init} and (u 1 , v 1 ) • • • (u n , v n )
is the sequence of rules associated to sc and σ r,s is the substitution defined in Definition 4.

The initial knowledge typically contains the names and the public keys of all agents and the private keys of all dishonest agents.

Example 3 Consider again the Needham-Schroeder protocol. Let Π(1) and Π(2) the two roles introduced in Example 2. This protocol is well-known to be insecure w.r.t. m = Y and T 0 = {priv(c), pub(c), a, b, pub(a), pub(b)}. Let s 1 and s 2 be two session numbers (s 1 = s 2 ) and consider sc = (1, s 1 ) (2, s 2 ) (1, s 1 ) (2, s 2 ). The constraint system C associated to T 0 , sc and mσ 1,s 1 σ 2,s 2 = n Y,s 2 (according to Definition 5) is given below.

C :=              T 0 , init init T 1 def = T 0 , init, enca( n X,s 1 , a , pub(c)) enca( y s 2 , a , pub(b)) T 2 def = T 1 , enca( y s 2 , n Y,s 2 , pub(a)) enca( n X,s 1 , x s 1 , pub(a)) T 2 , enca(x s 1 , pub(c)) enca(n Y,s 2 , pub(b)) T 2 , enca(x s 1 , pub(c)) n Y,s 2 The substitution σ = {y s 2 → n X,s 1 , x s 1 → n Y,s 2 } is a solution of C.
RR n 6234

3 Composition result

Hypothesis

Even if a protocol is secure for an unbounded number of sessions, its security may collapse if the protocol is executed in an environment where other protocols sharing some common keys are executed. We have seen a first example in introduction. To avoid a cyphertext from a protocol Π 1 to be decrypted in an another protocol Π 2 , we introduce the notion of well-tagged protocol.

Definition 6 (well-tag, α-tag) Let α be a term. We say that a term t is α-tagged if for every

t ′ ∈ St(t) of the form t ′ = enc(t 1 , t 2 ), t ′ = enca(t 1 , t 2 ), or t ′ = sign(t 1 , t 2 ), we have t 1 = α, t ′ 1 for some term t ′ 1 .
A term is said well-tagged if it is α-tagged for some term α. A protocol Π is α-tagged is any term occurring in the role of the protocol is α-tagged. A protocol is said well-tagged if it is α-tagged for some term α.

Requiring that a protocol is well-tagged can be very easily achieved in practice: it is sufficient for example to add the name of the protocol in each encrypted term. Moreover, note that (as opposite to [START_REF] Guttman | Protocol independence through disjoint encryption[END_REF]) this does not require that the agents check that nested encrypted terms are correctly tagged. For example, let Π be a protocol with one role as follows:

Π(1) = (enca( α, x , pub(a)) → enca( α, x , pub(b))).
The protocol Π is α-tagged and still the message enca( α, enc(a, k) , pub(a)) (which is not α-tagged) would be accepted by the agent playing the role.

Tagging protocols is not sufficient, indeed critical long-term keys should not be revealed in clear. Consider for example the following two well-tagged protocols

P 3 : A → B : {α, s} k ab P 4 : A → B : k ab
The security of protocol P 3 is again compromised by the execution of P 4 . Thus we will require that long-term keys (except possibly the public ones) do not occur in plaintext in the protocol.

Definition 7 (plaintext) The set plaintext (t) of plaintext of a term t is the set of extended names and variables, that is recursively defined as follows.

plaintext

(u) = {u} if u is a variable or a name plaintext (f (u)) = {f (u)} for f ∈ {pub, priv} plaintext ( u 1 , u 2 ) = plaintext (u 1 ) ∪ plaintext (u 2 ) plaintext (f (u 1 , u 2 )) = plaintext (u 1 ) for f ∈ {enc, enca, sign}
This notation is extended to set of terms and protocols as expected .

INRIA Some weird protocols may still reveal critical keys in a hidden way. Consider for example the following one role (α-tagged) protocol.

Π(1) = (init → enc( α, a , k ab )), (enc( α, a , x) → x)
While the long-term key k ab does not appear in plaintext, the key k ab is revealed after simply one normal execution of the role. This protocol is however not realistic since an unknown value cannot be learned (and sent) if it does not appear previously in plaintext. Thus we will further require (Condition 2 of Theorem 1) that a variable occurring in plaintext in a sent message, has to previously occur in plaintext in a received message.

Composition theorem

We show that any two well-tagged protocols can be safely composed as soon as they use different tags and that critical long-term keys do not appear in plaintext.

Theorem 1 Let Π 1 and Π 2 be two well-tagged protocols such that Π 1 is α-tagged and Π 2 is β-tagged with α = β. Let T 0 (intuitively the initial knowledge of the intruder) be a set of extended names. Let KC = (n(Π 1 ) ∪ n(Π 2 )) T 0 be the set of critical extended names. Let m be a term constructed from Π 1 such that m is α-tagged and vars(m) ⊆ vars(Π 1 ). Moreover, we assume that 1. critical extended names do not appear in plaintext, that is

KC ∩ (plaintext(Π 1 ) ∪ plaintext (Π 2 )) = ∅.
2. for any role (rcv 1

N 1 → snd 1 ) • • • (rcv k N k → snd k ) of Π 1 or Π 2 , for any variable x ∈ plaintext (snd i ), we have x ∈ 1≤j≤i N j ∪ {plaintext (rcv j )}.
Then Π 1 preserves the secrecy of m for the initial knowledge T 0 if and only if Π 1 | Π 2 preserves the secrecy of m for T 0 .

We have seen in Section 3.1 that conditions 1 and 2 are necessary conditions. Moreover, condition 2 will be satisfied by any realistic (executable) protocol. We require that terms from Π 1 and Π 2 are tagged with distinct tags for simplicity. The key condition is actually that for any encrypted (or signed) subterm t 1 of Π 1 and for any encrypted (or signed) subterm t 2 of Π 2 , the terms t 1 and t 2 cannot be unified.

Theorem 1 is proved by contradiction. Assume that Π 1 | Π 2 does not preserve the secrecy of m for T 0 . It means that there exists a scenario sc for Π 1 | Π 2 such that the constraint system associated to sc, T 0 and m is satisfiable. Proposition 1 ensures that in this case, there exists a scenario sc ′ for Π 1 such that the constraint system associated to sc ′ , T 0 and m is satisfiable, which means that Π 1 does not preserve the secrecy of m for some initial knowledge T 0 , contradiction.

Proposition 1 Let Π 1 = [k 1 ] → Roles, Π 2 = [k 2 ]
→ Roles, T 0 and m defined as in Theorem 1 and satisfying the conditions 1 and 2. Let k = k 1 +k 2 and sc be a scenario for

Π 1 | Π 2 .
For any role number 1 ≤ i ≤ k, let s i ∈ N such that (i, s i ) ∈ sc or ∀j, (j, s i ) ∈ sc. Let C be the constraint system associated to sc, T 0 and mσ 1,s 1 • • • σ k,s k . Let sc ′ = sc| Π 1 and C ′ be the constraint system associated to sc ′ , T 0 and mσ 1,

s 1 • • • σ k 1 ,s k 1 . If C is satisfiable, then C ′ is also satisfiable.
The next section is devoted to the (sketch of) proof of this proposition.

Proof of our combination result

To prove our decision procedure, we first refine an existing decision procedure for solving constraint systems. Several decision procedures already exist [START_REF] Millen | Constraint solving for bounded-process cryptographic protocol analysis[END_REF][START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF][START_REF] Cortier | Deciding key cycles for security protocols[END_REF][START_REF] Rusinowitch | Protocol insecurity with finite number of sessions and composed keys is NP-complete[END_REF] for solving constraint systems. Some of them [START_REF] Millen | Constraint solving for bounded-process cryptographic protocol analysis[END_REF][START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF][START_REF] Cortier | Deciding key cycles for security protocols[END_REF] are based on a set of simplification rules allowing a general constraint system to be reduced to some simpler one, called solved, on which satisfiability can be easily decided. A constraint system is said solved [START_REF] Cortier | Deciding key cycles for security protocols[END_REF] if it is different from ⊥ and if each of its constraints is of the form T

x, where x is a variable. Note that the empty constraint system is solved. Solved constraint systems are particularly simple since they always have a solution. Indeed, let T 1 be the smallest (w.r.t. inclusion) left hand side of a constraint. From the definition of a constraint system we have that T 1 is non empty and has no variable. Let t ∈ T 1 . Then the substitution τ defined by xτ = t for every variable x is a solution since T ⊢ xθ for any constraint T x of the solved constraint system.

The simplification rules we consider are given below. All the rules are indexed by a substitution (when there is no index then the identity substitution is implicitly considered). We write C * σ C ′ if there are C 1 , . . . , C n such that C σ 0 C 1 σ 1 . . . σ n C ′ and σ = σ 0 σ 1 . . . σ n . Our rules are the same than in [START_REF] Cortier | Deciding key cycles for security protocols[END_REF] except that we forbid unification of terms headed by . We show that it still forms a complete decision procedure (see Appendix A). Correction and termination are still ensured by [START_REF] Cortier | Deciding key cycles for security protocols[END_REF].

R 1 : C ∧ T u C if T ∪ {x | T ′ x ∈ C, T ′ R} ⊢ u R 2 : C ∧ T u σ Cσ ∧ T σ uσ if σ = mgu(t,
: C ∧ T u ⊥ if vars(T, u) = ∅ and T ⊢ u R 5 : C ∧ T f (u, v) C ∧ T u ∧ T v for f ∈ { , enc, enca, sign}
Theorem 2 Let C be an unsolved constraint system.

1. (Correctness) If C * σ C ′ for some constraint system C ′ and some substitution σ and if θ is a solution of C ′ then σθ is a solution of C.

(Termination)

There is no infinite chain

C σ 1 C 1 . . . σ n C n .
Proving that forbiding unification between pairs still leads to a complete decision procedure required in particular to introduce a new notion of minimality for tree proofs for deduction.

Note that this result is of independent interest. Indeed, we provide a more efficient decision procedure for solving constraint systems, thus for deciding secrecy for a bounded number of sessions. Of course, the theoretical worst-case complexity remains the same (NP).

Proposition 1 is then proved in three main steps (see Appendix). First, Theorem 2 serves as a key result for proving that if C is satisfiable, then there exists a solution θ such that every term in Cθ is well-tagged. Intuitively, it shows that there is a solution where messages from Π 1 and Π 2 are not mixed up.

Second, conditions 1 and 2 ensure that for any solution θ of C, the critical extended names of KC do not appear in plaintext in Cθ.

Third, thanks to the two previous steps, we prove that β-tagged terms (intuitively messages from Π 2 ) are not useful for deducing α-tagged terms. The proof required in particular the introduction of a new locality lemma for deduction of ground terms. We deduce that, removing from C all constraints inherited from Π 2 and all β-tagged terms, we obtain a satisfiable constraint C ′ that is associated to a scenario of Π 1 .

Conclusion

In this paper, we have shown how to safely compose secure protocols by tagging encryption, focusing on secrecy properties. Whenever a protocol preserves the secrecy of some data s, it still preserves s secrecy when other tagged protocols are executed in the same environment. We plan to consider the protocol composition problem for larger classes of security properties. In particular, we believe that our result can be extended to authentication-like properties.

More broadly, we foresee composition results in a more general way. In this paper, protocols are composed in the sense that they can be executed in the same environment. We plan to develop composition results where protocols can use other protocols as subprograms. For example, a protocol could use a secure channel, letting the implementation of the secure channel underspecified. This secure channel could be then possibly implemented by any protocol establishing session keys.

A Proof of completeness

Let T 1 ⊆ T 2 ⊆ . . . ⊆ T n . We say that a proof π of T i ⊢ u is left-minimal if for any j < i such that T j ⊢ u, π ′ is a proof of T j ⊢ u where π ′ is obtained from π by replacing T i with T j in the left hand side of each node of π.

Definition 8 (simple)

We say that a proof π is simple if any subproof of π is left-minimal, any term of the form u 1 , u 2 obtained by application of a decomposition rule or an axiom rule is followed by a projection rule a composition rule is not directly followed by a decomposition rule.

Example 4 Let T 1 = {a} and T 2 = {a, enc( a, b , k), k}. We have that T 2 ⊢ a, b .

T 2 ⊢ enc( a, b , k) T 2 ⊢ k T 2 ⊢ a, b
The proof above is not a simple proof of T 2 ⊢ a, b . The term a, b has been obtained by an application of a decomposition rule. Thus we have to decompose it. A simple proof of T 2 ⊢ a, b is described below:

T 2 ⊢ a T 2 ⊢ enc( a, b , k) T 2 ⊢ k T 2 ⊢ a, b T 2 ⊢ b T 2 ⊢ a, b
Lemma 1 If T i ⊢ u then there is a simple proof of it.

Given a constraint system C, we say that T i is a minimal unsolved left hand side of C if T i is a left hand side of C and for all T u ∈ C such that T T i , u is a variable.

Lemma 2 Let C be an unsolved constraint system, θ be a solution to C and T i be a minimal unsolved left hand side of C. If there is a simple proof of T i θ ⊢ u having the last rule an axiom or a decomposition then there is t ∈ St(T i ) X such that tθ = u.

Proof. Consider a simple proof π of T i θ ⊢ u. Let j be minimal such that the proof π ′ obtained from π by replacing T i with T j is a proof of T j θ ⊢ u. According to the last applied rule in the proof, we have:

INRIA

The last rule is an axiom. Then u ∈ T j θ and hence there is t ∈ T j such that tθ = u. If t is a variable then T t t is a constraint in C with T t T j (see the definition of a constraint system). Hence T t θ ⊢ tθ, that is T t θ ⊢ u, which contradicts the minimality of j.

The last rule is a decomposition. Suppose that it is a symmetric decryption. Then, in such a case, there exists w such that T j θ ⊢ enc(u, w) and T j θ ⊢ w. By simplicity of the proof, the last rule applied to obtain enc(u, w) can not be a composition. Hence, it is either an axiom or a decomposition. Then, applying the induction hypothesis we have that there is t ∈ St(T j ), t not a variable, such that tθ = enc(u, w).

It follows that t = enc(t ′ , t ′′ ) with t ′ θ = u. If t ′ is a variable then T t ′ θ ⊢ t ′ θ, that is T t ′ θ ⊢ u
which contradicts the minimality of j. Hence t ′ is not a variable. For the other decomposition rules, the same reasoning holds.

Let t be a term, we denote by comp(t) the components of the term t. This notion is formally defined as follows: comp( t 1 , t 2 ) = comp(t 1 ) ∪ comp(t 2 ) and comp(t) = t otherwise.

Lemma 3 Let C be an unsolved constraint system, θ be a solution of C and T i be a minimal unsolved left hand side of C such that for all t 1 , t 2 ∈ St(T i )

t 1 θ = t 2 θ implies t 1 or t 2 is a variable or a pair If u i ∈ St(T i ) X and T i θ ⊢ u i θ then T ′ i ⊢ u i where T ′ i = T i ∪ {x | T x ∈ C, T T i }.
Proof. Let j be minimal such that T j θ ⊢ u i θ. Thus j ≤ i and T j ⊆ T i . Consider a simple proof of T j θ ⊢ u i θ. We reason by induction on the depth of the proof. We can have that:

The proof is reduced to an application of the rule axiom that might be followed by several application of the projection rules until the resulting term is not a pair. Since the proof is a simple proof, we have that u i θ is not a pair. Hence, u i is not a pair.

There exists t ∈ T j such that u i θ ∈ comp(tθ). Either u i θ = t ′ θ for some t ′ ∈ comp(t) X or u i θ ∈ comp(xθ) for some x ∈ comp(t) ∩ X . In the first case, we easily deduce that neither u i nor t is a pair or a variable and hence by hypothesis, we have that u i = t ′ and hence T ′ i ⊢ u i . In the second case, we have that T x θ ⊢ xθ. Thus T x θ ⊢ u i θ which contradicts the minimality of j, since T x T j .

The proof ends with an application of a decomposition rule that might be followed by several application of the projection rules until the resulting term is not a pair. Note that, since the proof is a simple proof, we have that u i θ is not a pair. Hence u i is not a pair.

Suppose for example that it is the symmetric decryption rule. That is, there exist w 1 , w 2 such that T j θ ⊢ enc(w 1 , w 2 ), T j θ ⊢ w 2 and u i θ ∈ comp(w 1 ). The last rule applied to obtain T j θ ⊢ enc(w 1 , w 2 ) was not a composition by simplicity of the proof.

We can hence apply Lemma 2 and obtain that there is t ∈ St (T j ) X such that tθ = enc(w 1 , w 2 ). Since t is not a variable, we have that t = enc(t 1 , t 2 ) with t 1 θ = w 1 and t 2 θ = w 2 . Either u i θ = pθ for some p ∈ comp(t 1 ) X or u i θ ∈ comp(xθ) for some x ∈ comp(t 1 ) ∩ X . In the second case, we have that T x θ ⊢ xθ. Thus T x θ ⊢ u i θ which contradicts the minimality of j, since T x T j . In the first case, we easily deduce that neither u i nor p is a variable or a pair and hence by hypothesis, we have that u i = p. We can apply the induction hypothesis on T j θ ⊢ enc(t 1 , t 2 )θ (this subproof is simple) to obtain that

T ′ i ⊢ enc(t 1 , t 2 ). Now, it t 2 is a variable then t 2 ∈ T ′ i , thus T ′ i ⊢ t 2 .
Otherwise, if t 2 is not a variable then, by induction hypothesis on T j θ ⊢ t 2 θ (this subproof is a simple one), we obtain T ′ i ⊢ t 2 . Hence, in both cases, we obtain that T ′ i ⊢ t 2 . Then, together with T ′ i ⊢ enc(t 1 , t 2 ) and u i ∈ comp(t 1 ), it follows that T ′ i ⊢ u i . For the other decomposition rules the same reasoning holds.

The last rule is a composition. Suppose that it is the symmetric encryption rule. Then u i θ = enc(w 1 , w 2 ) and T j θ ⊢ w 1 and T j θ ⊢ w 2 . Since u i is not a variable, we have that

u i = enc(v ′ 1 , v ′ 2 ), v ′ 1 θ = w 1 and v ′ 2 θ = w 2 . If v ′ 1 (resp. v ′ 2 ) is a variable then v ′ 1 (resp. v ′ 2 ) is in T ′ i (this is because v j ∈ St(T i ))
. Otherwise, we apply our induction hypothesis (note that the two subproofs are simple). Hence, in both cases, we have that

T ′ i ⊢ v ′ 1 and also that T ′ i ⊢ v ′ 2 .
Hence, we easily deduce that T ′ i ⊢ u i . For the other composition rules the same reasoning holds.

Proposition 2 (completeness) Let C be an unsolved constraint system and θ be a solution of C. Then, there is a constraint system C ′ and a solution τ of C ′ such that C σ C ′ and θ = στ .

Proof. Consider the minimal unsolved constraint T i u i . Hence, we have that u i is not a variable whereas u j is a variable for all j < i. Firstly, assume that u i = v 1 , v 2 for some terms v 1 , v 2 . In such a case, let C ′ be the constraint system obtained from C by applying R and τ = θ. Since T i θ ⊢ u i θ, we have also that

T i θ ⊢ v 1 θ and T i θ ⊢ v 2 θ meaning that τ = θ is a solution of C ′ .
Now, assume that u i is neither a variable nor a pair and consider a simple proof of T i θ ⊢ u i θ. According to the last applied rule in this proof, we have:

1. The last rule is a composition.

Suppose that it is the symmetric encryption rule. Hence, there are w 1 , w 2 such that T i θ ⊢ w 1 and T i θ ⊢ w 2 and enc(w

1 , w 2 ) = u i θ. Since u i is not a variable, there ex- ist v 1 , v 2 such that u i = enc(v 1 , v 2 )
. Let C ′ be the constraint system obtained from C by applying the simplification rule R enc on T enc(v 1 , v 2 ). Since v 1 θ = w 1 and v 2 θ = w 2 , the substitution θ is also a solution to C ′ . For the other composition rules the same reasoning holds, applying this time the corresponding R f rule.

INRIA 2.
The last rule is an axiom or a decomposition. Applying Lemma 2 we obtain that there is t ∈ St(T i ) X such that tθ = u i θ. We distinguish two cases: t = u i . Note that u i is neither a pair nor a variable. Since tθ = u i θ and t is not a variable, we easily deduce that t is not a pair. Hence, we can apply the simplification rule R 2 .

t = u i . In such a case, we have that u i ∈ St (T i ). Either there are two distinct non variable and non pair terms t 1 , t 2 ∈ St (T i ) such that t 1 θ = t 2 θ and we apply the simplification rule R 3 . Otherwise, the simplification rule R 1 can be applied. This follows from Lemma 3.

B Proof of our combination result

The left-hand side of a constraint system C, denoted by lhs(C), is the maximal left-hand side of the constraints of C. The right-hand side of a constraint system C, denoted by rhs(C), is the set of right-hand sides of its constraints. The set vars(C) denotes the set of variables occurring in C and ⊥ denotes the unsatisfiable system.

B.1 Existence of a solution without any mixing

Consider a constraint system C issued from Π 1 | Π 2 . The goal of this subsection is to establish the existence of a solution of C having some features (see Proposition 3).

Lemma 4 Let T α and T β be two sets of terms which are respectively α-tagged and β-tagged and such that vars(T α )∩vars(T β ) = ∅. Let C be a constraint system such that lhs(C)∪rhs(C) ⊆ St(T α ∪ T β ). Let C ′ be a constraint system such that C * σ C ′ for some substitution σ. We have that lhs(C ′ )∪rhs(C ′ ) ⊆ St (T α σ ∪T β σ). Moreover, terms in T α σ and T β σ are respectively α-tagged and β-tagged, n(T α σ) ⊆ n(T α ), n(T β σ) ⊆ n(T β ) and vars(T α σ) ∩ vars(T β σ) = ∅.

Proof. This result is easy to prove by induction on the length ℓ of the derivation from C to C ′ . When ℓ = 0, the result is obvious. Now, assume that ℓ ≥ 1. In such a case, we have that there exists C 1 , σ 1 and σ 2 such that C σ 1 C 1 * σ 2 C ′ and σ = σ 1 σ 2 . If the rule involved in the first step is R 1 , R 4 or R 5 , then we easily conclude by applying the induction hypothesis. Now, assume that the simplification rule involved in the first step is either R 2 or R 3 . In such a case, we know that σ 1 = mgu(t 1 , t 2 ) with t 1 , t 2 ∈ St(T α ∪ T β ) Actually, it is impossible that t 1 ∈ St (T α ) and t 2 ∈ St(T β ) (or the converse). Indeed, t 1 , t 2 are neither variables, nor pairs and have to contain the same tag to be unifiable. Hence, we know that t 1 , t 2 ∈ St(T α ) (or t 1 , t 2 ∈ St(T β )). Now, it is easy to see that σ 1 is α-tagged (or β-tagged), thus T α σ 1 (or T β σ 1 ) too. Since vars(T α ) ∩ vars(T β ) = ∅, we have that

T β σ 1 = T β (or T α σ 1 = T α ).
Moreover, it is easy to see that n(T α σ 1 ) ⊆ n(T α ) and n(T β σ 1 ) ⊆ n(T β ). Then, we can apply our induction hypothesis on C 1 * σ 2 C ′ . Putting all together we easily conclude.

RR n 6234

Lemma 5 Let T be a set of ground terms and u be a ground term such that T ⊢ u. Then, we have that plaintext (u) ⊆ plaintext(T ).

Proof. let π be a proof of T ⊢ u. We prove this result by induction on the depth of π. We can have:

The last rule is an axiom. Then u ∈ T and we have that plaintext (u) ⊆ plaintext (T ).

The last rule is a composition. Suppose for example that it is the symmetric encryption rule. Then u = enc(u 1 , u 2 ), T ⊢ u 1 and T ⊢ u 2 . By definition, we have that plaintext (u) = plaintext (u 1 ). Hence, we easily conclude by applying our induction hypothesis on T ⊢ u 1 .

The last rule is a decomposition. Suppose for example that it is the symmetric decryption rule. In such a case, we have that T ⊢ enc(u, v) and T ⊢ v for some term v. By induction hypothesis, plaintext (enc(u, v)) ⊆ plaintext(T ). Hence, we easily conclude that plaintext (u) ⊆ plaintext (T ).

Definition 9 Let C be a constraint system. We say that C satisfies the origination property if the following holds if x ∈ plaintext (T ) ∩ X for some (T u) ∈ C then

T p x def = min{T ′ | (T ′ u ′ ) ∈ C and x ∈ plaintext (u ′ )} exists and T p x T .
Intuitively, this means that when a variable x appears at a plaintext position on the lefthand side of a constraint, then x appears also at a plaintext position on the right-hand side of a smaller constraint (w.r.t. the inclusion ordering of the left-hand sides of the constraints) Proposition 3 Let T 0 and KC be two sets of extended names such that init ∈ T 0 . Let T α and T β be two sets of terms which are respectively α-tagged and β-tagged and such that vars(T α ) ∩ vars(T β ) = ∅ and (plaintext (T α ) ∪ plaintext (T β )) ∩ KC = ∅.

Let C be a constraint system such that lhs(C) ⊆ T 0 ∪ T α ∪ T β , rhs(C) ⊆ T α ∪ T β and which satisfies the origination property. If C is satisfiable, then there exists a solution θ ′ of C such that 1. T α θ ′ is a set of α-tagged terms and n(T

α θ ′ ) ⊆ n(T α ) ∪ {init}, 2. T β θ ′ is a set of β-tagged terms and n(T β θ ′ ) ⊆ n(T β ) ∪ {init}, 3. for all x ∈ plaintext (T α ∪ T β ), we have that plaintext (xθ ′ ) ∩ KC = ∅.

INRIA

Proof. Let T 0 , T α , T β and C be as described in the proposition and let θ be a solution of C. Thanks to our completeness result (Theorem 2), we know that there exists a constraint system C ′ in solved form and a substitution σ such that C * σ C ′ . Let θ ′ = στ where xτ = init for every x ∈ vars(C ′ ). It is clear that θ ′ is a solution of C, it remains to show that θ ′ satisfies the requirements. Thanks to Lemma 4, it is easy to establish that terms in T α σ are α-tagged and also that n(T α σ) ⊆ n(T α ), terms in T β σ are β-tagged and also that n(T β σ) ⊆ n(T β ).

From this, it is easy to establish the two first conditions. terms in T α θ ′ = T α στ are α-tagged and n(T α θ ′ ) ⊆ n(T α ) ∪ {init},

terms in T β θ ′ = T β στ are β-tagged and n(T β θ ′ ) ⊆ n(T β ) ∪ {init}. Now, let V = {x ∈ plaintext (T α ∪ T β ) ∩ X | plaintext (xθ ′ ) ∩ KC = ∅}. If V = ∅, then the condition holds. Otherwise, let x ∈ V such that T p
x is minimal w.r.t. the inclusion ordering (see Definition 9 for the definition of T p x ). Since C satisfies the origination property, there exists (T p x u) ∈ C such that x ∈ plaintext (u) and x ∈ plaintext(T p x ). We have that plaintext(uθ ′ ) ∩ KC = ∅ and thanks to Lemma 5, we deduce that plaintext (T p x θ) ∩ KC = ∅. It is easy to see that plaintext (T p x ) ∩ KC = ∅ since this property holds for T α , T β and T 0 . Hence, we deduce that there exists y ∈ vars(T p x ) such that plaintext (yθ) ∩ KC = ∅ and y ∈ plaintext (T p x ). This means that there exists a variable y ∈ V such that T p y T p x , contradiction.

B.2 Getting rid of the terms coming from Π 2

We define a function, denoted by • , whose goal is to project terms which come from Π 2 (and which are β-tagged) onto a special term init. Given a set Names of names, we define the function • inductively as follows:

u = init if u ∈ Names, u = u if u is a name and u ∈ Names, f ( β, u 1 , u 2 ) = init if f ∈ {enca, enc, sign} f (u 1 , . . . , u n ) = f (u 1 , . . . , u n ) otherwise
Before to prove Lemmas 7 and 8 which will be useful to establish our main result (Proposition 1), we need to show a locality lemma (Lemma 6). This locality lemma relies on the following definition.

Definition 10 (St plain (t)) Let t be a ground term. The set St plain (t) of subterms of t that appear at a plaintext position is inductively defined as follows:

St plain (u) = {u} if u ∈ n(u) St plain (f (u 1 , u 2 )) = {f (u 1 , u 2 )} ∪ St plain (u 1 ) if f ∈ {enc, enca, sign} St plain ( u 1 , u 2 ) = { u 1 , u 2 } ∪ St plain (u 1 ) ∪ St plain (u 2 ).
Lemma 6 (locality) Let T be a set of ground terms and u be a ground term such that T ⊢ u. Let π be a proof of T ⊢ u which is minimal w.r.t. its number of nodes. Then π only involves terms in St(T, u). Moreover, if π ends with an instance of a decomposition rule or an instance of the axiom rule then π only involves terms in St(T ) and u ∈ St plain (T ).

Proof. Let π be a proof of T ⊢ u which is minimal w.r.t. to its number of nodes. We will show the result by induction on π. We can have that:

The last rule is an axiom. In such a case, we easily conclude.

The last rule is a composition. Suppose for example that it is the symmetric encryption rule. In such a case, we have that u = enc(u 1 , u 2 ). Let π 1 (resp. π 2 ) be the subproof of π ending on T ⊢ u 1 (resp. T ⊢ u 2 ). By induction hypothesis, we know that π 1 (resp. π 2 ) only involves terms in St (T, u 1 ) (resp. St (T, u 2 )). Hence, we easily deduce that π only involves terms in St(T, u). The same reasoning holds for the other composition rules.

The last rule is a decomposition. Suppose for example that it is the symmetric decryption rule. In such a case, we have that

π 1 = . . . T ⊢ enc(u, v) π 2 = . . . T ⊢ v T ⊢ u
Note that, by minimality of π, the proof π 1 necessarily ends with a decomposition rule. Hence, by induction hypothesis, we know that π 1 only involves terms in St (T ) and also that enc(u, v) ∈ St plain (T ). Then, we easily deduce that π only involves terms in St(T ) and also that u ∈ St plain (T ). For the other decomposition rules a similar reasoning holds. In the case of the asymmetric decryption rule, we have that v ∈ St(T ) since a term of the form priv(v ′ ) can only be obtained by the axiom rule or an instance of a decomposition rule.

Lemma 7 Let T 0 be a set of extended names and Names be a set of names such that n(T 0 )∩ Names = ∅ and init ∈ T 0 . Let v be a β-tagged term such that plaintext (v) ⊆ T 0 ∪ Names. Then, we have that T 0 ⊢ v.

The proof below relies on the notion of component which is formally defined in Appendix A.

Proof. We will show that for every p ∈ comp(v), we have that T 0 ⊢ p. By definition of • , we have that

{p | p ∈ comp(v)} = {p ′ | p ′ ∈ comp(v)}.
INRIA Then, we easily deduce that T 0 ⊢ p ′ for every p ′ ∈ comp(v), and thus T 0 ⊢ v.

Let p ∈ comp(v). We distinguish three cases:

1. p is of the form enc(w 1 , w 2 ), enca(w 1 , w 2 ) or sign(w 1 , w 2 ). In such a case, since p is β-tagged, we have that p = init, thus T 0 ⊢ p.

2. p is of the form pub(t) (or priv(t)), thus pub(t) ∈ T 0 ∪ Names. We have that p ∈ T 0 and thus p ∈ T 0 since n(T 0 ) ∩ Names = ∅.

3. p is a name. We have that p ∈ plaintext (v) and p ∈ T 0 ∪ Names, thus T 0 ⊢ p. This allows us to conclude.

Remark. The condition T 0 ∩ Names = ∅ is not sufficient to prove Lemma 7. For instance, let v = pub(a), Names = {a} and T 0 = {pub(a)}. We have that v = pub(init) and v is not deducible from T 0 .

Lemma 8 Let T 0 be a set of extended Names and Names be a set of names such that n(T 0 ) ∩ Names = ∅ and init ∈ T 0 . Let T α be a set of α-tagged terms and T β be a set of β-tagged terms such that plaintext (T β ) ⊆ T 0 ∪ Names. Let u be a ground term such that T 0 , T α , T β ⊢ u. Then we have that T 0 , T α , T β ⊢ u.

Proof. By hypothesis, we have T 0 , T α , T β ⊢ u. Let π be a proof of T 0 , T α , T β ⊢ u which is minimal w.r.t. its number of nodes. We will show that T 0 , T α , T β ⊢ u by induction on the proof. We can have that:

The last rule is an axiom. In such a case, we have that u ∈ T 0 ∪ T α ∪ T β . We easily deduce that u ∈ T 0 ∪ T α ∪ T β . This allows us to conclude that T 0 , T α , T β ⊢ u.

The last rule is a composition. Either u = init and we easily conclude. Otherwise, suppose for example that the last rule is the symmetric encryption rule. In such a case, we have that u = enc(u 1 , u 2 ) and u = enc(u 1 , u 2 ). By induction hypothesis, we know that T 0 , T α , T β ⊢ u 1 and T 0 , T α , T β ⊢ u 2 . Hence, we deduce that T 0 , T α , T β ⊢ enc(u 1 , u 2 ), that is T 0 , T α , T β ⊢ u

The last rule is a decomposition. Suppose for example that it is the symmetric decryption rule. In such a case, we have that

π 1 = . . . T 0 , T α , T β ⊢ enc(u, v) π 2 = . . . T 0 , T α , T β ⊢ v T 0 , T α , T β ⊢ u
If u is not of the form β, u 1 for some term u 1 , then by applying our induction hypothesis, we easily conclude since enc(u, v) = enc(u, v). Now, we have to consider the case where u is of the form β, u 1 . By minimality of the proof we know that π 1 ends either with an instance of axiom or with an instance of a decomposition rule. Hence, by Lemma 6, we have that enc(u, v) ∈ St plain (T 0 ∪ T α ∪ T β ). Moreover, since enc(u, v) is β-tagged, we finally deduce that enc(u, v) ∈ St plain (T β ) and hence u ∈ St plain (T β ). Since plaintext(T β ) ⊆ T 0 ∪ Names, we easily deduce that plaintext (u) ⊆ T 0 ∪ Names and Lemma 7 allows us to conclude that T 0 ⊢ u.

For the other decomposition rules, a similar reasoning holds.

B.3 Proof of the Proposition 1

Proposition 1 Let Π 1 = [k 1 ] → Roles, Π 2 = [k 2 ]
→ Roles, T 0 and m defined as in Theorem 1 and satisfying the conditions 1 and 2. Let k = k 1 +k 2 and sc be a scenario for

Π 1 | Π 2 .
For any role number 1 ≤ i ≤ k, let s i ∈ N such that (i, s i ) ∈ sc or ∀j, (j, s i ) ∈ sc. Let C be the constraint system associated to sc, T 0 and mσ 1,s Let C be the constraint system associated to sc, T 0 and m 1 = mσ 1,s 1 • • • σ k,s k . Let sc ′ = sc| Π 1 , i.e. the sequence obtained from sc by removing any element (r, s) where r is a role of Π 2 . Let C ′ be the constraint system associated to sc ′ , T 0 and the term m 2 = mσ 1,s 1 • • • σ k 1 ,s k 1 .

Note that m 1 = m 2 since vars(m) ⊆ vars(Π 1 ). In the remainder, we will denote it by m ′ . For sake of simplicity, we will assume that init ∈ T 0 . The constraint systems C and C ′ are as follows:

C :=            T 0 u 1 T 0 , v 1 u 2 T 0 , v 1 , v 2 u 3 • • • • • • T 0 , v 1 , . . . , v n m ′ C ′ :=            T 0 u i 1 T 0 , v i 1 u i 2 T 0 , v i 1 , v i 2 u i 3 • • • • • • T 0 , v i 1 , . . . , v i n m ′
where i 1 • • • i n is a sequence obtained from 1 • • • n by removing any element j when the j th element, say (r, s), of the sequence sc is such that k 1 < r ≤ k. Intuitively, we remove the elements corresponding to a step of the protocol Π 2 . Now, before to apply Proposition 3, we have to check that all the hypothesis are satisfied. Let T α = {u i 1 , v i 1 , . . . , u i n , v i n , m ′ }, and T β = {u j , v j | 1 ≤ j ≤ n and j ∈ {i 1 , . . . , i n }}.

INRIA

2. 1 Syntax

 1 Cryptographic primitives are represented by function symbols. More specifically, we consider the signature F = {enc, enca, sign, , pub, priv} together with arities of the form ar(f ) = 2 for the four first symbols and ar(f ) = 1 for the two last ones. The symbol represents the pairing function. The terms enc(m, k) and enca(m, k) represent respectively the message m encrypted with the symmetric (resp. asymmetric) key k. The term sign(m, k) represents the message m signed by the key k. The terms pub(a) and priv(a) represent respectively the public and private keys of an agent a. We fix an infinite set of names N = {a, b . . .} among which we distinghuish two particular names init and stop; and an infinite set of variables INRIA X = {x, y . . .}. The set of Terms is defined inductively by

INRIA

2 .

 2 (Completeness) If θ is a solution of C, then there exist a solved constraint system C ′ and substitutions σ, θ ′ such that θ = σθ ′ , C * σ C ′ and θ ′ is a solution of C ′ .

  [START_REF] Abadi | Prudent engineering practice for cryptographic protocols[END_REF]

  • • • σ k,s k . Let sc ′ = sc| Π 1 and C ′ be the constraint system associated to sc ′ , T 0 and mσ 1,s 1 • • • σ k 1 ,s k 1 . If C is satisfiable, then C ′ is also satisfiable. Proof. Let Π 1 : [k 1 ] → Roles, Π 2 : [k 2 ] → Roles, T 0 and m defined as in Theorem 1. Let k = k 1 + k 2 and sc be a scenario for Π 1 | Π 2 . For any role number 1 ≤ i ≤ k, let s i ∈ N such that (i, s i ) ∈ sc or ∀j, (j, s i ) ∈ sc. Let (u 1 , v 1 ) • • • (u n , v n ) bethe sequence of rules associated to sc.

RR n 6234


Cyrine Nasri
email: cyrine.nasri@loria.fr

Kamel Smaïli

Chiraz Latiri
email: chiraz.latiri@gnet.tn

Kamel Smaili
email: smaili@loria.fr

Chiraz Latiri Sma

Training phrase-based SMT without explicit word alignment

Keywords: Statistical Machine Translation, Inter-lingual triggers, Multivariate Mutual Information. 1

come

Introduction

The current best performing statistical machine translation systems are based on phrase-based models: the basic idea of phrase-based translation is to segment the given source sentence into phrases, then translate each phrase and nally compose the target sentence from these phrase translations. It is important to point out that the current phrase-based models are not based on any deep linguistic concept. Interestingly enough, the power of phrase-based translation is due to the quality of the phrase table. State-of-the-art statistical machine translation uses phrases as translation units to incorporate context into translation models, as described in [START_REF] Koehn | Statistical phrase-based translation, Conference of the North American Chapter of the Association for Computational Linguistics on Human Language Technology[END_REF], [START_REF] Zens | Phrase-Based Statistical Machine Translation[END_REF] and [START_REF] Zens | Improvements in Phrase-Based Statistical Machine Translation[END_REF]. There are many ways to acquire such a table. The mostly applied phrase pairs extraction method is the so-called Viterbi Extract [START_REF] Zens | Improvements in Phrase-Based Statistical Machine Translation[END_REF]. In this approach, a source and a target phrase are considered to be translations of each other, if their words are only aligned within this phrase pair and not to the words outside. Collecting phrases and their corresponding translations extracted from all the sentences in the bilingual training corpus, achieves a phrase table with a set of phrase pairs with scores indicating their translation accuracy. The decoder based on log-linear model produces target sentences from left to right by covering the source phrases in a certain order [START_REF] Lavecchia | Discovering phrases in machine translation by simulated annealing Interspeech[END_REF]. The log-linear model uses several features such as relative frequencies of the phrase pairs, a word-based lexicon model, a target language model, a source phrase reordering model, as well as a word and phrase penalty model. Currently, this is the most widely method used for producing phrases and decoding.

Other approaches have been investigated to obtain phrase pairs in less heuristic ways. Zhang in [START_REF] Zhang | Integrated Phrase Segmentation and Alignment Algorithm for Statistical Machine Translation[END_REF] presented an integrated phrase segmentation/alignment algorithm (ISA) for statistical machine translation, which segments and aligns phrases simultaneously. Without training a word alignment model, phrases are identied based on the similarities of mutual information values among word alignment points. Venugopal in [START_REF] Venugopal | Eective Phrase Translation Extraction from Alignment Models[END_REF] presented a technique that begins with an improved IBM models to create knowledge, that represents eectively local and global phrase contexts. Another method proposed by Lavecchia in [START_REF] Lavecchia | Discovering phrases in machine translation by simulated annealing Interspeech[END_REF] retrieves valid linguistic phrases without using any alignments. This method identies rst the best part-of-speech phrases and then from these class phrases, they extracted the corresponding phrases which improve the perplexity of the source language. For instance, noun Pre noun is one of the retrieved part-of-speech phrases and from this pattern and the source corpus a phrase as Table de Salon is extracted. The obtained phrases are linguistically pertinent and consequently the derived phrases are also relevant. These obtained phrases are then used to rewrite the source training corpus in terms of phrases. The words of this phrase are gathered and used to rewrite the source training corpus. In the following, we detail our method which is based on the inter-lingual triggers.

2

Inter-lingual Triggers

Inter-lingual triggers are inspired from triggers concept used in statistical language modeling [START_REF] Tillmann | Lehrstuhl Fur Informatik Vi Word Triggers and the EM Algorithm[END_REF]. A trigger is a set composed of words and its best correlated triggered words in terms of mutual information (MI). In [START_REF] Lavecchia | Using inter-lingual triggers for machine translation[END_REF], the authors proposed to determine correlations between words coming from two dierent languages. Each inter-lingual trigger is composed of a triggering source linguistic unit and its best correlated triggered target linguistic units. Based on this idea, they found among the set of triggered target units, potential translations of the triggering source words. Inter-lingual triggers are determined on a parallel corpus according to mutual information measure namely:

where a and b are respectively a source and a target words. P (a, b) is the joint probabilities and P (a) and P (b) are marginal probabilities.

For each source unit a, the authors kept its k best target triggered units. This approach has been extended to take into account triggers of phrases [START_REF] Lavecchia | Discovering phrases in machine translation by simulated annealing Interspeech[END_REF]. The drawback of this method is that phrases are built in an iterative process starting from single words and joining others to them until the expected size of phrases is reached. In other words, at the end of the rst iteration, sequences of two words are built, the following iteration produces phrase of three words and so on until the stop-criteria is reached. Then, once all the source phrases are built, their corresponding phrases in the target language are retrieved by using n-to-m inter-lingual trigger approach which means that a phrase of n words triggers a phrase of m words [START_REF] Lavecchia | Discovering phrases in machine translation by simulated annealing Interspeech[END_REF]. In order to avoid the propagation of errors due to the cascade of steps in the previous method, we propose a new approach based on multivariate mutual information which allows to retrieve source phrases given target ones.

3

Training phrase with Multivariate Mutual Information Multivariate Mutual Information (MMI) calculates the degree of correlation between n random variables. This concept is very interesting since we propose to take advantage of this principle by associating k words in the source language and r words in the target language with n = k + r.

M M I(A 1 , A 2 , ..., A n ) = P (A 1 , A 2 , ..., A n ) log P (A 1 , A 2 , ..., A n ) P (A 1 )P (A 2 )...P (A n ) (2)
Our method allows creating inter-lingual triggers, their estimation is based on M M I. For instance for the trigger petit déjeuner → breakfast, we proceed as follows: A 1 = petit, A 2 = déjeuner, and A 3 = breakfast. P (A 1 , A 2 , A 3 ) is the probability that the wordspetit, déjeuner and breakfast occur simultaneously. P (A 1 ), P (A 2 ), P (A 3 ) are respectively the probabilities of petit, déjeuner and breakfast.

Selecting phrases in terms of their size

In this work, we started by identifying the longest phrase with their translations and then, the less longest and nally arriving to phrases of two words. This is motivated by the fact that we would like to appreciate the real contribution of each segment without the inuence of its sub-segments. In fact, a long segment is linguistically more informative than a shorter one included into it. The algorithm, we proposed is based on retrieving phrases and their translations by using MMI as described in the following algorithm. For a xed length of a trigger, the concatenation of its words constitute the source phrase. And all the words of its triggered sequence constitute the target phrase. It should be noted, that in this algorithm we suppose that the translation table is from English to French. Now we know that, in most cases for a French sentence, its equivalent in English is shorter. That is why, in the proposed algorithm, for each xed length of phrase, we look for a triggered phrase of the same length or longer by one word. More details are given in [START_REF] Nasri | A new method for learning Phrase Based Machine Translation with Multivariate Mutual Information[END_REF]. This method leads to remarkable triggers where the triggered words could be considered as potential translations of the trigger or very close in terms of meaning. For each source phrase, the 20 best triggers are kept. Table 1 illustrates some examples of obtained French-English triggers. The experiments presented below have been conducted on the proceeding of the European Parliament [START_REF] Koehn | Europarl: A Parallel Corpus for Statistical Machine Translation[END_REF]. We used French-English parallel corpus. Table 2 shows the parallel corpus statistics used in our experiments. So far, we have only discussed how to collect a set of phrase pairs. More is needed to turn this set into a probabilistic phrase translation table. For that, we use the principle proposed in [START_REF] Lavecchia | Discovering phrases in machine translation by simulated annealing Interspeech[END_REF] to compute phrase translation probabilities. The translation table is obtained by assigning for each trigger a conditional probability calculated as follows:

∀f, e i ∈ T rig(f

) P (e i |f ) = M M I(e i , f ) ei∈T rig(f ) M M I(e i , f ) (3)
where Trig(f ) is the set of k English events triggered by the French event f. In table 3, we present the results of OSPD method. S 1 corresponds to word-toword translation and S8 corresponds to a translation using all the discovered phrases. The introduction of phrases of 8, 7 and 6 words improve the results by more than 2 points. This means that long phrases are suitable but not as relevant as the introduction of phrases of 5 words. These phrases bring more than 2.5 in terms of BLEU. But the best improvement is brought by sequence of words of 4,3, and 2 words: more than 4.5! Consequently, all these sequences of dierent sizes are necessary to improve the results. Phrases beyond of 8 words are not relevant. This method has a performance which is 1.1% less than the baseline method. This shows the feasibility to develop machine translation without any word alignment with acceptable results.

4 How to improve this method?

We would like to go further and to achieve results closer to those obtained by the baseline method which needs word alignment. For that, we analyze our method to identify its drawbacks.

Improving by selecting the best phrases

One of the drawback of this method is that we keep for each phrase its 20 best translations. This could include bad translations which would corrupt the results. In fact, the examples given in table 4 are considered as bad translations but unfortunately yet they are in the translation table. In [START_REF] Quirk | Do we need phrases? Challenging the conventional wisdom in Statistical Machine Translation[END_REF] the authors argue that extracting only minimal phrases, i.e the smallest phrases pairs that map each entire sentence pairs, does not degrade performances. By using signicance test, they remove unlikely phrase pairs which reduces the phrase table drastically and may even yield increases in performance [START_REF] Johnson | Improving Translation Quality by Discarding Most of the Phrase table[END_REF]. We propose in the following pruning phrase table by incorporating best translation pairs in terms of MMI without the need of integrating sequences step by step in terms of their length. We will call this method Best-Phrases Discovering (BP). To do that, we extract all the inter-lingual n-to-m-triggers as in [START_REF] Lavecchia | Discovering phrases in machine translation by simulated annealing Interspeech[END_REF] except, that instead of using classical mutual information, we use MMI. Then we sort all the discovered phrases in descending order according to their score. Only triggers that have a MMI greater than a xed threshold are kept. The impact of this selection is positive in terms of BLEU as presented in the evaluation section.

Lexical weights

Lexical weights were proposed in [START_REF] Koehn | Statistical phrase-based translation, Conference of the North American Chapter of the Association for Computational Linguistics on Human Language Technology[END_REF] to validate the quality of alignments. Given a bilingual phrase to score, the objective consists in checking how well each source word translates into the target words it links to. When a source word links to multiple target words, the average of their translation probabilities is calculated. A source-to-target lexical weight is then the product of all scores. The same calculation is done from target to source, and the result is a pair of lexical weights between 0 and 1. Because in our method, we do not proceed to any alignment and because lexical weights is important in Moses, we decided to adapt the classical technique with one major change. As, our method proposes phrases without any initial word-to-word alignments, we estimate a simple lexical translation probability distribution D based on word-to-word triggers [START_REF] Lavecchia | Using inter-lingual triggers for machine translation[END_REF]:

D(w j |w i ) = M I(w j |w i ) M I(w j |w i ) (4)
Where w i is a word in a language i and w j is a word in a language j.

5 Evaluation

In the following, we present several experiments to evaluate the impact of the improvements we proposed in order to boost our initial method. The method is evaluated by comparing it to the baseline one with a rened alignments from Giza++ [START_REF] Och | A Systematic Comparison of Various Statistical Alignment Models[END_REF]. Default set of options is used: 2 translation probabilities, 2 lexical weights and length penalty.

In gure 2, we evaluate the impact of the method based on selecting the best phrases (BP). We can notice that the best performance is achieved for a MMI threshold equal to 9.10 -5 . This curve shows also, if phrases are not selected judiciously, then the degradation of the performance is serious, more than 5 BLEU points are lost. On the Test corpus, the best performance is achieved for a MMI threshold equal to 5.10 -5 (gure 3). Obviously, the only threshold used is the one get on the development corpus which is close to the one get from the test corpus. In this test, we improve slightly the results, the performance reaches a BLEU of 43.82. The results are still bellow the standard one (44.3). To improve our results we combined several translation tables OSPD, BP and the baseline one. This table shows that by combining our two translation tables we are only 0.6% from the baseline method. This result conrms that it is possible to do almost as good as Och method without any word process alignment. By combining BP with the baseline method, we outperform the baseline result by 0.4%. This improvement reachs 0.6% when both translation tables (OSPD and BP) are combined with the baseline one. These last results illustrates that it is possible to improve the baseline translation table by using other phrases and for some of them, they get better scores than those proposed by the baseline one. Furthermore, our best method (BP) uses a smaller (12%) translation table than the baseline. In conclusion, we proposed two methods which do not require any word alignment. These two methods achieve results closer to the baseline method, around 1%, when they are used alone. When they are combined, we approach the baseline system and the dierence is only about 0.6%. The size of the BP translation table is 12% smaller than the baseline one. Then one question may arise, could our community accept a new method of retrieving phrases which does not require any word alignment, getting results closer to the classical one and with a smaller and more cleaned translation table? Besides that, the obtained phrases have an added value since they can enrich those achieved by the baseline method since we have shown that they can improve the reference results

M

  I(a, b) = P (a, b) log P (a, b) P (a)P (b)

Algorithm 1 :

 1 Oriented-Size Phrases Discovering (OSPD) m : maximum size of a source phrase n : maximum size of a target phrase for i = m to 1 do for j = n to 1 do if i = j or i = j+1 then 1. Train triggers model Xi -→ Yj (Xi: source phrase composed of i words, Yj : target phrase composed of j words) 2. Calculate M M I(x1, x2, . . . , xi, y1, y2, ..., yj) as shown in formula 2. 3. Include the retrieved phrases Xi = x1, x2, . . . xi and their best translations Yj = y1, y2, . . . yj into the translation table endif

Fig. 1 .

 1 Fig. 1. Algorithm 1: Oriented-Size Phrases Discovering (OSPD).

Fig. 2 .

 2 Fig. 2. Evolution of Bleu score in terms of MMI threshold on the DEV corpus

Fig. 3 .

 3 Fig. 3. Evolution of Bleu score in terms of MMI threshold on the Test corpus

Table 1 .

 1 Examples of retrieved phrases and their translations.

	French	English	MMI
	autour de la table around the table 0.0054
		around the	0.0022
		the table	0.0011
	a été prise	was taken	0.001
		been taken	0.00037
		has been taken	0.00034
	semaine denière	last week	0.016
		week	0.0095
		last	0.009

Table 2 .

 2 An overview of the experimental material.

	Corpus Sentences English words French words
	Training	0,5M	15M	16,6M
	Dev	1,4 K	14K	13,7K
	Test	500	1153	1352

Table 3 .

 3 Evolution of BLEU in accordance to the length of phrases introduced in the translation table.

	Set Selected Triggers Score BLEU
	S1	1FR -→ 1EN	34.16
	S2	S1 + 8FR	36.32
	S3	S2 + 7FR	36.36
	S4	S3 + 6FR	36.8
	S5	S4 + 5FR	39.58
	S6	S5 + 4FR	41.12
	S7	S6 + 3FR	43
	S8	S7 + 2FR	43.79
		Baseline (Och method)	44.3

Table 4 .

 4 Examples of bad English-French triggers.

	French phrase English phrase MMI ×10 -5
	les droits	human rights
	de l'homme	situation	3.2
	madame	president ladies
	le président	and gentlemen	6
	la semaine	president last
	dernière	week	4.6

Table 5 .

 5 Experiments with dierent models

	System	BLEU
	Baseline	44.3
	OSPD	43.79
	BP	43.82
	OSPD+BP	44.02
	BP+Baseline	44.48
	OSPD+BP+Baseline 44.57

Table 6 .

 6 Size of the dierent translation tables

		Baseline OSPD BP
		33,3 M	51 M 22,9 M
	6	Conclusion