diff -r 0c86acc069ad -r 5deda0549f97 doc-src/TutorialI/document/NS_Public.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/document/NS_Public.tex Thu Jul 26 17:16:02 2012 +0200 @@ -0,0 +1,517 @@ +% +\begin{isabellebody}% +\def\isabellecontext{NS{\isaliteral{5F}{\isacharunderscore}}Public}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Modelling the Protocol \label{sec:modelling}% +} +\isamarkuptrue% +% +\begin{figure} +\begin{isabelle} +\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% +\ ns{\isaliteral{5F}{\isacharunderscore}}public\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}event\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isakeyword{where}\isanewline +\isanewline +\ \ \ Nil{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\isanewline +\isanewline +\ {\isaliteral{7C}{\isacharbar}}\ Fake{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evsf\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\ \ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ Spy\ B\ X\ \ {\isaliteral{23}{\isacharhash}}\ evsf\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\isanewline +\isanewline +\ {\isaliteral{7C}{\isacharbar}}\ NS{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evs{\isadigit{1}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\ \ Nonce\ NA\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{1}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{23}{\isacharhash}}\ evs{\isadigit{1}}\ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ \ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\isanewline +\isanewline +\ {\isaliteral{7C}{\isacharbar}}\ NS{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evs{\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\ \ Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ A{\isaliteral{27}{\isacharprime}}\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{2}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{23}{\isacharhash}}\ evs{\isadigit{2}}\ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ \ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\isanewline +\isanewline +\ {\isaliteral{7C}{\isacharbar}}\ NS{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evs{\isadigit{3}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ B{\isaliteral{27}{\isacharprime}}\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{3}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Nonce\ NB{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ evs{\isadigit{3}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}% +\end{isabelle} +\caption{An Inductive Protocol Definition}\label{fig:ns_public} +\end{figure} +% +\begin{isamarkuptext}% +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{\isaliteral{5F}{\isacharunderscore}}public} to be a set of such traces. + +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{NS{\isadigit{2}}}. +A trace containing an event of the form +\begin{isabelle}% +\ \ \ \ \ Says\ A{\isaliteral{27}{\isacharprime}}\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}% +\end{isabelle} +may be extended by an event of the form +\begin{isabelle}% +\ \ \ \ \ Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}% +\end{isabelle} +where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{2}}}. +Writing the sender as \isa{A{\isaliteral{27}{\isacharprime}}} indicates that \isa{B} does not +know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather +than simply \isa{evs} helps us know where we are in a proof after many +case-splits: every subgoal mentioning \isa{evs{\isadigit{2}}} 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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Proving Elementary Properties \label{sec:regularity}% +} +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Secrecy properties can be hard to prove. The conclusion of a typical +secrecy theorem is +\isa{X\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}}. 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.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ Spy{\isaliteral{5F}{\isacharunderscore}}see{\isaliteral{5F}{\isacharunderscore}}priK\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public\isanewline +\ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Key\ {\isaliteral{28}{\isacharparenleft}}priK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}erule\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% +\begin{isamarkuptxt}% +The induction yields five subgoals, one for each rule in the definition of +\isa{ns{\isaliteral{5F}{\isacharunderscore}}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{NS{\isadigit{1}}}--\isa{{\isadigit{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}% +\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}evsf\ X{\isaliteral{2E}{\isachardot}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evsf\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }{\isaliteral{28}{\isacharparenleft}}Key\ {\isaliteral{28}{\isacharparenleft}}priK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Key\ {\isaliteral{28}{\isacharparenleft}}priK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}insert\ X\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad{\isaliteral{29}{\isacharparenright}}% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +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{\isaliteral{5F}{\isacharunderscore}}mp} to prepare the induction by moving two assumptions into the +induction formula.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ no{\isaliteral{5F}{\isacharunderscore}}nonce{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}NA{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ D{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Nonce\ NA\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}erule\ rev{\isaliteral{5F}{\isacharunderscore}}mp{\isaliteral{2C}{\isacharcomma}}\ erule\ rev{\isaliteral{5F}{\isacharunderscore}}mp{\isaliteral{29}{\isacharparenright}}\isanewline +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}erule\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ analz{\isaliteral{5F}{\isacharunderscore}}insertI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2B}{\isacharplus}}\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +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.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ unique{\isaliteral{5F}{\isacharunderscore}}NA{\isaliteral{3A}{\isacharcolon}}\isanewline +\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Crypt{\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A\ {\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts{\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ \ Crypt{\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts{\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ \ \ \ Nonce\ NA\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{3D}{\isacharequal}}A{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{3D}{\isacharequal}}B{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsection{Proving Secrecy Theorems \label{sec:secrecy}% +} +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +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.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{theorem}\isamarkupfalse% +\ Spy{\isaliteral{5F}{\isacharunderscore}}not{\isaliteral{5F}{\isacharunderscore}}see{\isaliteral{5F}{\isacharunderscore}}NB\ {\isaliteral{5B}{\isacharbrackleft}}dest{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ A\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ B\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +To prove it, we must formulate the induction properly (one of the +assumptions mentions~\isa{evs}), apply induction, and simplify:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}erule\ rev{\isaliteral{5F}{\isacharunderscore}}mp{\isaliteral{2C}{\isacharcomma}}\ erule\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% +\begin{isamarkuptxt}% +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}% +\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}evs{\isadigit{1}}\ NAa\ Ba{\isaliteral{2E}{\isachardot}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ B\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ evs{\isadigit{1}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }{\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }Nonce\ NAa\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{1}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Ba\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }{\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }NB\ {\isaliteral{5C3C6E6F7465713E}{\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\ {\isaliteral{28}{\isacharparenleft}}insert\ {\isaliteral{28}{\isacharparenleft}}Crypt\ K\ X{\isaliteral{29}{\isacharparenright}}\ H{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline +{\isaliteral{28}{\isacharparenleft}}if\ Key\ {\isaliteral{28}{\isacharparenleft}}invKey\ K{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H\isanewline +\isaindent{{\isaliteral{28}{\isacharparenleft}}}then\ insert\ {\isaliteral{28}{\isacharparenleft}}Crypt\ K\ X{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}insert\ X\ H{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline +\isaindent{{\isaliteral{28}{\isacharparenleft}}}else\ insert\ {\isaliteral{28}{\isacharparenleft}}Crypt\ K\ X{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}analz\ H{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\rulename{analz{\isaliteral{5F}{\isacharunderscore}}Crypt{\isaliteral{5F}{\isacharunderscore}}if}% +\end{isabelle} +The simplifier has also used \isa{Spy{\isaliteral{5F}{\isacharunderscore}}see{\isaliteral{5F}{\isacharunderscore}}priK}, proved in +{\S}\ref{sec:regularity} above, to yield \isa{Ba\ {\isaliteral{5C3C696E3E}{\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\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ NAa} is easy: \isa{NB} was +sent earlier, while \isa{NAa} is fresh; formally, we have +the assumption \isa{Nonce\ NAa\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{1}}}. + +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{\isaliteral{5F}{\isacharunderscore}}nonce{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{2}}}. + +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.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isacommand{theorem}\isamarkupfalse% +\ B{\isaliteral{5F}{\isacharunderscore}}trusts{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Says\ B\ A\ \ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ Says\ A{\isaliteral{27}{\isacharprime}}\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Nonce\ NB{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ A\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ B\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Nonce\ NB{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +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\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\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|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: