LINEBURG

 << Ļšåä. ńņš. ńņšąķčöą 2(āńåćī 9)ĪĆĖĄĀĖÅĶČÅ Ńėåä. ńņš. >>
lenger picks b randomly from {0, 1} and sets cā— ā enc(kpub , mb ); it then hands c to both D
and A. A may now resume querying D, but is not allowed to ask for the decryption of cā— .

15
After a polynomial number of queries, the A outputs a guess g. If g = b, the adversary wins.
A scheme is considered IND-CCA2 secure if no adversary wins with probability signiļ¬cantly
better than it could achieve by just guessing a random g to begin with. More formally:

Deļ¬nition 2 (IND-CCA2) A public key encryption scheme consisting of three algorithms,
S = (gen, enc, dec), is called indistinguishable against adaptive chosen ciphertext attack if
the following properties hold for any negligible function neg() and all large enough values of
the security parameter k with corresponding message space Mk :

Completeness: For all m ā Mk ,

Pr[ (kpub , kpriv ) ā gen(1k );
c ā enc(kpub , m);
m = dec(kpriv , c) ] > 1 ā’ neg(k)

oracle D,

Pr[ (kpub , kpriv ) ā gen(1k );
(m0 , m1 ) ā AD(kpriv ,Ā·) (kpub , 1k );
R
b ā {0, 1} ;
cā— = enc(kpub , mb )
ā— ,Ā·)
(kpub , cā— , 1k ) :
1
b=g ]< + neg (k)
2

The extra completeness property ensures that a message remains the same after under-
going encryption and decryption. We deļ¬ne negligible functions as follows:

Deļ¬nition 3 (Negligible Functions) A function f : N ā’ R is negligible in k if, for
1
any polynomial q, f (k) ā¤ for all suļ¬ciently large k. If f is negligible in k, we write
q(k)

f ā¤ neg(k).

2.2.2 Digital Signatures

Digital signatures are used when a party wants to indicate they have originated a message
m. A digital signature Ļ is dependent on some secret known only to the signer and on

16
the message being signed. The recipient of (m, Ļ) can then run a public veriļ¬cation algo-
rithm that will conļ¬rm or reject the messageā™s signature without requiring knowledge of
the signerā™s secret. In this thesis, we will restrict our attention to schemes that accomplish
this using signing and veriļ¬cation keys.
We also restrict our attention to party behavior or signature schemes that somehow bind
signatures to their messages ā“ this may be through the use of message revealing signatures
(where one can derive m from Ļ) or by treating a non-message revealing signature as invalid
unless explicitly attached to a particular message. For clarity of expression, we adopt the
latter practice and will always pair signatures with their messages in our examples.
More formally, we deļ¬ne a digital signature scheme as follows:

Deļ¬nition 4 (Digital Signatures) A digital signature scheme consists of three algorithms
(gen, sig, ver):

ā¢ gen : 1k ā’ K Ć— K , is a key generation algorithm. K and K are the sets of possible
signing and veriļ¬cation keys, respectively.

ā¢ sig : K Ć— M ā’ S, is a signing algorithm. M and C are the sets of possible messages
and signatures, respectively.

ā¢ ver : K Ć— M Ć— S ā’ B, is a veriļ¬cation algorithm. It outputs a boolean bit indicating
whether it accepts or rejects the message signature pair.

A common deļ¬nition for signature security is existential unforgeability under adaptive
chosen message attack (EUF-ACMA). As with IND-CCA2, we can describe the security
condition as a game between the adversary and the environment/challenger (Figure 2-2).
The challenger runs (ks , kv ) ā gen(1k ) and hands veriļ¬cation key kv to A, the adversary.
The challenger then gives ks to a signing oracle S. A can (adaptively) query S with messages
mi and receive back the corresponding signatures Ļi ā sig(ks , mi ). After some polynomial
number of queries, the adversary outputs a new message m that was never submitted as
a query to S, and a signature forgery Ļ. If ver(kv , m, Ļ) = 1, then the adversary wins.
A scheme is considered EUF-ACMA if no adversary is able to win with non-negligible
probability. We call the interaction between the adversary and the signing oracle an adaptive
chosen message attack (ACMA)

17
Existentially unforgeable under adaptive chosen message attack (EUF-ACMA)
1k time
-
gen
 (ks , kv )
kv -
mi
ks- 
(m0 , Ļ0 )
Challenger -
... A
S
mpoly(k)

(mpoly(k) , Ļpoly(k) )
-
(m, Ļ)


? ?
?
m = mi , for all 0 ā¤ i ā¤ poly(k)
& ver(kv , m, Ļ) = 1

Figure 2-2: The EUF-ACMA game

Deļ¬nition 5 (EUF-ACMA) A signature scheme consisting of three algorithms, Ī£ =
(gen,sig,ver), is called existentially unforgeable under adaptive chosen message attack (EUF-
ACMA) if the following properties hold for any negligible function neg() and all large enough
values of the security parameter k with corresponding message space Mk :

Completeness: For all m ā Mk ,

Pr[ (ks , kv ) ā gen(1k );
Ļ ā sig(s, m);
0 ā ver(m, Ļ, v) ] < neg(k)
.

Unforgeability: For any PPT forger A with access to signing oracle S,

Pr[ (ks , kv ) ā gen(1k );
(m, Ļ) ā AS(ks ,Ā·) :
1 ā ver(m, Ļ, kv ) and A never asked S to sign m ] < neg(k)

EUF-ACMA security allows for multiple valid signatures on the same message ā“ there
are some situations that require a stronger deļ¬nition of security. For example, there are

18
non-malleable unique signature schemes, which are schemes resilient to an ACMA with
only one valid signature for a given message and veriļ¬cation key. Even stricter are one-time
signature schemes, schemes that only sign one message once for a given veriļ¬cation key.
There is, however, a security deļ¬nition that is stronger than EUF-ACMA but weaker
than unique signatures. Schemes that meet this alternative security deļ¬nition are called
1
āstrongā [31, 5] or āsuper-secureā [23]. Usage of strong signatures are not as common as
EUF-ACMA or one-time signatures, but there are situations where one-time signatures are
used when only strong signatures are necessary [21].
Strong security is very similar to EUF-ACMA ā“ in fact, their deļ¬nitions diļ¬er only
slightly. In the deļ¬nition of EUF-ACMA, the adversary is required to output a valid
message/signature pair (m, Ļ) where m was never a query to the signing oracle. For strong
security, we make the adversaryā™s game easier: in order to win, it must output a valid pair
(m, Ļ), where (m, Ļ) itself was never a response from the oracle. Referring back to the
EUF-ACMA game in Figure 2-2, the strong signature game is the same as replacing the
second-to-last line with ā(m, Ļ) = (mi , Ļi ) for all 0 ā¤ i ā¤ poly(k).ā We consider this to be an
easier game since any adversary that wins the EUF-ACMA game wins the strong signature
game as well. By making the game easier, we make our security deļ¬nition stronger. A
strong signature scheme not only guarantees that past signatures donā™t help for forging
signatures on new messages, but that they also donā™t help for forging new signatures on old
messages.

Deļ¬nition 6 (Strong Signature Schemes) A signature scheme consisting of three algo-
rithms, Ī£ = (gen,sig,ver), is called strong if the following properties hold for any negligible
function neg() and all large enough values of the security parameter k with corresponding
message space Mk :

Completeness: For any m ā Mk ,

Pr[ (s, v) ā gen(1k );
Ļ ā sig(s, m);
0 ā ver(m, Ļ, v) ] < neg(k)
.
1
This is a diļ¬erent deļ¬nition of āsecure signaturesā than the one presented by Goldwasser, Micali, and
Yao in 1983 [24] which was eventually renamed EUF-ACMA security

19
Strict Unforgeability: For any PPT forger F with access to signing oracle S,

Pr[ (s, v) ā gen(1k );
(m, Ļ) ā F S(s,Ā·) :
1 ā ver(m, Ļ, v) and F never received (m, Ļ) from S ] < neg(k)

2.3 Formal Cryptography

Formal cryptography uses mathematical or logical systems to analyze protocols. The results
of such analysis, however, do not directly apply to real protocols because of the high level of
abstraction used. For the purpose of this thesis, we will focus on symbolic analysis and the
Dolev-Yao model. We ļ¬rst describe symbolic analysis and its importance in general terms,
before describing the speciļ¬cs of the Dolev-Yao model.

2.3.1 Symbols and Rules

In symbolic analysis, we think of messages as symbols and cryptographic operations as sym-
bolic operations on these messages. For example, if we had a message that we represented
with the symbol m, then the ciphertext of m encrypted under a public key K would be
the symbol {|m|}K , where we let {|Ā·|} represent encryption. If we have an entity, we can
represent the entityā™s initial knowledge as a set S of symbols. We can then write rules
governing the way new symbols are formed and handled based on what the entity knows
already. Given this initial set S , we can talk about the closure of S (denoted as C[S ]) which
is the result of applying these rules. Continuing with public key encryption, we might write
the following rules:

1. S ā C[S ]

2. If m ā C[S ] and K ā C[S ], then {|m|}K ā C[S ]

3. If {|m|}K ā C[S ] and K ā’1 ā C[S ], then m ā C[S ] (where K ā’1 is K ā™s corresponding
secret key)

Rule 1 says that anything the entity knows, it can derive. Rule 2 says that if the entity
can derive a message and a public key, then the entity can derive the ciphertext of the
message under the key. Lastly, Rule 3 says that if the entity can derive a ciphertext under

20
a particular public key and can also derive the corresponding private key, then the entity
can derive the ciphertextā™s plaintext.
We generally think of the formal model adversary as being in complete control of the
network it is a part of. The ability to represent the knowledge of an adversary during
a protocol run is important for this allows an analyzer to determine what messages an
adversary is capable of creating when trying to attack the protocol. The closure operation
does this, allowing a protocol checker to iterate all plausible attacks.

2.3.2 The Dolev-Yao Model

The Dolev-Yao model is a popular model for symbolic analysis which serves as the founda-
tion for a number of formal methods. There are many variants on the Dolev-Yao model and
we deļ¬ne one that serves our purpose of analyzing public key encryption. We also include
the notion of a local output as proposed in [16].
The ļ¬rst thing to deļ¬ne is the set of atomic symbols from which the Dolev-Yao algebra
is constructed.

Deļ¬nition 7 (The Dolev-Yao Message Algebra) Messages in the Dolev-Yao algebra
A are composed of atomic elements of the following types:

ā¢ Party identiļ¬ers (M) ā“ These are denoted by symbols P1 , P2 , .. for a ļ¬nite number
of names in the algebra. These are public and are associated with a role of either
Initiator or Responder.

ā¢ Nonces (R) ā“ These can be thought of as a ļ¬nite number of private, unpredictable
random-strings. These symbols are denoted by R1 , R2 , ... and so on.

e e
ā¢ Public keys (KP ub ) ā“ These are denoted by symbols KP1 , KP2 , ... which are public and
each associated with a particular party identiļ¬er.

ā¢ A garbage term, written G, to represent ill-formed messages,

ā¢ ā„, to represent an error or failure,

ā¢ Starting , to indicate that a protocol execution has begun, and

ā¢ Finished , to indicate that a protocol execution has ended.

21
Messages in the algebra can be compounded by the following symbolic operations:

ā¢ pair: A Ć— A ā’ A. When messages m and m are paired, we write m|m .

e
ā¢ encrypt : KP ub Ć— A ā’ A. When message m is encrypted with public key KP , we write
{|m|}K e
P

.
The Dolev-Yao algebra is free, meaning that no two distinct symbols represent the same
message. An important consequence of this is that we can deļ¬ne a parse tree for each
message which describes the unique symbolic structure of the message (see Figure 2-3).

e
R1 | {|P1 |}K e |R2 | KP0 e
KP
e
P0 KP 0 e
KP
1
1

e
R1 | {|P1 |}K e |R2 | KP0 e
KP1
e
KP
e
P0 KP 0
1

v
R1 | {|P1 |}K e |R2 KP0 e
KP
e
P0 KP 0
1

e
e KP0
KP0
e
R1 | {|P1 |}K e |R2 KP1
P0

R1 | {|P1 |}K e R2
P0

{|P1 |}K e
R1 P0

e
KP0
P1

Figure 2-3: Example Dolev-Yao parse tree

22
As mentioned in Section 2.3.1, one of the major beneļ¬ts of describing the world using
symbols is that we can enumerate the messages it is possible for an entity to make, based
on the symbols it already knows. In particular, we assume that the adversary completely
controls the network, but that any message delivered by the adversary must be derivable
from the adversaryā™s initial knowledge and the messages communicated by honest parties.
The adversaryā™s initial knowledge consists of all public keys (KP ub ), all identiļ¬ers (M),
and those nonces that the adversary itself generates (RAdv ). To derive new messages, the
adversary has only a few symbolic operations available to it: pairing two known elements,
separating a pair, encrypting with public keys, and decrypting messages whose keys belong
to corrupted parties (MAdv ā‚ M).
This restriction on the adversaryā™s ability to derive messages is captured by the Dolev-
Yao closure operation:

Deļ¬nition 8 (Closure) Let

ā¢ RAdv ā‚ R be the set of nonces associated with the adversary,

e e
ā¢ KAdv = {KP : P ā MAdv } be the set of encryption keys belonging to corrupted parties
e
(KAdv ā‚ KP ub ), and

Then the closure of a set S ā A, written C[S ], is the smallest subset of A such that:

1. S ā C[S ],

2. M āŖ KP ub āŖ RAdv ā C[S ],

e
3. If {|m|}K ā C[S ] and K ā KAdv , then m ā C[S ],

4. If m ā C[S ] and K ā KP ub , then {|m|}K ā C[S ],

5. If m|m ā C[S ], then m ā C[S ] and m ā C[S ], and

6. If m ā C[S ] and m ā C[S ], then m|m ā C[S ].

Symbolic Protocols
 << Ļšåä. ńņš. ńņšąķčöą 2(āńåćī 9)ĪĆĖĄĀĖÅĶČÅ Ńėåä. ńņš. >>