doc-src/TutorialI/Protocol/protocol.tex

removed obsolete IFOL.thy/FOL.thy values;

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

\index{protocols!security|(}

%crypto primitives 
\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.  The nonce in the reply must be cryptographically
protected, since otherwise an adversary could easily replace it by a
different one. 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}

\index{Needham-Schroeder 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\index{Lowe, Gavin|(} 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}  &&
      \qquad 3'.&\quad  C\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.

Whether this counts as an attack has been disputed.  In protocols of this
type, we normally assume that the other party is honest.  To be honest
means to obey the protocol rules, so Alice's running the protocol with
Charlie does not make her dishonest, just careless.  After Lowe's
attack, Alice has no grounds for complaint: this protocol does not have to
guarantee anything if you run it with a bad person.  Bob does have
grounds for complaint, however: the protocol tells him that he is
communicating with Alice (who is honest) but it does not guarantee
secrecy of the nonces.

Lowe also suggested a correction, 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.  Below, we shall look at parts of this protocol's correctness
proof. 

In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)}
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.%
\index{Needham-Schroeder protocol|)}


\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.  In the real world, decryption with the
wrong key succeeds but yields garbage.  Our model of encryption is
realistic if encryption adds some redundancy to the plaintext, such as a
checksum, so that garbage can be detected.


\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.
Thus he accumulates additional keys and nonces.  These he can use 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:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \
analz\ H\
\isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline
\ \ \ \ Snd:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ analz\ H\
\isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline
\ \ \ \ Decrypt\ [dest]:\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\
K)\ \isasymin\ analz\ H\isasymrbrakk\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
\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Y\ \isasymin
\ synth\ H\isasymrbrakk\ \isasymLongrightarrow\
{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ synth\ H"\isanewline
\ \ \ \ Crypt\ [intro]:\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Key K\
\isasymin \ H\isasymrbrakk\ \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
$A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.
A trace is simply a list, constructed in reverse
using~\isa{\#}.  Other event types include reception of messages (when
we want to make it explicit) and an agent's storing a fact.

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:
\begin{isabelle}
\ \ \ \ \ knows\ Spy\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ insert X\ (knows\ Spy\ evs)
\end{isabelle}
%
Combinations of functions express other important
sets of messages derived from~\isa{evs}:
\begin{itemize}
\item \isa{analz (knows Spy evs)} is everything that the spy could
learn by decryption
\item \isa{synth (analz (knows Spy evs))} is everything 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.  It is defined in terms of
\isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is
not a proper constant, so we declare it using \isacommand{syntax}
(cf.\ \S\ref{sec:syntax-translations}).
\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\ (knows\ Spy\ 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}\label{sec:regularity}

Secrecy properties can be 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
\isa{A}'s 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\ (knows\ Spy\ 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}.  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}).  

The proof is trivial.  No legitimate protocol rule sends any keys
at all, so only \isa{Fake} is relevant.  Indeed,
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, who must have known this key already. 
Either way, the induction hypothesis applies.

\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 short:
induction, simplification, \isa{blast}.  The first line uses the rule
\isa{rev_mp} to prepare the induction by moving two assumptions into the 
induction formula.
\begin{isabelle}
\isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline
\ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\
NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\
evs);\isanewline
\ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\
A\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\ evs);\isanewline
\ \ \ \ \ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline
\ \ \ \ \ \isasymLongrightarrow \ Nonce\ NA\ \isasymin \ analz\ (knows\
Spy\ evs)"\isanewline
\isacommand{apply}\ (erule\ rev_mp,\ erule\ rev_mp)\isanewline
\isacommand{apply}\ (erule\ ns_public.induct,\ simp_all)\isanewline
\isacommand{apply}\ (blast\ intro:\ analz_insertI)+\isanewline
\isacommand{done}
\end{isabelle}

The following 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 similar to the previous one.
\begin{isabelle}
\isacommand{lemma}\ unique_NA:\ \isanewline
\ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(knows\ Spy\ evs);\ \ \isanewline
\ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(knows\ Spy\ evs);\ \ \isanewline
\ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (knows\ Spy\ 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 because they fail for the original protocol.  The following
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\ (knows\ Spy\ evs)"
\end{isabelle}
%
To prove it, we must formulate the induction properly (one of the
assumptions mentions~\isa{evs}), apply induction, and simplify:
\begin{isabelle}
\isacommand{apply}\ (erule\ rev_mp,\ erule\ ns_public.induct,\ simp_all)
\end{isabelle}
%
The proof states are too complicated to present in full.  
Let's examine the simplest subgoal, that for message~1.  The following
event has just occurred:
\[ 1.\quad  A'\to B'  : \comp{Na',A'}\sb{Kb'} \]
The variables above have been primed because this step
belongs to a different run from that referred to in the theorem
statement --- the theorem
refers to a past instance of message~2, while this subgoal
concerns message~1 being sent just now.
In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$
we have \isa{Ba} and~\isa{NAa}:
\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}
%
The simplifier has used a 
default simplification rule that does a case
analysis for each encrypted message on whether or not the decryption key
is compromised.
\begin{isabelle} 
analz\ (insert\ (Crypt\ K\ X)\ H)\ =\isanewline 
\ (if\ Key\ (invKey\ K)\ \isasymin \ analz\ H\isanewline
\ \ then\ insert\
(Crypt\ K\ X)\ (anal\ z\ (insert\ X\ H))\isanewline 
\ \ else\ insert\ (Crypt\ K\ X)\ (analz\ H)) 
\rulename{analz_Crypt_if} 
\end{isabelle} 
The simplifier has also used \isa{Spy_see_priK}, proved in
{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}.

Recall that this subgoal concerns the case
where the last message to be sent was
\[ 1.\quad  A'\to B'  : \comp{Na',A'}\sb{Kb'}. \]
This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised,
allowing the spy to decrypt the message.  The Isabelle subgoal says
precisely this, if we allow for its choice of variable names.
Proving \isa{NB\ \isasymnoteq \ NAa} is easy: \isa{NB} was
sent earlier, while \isa{NAa} is fresh; formally, 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, such as whether or not the message just sent is
the very message mentioned in the theorem statement.
Some of the cases 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 theorems about the protocol are not hard to prove.  The
following one asserts a form of \emph{authenticity}: if
\isa{B} has sent an instance of message~2 to~\isa{A} and has received the
expected reply, then that reply really originated with~\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.

\medskip

Detailed information on this protocol verification technique can be found
elsewhere~\cite{paulson-jcs}, including proofs of an Internet
protocol~\cite{paulson-tls}.  We must stress that the protocol discussed
in this chapter is trivial.  There are only three messages; no keys are
exchanged; we merely have to prove that encrypted data remains secret. 
Real world protocols are much longer and distribute many secrets to their
participants.  To be realistic, the model has to include the possibility
of keys being lost dynamically due to carelessness.  If those keys have
been used to encrypt other sensitive information, there may be cascading
losses.  We may still be able to establish a bound on the losses and to
prove that other protocol runs function
correctly~\cite{paulson-yahalom}.  Proofs of real-world protocols follow
the strategy illustrated above, but the subgoals can
be much bigger and there are more of them.
\index{protocols!security|)}

\endinput