diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/protocol.tex --- 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}