Cryptographically Verified Implementations for TLS

Karthikeyan Bhargavan Ricardo Corin

Cédric Fournet Eugen Zălinescu
Microsoft Research, Cambridge MSR-INRIA Joint Centre, Orsay
{karthb, fournet}@microsoft.com {ricardo.corin, eugen.zalinescu}@inria.fr

ABSTRACT Symbolic vs Computational Cryptography. Two complementary

We intend to narrow the gap between concrete implementations of approaches have been successfully applied to protocol verification.
cryptographic protocols and their verified models. We develop and Symbolic models essentially treat cryptographic primitives as
verify a small functional implementation of the Transport Layer black boxes and focus on the logical properties of the protocol,
Security protocol (TLS 1.0). We make use of the same executable as pioneered by Needham and Schroeder [1978] and formalized by
code for interoperability testing against mainstream implementa- Dolev and Yao [1983]. They have led to efficient automated tools
tions, for automated symbolic cryptographic verification, and for [e.g. Blanchet, 2001], widely applied to the verification of large
automated computational cryptographic verification. We rely on a protocols.
combination of recent tools, and we also develop a new tool for Computational models tackle more concretely cryptographic as-
extracting computational models from executable code. We obtain sumptions; they treat primitives as probabilistic algorithms over
strong security guarantees for TLS as used in typical deployments. concrete bitstrings, and reason about the advantage of an adversary
with bounded computational capabilities. Computational models
sometimes lead to long, delicate, hand-crafted proofs; automated
Categories and Subject Descriptors tools are much more recent [Blanchet, 2006].
D.2.4 [Software Engineering]: Software/Program Verification; Implementations vs Abstract Models. Protocol specifications in-
C.2.0 [Computer-Communication Networks]: Security and Pro- clude many details; most (but not all) of them are of no importance
tection for security. In the process of distilling a formal cryptographic
model, most of these details are discarded. When is a protocol
General Terms model oversimplified? In contrast with formal guarantees proved
within the model, the relevance of the model relies on the expe-
Security, Verification
rience of the formalist. The problem is compounded when con-
sidering protocol implementations. Thus, as far as possible, we
1. VERIFYING PROTOCOLS propose to verify detailed protocol implementations and deploy-
AND IMPLEMENTATIONS ments, rather than simplified abstract models. Using automated
tools based on sound proof techniques, the details can either be
There has been much recent progress in formal methods and tools
safely erased, or dealt with by brute-force analysis.
for cryptography, enabling, in principle, the automated verification
of complex security protocols. In practice, however, these methods From Implementations to Cryptographic Models. More recent
and tools remain difficult to apply. Often, verification occurs inde- works [Goubault-Larrecq and Parrennes, 2005, Bhargavan et al.,
pendently of the development process, rather than during design, 2006] advocate the automatic extraction and verification of sym-
prototyping, and testing. Also, as a protocol or its implementations bolic cryptographic models from executable code.
evolve, it is difficult to carry over security guarantees from past for- Bhargavan et al. [2006] verify protocol implementations written
mal verification. Moreover, the verification of a system that uses a in F# [Syme, 2005], a dialect of ML, by compilation to symbolic
given protocol involves more than the cryptographic verification of models in ProVerif [Blanchet, 2001]. Their approach is to verify
an abstract model; it may rely as well on more standard analyses as much code as possible, while providing hand-written models for
of code (e.g. to ensure memory safety) and system configuration the rest, such as the core cryptographic libraries, which use bit-
(e.g. to enforce policy). For these reasons, we are interested in strings for concrete execution and symbolic terms for verification.
the integration of modern cryptographic verifiers into the arsenal of In this work, we rely on their tools for symbolic verification, and
software testing and verification tools. also experiment with direct computational cryptographic verifica-
tions of protocol implementations, by compilation to CryptoVerif,
a recent tool for computational cryptography [Blanchet, 2006].

Permission to make digital or hard copies of all or part of this work for Our Approach. The picture below outlines our approach to pro-
personal or classroom use is granted without fee provided that copies are tocol verification. It involves developing, testing, and verifying a
not made or distributed for profit or commercial advantage and that copies small reference implementation of the protocol plus typical appli-
bear this notice and the full citation on the first page. To copy otherwise, to cations. In contrast with specialized modelling languages for pro-
republish, to post on servers or to redistribute to lists, requires prior specific tocols, our use of a standard development platform enables early
permission and/or a fee.
CCS’08, October 27–31, 2008, Alexandria, Virginia, USA. testing, for instance to disambiguate the specification, experiment
Copyright 2008 ACM 978-1-59593-810-7/08/10 ...$5.00. with potential attacks, and confirm functional correctness.

459
 Contents. Section 2 recalls the main security features of TLS. Sec-
tion 3 outlines our reference implementation and reports on inter-
operability. Section 4 presents our results using symbolic models;
it also discusses formal security issues and related work. Section 5
describes a new tool for extracting computational models and relat-
ing computational security assumptions to concrete cryptography
APIs. Section 6 presents our results using computational models;
it also discusses cryptographic issues and related work.
An extended version of this paper and sample code appear at
http://msr-inria.inria.fr/projects/sec/fs2cv.

2. TRANSPORT LAYER SECURITY

The Secure Session Layer (SSL) protocol was promoted by Net-
scape as a means of providing privacy over the Internet, by secur-
ing HTTP connections between web browsers and servers. Its first
Verification consists of selecting a part of the implementation, public version, SSL 2.0 [Hickman, 1995], was released in 1994. Its
writing additional “verification harness” code that specifies the at- successor, SSL 3.0 [Frier et al., 1996], includes major changes and
tacker model, the cryptographic assumptions, and the target secu- addresses serious security flaws. It then evolved into an Internet
rity properties, and then compiling their combination to some auto- standard, named Transport Layer Security (TLS 1.0) [Dierks and
mated prover. Inasmuch as the verification tool chain is automated, Allen, 1999]. The latest standard, TLS 1.1 [Dierks and Rescorla,
one can easily re-verify the code base as it evolves. 2006] and the latest draft, TLS 1.2 [2008] include further improve-
In our experience, symbolic and computational verifications are ments and clarifications, notably changes designed to thwart new
complementary. Computational verification is more precise but cryptographic attacks. Since the three TLS versions are relatively
more difficult to achieve; we obtain results only for the crypto- similar, we refer to them generically as the TLS protocol(s).
graphic core of the protocol implementation. Symbolic verification To facilitate interoperability tests, our code targets mostly TLS
typically applies to the whole protocol, sometimes even including 1.0, the latest largely deployed version of the protocol. Next, we
the application, but does not detect low-level cryptographic errors. briefly recall its main security features. We follow the notations
Overall, we believe that the overhead of verification is getting af- and terminology of the RFC [Dierks and Allen, 1999]; we refer to
fordable, in comparison with design, development, and testing. The this document for a more general presentation.
next generation of tools could enable their integration in the devel- TLS 1.0. TLS provides secure communications between a client
opment process. and a server, with certificate-based server authentication and, op-
Implementing & Verifying TLS. As an extended case study, this tionally, client authentication. The protocol distinguishes between
paper considers implementations of TLS 1.0, one of the most widely sessions and connections; from an established session, each party
deployed communications protocols. Due to its popularity, many can derive one or more connections, and use them to send series of
systems embed an implementation of TLS and rely on its security messages. The protocol has two layers. The lower layer consists
for communications. of the record protocol, for exchanging messages using current con-
As well as being of practical importance, TLS is a well-under- nection parameters. The upper layer includes a handshake protocol
stood protocol, with a carefully written, self-contained specifica- for establishing sessions, as well as application protocols.
tion, a series of successive versions, and a large body of related Record Protocol. The record protocol receives uninterpreted data
verification work, providing a detailed history of security vulnera- from the upper layer. This data is first (possibly) split and com-
bilities and improvements. Also, TLS is not an academic protocol, pressed, then formatted into a series of records, and passed to a
optimized (or designed) for verification purposes. This sometimes lower, unprotected transport protocol.
complicates its security analysis, but also provides a good bench- Both parties independently maintain state for the read and write
mark for assessing verification techniques. directions of the connection. Each record is protected depending
Contributions. on the security parameters negotiated by the handshake protocol,
1. We program a small functional implementation of TLS. Us- which mostly include a ciphersuite, and on the current connection
ing simple client and server code, we confirm that our imple- states (e.g. keys and IVs). A ciphersuite specifies a key exchange
mentation interoperates with mainstream implementations. mode (either Diffie-Hellman- or RSA-based), an encryption algo-
rithm, and a hash algorithm. The encryption and hash algorithms
2. Relying on a combination of model-extraction and verifi- are relevant only to the record protocol, while the key exchange
cation tools, we obtain a range of positive security results, mode is relevant only to the handshake protocol.
covering both symbolic and computational cryptographic as- Initially, the ciphersuite is set to null, indicating no security trans-
pects of the protocol. We thus provide security guarantees formations. Thus, the messages of the handshake protocol are not
for code as it is used in typical deployments of TLS. protected by the record protocol, until shared security parameters
can be established.
3. To support computational verification, we develop a new tool
After the handshake, each fragment is protected using the mac-
for extracting cryptographic models from F# code. We be-
then-encrypt technique, and prefixing the result with a record header.
lieve this enables the first automated verification of executable
The record header has three fields: the content type of the sub-
code against standard cryptographic assumptions.
protocol the fragment belongs to, the version of the protocol used
4. We review known weaknesses for various versions of TLS, for processing this record, and the fragment length. The mac is
and discuss their detection as part of our verification process, computed by applying HMAC (with the hash algorithm and hash
for the corresponding weakened implementations of TLS. secret given by the security parameters and current state) to the

460
concatenation of the fragment, the record header, and the fragment where | is bitstring concatenation and random consists of 46 ran-
sequence number. The fragment and the resulting mac are then fed dom bytes.
to the encryption algorithm, in cipher block chaining (CBC) mode, From the pms and exchanged random values, both parties com-
after padding to a length that is a multiple of the block size. pute the master secret using an ad-hoc pseudo-random function
Handshake Protocol. The handshake protocol authenticates the (PRF). This function takes as input a secret and a seed, and gen-
server, optionally authenticates the client, establishes a shared mas- erates a stream of bytes, using HMAC (with two hash algorithms,
ter secret, derives cryptographic materials for their connections, MD5 and SHA1) as base primitive. For generating ms, the secret
and confirms that both parties agree on their exchanged parame- is pms and the seed is the concatenation of a fixed bitstring and the
ters. In this paper, we consider only RSA-based modes. We begin two nonces exchanged in the hello phase:
with the message flow for a handshake with an anonymous client: ms = PRF(pms, ‘‘master secret’’| cr | sr )
ClientHello ------>
ServerHello
The materials for the record protocol are generated similarly:
Certificate key_block = PRF(ms, ‘‘key expansion’’| sr | cr )
<------ ServerHelloDone
ClientKeyExchange is truncated and split into six secrets for the initial read and write
[ChangeCipherSpec]
connections: two encryption keys, two mac keys, and two IVs.
Finished ------>
[ChangeCipherSpec] The two ChangeCipherSpec messages appear in brackets be-
<------ Finished cause they are not considered part of the handshake itself; they
signal the use of the newly-negotiated algorithms and keys, so the
For our discussion, it is convenient to decompose the protocol into Finished messages are the first to be maced-and-encrypted by the
four phases, explained in more detail below. record protocol. These Finished messages contain a (hashed) tran-
1. the client and the server exchange connection parameters by script of the handshake to this point; their logical contents is
means of the hello messages; verify_data = PRF(ms, finished_label | MD5(hsm) | SHA1(hsm))
2. they establish an intermediate shared pre_master_secret (pms); where hsm is the concatenation of the sequence of handshake mes-
when using RSA, the client chooses pms, so the phase con- sages (including handshake subprotocol headers, but not the outer
sists of a single ClientKeyExchange message; TLS record headers). The resulting authentication guarantees are
3. they each compute a shared master_secret (ms); this enables detailed in Section 4. After a successful handshake, the parties can
the record layer to derive fresh cryptographic materials for start exchanging application data in both directions.
each direction of the record protocol; Resumption Protocol. Instead of performing a full handshake,
TLS offers the possibility of resuming a previously established ses-
4. they exchange ChangeCipherSpec messages, immediately fol- sion, or even duplicate an existing session to derive further connec-
lowed by Finished messages, to confirm that they share match- tions.
ing keys, check server authentication, and ensure integrity of Assume parties have already performed a successful handshake,
the handshake messages. thus establishing a session. The client can propose an abbreviated
The Hello messages include fresh nonces, a session identifier handshake by sending an Hello message that includes a fresh nonce
picked by the server, and session parameters; their logical content is and the old session identifier. If the server accepts this session iden-
tifier, both parties skip phases 2–3, immediately derive fresh cryp-
ClientHello(ver_min,ver_max,cr,rsid,cipher_suites,comp_methods)
tographic materials, and exchange Finished messages. Thus, the
ServerHello(version, sr, sid, cipher_suite, comp_method)
message flow for the abbreviated handshake is:
The Certificate message carries the server’s X.509 certificate; the
ServerHelloDone message has no payload. ClientHello ------>
ServerHello
TLS enables the negotiation of some connection parameters, that
[ChangeCipherSpec]
is, a protocol version, a ciphersuite, and a compression method. <------ Finished
These parameters are passed unprotected in the Hello messages: [ChangeCipherSpec]
the client expresses its preference as a range of parameters, then Finished ------>
the server sets the session parameters within that range. The nego-
tiation is authenticated later by the Finished messages, which them- Otherwise, a handshake continues as in the general case.
selves depend on these parameters. This circularity is a source of
concerns for TLS, discussed in Section 4. 3. REFERENCE IMPLEMENTATION
The client announces its highest supported version in the ver_max
Our code is entirely written in F# [Syme, 2005], a dialect of ML,
field of ClientHello and includes its lowest supported version ver_min
and executed on the .NET runtime. Its structure and programming
in the version field of the record header that encloses ClientHello
style reflects our goal to use the same code, as far as possible, for
(provisionally using this version’s record format). The server an-
four different tasks: symbolic execution for debugging; concrete
nounces its choice in the version field of ServerHello, and also in-
execution for interoperability testing; symbolic verification; and
cludes it in the enclosing record header.
computational verification.
The ClientKeyExchange message includes the RSA encryption
TLS is usually implemented as a library, linked to web-based ap-
of a fresh random pms, using the public key of the received cer-
plications such as browsers or web servers. The figure below gives
tificate. In order to confirm the highest version supported by the
the structure of our reference TLS implementation; each box rep-
client, the protocol version byte ver_max is embedded in pms, and
resents an F# module; each arrow represents a direct dependency
also influences the padding before RSA encryption:
between modules. Hence, the modules Handshake and Record im-
pms = ver_max | random plement the handshake and record protocols, respectively; and their

461
 Record Module. The Record module exports two functions:
val send: ConnectionId → bytes → unit
val recv: ConnectionId → bytes

It uses a database of active connections, indexed by ConnectionIds.

The handshake protocol populates this database with new connec-
tions as they are established.
The type Connection represents an established TLS connection:
type Connection = { type ConnectionState = {
net_conn: Net.conn; cipher_state: CipherState;
crt_version: ProtocolVersion; mackey: bytes;
read: ConnectionState; seq_num: int;
write: ConnectionState; } sparams: SecurityParameters; }
It is a record type storing the underlying TCP connection net_conn,
the version used during this connection, and the read and write
connection states. Each read or write connection state is a record
containing the cipher state (represented in our case, i.e. for block
ciphers, by the encryption key and the current initialization vec-
tor), the key used for macing mackey, the current sequence num-
ber seq_num, and the security parameters sparams established by
interfaces enable some Application module to send and receive mes- the handshake protocol (including, for example, the encryption and
sages over TLS. Module Formats contains functions to build and hash algorithms).
parse formatted TLS messages; it relies on Conversions for low- Given an established TLS connection with identifier id, the send
level encodings of strings and TLS-specific tags. Modules Crypto, and recv functions write and read payloads over the connection, in
Net, and Prins provide library functions that are not specific to TLS. accordance with the record protocol. As they process messages,
In the rest of this section, we outline the interfaces and imple- they log the following security events:
mentations of these modules. (The full paper gives more details.) Send(id,entity,payload)
Recv(id,entity,payload)

Libraries for Networking and Cryptography. The module Net de- where entity is either Client or Server. The event Send(id,entity,
fines functions to set up and use TCP connections. For example, payload) logs that entity sends message payload over the connection
by calling connect with a URI u, a client application can create a id. The event Recv(id,entity,payload) logs that entity accepts mes-
TCP socket to a server listening at u. It can then call the func- sage payload as valid over the connection id (after cryptographic
tions send and recv to exchange messages on this connection. The record processing, before passing it to the application). These events
module Crypto defines standard cryptographic primitives. For ex- have no effect at runtime; they are used only to specify our security
ample, the Handshake module creates a fresh pms using mkNonce goals for verification.
and encrypts it using rsa_encrypt, while the Record module calls To illustrate our coding style, we detail the code for the recv
hmacsha1 and aes_encrypt to mac-and-encrypt messages. The mod- function, which takes one argument, a connection identifier connid,
ule Prins (for principals) defines functions to create and retrieve and returns a record payload msg.
X.509 certificates. let recv (connid:ConnectionId) =
Our concrete implementation of these libraries relies on vari- let conn = getConnection connid in
ous classes in the .NET Framework; for instance, the Crypto mod- let conn, input = recvRecord conn in
ule implements hmacsha1 by calling the ComputeHash method in let conn, msg = verifyPayload conn CT_application_data input in
System.Security.Cryptography.HMACSHA1, and Net uses System. let id,entity = connid in Pi.log tr (Recv (id,entity,msg));
storeConnection connid conn;
Net.Sockets.TcpClient to implement connect. msg
Following an approach proposed by Bhargavan et al. [2006] (see
the figure in Section 1), we also develop a symbolic implemen- The function is written as a sequence of function calls. It first calls
tation of these libraries, for use in symbolic verification and de- getConnection to retrieve the connection record conn; it then calls
bugging. In this version, the Crypto module models hashing and recvRecord, which blocks until the next message input is received
encryption as algebraic datatype constructors for an abstract type; on the connection; it calls verifyPayload (detailed below) to decrypt
for instance, hmacsha1(key,text) simply returns a term HMACSHA1 the payload msg and verify the mac; it calls Pi.log to log a Recv
(key,text) representing the keyed hash; Net models connections as event as described above; and finally calls storeConnection to up-
communications on local channels between processes; Prins mod- date the connection database with the new connection parameters
els the X.509 store as a local private database. before returning msg. The cryptographic checks are all performed
Both versions of the library modules implement the same inter- in the verifyPayload function:
faces. By compiling our reference TLS implementation and appli- let verifyPayload (conn:Connection) (ct:ContentType) (input:bytes)=
cations against the concrete libraries, we obtain an executable that let (bct, bver, blen, ciphertext) = parseRecord input in
can be deployed on the network and tested against remote clients let rct, rver, rlen = getAbstractValues bct bver blen in
and servers. By compiling against the symbolic libraries, we ob- let ver = conn.crt_version in
tain an executable that can be used for generating symbolic traces if rver = ver then
let connst = conn.read in
for local debugging. For symbolic (and computational) verifica- let connst, plaintext = decrypt ver connst ciphertext in
tion, we assume that the concrete implementation of these libraries let payload, recvmac = parsePlaintext ver connst plaintext in
follows their models; as such, these libraries represent the trusted let len = bytes_of_int 2 (length payload) in
computing base for our verification results. let bseq = bytes_of_seq connst.seq_num in

462
 let maced = append5 bseq bct bver len payload in A server calls accept to listen on a TCP connection for a TLS
let conn = updateConnection_read conn connst in connection request; when a client calls connect over the same TCP
checkContentType ct rct payload; connection, the client and server engage in the full handshake pro-
if hmacVerify connst maced recvmac = true then
(conn,payload)
tocol to establish a new session and a new connection in each di-
else failwith "bad record mac" rection. Upon completion of the handshake protocol, both accept
else failwith "bad version" and connect construct their own Session record and Connection
record and populate them with all the values authenticated by the
The function takes three arguments: a connection record conn, an handshake protocol, including, for instance, the session identifier,
expected content type, and a message input received over conn, ciphersuite, security parameters, and computed keys. To indicate
and returns an updated connection conn and the received message the completion of the protocol and agreement on these values, the
payload. Most of the function prepares materials for calling the two functions log the following event
two cryptographic functions decrypt and hmacVerify. The call to
decrypt decrypts ciphertext using the algorithm, key, and initial- SendFinished(id,entity,subject,pms,session,read,write)
ization vector stored in the connection read state connst, to yield and the AcceptFinished event with the same parameters. Each event
plaintext and a new connst with an updated initialization vector. The contains the connection id, the entity which logs it, the subject
decrypted plaintext consists of a payload and a mac recvmac. The of the server’s certificate, the pre_master_secret, a full Session
call to hmacVerify verifies the mac, using the algorithm and mac record, and read and write connection states for the Connection
key in connst, thereby authenticating the sequence number, content records in the indicated direction.
type, protocol version, ciphertext length, and payload. The func- Clients can call resume for such sessions to trigger the resump-
tion fails with an exception if the mac is incorrect, if the version, tion protocol. Upon its completion, the resume function logs the
content type, or sequence number do not match the expected val- following event:
ues, if the message is an alert, or if any parsing function fails. In all SendFinishedRes(id,entity,subject,pms,session,read,write,ch,sh)
other cases, it returns an updated connection state and payload.
and the AcceptFinishedRes event with the same parameters, which
Coding for Verification. As illustrated in these two functions,
have the same meaning as for the full handshake. In addition the
our subset of F# is rich enough to write modular code that ac-
client and server Hello records are tracked. Note that all fields in
counts for detailed message formats, cryptographic operations, and
session (including for example session.ch and session.sh) refer
security events. Our code uses typical functional language fea-
to the initial full handshake, while the last two parameters ch and
tures such as nested function applications, tuples, records, algebraic
sh refer to the Hello messages in the abbreviated handshake. The
datatypes, pattern matching, exceptions, and modules. However,
servers executing accept also log these two events if a resumption
we avoid other features such as references, higher-order functions,
protocol has been completed.
and classes, because they are not presently supported by our veri-
fication tools. Moreover, since every library function or operating Sample Applications and Interoperability. Using our reference
system call that we use must be given a symbolic model, we define implementation, we write three applications:
and use only the minimal set of libraries described above. (We do • a client that connects to an arbitrary HTTPS URI and re-
not use, for example, any file I/O operation.) trieves a web page over a TLS connection;
We use recursive functions sparingly, because they usually lead
to non-terminating runs of ProVerif, and are difficult to verify in • a server that listens at an HTTPS URI and serves up a single
CryptoVerif. For example, we have a recursive list membership web page;
function for lists of publicly known elements, but no list concate- • a mutually authenticated client-server application where the
nation over private data. Moreover, we tend to separate purely client authenticates to the server using a password over a TLS
functional code from code that has side effects, such as events connection.
or networks operations. Purely functional code like verifyPayload
translates to reductions in ProVerif and equations in CryptoVerif, In our experiments, our client application can access basic pages
whereas functions like recv translate to processes, which are more from a variety of web servers running IIS or Apache. Our server ap-
complex to verify. plication successfully serves pages to clients running Internet Ex-
plorer or Firefox. Both applications successfully resume sessions,
Handshake Module. The Handshake module exports four func- when triggered for instance to refresh a web page displayed in a
tions that enable client and server applications to set up new ses- previous session. Hence, we experimentally establish that our ref-
sions, resume old sessions, and close connections. erence implementation is interoperable with the mainstream TLS
val connect: Net.conn → ServerName → ConnectionId ∗ SessionId implementations used by these browsers and web servers, including
val resume: Net.conn → SessionId → ConnectionId ∗ SessionId OpenSSL and the Windows CryptoAPI. Moreover, as our client-
val accept: Net.conn → CertName → ConnectionId ∗ SessionId server application demonstrates, applications with additional secu-
val close: ConnectionId → bool → unit
rity properties can be built on top of our TLS implementation.
It maintains a database of active sessions indexed by SessionIds. In comparison to mainstream implementations, our reference im-
The type Session characterizes a TLS session: plementation supports a smaller subset of the standard. We focus
type Session = { on TLS 1.0 in RSA mode for the key exchange. In this mode, we
sid: bytes; ch: ClientHello; support all ciphersuites using AES, DES, RC4, SHA, and MD5 al-
ms: bytes; sh: ServerHello; gorithms. Our implementation does not support data compression,
server_cert: Certificate; pms: bytes; } nor fragmentation; it does not send alerts and fails silently upon re-
It is a record of a session identifier sid, the master secret ms, the ceiving a bad message. Despite these limitations, our experiments
server certificate, the client and server Hello message and the pms. show that it is adequate for writing simple client and server applica-
All these fields are exchanged during the full handshake which es- tions. We found that having an implementation to experiment with
tablished the session. The fields in the left column suffice to run the helped to understand disambiguate details of the specification. It
protocol; the other fields are included only for the security analysis. also enabled us to try out attacks on our and other implementations.

463
4. SYMBOLIC VERIFICATION are also correlated. These variables provide complete coverage of
Our symbolic verification is based on an existing tool chain con- the current state of both parties as they switch to the application
sisting of a model extractor [Bhargavan et al., 2006], that com- protocol, as well as additional parameters used in the negotiation.
piles code written in F# to process models in an applied pi cal- As a minor, technical point, there is no formal agreement on
culus [Abadi and Fournet, 2001], and the state-of-the-art verifier the client’s lowest supported version for TLS (ver_min): the adver-
ProVerif, which analyzes such models automatically. For many sary may change this value, together with the first message record
protocol implementations, the verifier either proves the security format, in ClientHello, without detection. However, this seems in-
goals or produces a counter-example. In some cases, however, the nocuous as long as (1) the client checks that version ≥ ver_min and
analysis may not terminate; in others, it may take several gigabytes (2) whenever the server accepts the first message, version does not
of memory. To use this tool chain, we write symbolic implementa- depend on ver_min.
tions for low-level libraries as described in Section 3, we define the Resumption Protocol. We obtain a similar authentication theorem
attacker model in terms of the interface exposed by these libraries for the resumption protocol.
and by our reference implementation, and we write our authentica-
tion and secrecy goals as correspondence between events logged by T HEOREM 2 (R ESUMPTION AUTHENTICATION ). In any run
functions in the interface. Then we can extract a symbolic model of Sys, for any AcceptFinishedRes event, either there is a SendFin-
from the reference implementation and verify security queries au- ishedRes event with opposite entities (client/server or server/client)
tomatically. If the tool proves a query, we obtain a security the- and matching connection and session parameters, or one of the en-
orem about the protocol implementation, against all attackers that tities is corrupted. Moreover, within each AcceptFinishedRes and
use its interface. Our results rely on the correctness of the core SendFinishedRes event, the new ServerHello message has the same
translations and algorithms underpinning the model extractor and session id and ciphersuite as the old session.
ProVerif [Blanchet, 2001, Bhargavan et al., 2006].
We also prove secrecy queries for all the secrets generated dur-
Attacker Model. The attacker capabilities are given by the inter- ing the handshake, including the pms, ms, and all four keys. These
faces of the modules: Net, Crypto, Prins, Handshake, and Record. queries assert syntactic secrecy; they show that the secret values are
Access to the functions given in these interfaces yields a (standard) not obtained by the attacker, unless he has compromised the server
symbolic threat model, where the attacker can or controls the client. For brevity, we omit the formal security the-
• control the network (Net), and perform cryptographic opera- orem which can be found in the full version.
tions (Crypto), Record Protocol. For the record protocol, authentication is spec-
ified as a correspondence between the Recv events emitted when
• create any number of servers by generating certificates and a receiver accepts a message to prior Send events emitted when
compromise any server by reading its private key (Prins), messages are sent.
• open arbitrarily many sessions between clients and servers of T HEOREM 3 (R ECORD AUTHENTICATION ). In any run of
its choice, obtaining connection and session ids, and trigger Sys, for any Recv event, either there is a Send event with oppo-
the resumption protocol for any session id (Handshake), site entities (client/server or server/client) and matching connec-
• send and receive messages over the record layer (Record). tion identifiers and records or one of the entities is corrupted.
In addition, we prove the syntactic secrecy of record payloads,
Let Sys denote the program consisting of the symbolic imple-
when the payloads are freshly generated values. As usual, the pay-
mentations of the libraries Net, Crypto, Prins, and Conversions,
load is secret only if the server is uncorrupted and the client is not
along with our reference implementations for Handshake, Record,
controlled by the attacker. The formal secrecy theorem appears in
and Formats. We prove authentication and secrecy properties for
the full paper.
this full program, although in the following, we describe the verifi-
cation results separately for each part of the protocol. Reconstructing Known Attacks on TLS. Previous formal and in-
formal analyses of SSL and TLS have uncovered a range of vul-
Handshake Protocol. We first present symbolic authentication
nerabilities and attacks. For instance, SSL 2.0 does not guarantee
results for the handshake protocol. Authentication is specified as
integrity of many elements of the handshake negotiation, including
a correspondence from events triggered when a party accepts the
the ciphersuite. Hence, if both client and server prefer to use strong
peer’s Finished message to prior events triggered when the party
cryptography but also allow weak cryptography, then an attacker
sends that message. The more information these events record, the
may convince them both to establish a session with weak cryptog-
stronger the property. We say that a server has been corrupted when
raphy. In our model, implementations of SSL 2.0 do not satisfy
its private key has been leaked to the attacker. We say that a client
handshake authentication (Theorem 1). Our tools fail to prove our
is corrupted if its pms is known to the attacker.
authentication queries for such implementations, and instead gen-
T HEOREM 1 (F ULL H ANDSHAKE AUTHENTICATION ). erate counter-examples indicating the attack.
In any run of Sys, for any AcceptFinished event, either there is a Recent versions (since SSL 3.0) provide more extensive integrity
SendFinished event with opposite entities (client/server or server/ guarantees for the handshake. Still, Wagner and Schneier [1996]
client) and matching connection and session parameters, or one of found several attacks on the handshake and resumption protocols
the entities is corrupted. of SSL 3.0. They found that if both parties also support SSL 2.0
for backward compatibility, then version rollback attacks become
(The precise ProVerif queries for all theorems in this section are possible: an attacker can convince them to use SSL 2.0, and then
included in the full version.) Here, almost all fields of the session exploit any cryptographic flaws of the earlier version. TLS includes
records at the client and server are correlated. These include sid, two mechanisms to address this problem, both in the ClientKeyEx-
pms, ms, server_cert, and also cr, sr, version, and cipher_suite from change message, so that a server can identify SSL-only clients.
ch and sh in session. The derived cryptographic materials (within For instance, TLS clients embed ver_max within pms, but SSL 2.0
the read and write connection states, from the client’s viewpoint) clients do not.

464
 However, these mechanisms still do not suffice with the resump- that the correct decryption of an encrypted message yields the orig-
tion protocol, since the abbreviated handshake does not contain inal plaintext) and minimal negative assumptions (bounding, for
the ClientKeyExchange message. Hence, resumption authentication instance, the probability that a polynomial adversary may break a
(Theorem 2) guarantees only that the new connection parameters particular usage of encryption).
excluding ServerHello.version are correlated with the old session
parameters. Experimentally, we found that deployed server imple- 5.1 CryptoVerif (Review)
mentations of TLS are vulnerable to this version rollback attack The CryptoVerif verifier can prove the security of a given proto-
from TLS 1.0 to SSL 3.0 during resumption. However, we did not col under a set of security assumptions for its cryptographic primi-
find the more dangerous rollback from TLS 1.0 to SSL 2.0, partly tives, within a probabilistic polynomial-time (PPT) model of com-
because the length of the session id parameter fortunately differs putation. We briefly present the tool; we refer to Blanchet [2006],
between these two versions. Blanchet and Pointcheval [2006] for an explanation of CryptoVerif
Our method also catches common errors in TLS implementa- syntax and semantics.
tions, such as not verifying server certificates, or not checking that CryptoVerif takes as input a script, written in a variant of the
the received sequence number is correct. Such errors result in pi calculus with an explicit polynomial bound for every replicated
counter-examples to our authentication queries. process. Thus, processes represent PPT Turing machines that ex-
On the other hand, it is worth pointing out that several well- change finite bitstrings through an adversary, modelled as an (un-
known attacks on TLS are outside the scope of our symbolic (and known) PPT machine. In the script, cryptographic assumptions are
computational) model. These include cryptanalyses on the underly- introduced through type and function declarations, equations, in-
ing cryptographic functions, traffic analyses, and padding attacks. equations, and game-based equivalences. The equations and in-
Previous Symbolic Analyses. In a long line of works, researchers equations are typically used to describe minimal positive assump-
have used various techniques to verify models, and more recently, tions (the functional correctness of the primitive), whilst the game-
implementations, of different versions of SSL and TLS. Here, we based equivalences are used to state minimal negative assumptions.
describe only those most closely related to our work. Section 6 gives some examples.
Mitchell et al. [1998] study a model of SSL 3.0 using the Murphi Proofs, Games, and Indistinguishability. The input script can be
tool. They use model-checking to perform a finite-state exploration seen as an initial game, modelling the protocol, to which Cryp-
of a sequence of simple protocols with increasing complexity, in- toVerif applies transformations, until a final game that satisfies tar-
cluding a version of SSL 3.0 with both handshake and resumption get security conditions is reached—this proof technique is known
protocols, but limited to finite configurations consisting of, for ex- as game-hopping.
ample, two clients and a server. Each transformation between two consecutive games preserves
Paulson [1999] develops formal, machine-checked proofs for a PPT indistinguishability, that is, the adversary cannot distinguish
model of TLS 1.0 in Isabelle, with authentication and secrecy theo- the games before and after the transformation. Example transfor-
rems that, like ours, apply to more general configurations of clients mations include the application of an equivalence stating the secu-
and servers. His model includes both handshake and resumption rity of a cryptographic primitive, and the semantics-preserving rear-
but does not address version rollback issues within resumption. rangement of code, such as inlining and partial evaluation. Cryp-
He et al. [2005] apply logic-based proof techniques to the IEEE toVerif runs either automatically or interactively, in which case it
802.11i protocol, and include a simple model of TLS as a subproto- receives guidance from the user for selecting transformations.
col. Using PCL, they prove agreement on all exchanged messages Process and Variable Instances. Processes in CryptoVerif can
and secrecy of the pre-master secret. be replicated polynomially in a given security parameter, enabling
Ogata and Futatsugi [2005] show secrecy of the pre-master secret multiple parallel executions. A special find command permits to
and liveness properties for the handshake protocol with resumption access the different variable instances of each process replica.
using the OTS/CafeOBJ tool. Target Security Properties. CryptoVerif can deal with authentica-
Kamil and Lowe [2008] report on an analysis of a detailed strand tion and secrecy properties, specified as follows.
spaces model of the handshake and record protocols. They prove Authentication is expressed using correspondences, much as in
authentication and secrecy theorems similar to ours, and also show our symbolic models. Correspondences typically assert that, if
that the record protocol provides two authenticated streams and sat- some event is executed, then other events must also have been exe-
isfies session independence. cuted, with matching parameters, at least with overwhelming prob-
Jürjens [2006] verifies a Java implementation of the TLS hand- ability; this last bit reflects the computational nature of the model.
shake protocol for secrecy and authentication properties. His anal- Secrecy is expressed using indistinguishability between two con-
ysis works on the control-flow graph and does not account for mul- figurations. (It is often called strong secrecy in symbolic models, in
tiple versions or low-level message formats. contrast with the weaker notion of syntactic secrecy.) CryptoVerif
Chaki and Datta [2008] apply software model checking on Open- has two notions of secrecy. The weaker notion (query secret1 in
SSL code to verify secrecy and authentication for configurations of CryptoVerif) states that the adversary cannot distinguish the value
up to three servers and clients. of a variable in a specific instance from a random value; the stronger
notion (query secret) states that the adversary cannot distinguish
5. A COMPUTATIONAL VERIFIER FOR the sequence of all the values of variable instances from a sequence
of independent random values.
PROTOCOL IMPLEMENTATIONS
This section describes our computational verification approach 5.2 Compiling to CryptoVerif Scripts
and tools; Section 6 applies them to TLS. Compared with sym- We describe the design and implementation of a new model extrac-
bolic models, computational models adopt a less optimistic ap- tor that translates protocol implementations written in F# to Cryp-
proach to cryptography: rather than giving the adversary essentially toVerif scripts. The extractor takes three inputs: protocol modules
the same capabilities as ordinary protocol participants, they spec- written in F#, such as the modules in our reference implementation,
ify both minimal positive assumptions (guaranteeing, for instance, a computational model of the cryptographic libraries expressed as

465
CryptoVerif assumptions, and security goals for the protocol ex- Verification. The full CryptoVerif script consists of the computa-
pressed as CryptoVerif queries. Given these inputs, it generates a tional models of the libraries, the type definitions in the protocol
CryptoVerif script that can be verified either automatically or inter- implementation, and the top-level process representing the oracle
actively. In the rest of this section, we outline the various steps of interface provided by the implementation to the attacker. We then
the translation. write security goals as CryptoVerif queries for this process, and
Computational Models for Libraries. We first define models for proceed with verification.
all the functions in the library modules, such as Net, Crypto, and Besides the scripts obtained from our reference TLS implemen-
Prins. Our model of Net treats connections as public channels; tation (Section 6), our largest case-study so far, we have extracted
hence, calls to Net.send and Net.recv send and read messages from CryptoVerif scripts from the code of several sample protocols, in-
a single public channel that is controlled by the attacker. Our model cluding the Otway-Rees protocol and a password-based authen-
of Crypto defines cryptographic primitives as uninterpreted func- tication protocol; we could verify both authentication properties,
tions in CryptoVerif. For each primitive, we then add equations, expressed as non-injective correspondences between events, and
inequations, and equivalences to encode the specific cryptographic strong secrecy properties for keys and payloads. Although all our
notions we wish to use. Functions for generating fresh values, such scripts are currently automatically verified by CryptoVerif, manual
as mkNonce, are written using the CryptoVerif primitive new that guidance may be required in general, in the form of advice.
chooses a random bitstring uniformly from a type, such as the set of Challenges (Future Work). We mention two challenges with script
all nonces. Our model of Prins maintains a private array of public- extraction. First, as detailed in Section 3, libraries such as Prins rely
private keypairs; it allows a polynomial number of such keypairs on private databases to store local state and cryptographic materi-
but does not model key compromise. In contrast with Net and Prins, als for principals. This programming style is delicate to translate
which are generic, Crypto must be written specifically for the pro- to CryptoVerif, which does not support private channels. We are
tocol at hand; the specific definitions used for TLS are described in considering models that combine local variable bindings (for data
Section 6. writes) and find commands (for data lookups).
Code Transformations. The model extractor applies a series of More theoretically, we would like to show the correctness of our
code transformations to generate a smaller, more specialized source translation, with respect to a probabilistic, polynomial-time seman-
program. These transformations include aggressive inlining of non- tics for F#. This would enable us to carry over the computational
recursive functions, partial evaluation of functions and patterns, properties verified by CryptoVerif to our source programs, in terms
and dead-code elimination. Data structures such as records are of PPT adversaries with access to selected F# interfaces.
translated to simpler forms such as tuples, and all type abbrevia-
tions are inlined. All functions that do not appear in the interfaces 6. COMPUTATIONAL VERIFICATION
are eliminated, and all modules are flattened into a single module This section provides computational security properties for code
by suitably qualifying the names of functions, variables, and types. that implements two stages of TLS: the full record layer and the
This single module then consists of datatype definitions, function ClientKeyExchange phase of the handshake stage, respectively.
definitions, and top-level code that evaluates expressions and binds
variables. 6.1 Record protocol
Algebraic Datatypes. For each algebraic datatype, the translation In addition to our code for the record protocol (module Record in
produces a CryptoVerif type declaration with transparent construc- Section 3), we write F# wrapper code that sets up a secure connec-
tors, thereby reflecting our assumption that constructors are used tion (module Connected). From these modules, we automatically
only for tagging data, not for hiding information. For instance, the extract the computational model using the tool of Section 5. This
F# declaration type t = A of bytes yields a CryptoVerif type t and yields polynomially-replicated communicating sender and receiver
a type constructor A that is declared to be invertible; hence it is processes, wrapped up in a context that sets up a shared connection
always possible to obtain the bitstring x from A(x). including a master secret ms and random values cr and sr. We as-
sume that neither the client nor the server is corrupted hence these
Functions as Processes. For each function definition let f x = e,
values are not known to the attacker.
the translation first transforms the body expression e in continu-
In order to obtain the final CryptoVerif script, we include Cryp-
ation-passing style, into a sequence of imperative commands e’:
toRecord.cv to the above processes; it contains a hand-written im-
each line in e’ is either a function call or a pattern match. Each line
plementation of module Crypto that embeds our cryptographic as-
is then translated to CryptoVerif: function calls become processes
sumptions described below.
that call CryptoVerif function symbols; pattern matches become
let processes. Some function calls are specially translated: calls Security Notions for PRF, MAC and Symmetric Encryption. We
to fork spawn parallel processes; calls to log yield primitive event present our assumptions for the security primitives of the record
recording processes. Finally, the whole function definition is trans- protocol. (The full paper lists the corresponding CryptoVerif defi-
lated to a process of the form let f = in(callf, x);...; out(resultf, r) that nitions.)
takes its arguments on channel callf and returns its result on channel PRF. We specify security in the Random Oracle model [Bellare
resultf. Since these channels are public, the opponent may call any and Rogaway, 1993], as an equivalence that replaces every call to
of the functions in the public interface, as oracles. PRF by a table lookup, such that the first call generates a fresh ran-
Top-level Process. Each variable binding let x = e in the source dom value. Blanchet and Pointcheval [2006] use a similar equiva-
code translates to a process context that binds x to the result of lence for proving the security of a signature scheme.
evaluating e. The expression e is translated to a process, as ex- MAC. The message authentication code scheme has three func-
pressions in function definitions, possibly spawning processes us- tions, mkgen, mac, and check for generating a mac key from a seed,
ing fork. Hence, the top-level process that represents the full sys- macing a message, and verifying a mac, respectively. We assume
tem consists of bindings for all variables, parallel threads for all unforgeability under chosen message attacks (UF-CMA), stated as
spawned processes, and N replicas for each function process, where an equivalence that replaces every call to mac and check, so that
N is a polynomial in the security parameter. check performs instead a table lookup on any previously-generated

466
macs. Blanchet [2006, Proposition 2] also relies on this equiva- server corruption, and we verify only a single established connec-
lence, and shows that it is indeed implied by UF-CMA. tion between an honest sender and an honest receiver (however, us-
SPRP. The symmetric encryption scheme has three functions kgen, ing this single connection, a polynomial number of messages can
symenc, and symdec for generating a symmetric key from a seed, be concurrently exchanged between the sender and receiver). These
encrypting a message, and decrypting a message, respectively. Since restrictions stem from limitations in the current version of our com-
the ciphersuites we consider use AES and DES, we model this piler and of CryptoVerif. As future work, we foresee no difficulty
scheme as a block cipher, and assume the usual notion of super in reflecting computationally all the symbolic results of Section 4.
pseudo-random permutation (SPRP) [Phan and Pointcheval, 2004],
entailing that encryption is a random permutation, at least for ran-
6.2 Handshake protocol
domly chosen keys. (The “super” qualifier indicates that the ad- We consider the code for the first stage of the handshake protocol,
versary has also access to a decryption oracle.) We model SPRP up to the sending of the ClientKeyExchange message, and show the
in CryptoVerif as an equivalence that replaces every call to encryp- secrecy of the encrypted pms inside the ClientKeyExchange mes-
tion and decryption operations by lookups (via the CryptoVerif find sage. For this proof, we disable all the code in Handshake module
command) on a table that relates previous encryption and decryp- for the subsequent stages. Similarly to the record protocol, we write
tion queries with freshly generated random values. F# wrapper code in Certified that sets up a public/private keypair of
a trusted server. Using the tool of Section 5, we extract the polyno-
Record Authentication. Relying on the same events Send and
mially replicated processes from Certified and Handshake.
Recv as in Section 4, we express our security property as a cor-
respondence query within CryptoRecord.cv. Let Sys be the script Security Notions for Asymmetric Encryption. We manually craft
composed of CryptoRecord.cv (embedding PRF, MAC, and SPRP CryptoHandshake.cv with our cryptographic declarations and as-
assumptions) and the translation of Connected and Record. Cryp- sumptions. We have functions skgen and pkgen for creating private
toVerif automatically proves record authentication, through 8 game and public keys; we also have functions enc and dec to encrypt
transformations in less than a second. and decrypt messages. (We assume a probabilistic scheme, so the
encryption function inputs a seed as well.)
T HEOREM 4 (R ECORD AUTHENTICATION ). In any polyno- We use a strong notion of security for asymmetric encryption,
mial run of Sys, with overwhelming probability, for any Recv event, namely indistinguishability against chosen-ciphertext attacks (IND-
there is a Send event with opposite entities (client/server or server/- CCA2). We use the standard equivalence from the CryptoVerif li-
client) and matching connection identifiers and records. braries, which replaces encrypted plaintexts with a message con-
sisting of only zeroes (of the appropriate length), and replaces de-
Record Secrecy. In order to check secrecy of the communicated cryptions by table lookups.
payloads, we extend Record with a new function definition
Secrecy of the Pre-master Secret. As specified in TLS 1.0, the pre-
let send’ (id:ConnectionId) = master secret is the concatenation of a two-byte constant TLS1p0
let payload = mkNonce() in send id payload plus 46 bytes of random. Let Sys 00 be the script composed of Cryp-
This function is translated to a CryptoVerif process that, instead toHandshake.cv (embedding the IND-CCA2 assumption) and the
of inputting a payload from the adversary, generates and sends a translation of Certified and Handshake (up to the sending of the
ClientKeyExchange message). CryptoVerif verifies the secrecy of
freshly generated payload. In order to prove secrecy of payload,
random, through 6 game transformations.
we exclude the recv function (which would otherwise act as an or-
acle) and obtain a variant Sys 0 of the system Sys of Theorem 4. T HEOREM 6 (PMS R ANDOM S ECRECY ). In any polynomial
CryptoVerif verifies the secrecy of payload, through 26 game trans- run of Sys 00 , the sequence of random values within pre-master se-
formations. crets is indistinguishable from a sequence of independent random
T HEOREM 5 (R ECORD S ECRECY ). In any polynomial run of values.
Sys 0 , the sequence of sent payload values is indistinguishable from
a sequence of independent random values. Attacks and Differences with Symbolic Model. Our secrecy prop-
erty is close to the symbolic notion of strong secrecy but is finer
Attacks and Differences with the Symbolic Model. Symbolically, than syntactic secrecy. For instance, symbolically, we can estab-
it is possible to show secrecy not only for the record payloads, but lish syntactic secrecy for the full pms with the embedded protocol
also for the used keys. Computationally, however, one can only version constant, not just random. Even computationally, it may
show key secrecy before they are actually used; this is the case for be possible to prove computational secrecy of the whole pms, as
the session keys of the record protocol and the pre-master secret of shown in independent ongoing work [Morrissey et al., 2008], if we
the handshake protocol (Section 6.2). model asymmetric encryption using a weaker one-wayness prop-
Another difference can be seen in the following variant of the erty that allows the adversary to recover some parts of pms.
record protocol, where instead of mac-then-encrypting, we only We were unable to prove full handshake and resumption authen-
encrypt the payload and keep the mac in the clear. In this case, tication computationally, due to limitations of our verification tools.
CryptoVerif fails to find a proof of Theorem 5, and with reason: We leave these as future work.
nothing in the equivalence of macs ensures that the maced payload
should be kept secret. Interestingly, this variant protocol remains 6.3 Previous Computational Analyses
secure in the symbolic model, as the mac function (modelled as a There are many analyses of TLS in computational settings; we fo-
non-invertible hmacsha1 function) leaks nothing. This is another cus on the positive results, although we still mention important neg-
evident illustration of the difference in abstraction levels between ative results.
symbolic and computational models. Krawczyk [2001] shows that the mac-then-encrypt operation (as
The protocol model we verify here is more limited in comparison used in the computational analysis of our record protocol) is safe
to the symbolic one: we do not consider resumption, nor the com- when the mac is UF-CMA and the encryption scheme is used in
position of the record and handshake protocols. We do not model CBC mode and is IND-CPA. Phan and Pointcheval [2004] describe

467
notions of PRP and SPRP (which we model in CryptoVerif) and D. Dolev and A. Yao. On the security of public key protocols. IEEE
their equivalences to standard semantic security and security against Transactions on Information Theory, IT–29(2):198–208, 1983.
lunchtime attacks. P.-A. Fouque, D. Pointcheval, and S. Zimmer. HMAC is a randomness
More recently, Fouque et al. [2008] argue for the suitability of extractor and applications to TLS. In ACM Symposium on Information,
the HMACSHA1 construction as a PRF as used in TLS (whereas Computer and Communications Security (ASIACCS’08), pages 21–32,
our model assumes a random oracle). Related to this, Gajek et al. 2008.
[2008] study randomness extraction from pre-master secret to mas- A. Frier, P. Karlton, and P. Kocher. The SSL protocol version 3.0. Internet
ter secret in the standard model (something we do not address com- Draft, IETF, 1996.
putationally as we focus on the pre-master secret exchange and on
the record stages only). S. Gajek, M. Manulis, A.-R. Sadeghi, and J. Schwenk. Provably secure
browser-based user-aware mutual authentication over TLS. In ACM
Jonsson and B. S. Kaliski [2002] give a security reduction for
Symposium on Information, Computer and Communications Security
the security of TLS/SSL when instantiated with RSA-PKCS-1v1_5 (ASIACCS’08), pages 300–311, 2008.
(modelling the PRF as a random oracle). This contrasts with our
work in which the encryption primitive is not explicitly considered J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on
but assumed to be IND-CCA2. real C code. In 6th International Conference on Verification, Model
Checking and Abstract Interpretation (VMCAI’05), pages 363–379,
Padding attacks have been exploited for TLS both for asymmet- 2005.
ric encryption using PKCS #1 [Bleichenbacher, 1998] and for sym-
metric encryption in CBC mode [Yau et al., 2005], when the adver- C. He, M. Sundararajan, A. Datta, A. Derek, and J. C. Mitchell. A modular
sary is given an oracle that says whether plaintexts are correctly correctness proof of IEEE 802.11i and TLS. In 12th ACM conference on
Computer and Communications Security (CCS’05), pages 2–15, 2005.
padded or not. In our model, we do not consider this oracle; further
we assume that an application encrypts only one block at a time. K. E. Hickman. The SSL protocol. Draft specification, Netscape, 1995.
Finally, Klima et al. [2003] use the version check in the Client-
J. Jonsson and J. B. S. Kaliski. On the security of RSA encryption in TLS.
KeyExchange to construct timing attacks over RSA-based sessions.
In 22nd Annual International Cryptology Conference (CRYPTO’02),
In our model we do not consider side channel attacks. pages 127–142, 2002.
J. Jürjens. Security analysis of crypto-based java programs using
Acknowledgments automated theorem provers. In 21st IEEE/ACM International
We thank Martín Abadi, Bruno Blanchet, Andy Gordon, and Bog- Conference on Automated Software Engineering (ASE’06), pages
dan Warinschi for their helpful comments. 167–176, 2006.
A. Kamil and G. Lowe. Analysing TLS in the strand spaces model.
References Technical report, Oxford University Computing Laboratory, 2008.
M. Abadi and C. Fournet. Mobile values, new names, and secure V. Klima, O. Pokorny, and T. Rosa. Attacking RSA-based sessions in
communication. In 28th ACM Symposium on Principles of SSL/TLS. In Cryptographic Hardware and Embedded Systems
Programming Languages (POPL’01), pages 104–115, 2001. (CHES’03), pages 426–440, 2003.
M. Bellare and P. Rogaway. Random oracles are practical: A paradigm for H. Krawczyk. The order of encryption and authentication for protecting
designing efficient protocols. In 1st ACM Conference on Computer and communications (or: How secure is SSL?). In 21st Annual International
Communications Security (CCS’93), pages 62–73, 1993. Cryptology Conference (CRYPTO’01), pages 310–331, 2001.
K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of SSL
implementations of security protocols. In 19th IEEE Computer Security 3.0. In 7th conference on USENIX Security Symposium (SSYM’98),
Foundations Workshop (CSFW’06), pages 139–152, 2006. pages 201–216, 1998.
B. Blanchet. An efficient cryptographic protocol verifier based on Prolog P. Morrissey, N. Smart, and B. Warinschi. A modular security analysis of
rules. In 14th IEEE Computer Security Foundations Workshop the TLS handshake protocol. Cryptology ePrint Archive: Report
(CSFW’01), pages 82–96, 2001. 2008/236, 2008.

B. Blanchet. A computationally sound mechanized prover for security R. Needham and M. Schroeder. Using encryption for authentication in
protocols. In IEEE Symposium on Security and Privacy, pages large networks of computers. Communications of the ACM, 21(12):
140–154, 2006. 993–999, 1978.

B. Blanchet and D. Pointcheval. Automated security proofs with K. Ogata and K. Futatsugi. Equational approach to formal analysis of
sequences of games. In 26th Annual International Cryptology TLS. In 25th IEEE International Conference on Distributed Computing
Conference (CRYPTO’06), pages 537–554, 2006. Systems (ICSCS’05), pages 795–804, 2005.

D. Bleichenbacher. Chosen ciphertext attacks against protocols based on L. C. Paulson. Inductive analysis of the Internet protocol TLS. ACM
rsa encryption standard PKCS #1. In 18th Annual Cryptology Transactions on Information and System Security, 2(3):332–351, 1999.
Conference (CRYPTO’98), pages 1–12, 1998.
D. H. Phan and D. Pointcheval. About the security of ciphers (semantic
S. Chaki and A. Datta. Automated verification of security protocol security and pseudo-random permutations). In Selected Areas in
implementations. Technical Report CMU-Cylab-08-002, Carnegie Cryptography, pages 182–197, 2004.
Mellon University, 2008.
D. Syme. F#, 2005. http://research.microsoft.com/fsharp/.
T. Dierks and C. Allen. The TLS protocol version 1.0. RFC 2246, IETF,
1999. D. Wagner and B. Schneier. Analysis of the SSL 3.0 protocol. In 2nd
USENIX Workshop on Electronic Commerce (WOEC’96), pages 29–40,
T. Dierks and E. Rescorla. The Transport Layer Security (TLS) protocol 1996.
version 1.1. RFC 4346, IETF, 2006.
A. K. L. Yau, K. G. Paterson, and C. J. Mitchell. Padding oracle attacks on
T. Dierks and E. Rescorla. The Transport Layer Security (TLS) protocol CBC-mode encryption with secret and random IVs. In Fast Software
version 1.2. Internet Draft, IETF, 2008. Encryption, pages 299–319, 2005.

468