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 INDCCA2 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 (INDCCA2) 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)
Ciphertext indistinguishability: For any PPT adversary A with access to decryption
oracle D,
Pr[ (kpub , kpriv ) ā gen(1k );
(m0 , m1 ) ā AD(kpriv ,Ā·) (kpub , 1k );
R
b ā {0, 1} ;
cā— = enc(kpub , mb )
ā— ,Ā·)
(kpub , cā— , 1k ) :
g ā AD(kpriv ,c
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 nonmessage 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 (EUFACMA). As with INDCCA2, we can describe the security
condition as a game between the adversary and the environment/challenger (Figure 22).
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 EUFACMA if no adversary is able to win with nonnegligible
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 (EUFACMA)
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 22: The EUFACMA game
Deļ¬nition 5 (EUFACMA) 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)
EUFACMA 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
nonmalleable 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 onetime
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 EUFACMA but weaker
than unique signatures. Schemes that meet this alternative security deļ¬nition are called
1
āstrongā [31, 5] or āsupersecureā [23]. Usage of strong signatures are not as common as
EUFACMA or onetime signatures, but there are situations where onetime signatures are
used when only strong signatures are necessary [21].
Strong security is very similar to EUFACMA ā“ in fact, their deļ¬nitions diļ¬er only
slightly. In the deļ¬nition of EUFACMA, 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
EUFACMA game in Figure 22, the strong signature game is the same as replacing the
secondtolast 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 EUFACMA 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 EUFACMA 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
DolevYao model. We ļ¬rst describe symbolic analysis and its importance in general terms,
before describing the speciļ¬cs of the DolevYao 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 DolevYao Model
The DolevYao 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 DolevYao 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 DolevYao algebra
is constructed.
Deļ¬nition 7 (The DolevYao Message Algebra) Messages in the DolevYao 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
randomstrings. 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 illformed 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 mm .
e
ā¢ encrypt : KP ub Ć— A ā’ A. When message m is encrypted with public key KP , we write
{m}K e
P
.
The DolevYao 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 23).
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 23: Example DolevYao 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 mm ā C[S ], then m ā C[S ] and m ā C[S ], and
6. If m ā C[S ] and m ā C[S ], then mm ā C[S ].
Symbolic Protocols