# «Safely composing security protocols V´ronique Cortier · St´phanie Delaune e e Received: date / Accepted: date Abstract Security protocols are ...»

Formal Methods in System Design manuscript No.

(will be inserted by the editor)

Safely composing security protocols

V´ronique Cortier · St´phanie Delaune

e e

Received: date / Accepted: date

**Abstract**

Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the

security of a protocol in the presence of an active attacker that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols are executed, possibly sharing some common keys like public keys or long-term symmetric keys.

In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication.

Keywords composition · security protocols · veriﬁcation 1 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 security protocols is diﬃcult 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 ´ This work has been partly supported by the RNTL project POSE and the ARA SSIA Formacrypt.

V´ronique Cortier e LORIA, CNRS & INRIA project Cassis, Nancy, France E-mail: cortier@loria.fr St´phanie Delaune e LORIA, CNRS & INRIA project Cassis, Nancy, France LSV, CNRS & INRIA project Secsi & ENS de Cachan, France E-mail: delaune@lsv.ens-cachan.fr 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 [38], and decidable for an unbounded number of sessions under some additional restrictions (e.g. [27, 3, 11, 18, 40]).

Many tools have also been developed to automatically verify cryptographic protocols (e.g. [10, 7, 33, 41, 39, 24]). Of course, considering formal models require the use of abstract models that rules out some practical attacks. Recently, a new line of research is aiming at obtaining higher guarantees using formal approaches (see e.g. [2, 8]).

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 are executed, possibly sharing some common keys like public keys or long-term symmetric keys. The interaction with the other protocols may dramatically damage the security of a protocol. Consider for example the two following naive protocols.

A → B : {Na }pub(B)

**P2 :**

A → B : {s}pub(B)

**P1 :**

B → A : Na In protocol P1, the agent A simply sends a secret s encrypted under B’s public key. In protocol P2, 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 P1 executed alone easily guarantees the secrecy of s, even against active adversaries, the secrecy of s is no more guaranteed when the protocol P2 is executed. Indeed, an adversary may use the protocol P2 as an oracle to decrypt any message. More realistic examples illustrating interactions between protocols can be found in e.g. [30].

however, most protocols currently make use of diﬀerent keys. In this paper, we provide a simple criteria for safely composing protocols that share keys.

The idea of adding an identiﬁer in encrypted messages is not novel. It follows the spirit of the rules proposed in the paper of Abadi and Needham on prudent engineering practice for cryptographic protocols [1] (Principle 10). The use of unique protocol identiﬁers is also recommended in [30, 14] and has also been used in the design of fail-stop protocols [28]. However, to the best of our knowledge, it has never been proved that it is suﬃcient for securely executing several protocols in the same environment. Note that some other results also use tags for diﬀerent purposes. For instance, Blanchet uses tags to exhibit a decidable class [11] but his tagging policy is stronger since any two encrypted subterms in a protocol have to contain diﬀerent tags. Following our approach, Delaune et al. have recently showed [26] that tagging hashes enable to preserve resistance against guessing attacks under composition.

Related work. A result closely related to ours is the one of Guttman and Thayer [29].

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 diﬀerent. 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 diﬀerence with our result is that this hypothesis has to hold not only on the protocol speciﬁcation but also on any valid ′ execution of the protocol. In particular, considering again the protocol P2, 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 identiﬁer.

A more detailed comparison can be found in Section 5.1.

Another result has been recently obtained by Andova et al. for a broader class of composition operations [4]. Their result do not allow one 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 ciphertext forwarding, that is, when agents have to forward unknown message components.

Datta et al. (e.g. [25]) have also studied secure protocol composition in a 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 componentbased design of protocols.

Our work is also related to those of Canetti et al. who study universal composability of protocols [12] in a diﬀerent context (cryptographic model). They consider composition in a broader sense than our composition result. Indeed, they both enable composition of a protocol with arbitrary other protocols and composition of a protocol with copies of itself. However, in the initial approach [12], they do not allow shared data between protocols, meaning that new encryption and signing keys have to be generated for each component. Composition theorems that allow joint states between protocols are proposed in further work (see e.g. [15, 9, 13]). Several limitations on the applicability of the results are listed in a recent paper of K¨ sters u and Tuengerthal [31]. In [31], the authors propose a new construction for a joint state theorem in the context of asymmetric encryption and signature (no symmetric encryption nor hash as in our formal model). This result allows in particular to compose a protocol with arbitrary protocols using the same kind of construction: they add an identiﬁer in each encryption.

A preliminary version of our results has been presented at FSTTCS’07 [22].

However, in the conference version we prove composability for tagged protocols and secrecy property only. We now consider a weaker hypothesis (non uniﬁable encrypted messages) and a much larger class of security properties.

Plan of the paper. After some preliminaries (Section 2), we describe the model of protocols in Section 3. In Section 4, we deﬁne the logic of security properties for which our composition result holds. Then, in Section 5, we formally state our composition result (Theorem 1) providing examples and discussion. The remaining of the paper is devoted to the proof of this composition result by relying on constraint solving techniques. We ﬁrst show in Section 6 that we can control the form of minimal attacks. Actually, this result is of independent interest since we provide a decision procedure for solving constraint systems which is more eﬃcient than the one proposed in [23]. Then we explain in Section 7 how to simplify the formula representing the security properties. The ﬁnal proofs are in Section 8. To ease the understanding of the result, we postpone some of the proofs in the Appendix.

2 Messages and Intruder Capabilities

2.1 Syntax

We write vars(t) (resp. names(t), agents(t)) for the set of variables (resp. names, agents) occurring in t. A term is ground if and only if it has no variable. We write St(t) for the set of subterms of a term t. For example, let t = enc( a, b, k), we have that St(t) = {t, a, b, a, b, k}, vars(t) = ∅, names(t) = {k}, agents(t) = {a, b}. These notions are extended as expected to sets of terms. Extended names are names, agents or terms of the form priv(a). The set of Extended names associated to a term t, denoted n(t), is

** n(t) = names(t) ∪ {a, priv(a) | a ∈ agents(t)}.**

For example, we have that n(enc(n, a)) = {n, a, priv(a)}. Substitutions are written σ = {x1 → t1,..., xn → tn } with dom(σ) = {x1,..., xn }. The substitution σ is closed if and only if all the ti are ground. The application of a substitution σ to a term t is written σ(t) or tσ. Two terms t1 and t2 are uniﬁable if t1 σ = t2 σ for some substitution σ, otherwise there are non-uniﬁable. Lastly, we assume a set P of predicates together with their arities.

**2.2 Intruder capabilities**

The ability of the intruder is modeled by a deduction system described in Figure 1 and corresponds to the usual Dolev-Yao rules. The ﬁrst line describes the composition rules. The two last lines describe the decomposition rules and the axiom. Intuitively, these deduction rules say that an intruder can compose messages by pairing, signing, hashing, encrypting 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 veriﬁcation 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 (Veriﬁcation)

** T ⊢ sign(u, 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 deﬁned 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.

Example 1 The term k1, k2 is deducible from the set T1 = {enc(k1, k2 ), k2 }. A

**proof of T1 ⊢ k1, k2 is:**

Fig. 1 Intruder deduction system.

3 Models for security protocols In this section we give a language for specifying protocols and deﬁne their execution in the presence of an active adversary.

3.1 Syntax We consider protocols speciﬁed in a language 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 deﬁned by a role describing a sequence of events. The main events we consider are communication events (i.e. message receptions and message transmissions) and new events to model random numbers generation. To be able to specify a large class of security properties (a logic of properties is given in Section 4), we also consider status events. Those events are issued by participant to denote their current state in the execution of a protocol role.

**Deﬁnition 1 (event) An event is one of the following:**

– a communication event, i.e. a message reception, denoted by rcv(m) or a message transmission, denoted by snd(m), where m is a term; or – a new event, denoted by new X where X is a variable; or – a status event of the form P (t1,..., tn ) where each ti is a term (not necessarily ground) and P ∈ P is a predicate symbol of arity n.

Typically status events give information about the state of the principal. For instance, we will consider a status event that indicates that the principal has started or ﬁnished an execution. The set of variables of an event is deﬁned as expected, considering all the terms occurring in the event’s speciﬁcation.

Deﬁnition 2 (roles) A role is a ﬁnite sequence of events e1 ;... ; eℓ such that

1. for any sent or status event ei, for any variable x ∈ vars(ei ), we have that x ∈ 1≤ji vars(ej ), and

2. a variable occurring in a new event does not appear previously in the sequence.

The length of a role is the number of events in its sequence.