--- a/doc-src/TutorialI/Protocol/protocol.tex Mon Jul 23 14:30:53 2007 +0200
+++ b/doc-src/TutorialI/Protocol/protocol.tex Mon Jul 23 14:31:34 2007 +0200
@@ -130,518 +130,7 @@
\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
+\input{Protocol/document/Message}
+\input{Protocol/document/Event}
+\input{Protocol/document/Public}
+\input{Protocol/document/NS_Public}