doc-src/TutorialI/Protocol/protocol.tex

 % $Id$
 \chapter{Case Study: Verifying a Cryptographic Protocol}
 \label{chap:crypto}
 
-%crypto primitives FIXME: GET RID OF MANY
+%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
+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. 
+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

 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!
+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

 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}   & 
+  &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}
+  &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.
 
-Lowe also suggested a fix, namely to include Bob's name in message~2:
+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.
+will Bob.  Below, we shall look at parts of this protocol's correctness
+proof. 
 
 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

 \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}:
+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

 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.
+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,
-perhaps learning additional keys and nonces.  He uses the items he has
-accumulated to compose new messages, which he may send to anybody.  
+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\
+\ \ \ \ Inj\ [intro,simp]\ :\ "X\ \isasymin \ H\
 \isasymLongrightarrow\ X\
 \isasymin
 \ analz\ H"\isanewline
-\ \ \ \ Fst:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\
+\ \ \ \ Fst:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \
+analz\ H\
 \isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline
-\ \ \ \ Snd:\ \ \ \ \ "\isacharbraceleft |X,Y|\isacharbraceright \ \isasymin \ analz\ H\
+\ \ \ \ Snd:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ analz\ H\
 \isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline
 \ \ \ \ Decrypt\ [dest]:\ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ "[|Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\
-K):\ analz\ H|]\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\
+K):\ 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}$. 

 \ \ \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
+\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Y\ \isasymin
+\ synth\ H\isasymrbrakk\ \isasymLongrightarrow\
+{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ synth\ H"\isanewline
 \ \ \ \ Crypt\ [intro]:\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ "[|X\ \isasymin \ synth\ H;\ \ Key K\
-\isasymin \ H|]\ \isasymLongrightarrow\ Crypt\ K\ X\
+\ \ \ \ \ \ \ \ \ \ \ \ \ "{\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

 
 
 \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{\#}.  
+\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{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}:
+message that was sent:
+\begin{isabelle}
+\ \ \ \ \ knows\ Spy\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\
+\isacharbraceleft X\isacharbraceright \ \isasymunion\ (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 the items that the spy could
+\item \isa{analz (knows Spy evs)} is everything that the spy could
 learn by decryption
-\item \isa{synth (analz (knows Spy evs))} is the items that the spy
+\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, is defined in terms of
-\isa{invKey} and \isa{pubK} by a translation.
+\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}
 \begin{isabelle}
 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
 \isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)"
 \end{isabelle}

 \ \ \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
+\ \ \ 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

 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 
+\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
-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.
+\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\ (spies\ evs))\ =\ (A\ \isasymin \
+(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}.  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}):
+\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

 \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.
+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 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.
+and he doesn't know this particular value.  The proof script is short:
+induction, simplification, \isa{blast}.
+\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(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
+\ \ \ \ \ "\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, 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.
+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\ (spies\ evs)"
-\end{isabelle}
-%
-To prove this, we must formulate the induction properly (one of the
-assumptions mentions~\isa{evs}), apply induction, and simplify.
+\ \ \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 just look
-at the easiest subgoal, that for message~1:
+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.\ \ \ \ }\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}). 
+%
+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, some of which are proved by unicity, others by
+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 proofs are straightforward.  This theorem asserts that if
+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 came from~\isa{A}.  The proof is a
-simple induction.
+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 
+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
+
+\medskip
+
+Detailed information on this protocol verification technique can be found
 elsewhere~\cite{paulson-jcs}, including proofs of an Internet
-protocol~\cite{paulson-tls}.
+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.
 
 
 \endinput