LINEBURG

ńņšąķčöą 5 |

returns, ā„ then nothing is appended to t).

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

with plaintext m, then ādecā, PID, SID , c, m is appended to t. (If Fcpke returns, ā„

then nothing is appended to t).

tracep,A,Z (k, z, r) denotes t upon completion of the protocol execution. Let tracep,A,Z (k, z)

denote the random variable for tracep,A,Z (k, z, r) when r is uniformly chosen. Let tracep,A,Z

denote the probability ensemble {tracep,A,Z (k, z)}kāN,zā{0,1}ā—

Because of the linear manner in which the environment, adversary, and parties are

activated in the UC framework, the order in which new elements are appended to the trace

is unambiguous for a particular tracep,A,Z (k, z, r).

We now deļ¬ne a mapping from concrete traces to symbolic traces. It should be clear

that the mapping will result in a sequence of interactions between parties and the adversary

which resembles a Dolev-Yao trace. The purpose of the subsequent Mapping Lemma is to

prove that a concrete protocolā™s trace maps to a valid Dolev-Yao trace of the corresponding

symbolic protocol with 1 ā’ neg(k) probability.

Deļ¬nition 16 (The mapping from concrete traces to symbolic traces) Let p be a

concrete Fcpke /Fsig -hybrid protocol and let t be a trace of an execution of p with security

parameter k, environment Z with input z, and random input vector r. We determine the

43

mapping of t to a Dolev-Yao trace in two steps. (These steps can be thought of as two

āpassesā on the string t.)

(I.) First, we read through the string t character by character, in order, and inductively

deļ¬ne the following partial mapping f from {0, 1}ā— to elements of the algebra A. (Note that

the patterns in t addressed below may be nested and overlapping. That is, the same substring

may be part of multiple patterns. A pattern is recognized as soon as the last character in

the pattern is read.)

ā¢ Whenever we encounter a pattern of the form ānameā, Ī² for some string Ī² and

f ( ānameā, Ī² )is not yet deļ¬ned then set f ( ānameā, Ī² ) = P for some new symbol

P ā M not in the range of f so far.

ā¢ Whenever we encounter in some event a pattern of the form ārandomā, Ī² for some

string Ī² and f ( ārandomā, Ī² ) is not yet deļ¬ned then set f ( ārandomā, Ī² ) = N for

some new symbol N ā R that is not in the range of f so far.

ā¢ Whenever we encounter a pattern of the form āpidā, PID , āsidā, SID for some

strings PID, SID, and f ( āpubkeyā, PID, SID ) is not yet deļ¬ned, then set

f ( āpubkeyā, PID, SID ) = K for some new K ā KP ub not in the range of f .

ā¢ Whenever we encounter a pattern of the form āpairā, Ī²1 , Ī²2 , then proceed as fol-

lows. First, if f (Ī²1 ) is not yet deļ¬ned then set f (Ī²1 ) = G, where G is the garbage

symbol. Similarly, if f (Ī²2 ) is not yet deļ¬ned then set f (Ī²2 ) = G. Finally, set

f ( āpairā, Ī²1 , Ī²2 ) = f (Ī²1 )|f (Ī²2).

ā¢ Whenever we encounter a pattern of the form āciphertextā, PID, SID , m, c for some

strings PID, SID, m, c, then f is expanded so that f ( āciphertextā, PID, SID , c ) =

{|f (m)|}f ( āpubkeyā, PID,SID ) . (Recall that such a pattern is generated whenever an

encryption call to Fcpke is made. Also, at this point both f (m) and f ( āpubkeyā, PID, SID )

must already be deļ¬ned, since this is an encryption call made by a party running a

simple protocol.)

ā¢ Whenever we encounter a pattern of the form ādecā, PID, SID , c, m , then proceed

as follows. First, if f (m) is not yet deļ¬ned, then set f (m) = G, where G is the garbage

symbol. Next, set f ( ādecā, PID, SID , c ) = {|f (m)|}f ( āpubkeyā, PID,SID ) . (Recall

that such a pattern is generated whenever a decryption call to Fcpke is made. The

44

case where f (m) = G occurs when a ciphertext was not generated via the encryption

algorithm. It includes both the case where the decryption algorithm fails and the case

where the decryption algorithm outputs a message that cannot be parsed by simple

protocols.)

(II.) In the second step, we construct the actual Dolev-Yao trace. Let t = G1 ||G2 || . . . tn

be the concrete trace. Then construct the Dolev-Yao trace t by processing each G in turn,

as follows:

ā¢ If Gi = āinputā, (SID, RID), m , then we ļ¬nd m = f (m), and generate the symbolic

event H = [āinputā, P , m] (where P is the symbolic name of the input recipient).

ā¢ If Gi = āciphertextā, PID, SID , m, c or Gi = ādecā, PID, SID , c, m , then no sym-

bolic event is generated.

ā¢ If Gi = āoutputā, PID, m then Gi is mapped to the symbolic participant event

(f ( ānameā, PID ), output , f (m)).

ā¢ If Gi = āmessageā, PID, m then Gi is mapped to the symbolic participant event

(f ( ānameā, PID ), message , f (m)).

ā¢ If G = āadvā, PID, m , let m = f (m). Then there are two cases:

1. m is in the closure of the symbolic interpretations of the messages sent by the

parties in the execution so far, i.e.

māC m : m = f (m ) and the event āmessageā, PID, m is a prior event in t .

In this case there exists a ļ¬nite sequence of adversary events that produces mi .

Then G is mapped to this sequence of events Hi1 , Hi,2 . . . Hi,n so that the message

of Hi,n ā’1 is mi and Hi,n = [ādeliverā, (i, n ā’ 1), P ] (where P is the Dolev-Yao

name of the concrete participant who received the message from the concrete

adversary).

45

2. Otherwise, m is not in the above closure. In this case, G maps to the Dolev-Yao

event [āfailā, mi ].

The desired result is then to show that if t is the concrete trace of a simple protocol p,

then the mapping of t, t is a valid Dolev Yao trace of the symbolic protocol p. This is the

Mapping Lemma of [16].

Lemma 2 (The Mapping Lemma) Let F denote the ideal functionality Fcpke . For all

simple protocols p, adversaries A, environments Z, and inputs z of length polynomial in the

security parameter k,

Pr t ā traceF (k, z) : t is a valid DY trace for p ā„ 1 ā’ neg(k)

p,A,Z

Weā™ll postpone the Mapping Lemmaā™s proof until Chapter 7 when we will prove the

Mapping Lemma for both public key encryption and digital signatures based on the ideal

function formulations presented in Chapter 5.

3.5 Dolev-Yao Back to UC: DY Mutual Authentication and

F2ma

After a concrete simple protocol has been transformed into a symbolic protocol, we can

determine whether or not the symbolic protocol satisļ¬es a certain criterion. Having done

this, it remains to be shown that the criterion satisfaction implies the meeting of the con-

crete protocolā™s goals. In their paper, Canetti and Herzog consider two diļ¬erent protocol

objectives: mutual authentication and key exchange. We limit our discussion in this thesis

to mutual authentication. They deļ¬ne Dolev-Yao mutual authentication as follows:

Deļ¬nition 17 (Dolev-Yao 2-party mutual authentication) A Dolev-Yao protocol P

provides Dolev-Yao mutual authentication (DY-MA) if all Dolev-Yao traces for P that

include an output message Finished |P0 |P1 |m by participant P0 , where P0 , P1 ā MAdv ,

include also a previous input message Starting |P1 |P0 |m by P1 .

Or, in other words, the party P0 only thinks the protocol has completed successfully if

the party it wants to authenticate with, P1 , believes it is engaged in the protocol instance

with P0 .

46

Functionality F2ma

1. The functionality F2ma begins with a variable Finished set to false.

2. Upon receiving an input (Authenticate, SID, P, P , RID) from some party P, where

RID ā {Initiator, Responder}, do:

(a) If this is the ļ¬rst input (i.e., no tuple is recorded) then denote P0 = P, P1 = P ,

and record the pair (P0 , P1 ).

(b) Else, if the recorder pair (P0 , P1 ) satisļ¬es P = P1 and P = P0 , set Finished to

true.

(c) In either case, send the pair (P, P ), RID to the simulator.

3. Upon receiving from the simulator a request (Output, SID, X), if X is either P0 or P1 ,

and Finished is true then send Finished to X. Else, do nothing.

Figure 3-5: The 2-party mutual authentication functionality

They then showed that for ideal 2-party mutual authentication (Figure 3-5), the follow-

ing holds:

Theorem 3 Let p be a simple two-party protocol. Then p realizes F2ma if and only if the

corresponding symbolic protocol p satisļ¬es Dolev-Yao 2-party mutual authentication

At the end of this chain of protocol transforming, mapping, and constraint proving,

we ļ¬nally have a computationally sound argument that a concrete protocol realizes its

protocol goal as described by an ideal functionality. Using this framework, Canetti and

Herzog describe the process for proving that for protocol p instantiated with IND-CCA2

secure encryption and a suļ¬ciently secure key distribution system, if p satisļ¬es Dolev-Yao

2-party mutual authentication, then p realizes F2ma . Or, in the language of UC traces,

idealF2ma ,S,Z ā execp,A,Z .

47

48

Chapter 4

Analyzing Previous Ideal

Functionality Formulations

Ideal functionalities capture our intuition for how a cryptographic operations should occur.

Armed with an ideal functionality description, we can ļ¬nd concrete schemes and protocols

that securely realize the ideal and use them in protocols secure in the knowledge that they

will behave in a manner weā™d expect. Correctly deļ¬ning an ideal functionality, however,

has proven to be more diļ¬cult than previously thought, as evidenced by the constant revi-

sion of proposed ideal functionalities for seemingly straightforward cryptographic concepts

[12, 18, 16, 17, 6]. In this section we draw attention to an implicit assumption made in

many functionality formulations which leads to undesired behavior, particularly when the

functionality is used in the UCSA framework. We then analyze the current formulations of

ideal public key encryption and digital signature functionalities, identifying properties that

are present but undesired or desired by not present in these formulations.

In particular, the formulation for ideal public key encryption used in [16] (Fpke , Figure

3-3) provides too much power to the adversary, allowing the adversary to learn information

it should not have access to. This over-empowerment was missed when constructing the

UCSA framework and, uncorrected, invalidates the frameworkā™s Mapping Lemma.

The current formulation for ideal signatures (Fsig [15], Figure 4-3) is valid in the envi-

ronment for which it was proposed ā“ one where it is assumed that all signatures generated

are public knowledge. However, when the signature functionality is combined with encryp-

tion functionality, this is not longer true and a diļ¬erent formulation must be deļ¬ned if

49

signatures are to be used in conjunction with other cryptographic primitives in protocol

proving frameworks such as the UCSA framework.

Throughout the chapter, we will illustrate these undesired ideal functionality behaviors

using example protocols. In these examples we employ the following notation for readability

and to avoid ambiguity with Dolev-Yao notation. For public key encryption, we use encA (m)

to denote the ciphertext for message m, encrypted under party Aā™s encryption key. For

digital signatures we use sigA (m) to denote the signature of message m for party Aā™s

veriļ¬cation key.

4.1 Implicit Restrictions on Ideal Realizations

The ideal functionality literature has primarily focused on realizing ideal functionalities

through use of stateless (or āmemorylessā), local algorithms. By āstateless,ā we mean each

algorithm does not maintain state between invocations; by ālocal,ā we mean there is no

direct communication between the invocations of a schemeā™s algorithms (e.g. my instance

of enc does not directly communicate with your instance of dec or even with my own

instance of dec). This focus is often made implicitly and shortchanges the power of the

UC framework ā“ the ability to fully abstract the implementation details of a functionalityā™s

underlying implementation.

If a proof showing a particular security type realizes an ideal functionality assumes the

implementing scheme lacks state and is local, then the results of the proof may not extend

to schemes that do not meet this assumption. For example, a signature scheme where sig

appends all previous signatures to each new signature is still technically EUF-ACMA, but

violates our intuition for how a secure signature scheme should act.1 There has been work

on stateful signature schemes [7, 15], but such papers are less common and, at times, miss

some subtleties of this condition.2

Taking these schemes into consideration is important. In addition to schemes that

purposefully maintain state or use remote input, many schemes which are local and stateless

are used in such a way that introduces state or external input. A real world use of an

1

To see why, consider a protocol where a party A takes a message m, and broadcasts encB (m, sigA (m)).

An adversary (who is not party B) should remain unable to produce Aā™s signature on message m. How-

ever, the moment party A signs some other message m and communicates (m , sigA (m )) in the clear, the

adversary learns the previous signature sig(m)A despite our intuition that it should remain hidden.

2

Canettiā™s [15] formulation of Fsig is, in fact, realizable by EUF-ACMA schemes with state. The problem,

as we shall see in Section 4.3.2, stems from the Fsig formulation itself.

50

encryption or signature scheme might reset its key after some ļ¬xed number of uses. A

protocol might call for encrypted messages to contain a counter that increases with each

message exchanged. A device that holds secret plaintexts may encrypt any message but

only decrypt ciphertexts it generates itself. There is a uniform and intuitive sense of the

security/behavior we expect from any encryption or signature scheme, and deļ¬nitions such

as IND-CCA2 and EUF-ACMA only capture it for local, stateless algorithms. A properly

formulated description of an ideal functionality, however, can serve as a standard for security

expectations, independent of the underlying scheme details.

4.2 Public Key Encryption

In past formulations of Fpke and Fcpke (Figures 3-3 and 3-4), the ideal functionalities have

allowed the adversary to choose the ciphertext strings. Since it was still diļ¬cult for ad-

versaries to decrypt ciphertexts, it was felt that allowing adversaries to choose these values

avoided placing too strong a limitation on concrete schemes realizing the ideal functionality.

Giving the adversary this power means the adversary knows the value of all cipher-

texts generated by protocol participants. As the double encryption protocol in ļ¬gure 4-1

illustrates, this is a problem:

Aā’B: R

A ā B : encA {R, encB {m}}

Figure 4-1: A double encryption protocol

For honest participants A and B, it is clear that a passive adversary watching this

exchange only learns R and encA {R, encB {m}}. However, in an environment with ideal

functionalities (Figure 4-2), a passive adversary learns the values R, encB {m} = c, and

encA {R, encB {m}} = c .

The Fpke ideal functionality does not require any unpredictability of the ciphertext, other

than message independence. This unpredictability is a desired property, it just happens that

its speciļ¬cation is not needed when being realized by stateless encryption schemes. To make

this requirement explicit, we will modify Fpke in Section 5.1 to no longer ask the adversary

for encryption values. Instead, the adversary will provide a randomized algorithm which

51

Aā’B:R

B ā’ Fcpke : (encrypt, m)

Fcpke ā’ Adv : (encrypt, B)

Fcpke ā Adv : (ciphertext, c)

B ā Fcpke : (ciphertext, c)

B ā’ Fcpke : (encrypt, A, (R, c))

Fcpke ā’ Adv : (encrypt, A)

Fcpke ā Adv : (ciphertext, c )

B ā Fcpke : (ciphertext, c )

AāB:c

Figure 4-2: The double encryption protocol, expanded

will be executed to generate values. The adversaryā™s power in this new deļ¬nition is strictly

weaker than in the previous deļ¬nition.

4.3 Signatures and Certiļ¬cation with Encryption

Literature concerning ideal signature functionality has generally limited itself to an envi-

ronment where the signature functionality is the only one present. While determining a

satisfactory formulation in this type of environment is useful, it is merely a precursor to a

more powerful concept of an ideal signature functionality in an environment that includes

other ideal functionalities. Such a formulation would allow security proofs for protocols

involving multiple cryptographic primitives.

Unfortunately, the limited version of ideal signature functionality does not trivially

translate into one suited for coexistence with other ideal functionalities. In this subsection

we describe some of the inadequacies with the current Fsig and derivative Fcert formulations.

4.3.1 Fsig and Fcert

In [14, 15], Canetti presented a revised formulation for ideal signature functionality which

we reproduce in Figure 4-3 with some slight modiļ¬cations for consistency. He showed this

formulation of Fsig is realizable by a concrete signature scheme if and only if the scheme is

EUF-ACMA and could be combined with an ideal certiļ¬cate authority Fca to produce ideal

certiļ¬cation Fcert (Figure 4-4). In these formulations, it is assumed there are no encryption

like ideal functionalities in the environment.

52

Functionality Fsig

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, hand (KeyGen, sid)

to the adversary. Upon receiving (Verification Key, sid, v) from the adversary,

output (Verification Key, sid, v) to S, and record the pair (S, v). v is now the

veriļ¬cation key for S.

Signature Generation: Upon receiving a value (Sign, sid, m) from S,

1. Verify that sid = (S, sid ) for some sid . If not, then ignore the request.

2. Send (Sign, sid, m) to the adversary.

3. Upon receiving (Signature, sid, m, Ļ) from the adversary, verify that no entry

(m, Ļ, v, 0) is recorded. If it is, then output an error message to S and halt.

Else, output (Signature, sid, m, Ļ) to S, and record the entry (m, Ļ, v, 1).

Signature Veriļ¬cation: Upon receiving a value (Verify, sid, m, Ļ, v ) from some

party P , hand (Verify, sid, m, Ļ, v ) to the adversary. Upon receiving

(Verified, sid, m, Ļ) from the adversary do:

1. If v = v and the entry (m, Ļ, v, 1) is recorded, then set f = 1.

2. Else, if v = v, the signer is not corrupted, and no entry (m, Ļ , v, 1) for any Ļ

is recorded, then set f = 0 and record the entry (m, Ļ, v, 0).

3. Else, if there is an entry (m, Ļ, v , f ) recorded, then let f = f .

4. Else, let f = Ļ and record the entry (m, Ļ, v , Ļ).

Output (Verified, id, m, f ) to P .

Figure 4-3: The [14] signature functionality, Fsig .

53

Functionality Fcert

Signature Generation: Upon receiving a value (Sign, sid, m) from S,

1. Verify that sid = (S, sid ) for some sid . If not, then ignore the request.

2. Send (Sign, sid, m) to the adversary.

3. Upon receiving (Signature, sid, m, Ļ) from the adversary, verify that no entry

(m, Ļ, 0) is recorded. If it is, then output an error message to S and halt. Else,

output (Signature, sid, m, Ļ) to S, and record the entry (m, Ļ, 1).

Signature Veriļ¬cation: Upon receiving a value (Verify, sid, m, Ļ) from some party P ,

hand (Verify, sid, m, Ļ) to the adversary. Upon receiving (Verified, sid, m, Ļ) from

the adversary do:

1. If (m, Ļ, 1) is recorded, then set f = 1.

2. Else, if the signer is not corrupted and no entry (m, Ļ , 1) for any Ļ is recorded,

then set f = 0 and record the entry (m, Ļ, 0).

3. Else, if there is an entry (m, Ļ, f ) recorded, then let f = f .

4. Else, let f = Ļ and record the entry (m, Ļ, Ļ).

Output (Verified, id, m, f ) to P .

Figure 4-4: The [14] certiļ¬cation functionality, Fcert .

4.3.2 Adversarial Signature Selection

As with Fcpke , Fsig allows the adversary to select signature values. If signature functionality

exists in an environment with encryption, this leads to the same problem demonstrated in

Section 4.2. A slight modiļ¬cation (Figure 4-5) of our earlier counterexample illustrates this

weakness.

ńņšąķčöą 5 |

Copyright © Design by: Sunlight webdesign