LINEBURG


<< . .

 5
( 9)



. . >>

with ciphertext c, then “ciphertext”, PID, SID , m, c is appended to t. (If Fcpke
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
( 9)



. . >>

Copyright Design by: Sunlight webdesign