<< . .

( 9)

. . >>

We now de¬ne what it means for a party to engage in a symbolic protocol. A party running
a protocol in the Dolev-Yao model consists of the following components:

• An identity (represented by a symbol from M).

• A role in the protocol (either Initiator or Responder)

• An internal state “ we represent the party™s internal state as all messages received in
execution so far.

• An input port from which the party receives its initial input and state

• A communications port that the party uses to send and receive messages in A.

• A local output port where the party can output elements in A.

A protocol in the Dolev-Yao model is then de¬ned as a set of actions performed by
parties, based on their identity, role, internal state, and an incoming message.

De¬nition 9 (Symbolic Protocol) A symbolic protocol P is a mapping from states (S =
A— ), identities (M), roles (O), and messages (A, the incoming message) to a new state (S,
the old state plus the new message) plus an algebra value sent as a message (A — message)
and/or a value given as a local output (A — output). More formally, P is:

P : S — M — O — A ’ S — A — message — A — output

When a party terminates, it is set to a special state that only transitions to itself and
only outputs ⊥.

Technically there are no constraints on the messages that parties are asked to output “
this means we can de¬ne a symbolic protocol where a party is asked to output a message
that is not derivable from its internal state. These protocols are not particularly useful,
so we will only consider protocols that are derived from e¬ciently implementable protocols
(see Section 3.2). Intuitively, if we think of a closure operation C [S ] which is de¬ned in
terms of an honest party instead of the adversary, we can think of these good protocols as
ones where a party™s outputs during protocol execution must be within the closure of the
party™s internal state.

Dolev-Yao protocol trace

When a symbolic protocol is executed, the participants start with an internal state, then
respond to messages delivered by the adversary who can produce any message in the clo-
sure of its knowledge (which includes all messages communicated by participants). When
describing a protocol execution, we want to capture this initial state and the messages ex-
changed, as well as the internal operations performed by the adversary to produce messages
not explicitly communicated by honest participants. We call this description the Dolev-Yao
trace of the protocol execution.

De¬nition 10 (Dolev-Yao Trace) We inductively de¬ne a Dolev-Yao trace t for protocol
P as a description of events that occur during the execution of P.

t = H0 H1 H2 ... Hn’2 Hn1 Hn

where event Hi is either

• of the form [“input”, P, oi , P , S ], which indicates the initial input of participant P to
take the role oi and interact with participant P , assuming initial internal state S .

• an adversary event (where j, k < i) of the form

“ [“enc”, j, k, mi ], in which case mk ∈ KP ub and mi = {|mj |}mk ,
“ [“dec”, j, k, mi ], in which case mk ∈ KAdv , and mj = {|mi |}mk ,

“ [“pair”, j, k, mi ], in which case mi = mj |mk

“ [“extract-l”, j, mi ], in which case mj = mi |mk for some mk ∈ A,

“ [“extract-r”, j, mi ], in which case mj = mk |mi for some mk ∈ A,

“ [“random”, mi ], in which case mi = R for some R ∈ RAdv ,

“ [“name”, mi ], in which case mi = A for some A ∈ M,

“ [“pubkey”, mi ], in which case mi = K for some K ∈ KP ub ,

“ [“deliver”, j, Pi ], in which case the message mj is delivered to party Pi .

• or a participant event of the form [“output”, Pi , mi ] or [“message”, Pi , mi ], in which
case [“deliver”, k, pi ] is the most recent adversary event in the trace (for some k) and

the protocol action for Pi in its current role and internal state, upon receiving mk , is
to output/send message mi . ( P(Sj , oi , mk , Pi ) ’ (Si , mi , {output, message}) ).

2.3.3 Example: Needham-Schroeder Protocol

The classic example for illustrating the need and power of formal models is the Needham-
Schroeder protocol (Figure 2-4). Formally, we can de¬ne this protocol as the symbolic

A’B: {|A, RA |}K e

A ← B : {|RA , RB |}K e

A’B: {|RB |}K e

Figure 2-4: The Needham-Schroeder protocol (informally)

protocol PN S seen in Figure 2-5.
The purpose of this protocol is two-fold. Firstly, it functions as a way to exchange
secret numbers “ the two parties engaged in the protocol should be the only ones to learn
the values RA and RB . Secondly, the protocol attempts to provide authentication: at the
end of a successful protocol run, both parties should know each other™s identity, that they
are engaged in this protocol with each other, and what the values of RA and RB are.
This protocol was proposed in 1978 [30]. Seventeen years later, Lowe discovered and
repaired a ¬‚aw in the protocol™s satisfaction of the authentication conditions [26]. In Lowe™s
attack (Figure 2-6), A begins a protocol run with a malicious entity M . M then, posing as
A, begins a protocol run with B and convinces B that it is interacting with A.
At the end of this attack, B believes it is interacting with A but A believes it is in-
teracting with M . Lowe™s ¬x was to include the responder™s name in the second message,
making it

A ← B : {|B, RA , RB |}KA

Lowe then used a model checker to prove that no other attacks of a similar nature
were possible [27]. His attack illustrates the types of vulnerabilities that might be present
in a protocol but may be di¬cult to discover unless the underlying implementations of
cryptographic primitives are abstracted out.

Let DP represent the initial input/state of party P , let — denote a wildcard which
can be used to match anything, and let P be a place holder for the party identity
each party thinks it is engaged with. We de¬ne PN S to be the mappings:

• {DA } — A — Initiator — {} ’

{DA ∪ {RA }} — {|A|RA |}K e — message — Starting|A|P |KP — output

• {DA ∪ {RA }} — A — Initiator — {|RA |RP |}K e ’

S ⊥ — {|RP |}K e e
— message — F inished|A|P |KP — output

• {DB } — B — Responder — {|P |RP |}K e ’

{DB ∪ {RP , RB }} — {|RP |RB |}K e — message — Starting|B|P |KP — output

• {DB ∪ {RP , RB }} — B — Responder — {|RB |}K e ’

S ⊥ — F inished|B|P |KB — output

• S⊥ — — — — — — ’

S — — ⊥ —output

Figure 2-5: The Needham-Schroeder symbolic protocol, PN S

2.3.4 Strengths and Weaknesses of Symbolic Analysis

As the Section 2.3.3 example illustrates, abstracting cryptographic primitives to intuitive
symbolic operators allows high level analysis which can identify protocol vulnerabilities
that might be missed otherwise. An important byproduct of these formal analysis methods
is the ability to create protocol checkers which can automate the task of searching for
vulnerabilities (e.g. [9, 32, 29]).

While useful, formal method proofs are not rigorous. Symbolic analysis ignores the
details of how cryptographic primitives are realized or information the adversary may learn
outside of applying the closure operations. For example, most symbolic analysis tools do not
include exponentiation as a closure operation. Thus, if a protocol involves the transmitting
of values g and a, then uses the value ga , the model would not capture the fact that the

A ’ M : {|A, RA |}K e
M (A) ’ B : {|A, RA |}K e
M (A) ← B : {|RA , RB |}K e
A ← M : {|RA , RB |}K e
A ’ M : {|RB |}K e
M (A) ’ B : {|RB |}K e

Figure 2-6: Attacking the Needham-Schroeder protocol

adversary also knows ga . It is di¬cult to introduce exponentiation to these models since
many protocols rely on exponentiation properties that violate the freeness of the model™s
algebra (e.g. commutativity, (ga )b = (gb )a ).

In addition, the way primitives are used makes implicit assumptions about the security
of the concrete schemes implementing these cryptographic primitives. Looking back on
our symbolic rules for public key encryption, it is not hard to see that a scheme that
realizes encryption as the model uses it must be quite strong, at least IND-CCA2 secure
(indistinguishable against chosen ciphertext attack, 2 phases. See Section 2.2.1). Unless
a scheme with proper security characteristics is used when implementing these protocols,
proofs given in a formal model are incomplete at best.

By removing the details of cryptographic primitives, formal cryptography gives protocol
designers insight into protocol vulnerabilities that would be di¬cult to see otherwise. This
abstraction, however, is made with few or no restrictions or justi¬cations, weakening any
security guarantees one might wish to assert about the protocol.

2.4 The Universally Composable Security Framework

The universally composable (UC) secure framework [13] creates a model for analyzing pro-
tocol security by replacing cryptographic primitives and protocol goals with ideal function-
alities. Here we present an informal overview of the UC framework, focusing on concepts
that will be relevant for later sections of this thesis; we ¬rst describe how parties and pro-
tocols are modeled in the framework, then how these ideal functionalities work. Finally we
explain what it means for a protocol to securely realize an ideal functionality.

2.4.1 Parties and Protocols

Parties in the UC framework are modeled by sets of interactive Turing machines (ITMs).
All ITMs are required to run in PPT (as de¬ned in Section 2.1) with respect to security
parameter k. Each ITM represents a program running within a party, the programs commu-
nicate with other programs within the party using local input and output tapes. Each ITM
has a session-identi¬er (SID) identifying the session or protocol instance it is participating
in. Each ITM also has a party identi¬er (PID) identifying which party the ITM is a part
of. Each ITM™s identi¬er pair (SID,PID) is unique to the ITM. In addition, each party has
a role identi¬er (RID) which identi¬es the party™s role in a protocol as either initiator or
ITMs have incoming and outgoing communication tapes which model the messages sent
in and out of the network. The adversary itself is also an ITM with control over message
delivery between parties, subject to the synchrony guarantee. Within the set of parties
there are two types: corrupted parties and uncorrupted (or honest) parties. In the general
UC framework, the adversary is able to adaptively corrupt honest parties “ in this work,
however, we will limit ourselves to non-adaptive adversaries which are not allowed to corrupt
new parties during protocol execution.
A real world protocol is modeled as parties running the protocol in the presence of an ad-
versary and environment ITM Z, with input z. The parties, environment, and the adversary
are the protocol participants, all with the same security parameter k. The modeled proto-
col execution progresses as a sequence of activations of individual participants. Di¬erent
participants must abide by di¬erent rules when activated, but while activated, a participant
may read the appropriate tapes and write on the tape of at most one other participant.
Once an activation is complete, the participant whose tape was modi¬ed is activated next
“ if no communication tapes were modi¬ed, then the environment Z is activated next. The
following is a list of rules regulating each participant™s behavior:

1. The environment is the ¬rst participant to be activated. The environment may read
the local output tapes of all participants. It may then activate another party to run
the protocol or write on the local input tape of a party or the adversary.

2. The adversary may read its own tapes and the outgoing communication tapes of all
parties. It may either deliver a message (from some other party) on the incoming

communication tape of a party or report information to Z by writing on its own
output tape.

3. A party reads its input (either from the environment or the adversary) and writes
either an output on its local output tape or an outgoing message on its outgoing
communication tape. If the party is honest, it follows its code; if the party is corrupted,
the adversary is allowed to control the internal actions of the party.

Protocol execution ends with the halting of the environment Z, which outputs a single
bit. We designate this output as execp,A,Z (k, z, r) when Z is interacting with parties running
protocol p in the presence of adversary A on security parameter k, input z, and participant
randomness r = rZ , rA , r1 , r2 , .... We let execp,A,Z (k, z) be a random variable representing
execp,A,Z (k, z, r) where r is chosen at random. Let execp,A,Z be the probability ensemble
{execp,A,Z (k, z)}k∈N,z∈{0,1}— .
An important point to observe is that all participants are only able to read their own
local input and incoming communication tapes. This means communications from the
environment or adversary to participants are not visible to other participants.

2.4.2 Ideal Functionalities, Ideal Protocols, and Hybrid Protocols

Ideal functionalities are descriptions of how various functionalities or tasks should behave.
They are meant to capture our intuitive sense of what it means to do something like public
key encryption or mutual authentication. An ideal functionality F is modeled by an ITM
which interacts with the protocol parties and adversary, but not the environment. For
convenience, we will refer to the ITM running F as F. We represent the interaction between
an ideal functionality F and participants with a special type of protocol, called an ideal
protocol, denoted IF . In the ideal world, the ideal protocol for functionality F is to just
have participants give their inputs to F and accept its outputs. This exchange between a
party P and F is not visible to other participants,2 but when P receives a value from F, it
immediately copies the value to its local output tape.
As will become clearer later, an adversary™s interaction with the ideal functionality di¬ers
from that of the protocol parties. The adversary that interacts with the ideal protocols is
This is achieved by parties writing directly onto F™s input tape and F responding onto their input tape

called the simulator (S). We also use idealF,S,Z to represent the probability ensemble
{execIF ,S,Z (k, z)}k∈N,z∈{0,1}— .
A hybrid protocol is a protocol where parties execute as described before, but have access
to one or more copies of each ideal functionality. Instead of all parties and all protocol
instances interacting with the same ideal functionality, the parties may interact with any
number of ideal functionalities, distinguished by their unique SIDs. In the hybrid model,
parties no longer automatically copy the results of their ideal functionality to their output

2.4.3 Realizing Ideal Functionalities

We now have a protocol model where primitives have been replaced with ideal functionalities
which behave precisely how we expect them to “ the question is then whether it™s possible
for a concrete cryptographic schemes to realize these ideal functionalities. Moreover, what
does it mean for a concrete scheme to realize an ideal functionality to begin with?
Intuitively, we want to say a scheme in the real world realizes an ideal functionality if
running a protocol using the concrete scheme does not result in anything that couldn™t have
happened in the ideal world. To formalize this notion, we use the environment to assert
that the results of the two worlds look the same.
In order to formalize, we need to de¬ne our notion of “looks the same.” As you recall,
we de¬ned the environment Z to output a single bit at the end of a protocol execution “
if the two worlds are indistinguishable, then all environments Z should be unable to act
di¬erently (output di¬erent bits) when interacting with the two worlds.

De¬nition 11 (Binary indistinguishability) Two binary distribution ensembles
{X(k, a)}k∈N,a∈{0,1}— and {Y (k, a)}k∈N,a are called indistinguishable (written X ≈

Y ) if for any c ∈ N there exists k0 ∈ N such that for all k > k0 and for all a we have

| Pr(X(k, a) = 1) ’ Pr(Y (k, a) = 1)| < neg(k) .

De¬nition 12 (Secure Realization of Ideal Functionality) Let F be an ideal func-
tionality and let p be a protocol. We say p securely realizes F if there exists a S such
that for any environment Z we have

idealF,S,Z ≈ execp,A,Z

This de¬nition says that a protocol p realizes F if for every adversary A wrecking havoc
in the real world with p there is some simulator S that could have done the same thing in
the ideal world with F (except in negligibly small instances of adversarial randomness).

The universal composition theorem

Say r is a protocol that securely realizes an ideal functionality F and p is some F-hybrid
protocol. We can construct the composed protocol pr where parties running p replace each
copy of F with a new instance of r with fresh randomness. If r is a G-hybrid protocol
(i.e. protocol r uses ideal functionality G), then pr is a G-hybrid protocol as well. The
universal composition theorem says that it doesn™t matter if the protocol realizing one ideal
functionality is itself a hybrid protocol “ the environment Z is still unable to distinguish
between protocol executions in the ideal world with these ideal functionalities and the real
world using concrete schemes. [13].

Theorem 1 (Universal Composition) Let F, G be ideal functionalities. Let p be a F-
hybrid protocol and let r be a protocol that securely realizes F. Then, for any adversary A,
there exists a simulator S such that for any environment Z,

<< . .

( 9)

. . >>

Copyright Design by: Sunlight webdesign