LINEBURG

ńņšąķčöą 4 |

execF

p,S,Z ā execpr ,A,Z

In particular, if p securely realizes functionality G, then so does pr .

This theorem has three important implications:

1. It implies that it is suļ¬cient to analyze the security of a single instance of a protocol.

If a single instance of the protocol securely realizes an ideal functionality, then it will

do so even when combined with other instances of itself or other protocols

2. The realization of ideal functionality G may be a hybrid protocol using other func-

tionalities F. In the context of this thesis, this will be important for showing that a

protocol achieve its goal:

32

Take a protocol goal and describe it as an ideal functionality G. If we want to know

whether or not a concrete protocol p realizes G, then we can analyze if the F-hybrid

version of p, with idealized cryptographic primitives, realizes G. If it does, then that

implies that the concrete p realizes its goals when instantiated with cryptographic

schemes that realize the ideal primitive functionalities.

3. In order for a concrete schemes to securely realize ideal functionality, each scheme must

be reinitialized with new randomness for every new instance of the protocol. This is

a rather onerous requirement since it means all parties must create and distribute

new keys at the beginning of each protocol instance, dramatically increasing protocol

overhead.

We can, however, remove this requirement by (eļ¬ectively) including the protocol

instance SID in each ciphertext (for schemes realizing Fpke ) scheme or signature (for

Fsig , described later) as shown in previous work of universal composition with joint

state [19].

33

34

Chapter 3

Universally Composable Symbolic

Analysis for Public Key Encryption

In 1981, Dolev and Yao proposed their symbolic model for analyzing protocols [22]. In it,

the analyzer thinks of cryptographic primitives as symbolic operations where everything

behaves in an intuitive manner. For example, symbols are unambiguous ā“ a nonce looks

very diļ¬erent from an encryption key which looks diļ¬erent from an entityā™s name. If a

message is encrypted, an entity without the proper key is unable to learn anything about

the messageā™s ciphertext: message length, (potentially) which key encrypted it, whether

the plaintext is the same as another ciphertextā™s, etc. These sorts of assumptions are very

strong and are not trivially satisļ¬able by most cryptographic schemes. Their model became

the foundation for a number of model variants and computational tools, but it wasnā™t until

recently that serious attention was given to reconciling the assumptions of the Dolev-Yao

model with computational cryptography.

In 2000, Abadi and Rogaway ļ¬rst oļ¬ered a way to meaningfully describe the compu-

tational security deļ¬nitions needed to satisfy the behavioral assumptions of cryptographic

primitives in the Dolev-Yao model [3, 4]. Subsequent works [2, 28, 25] have reļ¬ned the tech-

nique of Abadi and Rogaway. The idea is to convert the symbols of the Dolev Yao model

into bit strings using a concrete scheme for the cryptographic primitive in question. The

goal of such a proof is to show that a real world adversary is unable to produce anything

the symbolic adversary is unable to produce. This is done by considering an adversary that,

interacting with the translated bit-string version of a Dolev-Yao exchange, outputs a string

35

corresponding to the translation of a symbol not in the closure of symbolic adversary. Using

the stated security of the scheme used in translation, it is shown that the probability of this

happening, taken over the randomness of the translation and the adversary, is negligible

for all adversaries. This implies real world adversaries interacting with strings using this

scheme are no more powerful than their symbolic counterparts and we say that the scheme

realizes the Dolev-Yao security assumptions for that primitive.

Developing the techniques for translating Dolev-Yao assumptions to computational se-

curity deļ¬nitions was an important ļ¬rst step for creating computationally sound proofs of

protocol security, but it still left some doubt. A concrete scheme may realize the Dolev-Yao

notion of a primitive, but that still didnā™t prove that a protocol deemed āsecureā in the

Dolev-Yao model necessarily achieved a desired computational goal. In addition, the sym-

bolic protocol checkers needed to check the security of protocols in the context of multiple

protocol instances with potential composing issues ā“ perhaps giving further constraints not

originally considered when formulating the realization proof.

With these issues in mind, Ran Canetti and Jonathan Herzog proposed a new framework

for leveraging symbolic analysis of protocols to construct computational proofs of security

[16]. Symbolic analysis is eļ¬ective at automating proof security but suļ¬ers from composing

issues. The universally composable framework has simpliļ¬ed composing issues but still

involves relatively detailed cryptography when attempting to analyze protocols. Canetti

and Herzog layer Dolev-Yao analysis on top of the UC framework in order to capture the

complementary beneļ¬ts of both. This chapter describes their construction which is deļ¬ned

over mutual authentication protocols using public key encryption. In Chapter 7, we will

reconstruct the framework, but for protocols that use both public key encryption and digital

signatures.

The deļ¬nitions presented in this chapter are taken directly from Canetti and Herzogā™s

paper ([16]) with minor modiļ¬cations for clarity.

3.1 Overview

The general idea of the universally composable symbolic analysis framework is to translate

a real world protocol into a symbolic protocol in the Dolev-Yao model where we can then

subject it to automated analysis techniques to prove some symbolic criterion about the

36

Protocol Checker

Dolev-Yao Model Dolev-Yao Model

P, {|Ā·|}K e DY 2-party mutual authentication

Mapping Lemma

Ā§3.5

Ā§3.4

UC/Ideal World

UC/Ideal World

F2ma

p, Fcpke

Ā§3.3

Resulting UCSA proof

Real World

p, S

Figure 3-1: A graphical representation of the UCSA framework

protocol. We then step down through the abstraction levels and show that if the symbolic

protocol meets a symbolic criterion then the real world protocol achieves a real goal.

The protocol is ļ¬rst transformed into a protocol in the Fcpke -hybrid model, where the

use of encryption is replaced by use of ideal encryption functionality Fcpke . Actually, Fcpke

represents the ideal public key encryption functionality (Fpke ) combined with an idealized

key binding functionality since key distribution is implicit in the Dolev-Yao model (i.e. itā™s

just accepted that everyone knows everyone elseā™s public keys). By translating our protocol

into the Fcpke -hybrid model, the framework avoids these key distribution issues.

The Fcpke -hybrid version of the protocol is then translated into a symbolic protocol

in the Dolev-Yao model. In this form, automated tools can analyze the possible symbolic

traces for attacks. This analysis is particularly eļ¬cient in the framework since tools only

need to analyze the correctness of a single protocol instance, thanks to the guarantees of

the UC framework [13, 19]

After proving that the symbolic protocol satisļ¬es a particular symbolic property, it

37

remains to show that the symbolic property implies a real protocol goal. This is done by

showing that an ideal functionality that captures the intuition of the concrete protocolā™s

goal is realized by any Fcpke -hybrid protocol whose DY translation satisļ¬es the symbolic

property. It then follows that the real-world protocol realizes its goal, as described by the

goalā™s idealized functionality description.

3.2 Simple Protocols

As one might imagine, not all protocols are representable in the Dolev-Yao model. In par-

ticular, the translation of a real protocol to a symbolic protocol can only occur if the original

protocol is a āsimple protocol.ā A simple protocol is one where participants are only asked

to perform actions that are the natural analogues of symbolic operation: concatenation,

splitting, nonce generation, encryption, decryption, etc. A protocol that requires an hon-

est party to xor two values together, for example, would not be a simple protocol. The

Needham-Schroeder protocol, before and after Loweā™s ļ¬x, is a simple protocol. This is a

necessary restriction for the universally composable symbolic analysis framework as cur-

rently formulated. While this excludes a number of important protocols, the set of possible

simple protocols is still a rich one. We formally deļ¬ne simple protocols as follows:

Deļ¬nition 13 (Simple protocols) A simple protocol is a pair of interactive Turing ma-

chines (ITMs) {M1 , M2 }, one for each role, where each machine Mi implements an algorithm

described by a pair (Ī£, Ī ):

ā¢ Ī£ is a store, a mapping from variables to tagged values (explained further below) and

ā¢ Ī is a program that expects as input

ā“ The security parameter k,

ā“ Its SID SID, its PID PID, and its RID RID,

ā“ PID1 which represents the name for the other participant of this protocol execu-

tion.

The program tags the input values, binds them to variables in the store, and then acts

according to a sequence of commands consistent with the grammar in Figure 3-2.

38

Ī ::= begin; statementlist

::= input(SID, RID, PID0 , PID1 , RID2 , ...);

begin

(Store āroleā, RID , ānameā, PID0 , ānameā, PID1 , ānameā, PID2 ,...

in local variables MyRole, MyName, PeerName, OtherName2 ,...

respectively.

::=

statementlist statement statementlist

| finish

::=

statement newrandom(v)

(generate a k-bit random string r and store ārandomā, r in v)

| encrypt(v1, v2, v3)

(Send (Encrypt, PID, SID , v2) to Fcpke where v1 = āpidā, PID ,

receive c, and store āciphertextā, c, PID1 , SID in v3)

| decrypt(v1, v2)

(If the value of v1 is āciphertextā, c then send

(Decrypt, PID0 , SID , c ) to Fcpke instance PID0 , SID ,

receive some value m, and store m in v2 Otherwise, end.

| receive(v)

(Receive message, store in v)

| output(v)

(send value of v to local output)

| pair(v1, v2, v3)

(Store āpairā, Ļ1 , Ļ2 in v3, where Ļ1 and Ļ2 are the values of

v1 and v2, respectively.)

| separate(v1, v2, v3)

(if the value of v1 is ājoinā, Ļ1 , Ļ2 , store Ļ1 in v2

and Ļ2 in v3 (else end))

| if (v1 == v2 then statementlist else statementlist

(where v1 and v2 are compared by value, not reference)

::= output( āļ¬nishedā, v ); end.

finish

The symbols v, v1, v2 and v3 represent program variables. It is assumed that āpairā, Ļ1 , Ļ2

encodes the bit-strings Ļ1 and Ļ2 in such a way that they can be uniquely and eļ¬ciently

recovered. A partyā™s input includes its own PID, the PID of its peer, and other PIDs in the

system. Recall that the SID of an instance of Fcpke is an encoding PID, SID of the PID

and SID of the legitimate recipient.

Figure 3-2: The grammar of simple protocols

39

The structure of simple protocols makes it simple to ļ¬nd the Dolev-Yao counterpart to

a simple protocol:

Deļ¬nition 14 (Mapping of simple protocols to symbolic protocols) Let p = {M0 , M1 }

be a simple protocol. Then p is the Dolev-Yao protocol

Pi : S Ć— M Ć— O Ć— A ā’ S Ć— A Ć— message Ć— A Ć— output

that implements ITM M, except that:

ā¢ The variables of M are interpreted as elements of the symbolic message algebra A.

ā¢ Instead of receiving as input SID, PID0 , PID1 , RID, the store is initialized with its own

name P0 , its own key KP0 , and a name P1 and public key KP1 of the other participant.

The symbols P0 and P1 represent PID0 and PID1 , respectively. Similarly, the symbols

K0 and K1 represent PID0 , SID and PID1 , SID , respectively.

ā¢ Instead of creating a new random bit-string, the symbolic protocol returns R(i,n) and

increments n (which starts at 0),

ā¢ Instead of sending (Encrypt, PID, SID , M) to Fcpke and storing the result, the com-

posed symbol {|Ī£(M)|}KP is stored instead (where Ī£(M) is the value bound to the

1

variable M in the store Ī£).

ā¢ Instead of sending (Decrypt, PID0 , SID , C) to Fcpke and storing the result, the value

stored depends on the form of Ī£(C). If Ī£(C) is of the form {|M |}KP then the value

0

M is stored. Otherwise, the garbage value G is stored instead.

ā¢ Pairing and separation use the symbolic pairing operator.

ā¢ Lastly, the bit-strings āstartingā and āļ¬nishedā are mapped to the Dolev-Yao symbols

Starting and Finished , respectively.

3.3 Concrete to UC: Fpke and its Realization

In order to translate a real-world protocol into a F-hybrid protocol, we need to formulate

the ideal functionality used by the protocol then determine what computational security

deļ¬nition realizes it.

40

Proposals for ideal functionality formulations were part of the original description of the

UC framework [13], but, over time, a number of changes and corrections have been made

to these formulations in conjunction with an increased understanding of the security needs

for schemes realizing these functionalities [18, 6, 16, 15].

Canetti and Herzog present a revised formulation of Fcpke (Figure 3-4) which implies

the formulation of Fpke given in Figure 3-3.

Functionality Fpke

Fpke proceeds as follows over message domain {0, 1}ā—. The SID is assumed to consist of a

pair SID = (PIDowner , SID ), where PIDowner is the identity of a special party, called the

owner of this instance.

Key Generation: Upon receiving a value (KeyGen, sid) from some party S, verify that

sid = (S, sid ) for some sid . If not, then ignore the request. Else, do the following:

1. Hand (KeyGen, sid) to the adversary.

2. Receive a value e from the adversary and hand it to S. If the adversary has

not already done so, it also provides the description of deterministic polytime

algorithm D.

Encryption: Upon receiving a value (Encrypt, SID, e , m) from a party P proceed as follows:

1. If m ā D then return an error message to P.

/

2. If m ā D then

ā¢ If e = e , hand (Encrypt, SID, P) to the adversary. Else, hand

(Encrypt, SID, e , m, P) to the adversary.

ā¢ Receive a tag c from the adversary, record the pair (c, m), and hand c to

P. (If c already appears in a previously recorded pair then return an error

message to P.)

Decryption: Upon receiving a value (Decrypt, SID, c) from the owner of this instance, pro-

ceed as follows. (If the input is received from another party then ignore.)

1. If there is a recorded pair (c, m), then hand m to P.

2. Otherwise, compute m = D(c), and hand m to P.

Figure 3-3: The [16] public-key encryption functionality, Fpke

This formulation of Fpke is a variation on the one given by Canetti, Krawczyk, and

Nielsen [18] which they proved to be securely realizable by a concrete public key encryption

scheme if and only if the scheme is IND-CCA2. As we shall in Chapter 4, this formulation

of Fpke is also somewhat ļ¬‚awed, particularly for use in the framework being constructed.

This ļ¬‚aw will provide motivation for the redeļ¬ning of the functionality in Chapter 5.

41

Functionality Fcpke

Fcpke proceeds as follows, when parameterized by message domain D. The SID is assumed

to consist of a pair SID = (PIDowner , SID ), where PIDowner is the identity of a special party,

called the owner of this instance.

Initialization: Expect the ļ¬rst message received from the adversary to contain a descrip-

tion of a deterministic polytime algorithm, D.

Encryption: Upon receiving a value (Encrypt, SID, m) from a party P proceed as follows:

1. If m ā D then return an error message to P.

/

2. If m ā D then

ā¢ Hand (Encrypt, SID, P) to the adversary. (If the owner of this instance of

Fcpke is corrupted, then hand also the entire value m to the adversary.)

ā¢ Receive a tag c from the adversary, record the pair (c, m), and hand c to

P. (If ciphertext already appears in a previously recorded pair then return

an error message to P.)

Decryption: Upon receiving a value (Decrypt, SID, c) from the owner of this instance, pro-

ceed as follows. (If the input is received from another party then ignore.)

1. If there is a recorded pair (c, m), then hand m to P.

2. Otherwise, compute m = D(c), and hand m to P.

Figure 3-4: The [16] certiļ¬ed public-key encryption functionality, Fcpke

3.4 UC to Dolev-Yao: The Mapping Lemma

In order to be sure protocol execution and adversarial actions are the same in both the UC

and Dolev-Yao worlds, we need a way of describing the messages exchanged as well as the

meaningful internal states of participants. As youā™ll recall, in Section 2.3.2 we described

the outcome of a symbolic protocol execution with the symbolic trace. We now deļ¬ne an

analogue: the concrete protocol trace. Note that per our discussion in Section 3.1, this

deļ¬nition uses ideal functionality Fcpke rather than Fpke .

Deļ¬nition 15 (Traces of concrete protocols) Let p be a F-hybrid protocol. Inductively

deļ¬ne tracep,A,Z (k, z, r), as the trace of protocol p in conjunction with adversary A and

environment Z with inputs z, r, and security parameter k. Initially, the trace is the null

string. The trace then grows as the protocolā™s execution progresses.

ā¢ If the environment provides input m to a party with id (SID, RID), then

āinputā, (SID, RID), m is appended to the end of t.

ā¢ If the adversary provides input m to a party with id PID, then āadvā, PID, m is

42

appended to the end of t.

ā¢ If a party PID generates a new random string r, then ārandomā, r is appended to t.

ā¢ If a party pairs values m1 and m2 to form (m1 , m2 ), then āpairā, m1 , m2 is appended

to t.

ā¢ If a party PID writes a message m, it does so in one of two ways

ā“ if it writes m on its local output tape, then āoutputā, PID, m is appended to t.

ā“ if it writes m on its outgoing communication tape, then āmessageā, PID, m is

appended to t.

ā¢ If Fcpke is activated by party PID with call (Encrypt, PID, SID , m) and Fcpke responds

ńņšąķčöą 4 |

Copyright © Design by: Sunlight webdesign