FREE ELECTRONIC LIBRARY - Thesis, dissertations, books

Pages:   || 2 | 3 | 4 | 5 |   ...   | 7 |

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

-- [ Page 1 ] --

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


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 · verification 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 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 ´ 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 different keys. In this paper, we provide a simple criteria for safely composing protocols that share keys.

The idea of adding an identifier 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 identifiers 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 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 [11] but his tagging policy is stronger since any two encrypted subterms in a protocol have to contain different 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 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 not only on the protocol specification 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 identifier.

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 different 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 identifier 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 unifiable 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 define 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 first 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 efficient than the one proposed in [23]. Then we explain in Section 7 how to simplify the formula representing the security properties. The final 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 unifiable if t1 σ = t2 σ for some substitution σ, otherwise there are non-unifiable. 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 first 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 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 (Verification)

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 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.

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 define their execution in the presence of an active adversary.

3.1 Syntax We consider protocols specified 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 defined 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.

Definition 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 finished an execution. The set of variables of an event is defined as expected, considering all the terms occurring in the event’s specification.

Definition 2 (roles) A role is a finite 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.

Pages:   || 2 | 3 | 4 | 5 |   ...   | 7 |

Similar works:


«1 Screen Acting and the New Hollywood: An Interview with Ethan Hawke Gary Bettinson, Lancaster University Years ago Warren Beatty asked me for a meeting. He said something that I really took to heart, that if you can stay true to yourself regardless of the fashion of the times, eventually your way of thinking will come back in fashion again. He said the problem is that people who are always chasing the fashion are always slightly behind. Whereas if you just decide, whatever your course is, to...»

«21. Compliment Responses on Twitter Among Male And Female Celebrities Siti Yuhaida Aniiqah Binti Mohd Yusof and Tan Bee Hoon Centre of English Language Studies Institut Profesional Baitulmal 55100, Kuala Lumpur, Malaysia e-mail: ABSTRACT This study illustrates how compliment responses strategies differ across gender among celebrities in Malaysia. The objective of the study is to identify the patterns and strategies of compliment responses across gender among celebrities on twitter. Forty...»

«[ CH A P T E R T W E N T Y-T WO ] THE WHITMAN MASSACRE B oth the immigrant’s covered wagon and the Indian’s lodge or tepee were to be seen at Waiilatpu in late November 1847. How symbolic! The one brought the aggressive white people, skilled in the arts and crafts of their civilization; the other sheltered members of a proud race, still clinging to many of their age-old customs. In between these symbols was the Whitman mission. Whitman, realizing that the Indians would have to make an...»

«OSHA 3173-09R 2015 Este folleto presenta un panorama de los temas básicos relacionados con la Administración de Seguridad y Salud Ocupacional (OSHA, por sus siglas en inglés) y su funcionamiento. La información proporcionada no determina las responsabilidades relativas al cumplimiento impuestas por las normas institucionales o por la Ley de Seguridad y Salud Ocupacionales de 1970 (la Ley OSH). Puesto que las formas de interpretación y las políticas de aplicación de las normas pueden...»

«AETIAPTAMEHT OEPA3OB AHITfl TOPOAA MOCKBbI CT OqHOE OKPY}ITHOE YIIPABJIEHI,IE OEPA3 OB AIglPIfl BO TOCyAAPCTBEHHOE EIOAXETHOE OEPA3OBATEJTbHOE yrrpE)KAEHT{E IOPOAA MOCKBbI IIIMHA3VIfl Ng 2072 !npercrop OTIIET rro pe3yJrbTaTa M CaMOO6CJreAOBaHrrfl rocyqapcrBeHHoro 6ro4xeruoro odpa3oBareJrbHoro yqper(AeHuq rr{MHa3rrtr Ng 2072 Mocrcna, 2014 roa СОДЕРЖАНИЕ № Содержание Стр. Организационно-правовое обеспечение 3-8...»

«Northern Ireland Theatre Association response to the CAL Inquiry into Inclusion in the Arts of Working Class Communities March 2014 1. Background to the Northern Ireland Theatre Association (NITA) NITA is the representative body for professional theatre in Northern Ireland. Its activities are designed to build capacity and strengthen professional theatre infrastructure across Northern Ireland. It:  Promotes Northern Irish theatre on a local, national and international scale on behalf of its...»

«LIBER SAMEKH Theurgia Goetia Summa (Congressus cum Daemone) Sub figura DCCC 1 ЗВЕРЬ 666 использовал этот Ритуал для достижения Познания и Собеседования со своим Священным Ангелом-Хранителем на протяжении полугода, отведенного на проведение Операции Священной Магии АБРАМЕЛИНА-МАГА. (Ритуал составлен...»

«The City of Newcastle Agreement City of Newcastle Enterprise Agreement PO Box 489 (282 King Street) NEWCASTLE NSW 2300 Ph 02 4974 2000 Fax 02 4974 2222 Email mail@ncc.nsw.gov.au www.newcastle.nsw.gov.au City of Newcastle Enterprise Agreement 2010 PART A 1 Arrangement This Agreement is arranged as follows: Clause Subject Matter 1 Arrangement 2 Statement of Intent 3 Anti-Discrimination 4 Definitions 5 Skill Descriptors 6 Rates of Pay 7 Salary System 8 Use of Skills 9 Payment for Relief Duties /...»

«Radiation Physics Division 46110C RPD-P-06 ABSORBED-DOSE -TO-WATER CALIBRATIONS FOR IONIZATION CHAMBERS Purpose The purpose of this document is to describe the setup, measurement and reporting procedures for absorbed-dose-to-water calibrations. Scope The measurement service described in this document is listed as NIST service code 46110C. The procedure covers the absorbed-dose-to-water calibration of ionization chambers in a 60Co beam1 that is traceable to the NIST water calorimeter2. All...»

«4 Geochemical Modelling of Secondary Calcite Formation and Its Composition in Deep Saline Groundwaters – Case Study: Sellafield Adrian Bath and David Noy This section describes the work carried out for WP4 of PADAMOT by UK partners Intellisci and British Geological Survey (BGS). The work comprised the simulation of hydrogeochemical processes that are involved in the precipitation of late-stage secondary calcite. Simulations were carried out using batch-reaction modelling with the geochemical...»

«A map of social enterprises and their eco-systems in Europe Executive Summary Employment, Social Affairs and Inclusion A map of social enterprises and their eco-systems in Europe European Commission Contract Number: VC/2013/0339 under the Multiple Framework Contract for the provision of evaluation and evaluation related services to DG Employment, Social Affairs & Inclusion including support for impact assessment activities (VT 2008/087) Lot 1 Executive Summary December 2014 A map of social...»

<<  HOME   |    CONTACTS
2016 www.dis.xlibx.info - Thesis, dissertations, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.