doc-src/TutorialI/Protocol/document/NS_Public.tex

-%
-\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: