--- a/doc-src/TutorialI/Protocol/protocol.tex Tue Apr 24 14:26:05 2001 +0200
+++ b/doc-src/TutorialI/Protocol/protocol.tex Tue Apr 24 17:54:49 2001 +0200
@@ -2,7 +2,7 @@
\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}
@@ -10,10 +10,10 @@
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
@@ -31,9 +31,10 @@
\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
@@ -78,11 +79,11 @@
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
@@ -91,7 +92,18 @@
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} \\
@@ -100,7 +112,8 @@
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,
@@ -116,8 +129,8 @@
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}
@@ -149,17 +162,19 @@
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
@@ -170,17 +185,18 @@
\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}
%
@@ -206,12 +222,12 @@
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
@@ -260,10 +276,11 @@
\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
@@ -281,19 +298,26 @@
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
@@ -340,7 +364,7 @@
\ \ \ 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
@@ -397,10 +421,10 @@
notation to the inductive rules is straightforward.
-\section{Proving Elementary Properties}
+\section{Proving Elementary Properties}\label{sec:regularity}
-Secrecy properties are hard to prove. The conclusion of a typical secrecy
-theorem is
+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
@@ -410,25 +434,31 @@
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
@@ -443,33 +473,40 @@
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.
+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\ [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)"
+\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}
-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.
+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}
@@ -477,21 +514,33 @@
\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)"
+\ \ \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}
%
-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:
+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
@@ -504,27 +553,49 @@
\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
@@ -535,8 +606,8 @@
\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
@@ -546,9 +617,23 @@
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