数理解析研究所講究録
第 1562 巻 2007 年 79-86

79

Verifying security protocols using theorem provers
Miki Tanaka
National Institute of Information and Communications Technology
Koganei, Tokyo 184-8795, Japan
Email: miki.tanaka@nict.go.jp
Abstract

This is a report on a project in formal verification of cryptographic
protocol. We adapt Paulson’s work of verification of TLS (Transport
Security Layer) on $Isabelle/HOL[1]$ to the proof-assistant Coq. Paulson’s
trace model of TLS is translated into the Coq syntax and the proofs ofsecurity properties are explicitly constructed on the Coq system.

1

Introduction

It has been understood that getting security proofs right is very subtle and difficult. Hence, formal verification of security, employing so called formal method
technology has become a recent challenge in the field. The idea is to use somestrictly defined language (formal language) to model and reason about the system of which you want to verify the properties. Here (strictly defined” in effectmeans that the language and the reasoning mechanism are syntactically explicitly defined so that the reasoning process can be rigidly executed by computers.
Therefore, if one can establish a proof, in a formal manner using such techniques, that a security system has a certain security property, then, it is a goodquality guarantee of security for the system, modulo the assumptions with themodelling. Of course one can argue what counts as a “good quality guarantee“,
but at least here, there is no room for human errors that come to light after
many years in the process of machine reasoning.
Application of such technology to providing security guarantees for cryptographic protocols has been attempted for a while by now, starting from aroundthe discovery of an attack to the Needham-Schroeder Public Key protocol by
Lowe using a model-checker in 1995. Since then there have been various different
techniques in formal method at varying level in abstraction applied to security
proofs. Among those techniques we are interested in automated theorem proving because it allows for realistic modelling constraints and for extensibility withverification that takes computational complexity as pects into account.
We report on a study on Paulson’s formal verification of TLS (bansport
Layer Security) using Isabelle [1]. We adapted Paulson’s work to the proof assitant Coq, by translating the formal model into the Coq syntax and construct-80
ing the proof on Coq system. In the following we take a quick look at boththe method and the result: after reviewing the notion of automated theorem
proving itself, we quickly go though the syntax, or equivalently, the language,
for describing protocol execution on theorem provers. We don’t give the precise
definition of the syntax but it is the same as Paulson’s syntax, presented in thestyle of Coq. Then we briefly explain some of the security properties of TLS
that are proved by Paulson and also give their representations in Coq.

2

Automated Theorem Proving

Automated theorem proving is a research for using computers to reason in formal
languages based on various logics. Given that mathematical logic can be viewed
as pure symbolic manipulation, we can expect that computers can go quite far
with it, although we cannot expect them to provide a complete proof for all
possible valid statements
In this report we are interested in systems that use expressive higher orderlogics, and in such cases, the systems cannot be fully automated. Instead they
are often “interactive”, indicating that the users need to provide guides to thesystem when proving theorems. To what extent human involvement is required
differs depending on the system.
Paulson used interactive theorem prover Isabelle with higher order logic toprove some security property of the protocol Ransport Layer Security [1]. Both
Isabelle and Coq are in principle an LCF-style generic theorem prover. Isabelle isequipped with relatively strong automation, and is originally written by Paulson
and others [2]. The automation is based on the two parts called “simplifier” (therewriting engine) and “classical reasoner” (based on the tableaux method). Coq
is based on an intuitionistic type theory called Calculus of Indutive Construction
and allows one to extract certified programs from proofs.

3

Verification of Transport Layer Security

Paulson used interactive theorem prover Isabelle with higher order logic to provesome security property of the protocol Transport Layer Security [1].

3.1

TLS

TLS (Transport Layer Security, formerly called SSL, Secure Socket Layer) is a
protocol that provides secure connection above transport protocols such as TCP
and below application protocols such as HTTP, SMTP, etc. Currently, TLS ismostly used in combination with those application protocols and form HTTPS,
etc., to provide the secure connection version of those protocols. As it is used
extensibly in many activities by common users over the Internet, it has beenstandardized by IETF as RFC2246 [4] first time in 1999 (version 1.0). Originally
it was developed by Netscape as SSL from around 1996 and the current version
is TLSvl.1.

81
TLS protocol starts with a phase called “handshake” protocol. This phase isfor negotiation between the client and server on the encryption algorithms andso on (cipher suite) to be used and establishing session keys using public-key
based key exchange, before actually starting to send encrypted messages overthe connection. Some certificate issuing authority is typically assumed for the
public key based key exchange, providing authentication only for the server.
3.1.1

TLS Handshake

Our main concern is the handshake part of TLS since this is the part of the TLS
protocol Paulson modelled using Isabelle. In this section, we briefly explain asimplified version of this protocol as in [1]. Formal models are constructed basedon this version.
The client starts the negotiation by sending the ClientHello message containing his own name, a nonce Na, sessionID, and a cipher suite that the client wants
to use in the following communication. Receiving this, the server responds with
ServerHello message which contains another nonce Nb, sessionID and anothercipher suite of his own choice. Following ServerHello, the server also sends tothe client his own public key certificate signed by the CA. On receiving these,
the client generate another nonce called “pre-master secret (PMS)” and send it
to the server encrypted by the public key of the server (ClientKeyExchange).

Only the server should be able to decrypt this message, and hence, at this point,
the client and server share three nonces Na, Nb, PMS, and PMS is a sharedsecret. From these three, the both parties compute the “master secret (MS)”using some pseudo-random function. From this master secret both the client
and the server compute session keys to be used to encrypt subsequent communication. As confirmation, ach sends Finished messages, which consist of all
the preceding messages exchanged between them encrypted with the session key
just established.
$e$

3.2

Modelling Protocols

In order to model protocol execution syntactically, we take a view that communication protocol executions consist of sequences of message exchanges andsome related incidents (or, say, actions). We model such actions as “events” andthe execution of protocols are modelled by the notion of “traces”, which are defined as sequences (lists) of events. Then the security properties we would liketo prove become those of the set of traces that are associated to the particular
protocol of interest. Since lists are one of the most basic inductively defined
datatypes, the proofs of properties of traces are basically done by induction onlists.

3.2.1

A quick look on the syntax

The syntax consists of the following datatypes: agents, message, event, key.

82
Agents, Keys, Messages The datatype agent has three constructors. spy
and server to represent the assumed adversary and the assumed CA who signs
public key certificates. The third constructor Friend takes a natural number as
the index to represent unbounded number of ordinary participants.
Inductive agent

$:=$

Spy

$|$

Server$|$Friend : $natarrow agent$.

Agents are divided into two groups: whether they belong to the subset bad ornot. We as sume two axioms stating that $Spy\in bad$ and $Server\not\in bad$ . For Friend, in Coq it is also necessary to state explicitly that for any natural number
bad holds. The private keys of agents ineither Friend $i\in$ bad or Friend
bad are at Spy disposal.
The datatype keys are defined indirectly using functions. Keys for encryption and those for decryption are as sociated using the $invKey$ function. Publickeys are defined as publicKey a for any agent , and private keys are definedby composition: privateKey a $invKey$ (publ $icKeya$ ). The two kinds of sesvion keys, clientK and serverK, which are derived after successful execution ofhandshake, are defined using the function sessionK which takes three natural
numbers (nonces) and a flag indicating whether it is for the client or the server.
The fact that any session key is a symmetric key is stated as $invKeyk\cdot k$ .
We also need to state the injectivity of these functions so that we can concluded
the equality of the arguments from the equality of the values.
The datatype message is defined inductively: constructors Agent and Key arefor coercing data of type agent and key to those of type message. Similarly,
Nonce and Number are for natural numbers. Hash and MPair take one or two
messages, respectively, to produce another message, which is the hash and the) of the arguments. Finally crypt takes a key and apair (notation
message to produce a message, which is the encrypted message using the key.
$i$

$i$

$i\not\in$

$s$

.

$a$

$k$

$\{|x$.

$y|\}$

Events The datatype event corresponds to execution steps of protocols. An
execution of the protocol is modelled as a list of events, which are called “traces”.
We only need part of Paulson’s theory Event for the verification of TLS. We
distinguish two different kinds of event: says a $bx$ , where a are agents andis a message, represents the event when agent a sends message to agent .
The second kind, Notes a represents the event that agent a internally takenote of message .
$b$

$x$

$x$

$b$

$x$

$x$

Functions on message sets In the analysis, several functions on messages
are used: the function analz takes a set of messages and returns the set of
messages one can obtain by decomposing pairs and decrypting using the keys
contained in that set. This is the ability one expects for active advervaries interms of retrieving information from a set of known messages. The function
parts is similar but the decryption is obtained for free, providing the set ofsubmessages for the given set of messages. The third function synth is forcomposing new messages: it takes a set of messages as argument and returns theset of messages one can compose from the original set and the publicly available
information using taking pairs and hashes and encrypting using available keys.

83
Initial States and knowledge set The knowledge of agents during thecourse of protocol execution is described using the inductively defined function
knows a evs returns the set ofknows. Given a list of events evs and an agent
messages that agent a can obtain by observing the trace evs. At the start of
execution, all agents have associated initial states of their knowledge. For each
Friendand server, it consists of the set of all public keys of participating
agents and his own private key. For spy, in addition to above, he also knows theset of private keys of bad agents. The function spies is deflned as knows spy.
$s$

$a,$

$i$

3.2.2

TLS traces

Using the language defined in the previous section, each specific protocol ismodelled as a set of rules for generating traces that correspond to runs of the
protocol. For the case of TLS, the following inductive definition defines the set
of TLS traces. Here only a few out of 15 rules are shown.
Inductive tls : Ensemble (list event)tls-nil : In tls nil

$:$

.

$|$

-

(evs: list event) ( : message) ( : agent),
tls-fake :In -tls $evsarrow$
$a$

$x$

$\forall$$|$(synth (analz (spies initState evs)))In
In -tls ( $(Says$ Spy a x): : evs)-

1 tls-spyKeys :(evs: list event) (na nb
In –tls $evsarrow$(analz (spies initState evs))
In(analz (spies initState evs))
In(analz (spies initState evs))
In$\forall$---In -tls(( $Notes$

Spy

$m$

$xarrow$; nat) ( $r$ : role),\langle Nonce na)$arrow$(Nonce nb)(Nonce m)(MPair (Nonce (PRF
na nb))(Key (sessionK na nb $mr$ )))): : evs)
$arrow$$arrow$$m$

tls-nil is the rule for the base case stating that an empty list is a tls $trace$ .
The next two rules, tls-fake and $tls_{-}spyKeys$ are for describing $Spy’ s$ possible
behaviour. $tls4$ ake states that spy can say whatever message he can synthesize

and analyse from messages in his the knowledge he builds up during observing
the protocol run. $tls_{-}spyKeys$ states that when Spy knows three nonces, he canuse them to create a session key.
A new session in the handshake protocol is initiated by application of thefollowing rule:$|$(evs: list event) (na pa sid: nat) (a $b$ : agent),(used evs) (Nonce na)$tlsevsarrow\neg$ In

tls-clientHello :In$arrow$--$\neg(\exists x.

In$\forall$-\exists y, \exists z, PRFxyz-na)arrow$tls (( $Says$ a{ (Agent a). (Nonce na), (Number sid), (Number pa)
$b$

$|$

$|$

}): : evs)

An agent (client) should use a fresh nonce that is not in the range of $PRF$ tocreate a correct message to send to the other party (server).

84
The rule that plays the central role in the TLS handshake protocol is this:(evs: list event) (pms: nat) (a $bb$ ‘ : agent) (kb: key),(used evs) (Nonce pms)
$evsarrow\neg$ In:$|tls_{-}clientKeyExch$

In -tls$\forall$$arrow$-$PRFxyz=$ pms)kb)) $evsarrow$
List. In (Says ‘ a (certificate(Crypt kb (Nonce pms))): :In -tls (( $Says$ a(Notes aAgent , Nonce pms$\neg$($\exists x,$$\exists y,$$\exists z,$$arrow$

$b$

$b$

$b$

$b$

$\{|$

$|\}$

); : evs)

After the client and the server finished their hello messages, the client createsanother nonce pms and uses server’s public key $kb$ to send it securely. Afterapplication of this rule, the both party now have a shared secret pms.

3.3

Properties Proved

Paulson categorises the properties he proved in several criteria and discusses
them in detail in [1]. We consider that what he calls security theorems are thefinal goals of analysis. We proved in Coq all those security theorems and mostof other properties Paulson proved in his TLS theory script. In this section, we
present some of those security theorems using Coq syntax in order to give theflavour of the properties formally proved in Paulson’s model.
The property $analz_{-}insert_{-}key$ states that the loss of a session key won’t
allow the spy to learn more nonces that he should not know.
Lemma $analz_{-}insert_{-}key$ :In $-tlsevsarrow$(In -(analz (Add
(Nonce $n$ ))$rightarrow$

(In

–

-

$\forall$(evs: list event) ( $xyzn$ : nat) ( $r$ : role),$(8pies$

initState evs) (Key (sessionK $xyzr)))$ )(analz (spies initState evs)) (Nonce $n)$ ).

$analz_{-}insert_{-}key$

is proved by application of a useful lemma:(evs: list event) ( : nat) ,Lemma $analz_{-}image_{-}keys$ :In –tls evs, In $-Kkarrow$: Ensemble key, ($\forall$$n$$arrow$$\forall k$$\forall K$$\exists x$. .
$\exists y$$\exists z,$$\exists r$.

$xyzr-k$)sessionK$({\rm Im}--K$ Key) (spies initState evs))) (Nonce $n)$ )(analz (Union(In(analz (spies initState evs)) (Nonce $n)$ ).
(In$arrow$–-$rightarrow$–

This lemma states that, even if you add a set of session keys to Spy knowledge,
it does not let spy to learn any more nonce. The proof of $anal\bm{z}_{-}image.\lambda eys$ isquite complex.
Another set of examples we present here is about pms and ms.
$s$Lemma $Spy_{-}not_{-}see_{-}pms$ :V (evs: list event) (pms: nat) (a : agent),
Agent , Nonce pms
List. In (Notes a
$b$

$\{|$

$b$

$|\}$

)

$evsarrow$

In $-tlsevsarrow$
In –bad $aarrow\neg$ In –bad $barrow$(analz (spies initState evs)) (Nonce pms).
In$\neg$$\neg$–

85
This lemma states that when agents a and are not bad and the rule clientKeyExch
was applied between them and a shared secret pms is established, then pms is
not derivable from the Spy’s current knowledge. This lemma is used in proofs ofother lemmas. In particular, it is used in the similar lemma about the mastersecret ms$b$Lemma $Spy_{-}not_{-}see_{-}ms$ :(evs: list event) (pms na nb: $nat$ ) (a $b:$ agent) ,Agent $b.$ Nonce pms 1}) $evsarrow$
List. In (Notes a
In -tls $evsarrow$
In –bad $aarrow\neg$ In $-badbarrow$(analz (spies initState evs)) (Nonce $(PRF$ pms na nb)).
In$\forall$$\{|$$\neg$$\neg$-The proofs of both lemmas are quite substantial.

4

Proof in Coq

Adapting the proof scripts in Isabelle to Coq was not a simple task. This mainly
due to the fact that Isabelle is equipped with an efficient term rewriting engine
and proof search engine that allow reasonable automation, while Coq is more
focused on constructive proofs and proof checking and is equipped with some
automation tactics. At the moment, what we have proved are the lemmas given
by Paulson, but still, we consider this experience to be a valuable one. Paulson’s
original Isabelle proof scripts are well adapted for maximising the performanceof Isabelle’s simplifier and the reasoner; the lemmas are formulated in such a waythat the reasoner and the simplifier can make most use of them. However, thoseformulations were not the best for constructing more explicit proofs in Coq. So
we reformulated many of the lemmas and, as far as proving TLS properties go,
we could prove them without the help of many of lemmas Paulson prepared to
be used by the simplifier. Our current scripts (consisting of Message. , Event.v,
Public. and tls.v) have 1611emmas proved in total. Paulson’s Isabelle scripts
have more than 270 lemmas, although simple comparison is not appropriate
here because the Coq scripts do not contain some lemmas present in Isabelle
scripts that are not relevant for proving TLS properties. For many cases where
the proofs in Isabelle were just the combination of (blast’ and a few lines ofcodes for treating special subgoals, we had to explicitly construct proofs using
induction on the construction of TLS traces, which would normally produce 15
subgoals to start with. On the other hand, we could dispense with many lemmas
that are rather simple and seem to exist to help automation, because they areoften not very usable in the explicit proofs we need to provide with Coq. Again,
the numbers are only for a reference but the Coq scripts contain around 6500
lines of codes, while those for Isabelle scripts add up to around 2600.
As for the automation in Coq, we added to the Hint database all the constructors from the syntax, and some axioms stating several decision properties.
The basic strategy for most proofs is induction on the structure of TLS traces,
often combined with the case analysis for an agent being bad or not.
$v$

$v$

86

5

Conclusion

We have used the proof-assistant Coq to reformulate Paulson’s modelling andformal security proof of Transport Layer Security. Although two theorem provers
share a lot in common in principle, their usage and their mechanisms differ substantially, and hence, the resulting proofs are also very different. Our proofs
are more explicitly constructed than those done in Isabelle due to the fact thatthe level of automation is different with Coq. The proof script consists of four
files as is the case for Isabelle. We will soon make public the Coq proof scripts
adapted to V8.1.

Acknowledgment
This research was partially supported by the Ministry of Education, Culture,
Sports, Science and Technology, Japan (MEXT), Grant-in-Aid for Young Scientists (B), Grant number 187602935003.

References[1] L. Paulson, “Inductive analysis of the internet protocol TLS”, ACM Transactions on Information and System Security, vol.2, No.3, pages 332-351,

1999.

[2] T. Nipkow, L. Paulson, M. Wenzel, $Isabelle/HOL$ : a proof assistant forhigher-order logic”, Lecture Notes in Computer Science, Vol. 2283, 2002.
[3] The Coq proof assistant, http: $//coq$ . inria. fr.
[4] T. Dierks and C. Allen, “The TLS Protocol”, IETF, RFC 2246, January
1999. http: $//www$ . ietf. $org/rfc/rfc2246$ . txt.