<< . .

( 9)

. . >>

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:

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

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

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

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

Protocol Checker
Dolev-Yao Model Dolev-Yao Model
P, {|·|}K e DY 2-party mutual authentication

Mapping Lemma

UC/Ideal World
UC/Ideal World
p, Fcpke

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

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-

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.

Π ::= begin; statementlist
::= input(SID, RID, PID0 , PID1 , RID2 , ...);
(Store “role”, RID , “name”, PID0 , “name”, PID1 , “name”, PID2 ,...
in local variables MyRole, MyName, PeerName, OtherName2 ,...
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.

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

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

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

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.

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.

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

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

<< . .

( 9)

. . >>

Copyright Design by: Sunlight webdesign