doc-src/TutorialI/Protocol/protocol.tex

*** empty log message ***

% $Id$
\chapter{Case Study: Verifying a Cryptographic Protocol}
\label{chap:crypto}

%crypto primitives FIXME: GET RID OF MANY
\def\lbb{\mathopen{\{\kern-.30em|}}
\def\rbb{\mathclose{|\kern-.32em\}}}
\def\comp#1{\lbb#1\rbb}

Communications security is an ancient art.  Julius Caesar is said to have
encrypted his messages, shifting each letter three places along the
alphabet.  Mary Queen of Scots was convicted of treason after a cipher used
in her letters was broken.  Today's postal system incorporates security
features. The envelope provides a degree of
\emph{secrecy}.  The signature provides \emph{authenticity} (proof of
origin), as do departmental stamps and letterheads. 

Networks are vulnerable: messages pass through many computers, any of which
might be controlled by an adversary, who thus can capture or redirect
messages.  People who wish to communicate securely over such a network can
use cryptography, but if they are to understand each other, they need to
follow a
\emph{protocol}: a pre-arranged sequence of message formats. 

Protocols can be attacked in many ways, even if encryption is unbreakable. 
A \emph{splicing attack} involves an adversary's sending a message composed
of parts of several old messages.  This fake message may have the correct
format, fooling an honest party.  The adversary might be able to masquerade
as somebody else, or he might obtain a secret key.

\emph{Nonces} help prevent splicing attacks. A typical nonce is a 20-byte
random number. Each message that requires a reply incorporates a nonce. The
reply must include a copy of that nonce, to prove that it is not a replay of
a past message.  Nonces must be cryptographically protected, since
otherwise an adversary could easily generate fakes. You should be starting
to see that protocol design is tricky!

Researchers are developing methods for proving the correctness of security
protocols.  The Needham-Schroeder public-key
protocol~\cite{needham-schroeder} has become a standard test case. 
Proposed in 1978, it was found to be defective nearly two decades
later~\cite{lowe-fdr}.  This toy protocol will be useful in demonstrating
how to verify protocols using Isabelle.


\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol}

This protocol uses public-key cryptography. Each person has a private key, known only to
himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she
encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the
matching private key, which is needed in order to decrypt Alice's message.

The core of the Needham-Schroeder protocol consists of three messages:
\begin{alignat*}{2}
  &1.&\quad  A\to B  &: \comp{Na,A}\sb{Kb} \\
  &2.&\quad  B\to A  &: \comp{Na,Nb}\sb{Ka} \\
  &3.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
\end{alignat*}
First, let's understand the notation. In the first message, Alice
sends Bob a message consisting of a nonce generated by Alice~($Na$)
paired  with Alice's name~($A$) and encrypted using Bob's public
key~($Kb$). In the second message, Bob sends Alice a message
consisting of $Na$ paired with a nonce generated by Bob~($Nb$), 
encrypted using Alice's public key~($Ka$). In the last message, Alice
returns $Nb$ to Bob, encrypted using his public key.

When Alice receives Message~2, she knows that Bob has acted on her
message, since only he could have decrypted
$\comp{Na,A}\sb{Kb}$ and extracted~$Na$.  That is precisely what
nonces are for.  Similarly, message~3 assures Bob that Alice is
active.  But the protocol was widely believed~\cite{ban89} to satisfy a
further property: that
$Na$ and~$Nb$ were secrets shared by Alice and Bob.  (Many
protocols generate such shared secrets, which can be used
to lessen the reliance on slow public-key operations.)  Lowe found this
claim to be false: if Alice runs the protocol with someone untrustworthy
(Charlie say), then he can start a new run with another agent (Bob say). 
Charlie uses Alice as an oracle, masquerading as
Alice to Bob~\cite{lowe-fdr}.
\begin{alignat*}{4}
  &1.&\quad  A\to C  &: \comp{Na,A}\sb{Kc}   & 
      \qquad 1'.&\quad  C\to B  &: \comp{Na,A}\sb{Kb} \\
  &2.&\quad  B\to A  &: \comp{Na,Nb}\sb{Ka} \\
  &3.&\quad  A\to C  &: \comp{Nb}\sb{Kc}  &
      3'.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
\end{alignat*}
In messages~1 and~3, Charlie removes the encryption using his private
key and re-encrypts Alice's messages using Bob's public key. Bob is
left thinking he has run the protocol with Alice, which was not
Alice's intention, and Bob is unaware that the ``secret'' nonces are
known to Charlie.  This is a typical man-in-the-middle attack launched
by an insider.

Lowe also suggested a fix, namely to include Bob's name in message~2:
\begin{alignat*}{2}
  &1.&\quad  A\to B  &: \comp{Na,A}\sb{Kb} \\
  &2.&\quad  B\to A  &: \comp{Na,Nb,B}\sb{Ka} \\
  &3.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
\end{alignat*}
If Charlie tries the same attack, Alice will receive the message
$\comp{Na,Nb,B}\sb{Ka}$ when she was expecting to receive
$\comp{Na,Nb,C}\sb{Ka}$.  She will abandon the run, and eventually so
will Bob.

In ground-breaking work, Lowe~\cite{lowe-fdr} showed how such attacks
could be found automatically using a model checker.  An alternative,
which we shall examine below, is to prove protocols correct.  Proofs
can be done under more realistic assumptions because our model does
not have to be finite.  The strategy is to formalize the operational
semantics of the system and to prove security properties using rule
induction.


\section{Agents and Messages}

All protocol specifications refer to a syntactic theory of messages. 
Datatype
\isa{agent} introduces the constant \isa{Server} (a trusted central
machine, needed for some protocols), an infinite population of ``friendly''
agents, and the~\isa{Spy}:
\begin{isabelle}
\isacommand{datatype}\ agent\ =\ Server\ |\ Friend\ nat\ |\ Spy
\end{isabelle}
%
Keys are just natural numbers.  Function \isa{invKey} maps a public key to
the matching private key, and vice versa:
\begin{isabelle}
\isacommand{types}\ key\ =\ nat\isanewline
\isacommand{consts}\ invKey\ ::\ "key=>key"
\end{isabelle}
Datatype
\isa{msg} introduces the message forms, which include agent names, nonces,
keys, compound messages, and encryptions.  
\begin{isabelle}
\isacommand{datatype}\isanewline
\ \ \ \ \ msg\ =\ Agent\ \ agent\ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ |\ Nonce\ \ nat\ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ |\ Key\ \ \ \ key\ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ |\ MPair\ \ msg\ msg\ \ \ \isanewline
\ \ \ \ \ \ \ \ \ |\ Crypt\ \ key\ msg\ \ \ \isanewline
\end{isabelle}
%
The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$
abbreviates
$\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$.

Since datatype constructors are injective, we have the theorem
\begin{isabelle}
Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand\ X=X'.
\end{isabelle}
A ciphertext can be decrypted using only one key and
can yield only one plaintext.  This assumption is realistic if encryption
includes some built-in redundancy.


\section{Modelling the Adversary}

The spy is part of the system and must be built into the model.  He is
a malicious user who does not have to follow the protocol.  He
watches the network and uses any keys he knows to decrypt messages,
perhaps learning additional keys and nonces.  He uses the items he has
accumulated to compose new messages, which he may send to anybody.  

Two functions enable us to formalize this behaviour: \isa{analz} and
\isa{synth}.  Each function maps a sets of messages to another set of
messages. The set \isa{analz H} formalizes what the adversary can learn
from the set of messages~$H$.  The closure properties of this set are
defined inductively.
\begin{isabelle}
\isacommand{consts}\ \ analz\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline
\isacommand{inductive}\ "analz\ H"\isanewline
\ \ \isakeyword{intros}\ \isanewline
\ \ \ \ Inj\ [intro,simp]\ :\ \ \ "X\ \isasymin \ H\
\isasymLongrightarrow\ X\
\isasymin
\ analz\ H"\isanewline
\ \ \ \ Fst:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\
\isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline
\ \ \ \ Snd:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\
\isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline
\ \ \ \ Decrypt\ [dest]:\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ "[|Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\
K):\ analz\ H|]\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H"
\end{isabelle}
%
Note the \isa{Decrypt} rule: the spy can decrypt a
message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. 
Properties proved by rule induction include the following:
\begin{isabelle}
G\isasymsubseteq H\ \isasymLongrightarrow\ analz(G)\ \isasymsubseteq\
analz(H)
\rulename{analz_mono}\isanewline
analz (analz H) = analz H
\rulename{analz_idem} 
\end{isabelle}

The set of fake messages that an intruder could invent
starting from~\isa{H} is \isa{synth(analz~H)}, where \isa{synth H}
formalizes what the adversary can build from the set of messages~$H$.  
\begin{isabelle}
\isacommand{consts}\ \ synth\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline
\isacommand{inductive}\ "synth\ H"\isanewline
\ \ \isakeyword{intros}\ \isanewline
\ \ \ \ Inj\ \ \ [intro]:\ "X\ \isasymin \ H\ \isasymLongrightarrow\
X\ \isasymin \ synth\ H"\isanewline
\ \ \ \ Agent\ [intro]:\ "Agent\ agt\ \isasymin \ synth\ H"\isanewline
\ \ \ \ MPair\ [intro]:\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Y\ \isasymin
\ synth\ H|]\ \isasymLongrightarrow\
\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ synth\ H"\isanewline
\ \ \ \ Crypt\ [intro]:\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Key K\
\isasymin \ H|]\ \isasymLongrightarrow\ Crypt\ K\ X\
\isasymin \ synth\ H"
\end{isabelle}
The set includes all agent names.  Nonces and keys are assumed to be
unguessable, so none are included beyond those already in~$H$.   Two
elements of \isa{synth H} can be combined, and an element can be encrypted
using a key present in~$H$.

Like \isa{analz}, this set operator is monotone and idempotent.  It also
satisfies an interesting equation involving \isa{analz}:
\begin{isabelle}
analz (synth H)\ =\ analz H\ \isasymunion\ synth H
\rulename{analz_synth} 
\end{isabelle}
%
Rule inversion plays a major role in reasoning about \isa{synth}, through
declarations such as this one:
\begin{isabelle}
\isacommand{inductive\_cases}\ Nonce_synth\ [elim!]:\ "Nonce\ n\ \isasymin
\ synth\ H"
\end{isabelle}
%
The resulting elimination rule replaces every assumption of the form
\isa{Nonce\ n\ \isasymin \ synth\ H} by \isa{Nonce\ n\ 
\isasymin \ H}, expressing that a nonce cannot be guessed.  
%The theory also uses rule inversion with constructors \isa{Key}, \isa{Crypt}
%and \isa{MPair} (message pairing).

%
A third operator, \isa{parts}, is useful for stating correctness
properties.  The set
\isa{parts H} consists of the components of elements of~$H$.  This set
includes~\isa{H} and is closed under the projections from a compound
message to its immediate parts. 
Its definition resembles that of \isa{analz} except in the rule
corresponding to the constructor \isa{Crypt}: 
\begin{isabelle}
\ \ \ \ \ Crypt\ K\ X\ \isasymin \ parts\ H\ \isasymLongrightarrow\ X\
\isasymin \ parts\ H
\end{isabelle}
The body of an encrypted message is always regarded as part of it.  We can
use \isa{parts} to express general well-formedness properties of a protocol,
for example, that an uncompromised agent's private key will never be
included as a component of any message.


\section{Event Traces}\label{sec:events}

The system's behaviour is formalized as a set of traces of
\emph{events}.  The most important event, \isa{Says~A~B~X}, expresses the
attempt by~$A$ to send~$B$ the
  message~$X$.  A trace is simply a list, constructed in reverse
using~\isa{\#}.  

Sometimes the protocol requires an agent to generate a new nonce. The
probability that a 20-byte random number has appeared before is effectively
zero.  To formalize this important property, the set \isa{used evs}
denotes the set of all items mentioned in the trace~\isa{evs}.
The function \isa{used} has a straightforward
recursive definition.  Here is the case for \isa{Says} event:
\begin{isabelle}
\ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft
X\isacharbraceright \ \isasymunion\ (used\ evs)
\end{isabelle}

The function \isa{knows} formalizes an agent's knowledge.  Mostly we only
care about the spy's knowledge, and \isa{knows Spy evs} is the set of items
available to the spy in the trace~\isa{evs}.  Already in the empty trace,
the spy starts with some secrets at his disposal, such as the private keys
of compromised users.  After each \isa{Says} event, the spy learns the
message that was sent.  Combinations of functions express other important
concepts involving~\isa{evs}:
\begin{itemize}
\item \isa{analz (knows Spy evs)} is the items that the spy could
learn by decryption
\item \isa{synth (analz (knows Spy evs))} is the items that the spy
could generate
\end{itemize}

The function
\isa{pubK} maps agents to their public keys.  The function
\isa{priK} maps agents to their private keys, is defined in terms of
\isa{invKey} and \isa{pubK} by a translation.
\begin{isabelle}
\isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
\isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
\isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)"
\end{isabelle}
The set \isa{bad} consists of those agents whose private keys are known to
the spy.

Two axioms are asserted about the public-key cryptosystem. 
No two agents have the same public key, and no private key equals
any public key.
\begin{isabelle}
\isacommand{axioms}\isanewline
\ \ inj_pubK:\ \ \ \ \ \ \ \ "inj\ pubK"\isanewline
\ \ priK_neq_pubK:\ \ \ "priK\ A\ \isasymnoteq\ pubK\ B"
\end{isabelle}





\section{Modelling the Protocol}\label{sec:modelling}

Let us formalize the Needham-Schroeder public-key protocol, as corrected by
Lowe:
\begin{alignat*}{2}
  &1.&\quad  A\to B  &: \comp{Na,A}\sb{Kb} \\
  &2.&\quad  B\to A  &: \comp{Na,Nb,B}\sb{Ka} \\
  &3.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
\end{alignat*}

Each protocol step is specified by a rule of an inductive definition.  An
event trace has type \isa{event list}, so we declare the constant
\isa{ns_public} to be a set of such traces.
\begin{isabelle}
\isacommand{consts}\ \ ns_public\ \ ::\ "event\ list\ set"
\end{isabelle}

\begin{figure}
\begin{isabelle}
\isacommand{inductive}\ ns_public\isanewline
\ \ \isakeyword{intros}\ \isanewline
\ \ \ \ \ \ \ \ \ \isanewline
\ \ \ Nil:\ \ "[]\ \isasymin \ ns_public"\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \isanewline
\ \ \ Fake:\ "\isasymlbrakk evsf\ \isasymin \ ns_public;\ \ X\ \isasymin \ synth\ (analz\ (spies\ evsf))\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ Spy\ B\ X\ \ \#\ evsf\ \isasymin \ ns_public"\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \isanewline
\ \ \ NS1:\ \ "\isasymlbrakk evs1\ \isasymin \ ns_public;\ \ Nonce\ NA\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs1\ \ \isasymin \ \ ns_public"\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \isanewline
\ \ \ NS2:\ \ "\isasymlbrakk evs2\ \isasymin \ ns_public;\ \ Nonce\ NB\ \isasymnotin \ used\ evs2;\isanewline
\ \ \ \ \ \ \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs2\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs2\ \ \isasymin \ \ ns_public"\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \isanewline
\ \ \ NS3:\ \ "\isasymlbrakk evs3\ \isasymin \ ns_public;\isanewline
\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs3;\isanewline
\ \ \ \ \ \ \ \ \ \ \ Says\ B'\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymin \ set\ evs3\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \#\ evs3\ \isasymin \
ns_public"
\end{isabelle}
\caption{An Inductive Protocol Definition}\label{fig:ns_public}
\end{figure}

Figure~\ref{fig:ns_public} presents the inductive definition.  The
\isa{Nil} rule introduces the empty trace.  The \isa{Fake} rule models the
adversary's sending a message built from components taken from past
traffic, expressed using the functions \isa{synth} and
\isa{analz}. 
The next three rules model how honest agents would perform the three
protocol steps.  

Here is a detailed explanation of rule \isa{NS2}.
A trace containing an event of the form
\begin{isabelle}
\ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\
NA,\ Agent\ A\isasymrbrace)
\end{isabelle}
%
may be extended by an event of the form
\begin{isabelle}
\ \ \ \ \ Says\ B\ A\ (Crypt\ (pubK\ A)\
\isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace)
\end{isabelle}
where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ \isasymnotin \ used\ evs2}.
Writing the sender as \isa{A'} indicates that \isa{B} does not 
know who sent the message.  Calling the trace variable \isa{evs2} rather
than simply \isa{evs} helps us know where we are in a proof after many
case-splits: every subgoal mentioning \isa{evs2} involves message~2 of the
protocol.

Benefits of this approach are simplicity and clarity.  The semantic model
is set theory, proofs are by induction and the translation from the informal
notation to the inductive rules is straightforward. 


\section{Proving Elementary Properties}

Secrecy properties are hard to prove.  The conclusion of a typical secrecy
theorem is 
\isa{X\ \isasymnotin\ analz (knows Spy evs)}.  The difficulty arises from
having to reason about \isa{analz}, or less formally, showing that the spy
can never learn~\isa{X}.  Much easier is to prove that \isa{X} can never
occur at all.  Such \emph{regularity} properties are typically expressed
using \isa{parts} rather than \isa{analz}.

The following lemma states that \isa{A}'s private key is potentially
known to the spy if and only if \isa{A} belongs to the set \isa{bad} of
compromised agents.  The statement uses \isa{parts}: the very presence of
her private key in a message, whether protected by encryption or not, is
enough to confirm that \isa{A} is compromised.  The proof, like nearly all
protocol proofs, is by induction over traces.
\begin{isabelle}
\isacommand{lemma}\ Spy_see_priK\ [simp]:\ \isanewline
\ \ \ \ \ \ "evs\ \isasymin \ ns_public\isanewline
\ \ \ \ \ \ \ \isasymLongrightarrow \
(Key\ (priK\ A)\ \isasymin \ parts\ (spies\ evs))\ =\ (A\ \isasymin \
bad)"\isanewline
\isacommand{apply}\ (erule\ ns_public.induct,\ simp_all)
\end{isabelle}
%
The induction yields five subgoals, one for each rule in the definition of
\isa{ns_public}.  Informally, the idea is to prove that the protocol
property holds initially (rule \isa{Nil}), is preserved by each of the
legitimate protocol steps (rules \isa{NS1}--\isa{3}), and even is preserved
in the face of anything the spy can do (rule \isa{Fake}).  Simplification
leaves only the \isa{Fake} case (as indicated by the variable name
\isa{evsf}):
\begin{isabelle}
\ 1.\ \isasymAnd X\ evsf.\isanewline
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk evsf\ \isasymin \ ns_public;\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }(Key\ (priK\ A)\ \isasymin \ parts\ (knows\ Spy\ evsf))\ =\ (A\ \isasymin \ bad);\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }X\ \isasymin \ synth\ (analz\ (knows\ Spy\ evsf))\isasymrbrakk \isanewline
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ (Key\ (priK\ A)\ \isasymin \ parts\ (insert\ X\ (knows\ Spy\ evsf)))\ =\isanewline
\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }(A\ \isasymin \
bad)\isanewline
\isacommand{by}\ blast
\end{isabelle}
%
The \isa{Fake} case is proved automatically.  If
\isa{priK~A} is in the extended trace then either (1) it was already in the
original trace or (2) it was
generated by the spy, and so the spy must have known this key already. 
Either way, the induction hypothesis applies.  If the spy can tell himself
something, then he must have known it already.

\emph{Unicity} lemmas are regularity lemmas stating that specified items
can occur only once in a trace.  The following lemma states that a nonce
cannot be used both as $Na$ and as $Nb$ unless
it is known to the spy.  Intuitively, it holds because honest agents
always choose fresh values as nonces; only the spy might reuse a value,
and he doesn't know this particular value.  The proof script is three steps
long.
\begin{isabelle}
\isacommand{lemma}\ no_nonce_NS1_NS2\ [rule_format]:\ \isanewline
\ "evs\ \isasymin \ ns_public\ \isanewline
\ \ \isasymLongrightarrow \ Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \isanewline
\ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace \ \isasymin \ parts\ (spies\ evs)\ \isasymlongrightarrow \ \ \isanewline
\ \ \ \ \ \ Nonce\ NA\ \isasymin \ analz\ (spies\ evs)"
\end{isabelle}

This unicity lemma states that, if \isa{NA} is secret, then its appearance
in any instance of message~1 determines the other components.  The proof is
another easy induction.
\begin{isabelle}
\isacommand{lemma}\ unique_NA:\ \isanewline
\ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline
\ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(spies\ evs);\ \ \isanewline
\ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (spies\ evs);\ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline
\ \ \ \ \ \ \isasymLongrightarrow \ A=A'\ \isasymand \ B=B'"
\end{isabelle}


\section{Proving Secrecy Theorems}\label{sec:secrecy}

The secrecy theorems for Bob (the second participant) are especially
important, since they fail for the original protocol.  This theorem states
that if Bob sends message~2 to Alice, and both agents are uncompromised,
then Bob's nonce will never reach the spy.
\begin{isabelle}
\isacommand{theorem}\ Spy_not_see_NB\ [dest]:\isanewline
\ "\isasymlbrakk Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline
\ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline
\ \ \isasymLongrightarrow \ Nonce\ NB\ \isasymnotin \ analz\ (spies\ evs)"
\end{isabelle}
%
To prove this, we must formulate the induction properly (one of the
assumptions mentions~\isa{evs}), apply induction, and simplify.
The proof states are too complicated to present in full.  
Let's just look
at the easiest subgoal, that for message~1:
\begin{isabelle}
\ 1.\ \isasymAnd Ba\ NAa\ evs1.\isanewline
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk A\ \isasymnotin \ bad;\ B\ \isasymnotin \ bad;\ evs1\ \isasymin \ ns_public;\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NB\ \isasymnotin \ analz\ (knows\ Spy\ evs1);\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NAa\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Ba\ \isasymin \ bad\ \isasymlongrightarrow \isanewline
\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline
\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline
\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }NB\ \isasymnoteq \ NAa
\end{isabelle}
This subgoal refers to another protocol run, in which \isa{B} has sent
message~1 to somebody called~\isa{Ba}.  Agent \isa{Ba} 
is compromised, and so the spy has learnt the nonce that was just sent,
which is called~\isa{NAa}.  We need to know that this nonce differs from the
one we care about, namely~\isa{NB}\@.  They do indeed differ: \isa{NB} was
sent earlier, while \isa{NAa} was chosen to be fresh (we have the assumption
\isa{Nonce\ NAa\ \isasymnotin \ used\ evs1}). 

Note that our reasoning concerned \isa{B}'s participation in another
run.  Agents may engage in several runs concurrently, and some attacks work
by interleaving the messages of two runs.  With model checking, this
possibility can cause a state-space explosion, and for us it
certainly complicates proofs.  The biggest subgoal concerns message~2.  It
splits into several cases, some of which are proved by unicity, others by
the induction hypothesis.  For all those complications, the proofs are
automatic by \isa{blast} with the theorem \isa{no_nonce_NS1_NS2}.

The remaining proofs are straightforward.  This theorem asserts that if
\isa{B} has sent an instance of message~2 to~\isa{A} and has received the
expected reply, then that reply really came from~\isa{A}.  The proof is a
simple induction.
\begin{isabelle}
\isacommand{theorem}\ B_trusts_NS3:\isanewline
\ "\isasymlbrakk Says\ B\ A\ \ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline
\ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ evs;\ \isanewline
\ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \ \ \ \ \ \ \ \ \isanewline
\ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\
evs"
\end{isabelle}

From similar assumptions, we can prove that \isa{A} started the protocol
run by sending an instance of message~1 involving the nonce~\isa{NA}.  For
this theorem, the conclusion is 
\begin{isabelle}
\ \ \ \ \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\
A\isasymrbrace )\ \isasymin \ set\ evs
\end{isabelle}
%
Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA}
remains secret and that message~2 really originates with~\isa{B}.  Even the
flawed protocol establishes these properties for~\isa{A};
the flaw only harms the second participant.
Detailed information on this technique can be found
elsewhere~\cite{paulson-jcs}, including proofs of an Internet
protocol~\cite{paulson-tls}.


\endinput