On Symbolic Analysis of Cryptographic Protocols
by
Akshay Patil
Submitted to the Department of Electrical Engineering and Computer Science
in partial ful¬llment of the requirements for the degree of
Master of Engineering in Computer Science and Engineering
at the
MASSACHUSETTS INSTITUTE OF TECHNOLOGY
May 2005
c Akshay Patil, MMV. All rights reserved.
The author hereby grants to MIT permission to reproduce and distribute publicly
paper and electronic copies of this thesis document in whole or in part.
Author . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Department of Electrical Engineering and Computer Science
May 19, 2005
Certi¬ed by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Ronald L. Rivest
Viterbi Professor of Computer Science
Thesis Supervisor
Certi¬ed by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Ran Canetti
Visiting Scientist
Thesis Supervisor
Accepted by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Arthur C. Smith
Chairman, Department Committee on Graduate Students
2
On Symbolic Analysis of Cryptographic Protocols
by
Akshay Patil
Submitted to the Department of Electrical Engineering and Computer Science
on May 19, 2005, in partial ful¬llment of the
requirements for the degree of
Master of Engineering in Computer Science and Engineering
Abstract
The universally composable symbolic analysis (UCSA) framework layers DolevYao style
symbolic analysis on top of the universally composable (UC) secure framework to construct
computationally sound proofs of cryptographic protocol security. The original proposal
of the UCSA framework by Canetti and Herzog (2004) focused on protocols that only use
public key encryption to achieve 2party mutual authentication or key exchange. This thesis
expands the framework to include protocols that use digital signatures as well.
In the process of expanding the framework, we identify a ¬‚aw in the framework™s use of
UC ideal functionality Fpke . We also identify issues that arise when combining Fpke with
the current formulation of ideal signature functionality Fsig . Motivated by these discoveries,
we rede¬ne the Fpke and Fsig functionalities appropriately.
Thesis Supervisor: Ronald L. Rivest
Title: Viterbi Professor of Computer Science
Thesis Supervisor: Ran Canetti
Title: Visiting Scientist
3
4
Acknowledgments
My heartfelt thanks to my advisor Ron Rivest for his guidance and con¬dence in me.
Working with him has been a constant inspiration to achieve my very best.
To Ran Canetti for always answering my questions, even though he knows I™m lying
when I say they™ll only take a moment. His attention to detail and willingness to listen
have been lifesaving parachutes on the many occasions I™ve blindly charged forward in my
research.
To Jonathan Herzog for ¬rst introducing me to the UCSA framework. I would still
be utterly mysti¬ed by formal analysis if not for his ability to communicate clearly and
concisely.
To Be Blackburn, Maria Sensale, and Paula Mickevich for mothering me while I™ve been
3000 miles away from home.
To all the friends I™ve made during my years at MIT; their companionship has made my
time here truly enjoyable.
To the NSF and MIT for making this research possible “ I was supported by NSF grant
CCR032677 and the views expressed in this thesis are mine, not those of the NSF or MIT.
And to my family, whose love and support make everything possible.
5
6
Contents
1 Introduction 11
2 Preliminaries 13
2.1 Computational Cryptography . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Public Key Encryption and Digital Signature Security De¬nitions . . . . . . 14
2.2.1 Public Key Encryption . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.2.2 Digital Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Formal Cryptography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3.1 Symbols and Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3.2 The DolevYao Model . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.3.3 Example: NeedhamSchroeder Protocol . . . . . . . . . . . . . . . . 26
2.3.4 Strengths and Weaknesses of Symbolic Analysis . . . . . . . . . . . . 27
2.4 The Universally Composable Security Framework . . . . . . . . . . . . . . . 28
2.4.1 Parties and Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4.2 Ideal Functionalities, Ideal Protocols, and Hybrid Protocols . . . . . 30
2.4.3 Realizing Ideal Functionalities ..................... 31
3 Universally Composable Symbolic Analysis for Public Key Encryption 35
3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.2 Simple Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.3 Concrete to UC: Fpke and its Realization ................... 40
3.4 UC to DolevYao: The Mapping Lemma . . . . . . . . . . . . . . . . . . . . 42
3.5 DolevYao Back to UC: DY Mutual Authentication and F2ma . . . . . . . . 46
7
4 Analyzing Previous Ideal Functionality Formulations 49
4.1 Implicit Restrictions on Ideal Realizations . . . . . . . . . . . . . . . . . . . 50
4.2 Public Key Encryption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.3 Signatures and Certi¬cation with Encryption . . . . . . . . . . . . . . . . . 52
4.3.1 Fsig and Fcert . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.3.2 Adversarial Signature Selection . . . . . . . . . . . . . . . . . . . . . 54
4.3.3 Signature Looseness . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5 Rede¬ning Ideal Functionalities 57
5.1 Public Key Encryption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
5.2 Signatures and Certi¬cation with Encryption . . . . . . . . . . . . . . . . . 59
6 Realizing Ideal Functionalities 63
6.1 Public Key Encryption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
6.2 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
7 Adding Signatures to Universally Composable Symbolic Analysis 73
7.1 DolevYao Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
7.2 Simple Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
7.3 UC to DolevYao: The Revised Mapping Lemma . . . . . . . . . . . . . . . 80
7.4 DolevYao Back to UC: DY Mutual Authentication and F2ma . . . . . . . . 86
7.5 Using The Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
8 Future Research Directions 89
8.1 An EUFACMA Realizable Ideal Signature Functionality . . . . . . . . . . 89
8.2 Other primitives and protocol goals . . . . . . . . . . . . . . . . . . . . . . . 90
8.3 Mixing Ideal Functionalities . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
8
List of Figures
21 The INDCCA2 game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
22 The EUFACMA game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
23 Example DolevYao parse tree . . . . . . . . . . . . . . . . . . . . . . . . . . 22
24 The NeedhamSchroeder protocol (informally) . . . . . . . . . . . . . . . . . 26
25 The NeedhamSchroeder symbolic protocol, PN S . . . . . . . . . . . . . . . 27
26 Attacking the NeedhamSchroeder protocol . . . . . . . . . . . . . . . . . . 28
31 A graphical representation of the UCSA framework . . . . . . . . . . . . . . 37
32 The grammar of simple protocols . . . . . . . . . . . . . . . . . . . . . . . . 39
33 The [16] publickey encryption functionality, Fpke . . . . . . . . . . . . . . . 41
34 The [16] certi¬ed publickey encryption functionality, Fcpke . . . . . . . . . 42
35 The 2party mutual authentication functionality . . . . . . . . . . . . . . . 47
41 A double encryption protocol . . . . . . . . . . . . . . . . . . . . . . . . . . 51
42 The double encryption protocol, expanded . . . . . . . . . . . . . . . . . . . 52
43 The [14] signature functionality, Fsig . . . . . . . . . . . . . . . . . . . . . . . 53
44 The [14] certi¬cation functionality, Fcert . . . . . . . . . . . . . . . . . . . . 54
45 A mixed protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
46 The mixed protocol, expanded . . . . . . . . . . . . . . . . . . . . . . . . . 55
47 A vouching protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
51 The publickey encryption functionality, Fpke . . . . . . . . . . . . . . . . . 59
52 The certi¬ed publickey encryption functionality, Fcpke . . . . . . . . . . . . 60
53 The signature functionality, Fsig ........................ 61
54 The certi¬cation functionality, Fcert . . . . . . . . . . . . . . . . . . . . . . 61
9
71 A graphical representation of the UCSA framework with signatures . . . . . 73
72 Example DolevYao parse tree with signatures . . . . . . . . . . . . . . . . . 76
73 The grammar of simple protocols . . . . . . . . . . . . . . . . . . . . . . . . 78
74 The SPLICE authentication protocol . . . . . . . . . . . . . . . . . . . . . . 87
75 The SPLICE symbolic protocol, PSP LICE . . . . . . . . . . . . . . . . . . . 87
10
Chapter 1
Introduction
A cryptographic protocol is a set sequence of messages exchanged between two or more parties
who are trying to accomplish something. This “something” is what we call the protocol™s
goal “ perhaps it™s the ability to establish a shared secret or maybe it™s just the reassurance
that a certain someone is still alive. Whatever the goal, the ability to accomplish it, despite
the presence of some adversary bent on being evil, is what we call protocol security.
Proving protocol security is di¬cult. There are a number of things that can go wrong
on a number of di¬erent levels. In general, we have models and tools that help us analyze
di¬erent parts of the protocol at di¬erent level, but no one way of combining these analysis
results into single, convincing proof of protocol security
In [16], Ran Canetti and Jonathan Herzog proposed combining two seemingly compli
mentary bodies of work in order to create a uni¬ed framework for proving the security
of protocols. They layered the DolevYao model [22] on top of the universally composable
(UC) secure framework [13] in order to create a new framework they named universally
composable symbolic analysis (UCSA). This framework takes a protocol and its goal, then
justi¬ably abstracts the protocol to a form where automated tools can help generate a con
vincing proof that the protocol is secure, i.e. achieves its goal even in the presence of an
adversary.
Canetti and Herzog constructed universally composable symbolic analysis for protocols
that only use public key encryption. In this thesis we expand the framework to also include
digital signatures. In doing so, we identify and repair a ¬‚aw in their construction as well
as rede¬ne the ideal public key encryption and digital signature functionalities to include
11
some new and needed properties of interest.
The parts of this thesis Chapter 2 provides a brief explanations of the models and
security de¬nitions that are used in the universally composable symbolic analysis framework.
Chapter 3 then walks through Canetti and Herzog™s construction of the framework. Chapter
4 identi¬es a ¬‚aw in part of their construction and motivates the need for new de¬nitions
of UC functionalities Fpke and Fsig . Chapter 5 presents and explains the new de¬nitions,
followed by Chapter 6 which analyzes the computational security needed to realize them.
Finally, we once more present the universally composable symbolic analysis framework
in Chapter 7, complete with our ¬xes and the addition of digital signatures. Chapter 8
concludes with suggestions for related future research.
12
Chapter 2
Preliminaries
This chapter explains the models used to construct the UCSA framework as well as some
security de¬nitions that are important for understanding the results of the framework
2.1 Computational Cryptography
Computational cryptography treats cryptography as a branch of complexity theory, model
ing adversaries as probabilistic polynomialtime (PPT) algorithms and de¬ning security in
terms of an adversary™s probability in accomplishing certain tasks. Probabilistic polynomial
time means that the adversary can make random choices, but must ¬nish running in an
amount of time that is polynomial with respect to the size of the input it is running on.
Both the timee¬ciency and the success probability of the adversary are generally tied to
a number known as the security parameter, k, which is set by the environment.
Computational proofs are grounded in a class of computational complexity problems
widely believed to be “hard,” i.e. not solvable by a probabilistic algorithm in time poly
nomial to k. Examples of hard problems are the discrete log problem and factoring the
product of two large primes. A cryptographic scheme™s security is proved by assuming
the scheme isn™t secure, then constructing an e¬cient reduction to a hard problem, thus
reaching a believed contradiction.
Because of their mathematical foundation, computational proofs are desired when prov
ing cryptographic security. These proofs, however, are hard to construct when trying to
analyze protocols. In addition to potentially unforeseen interactions between the di¬erent
primitives used, there are often security concerns when multiple instances of a protocol are
13
being run simultaneously. While it is sometimes possible to provide a computational proof
of protocol security, doing so is di¬cult and requires signi¬cant e¬ort on the part of the
prover.
2.2 Public Key Encryption and Digital Signature Security
De¬nitions
In this section we de¬ne and explain the intuition behind computational notions of security
that will be useful later.
2.2.1 Public Key Encryption
An encryption scheme is a system allowing a party to transmit a message to another party
without an adversary learning the contents (or any function) of the message. With public
key encryption, this is achieved through the use of public and private keys. Before the
transmission of a message, a party B publishes a public key KB to all other parties. If party
A wishes to securely send a message m to B, A transmits the ciphertext of m encrypted
’1
with KB , {m}KB . Upon receiving {m}KB , B uses a private key KB that is known only to
’1
him, to decrypt the ciphertext and retrieve m. An adversary who knows KB but not KB
should not be able to extract any meaningful information about m when given {m}KB .
More formally, we de¬ne a public key encryption scheme as follows:
De¬nition 1 (Public Key Encryption) A public key encryption scheme consists of three
algorithms (gen, enc, dec):
• gen : 1k ’ K — K , is a key generation algorithm. K and K are the sets of possible
public and private keys, respectively.
• enc : K — M ’ C, is an encryption algorithm. M and C are the sets of possible
plaintext messages and ciphertexts, respectively.
• dec : K — C ’ M, is a decryption algorithm.
One of the strongest and common de¬nitions of public key encryption is indistinguisha
bility against adaptive chosen ciphertext attack (INDCCA2). With encryption, an adver
sary should be totally clueless about the contents of a ciphertext. For INDCCA2, we try
14
to capture this intuition by saying that even if an adversary picks two messages and is given
the ciphertext for one of them, it still can™t guess which of the two messages is the plaintext.
As with many security de¬nitions in computational cryptography, this type of security
is described as a game played between the adversary and a challenger (the challenger is how
we model what the adversary sees in the environment). As mentioned before, the adversary
is a probabilistic algorithm that runs in time polynomial to the security parameter k.
Indistinguishable under chosen ciphertext attack, 2phase (INDCCA2)
1k 
time
gen
pub , kpriv )
(k
Challenger
kpub 
c0
kpriv A

m0 
...
D
ci
mi 
(m0 1
,m )
(kpub , mb )
R
b ← {0, 1} 
enc
c—
c— 
—
c—  ci+ 1 = c
mi+1 
...
D —
cpoly(k) = c
mpoly(k) 
g
?
?
?
b=g
Figure 21: The INDCCA2 game
For INDCCA2, the game progresses as follows (Figure 21). The challenger runs
(kpub , kpriv ) ← gen(1k ) and hands kpub to A, the adversary. The challenger then gives
kpriv to a decryption oracle D. A can (adaptively) query D with ciphertexts ci and D will
send back the corresponding plaintexts mi ← dec(kpriv , ci ). After some number of queries,
polynomial with respect to k, A hands the challenger two messages m0 and m1 . The chal