doc-src/TutorialI/Protocol/document/NS_Public.tex
author paulson
Tue, 02 Feb 2010 09:48:20 +0000
changeset 35503 7bba12c3b7b6
parent 27094 2cf13a72e170
child 40406 313a24b66a8d
permissions -rw-r--r--
Correction of a tiny error
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23925
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     1
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     2
\begin{isabellebody}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     3
\def\isabellecontext{NS{\isacharunderscore}Public}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     4
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     5
\isadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     6
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     7
\endisadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     8
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
     9
\isatagtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    10
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    11
\endisatagtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    12
{\isafoldtheory}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    13
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    14
\isadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    15
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    16
\endisadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    17
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    18
\isamarkupsection{Modelling the Protocol \label{sec:modelling}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    19
}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    20
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    21
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    22
\begin{figure}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    23
\begin{isabelle}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    24
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    25
\ ns{\isacharunderscore}public\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}event\ list\ set{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    26
\ \ \isakeyword{where}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    27
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    28
\ \ \ Nil{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    29
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    30
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    31
\ {\isacharbar}\ Fake{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ X\ {\isasymin}\ synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    32
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ Spy\ B\ X\ \ {\isacharhash}\ evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    33
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    34
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    35
\ {\isacharbar}\ NS{\isadigit{1}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{1}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ Nonce\ NA\ {\isasymnotin}\ used\ evs{\isadigit{1}}{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    36
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    37
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharhash}\ evs{\isadigit{1}}\ \ {\isasymin}\ \ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    38
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    39
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    40
\ {\isacharbar}\ NS{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{2}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    41
\ \ \ \ \ \ \ \ \ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isadigit{2}}{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    42
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    43
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharhash}\ evs{\isadigit{2}}\ \ {\isasymin}\ \ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    44
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    45
\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    46
\ {\isacharbar}\ NS{\isadigit{3}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{3}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    47
\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isadigit{3}}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    48
\ \ \ \ \ \ \ \ \ \ \ Says\ B{\isacharprime}\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    49
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymin}\ set\ evs{\isadigit{3}}{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    50
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isacharhash}\ evs{\isadigit{3}}\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    51
\end{isabelle}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    52
\caption{An Inductive Protocol Definition}\label{fig:ns_public}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    53
\end{figure}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    54
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    55
\begin{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    56
Let us formalize the Needham-Schroeder public-key protocol, as corrected by
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    57
Lowe:
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    58
\begin{alignat*%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    59
}{2}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    60
  &1.&\quad  A\to B  &: \comp{Na,A}\sb{Kb} \\
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    61
  &2.&\quad  B\to A  &: \comp{Na,Nb,B}\sb{Ka} \\
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    62
  &3.&\quad  A\to B  &: \comp{Nb}\sb{Kb}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    63
\end{alignat*%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    64
}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    65
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    66
Each protocol step is specified by a rule of an inductive definition.  An
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    67
event trace has type \isa{event\ list}, so we declare the constant
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    68
\isa{ns{\isacharunderscore}public} to be a set of such traces.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    69
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    70
Figure~\ref{fig:ns_public} presents the inductive definition.  The
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    71
\isa{Nil} rule introduces the empty trace.  The \isa{Fake} rule models the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    72
adversary's sending a message built from components taken from past
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    73
traffic, expressed using the functions \isa{synth} and
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    74
\isa{analz}. 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    75
The next three rules model how honest agents would perform the three
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    76
protocol steps.  
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    77
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    78
Here is a detailed explanation of rule \isa{NS{\isadigit{2}}}.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    79
A trace containing an event of the form
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    80
\begin{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    81
\ \ \ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    82
\end{isabelle}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    83
may be extended by an event of the form
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    84
\begin{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    85
\ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    86
\end{isabelle}
35503
7bba12c3b7b6 Correction of a tiny error
paulson
parents: 27094
diff changeset
    87
where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}.
23925
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    88
Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    89
know who sent the message.  Calling the trace variable \isa{evs{\isadigit{2}}} rather
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    90
than simply \isa{evs} helps us know where we are in a proof after many
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    91
case-splits: every subgoal mentioning \isa{evs{\isadigit{2}}} involves message~2 of the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    92
protocol.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    93
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    94
Benefits of this approach are simplicity and clarity.  The semantic model
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    95
is set theory, proofs are by induction and the translation from the informal
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    96
notation to the inductive rules is straightforward.%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    97
\end{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    98
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
    99
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   100
\isamarkupsection{Proving Elementary Properties \label{sec:regularity}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   101
}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   102
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   103
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   104
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   105
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   106
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   107
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   108
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   109
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   110
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   111
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   112
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   113
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   114
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   115
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   116
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   117
\begin{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   118
Secrecy properties can be hard to prove.  The conclusion of a typical
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   119
secrecy theorem is 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   120
\isa{X\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}}.  The difficulty arises from
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   121
having to reason about \isa{analz}, or less formally, showing that the spy
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   122
can never learn~\isa{X}.  Much easier is to prove that \isa{X} can never
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   123
occur at all.  Such \emph{regularity} properties are typically expressed
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   124
using \isa{parts} rather than \isa{analz}.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   125
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   126
The following lemma states that \isa{A}'s private key is potentially
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   127
known to the spy if and only if \isa{A} belongs to the set \isa{bad} of
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   128
compromised agents.  The statement uses \isa{parts}: the very presence of
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   129
\isa{A}'s private key in a message, whether protected by encryption or
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   130
not, is enough to confirm that \isa{A} is compromised.  The proof, like
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   131
nearly all protocol proofs, is by induction over traces.%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   132
\end{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   133
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   134
\isacommand{lemma}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   135
\ Spy{\isacharunderscore}see{\isacharunderscore}priK\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   136
\ \ \ \ \ \ {\isachardoublequoteopen}evs\ {\isasymin}\ ns{\isacharunderscore}public\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   137
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   138
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   139
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   140
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   141
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   142
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   143
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   144
\isacommand{apply}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   145
\ {\isacharparenleft}erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   146
\begin{isamarkuptxt}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   147
The induction yields five subgoals, one for each rule in the definition of
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   148
\isa{ns{\isacharunderscore}public}.  The idea is to prove that the protocol property holds initially
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   149
(rule \isa{Nil}), is preserved by each of the legitimate protocol steps (rules
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   150
\isa{NS{\isadigit{1}}}--\isa{{\isadigit{3}}}), and even is preserved in the face of anything the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   151
spy can do (rule \isa{Fake}).  
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   152
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   153
The proof is trivial.  No legitimate protocol rule sends any keys
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   154
at all, so only \isa{Fake} is relevant. Indeed, simplification leaves
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   155
only the \isa{Fake} case, as indicated by the variable name \isa{evsf}:
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   156
\begin{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   157
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}evsf\ X{\isachardot}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   158
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   159
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   160
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }X\ {\isasymin}\ synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   161
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}insert\ X\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   162
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }{\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   163
\end{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   164
\end{isamarkuptxt}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   165
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   166
\isacommand{by}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   167
\ blast%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   168
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   169
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   170
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   171
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   172
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   173
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   174
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   175
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   176
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   177
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   178
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   179
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   180
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   181
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   182
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   183
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   184
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   185
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   186
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   187
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   188
\begin{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   189
The \isa{Fake} case is proved automatically.  If
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   190
\isa{priK\ A} is in the extended trace then either (1) it was already in the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   191
original trace or (2) it was
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   192
generated by the spy, who must have known this key already. 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   193
Either way, the induction hypothesis applies.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   194
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   195
\emph{Unicity} lemmas are regularity lemmas stating that specified items
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   196
can occur only once in a trace.  The following lemma states that a nonce
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   197
cannot be used both as $Na$ and as $Nb$ unless
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   198
it is known to the spy.  Intuitively, it holds because honest agents
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   199
always choose fresh values as nonces; only the spy might reuse a value,
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   200
and he doesn't know this particular value.  The proof script is short:
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   201
induction, simplification, \isa{blast}.  The first line uses the rule
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   202
\isa{rev{\isacharunderscore}mp} to prepare the induction by moving two assumptions into the 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   203
induction formula.%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   204
\end{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   205
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   206
\isacommand{lemma}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   207
\ no{\isacharunderscore}nonce{\isacharunderscore}NS{\isadigit{1}}{\isacharunderscore}NS{\isadigit{2}}{\isacharcolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   208
\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt\ {\isacharparenleft}pubK\ C{\isacharparenright}\ {\isasymlbrace}NA{\isacharprime}{\isacharcomma}\ Nonce\ NA{\isacharcomma}\ Agent\ D{\isasymrbrace}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   209
\ \ \ \ \ \ Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   210
\ \ \ \ \ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   211
\ \ \ \ \ {\isasymLongrightarrow}\ Nonce\ NA\ {\isasymin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isachardoublequoteclose}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   212
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   213
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   214
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   215
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   216
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   217
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   218
\isacommand{apply}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   219
\ {\isacharparenleft}erule\ rev{\isacharunderscore}mp{\isacharcomma}\ erule\ rev{\isacharunderscore}mp{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   220
\isacommand{apply}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   221
\ {\isacharparenleft}erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   222
\isacommand{apply}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   223
\ {\isacharparenleft}blast\ intro{\isacharcolon}\ analz{\isacharunderscore}insertI{\isacharparenright}{\isacharplus}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   224
\isacommand{done}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   225
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   226
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   227
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   228
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   229
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   230
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   231
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   232
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   233
\begin{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   234
The following unicity lemma states that, if \isa{NA} is secret, then its
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   235
appearance in any instance of message~1 determines the other components. 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   236
The proof is similar to the previous one.%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   237
\end{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   238
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   239
\isacommand{lemma}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   240
\ unique{\isacharunderscore}NA{\isacharcolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   241
\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt{\isacharparenleft}pubK\ B{\isacharparenright}\ \ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A\ {\isasymrbrace}\ {\isasymin}\ parts{\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   242
\ \ \ \ \ \ \ Crypt{\isacharparenleft}pubK\ B{\isacharprime}{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isacharprime}{\isasymrbrace}\ {\isasymin}\ parts{\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   243
\ \ \ \ \ \ \ Nonce\ NA\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   244
\ \ \ \ \ \ {\isasymLongrightarrow}\ A{\isacharequal}A{\isacharprime}\ {\isasymand}\ B{\isacharequal}B{\isacharprime}{\isachardoublequoteclose}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   245
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   246
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   247
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   248
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   249
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   250
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   251
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   252
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   253
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   254
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   255
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   256
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   257
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   258
\isamarkupsection{Proving Secrecy Theorems \label{sec:secrecy}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   259
}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   260
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   261
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   262
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   263
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   264
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   265
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   266
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   267
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   268
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   269
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   270
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   271
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   272
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   273
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   274
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   275
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   276
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   277
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   278
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   279
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   280
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   281
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   282
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   283
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   284
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   285
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   286
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   287
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   288
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   289
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   290
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   291
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   292
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   293
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   294
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   295
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   296
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   297
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   298
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   299
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   300
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   301
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   302
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   303
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   304
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   305
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   306
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   307
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   308
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   309
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   310
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   311
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   312
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   313
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   314
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   315
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   316
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   317
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   318
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   319
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   320
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   321
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   322
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   323
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   324
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   325
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   326
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   327
\begin{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   328
The secrecy theorems for Bob (the second participant) are especially
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   329
important because they fail for the original protocol.  The following
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   330
theorem states that if Bob sends message~2 to Alice, and both agents are
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   331
uncompromised, then Bob's nonce will never reach the spy.%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   332
\end{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   333
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   334
\isacommand{theorem}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   335
\ Spy{\isacharunderscore}not{\isacharunderscore}see{\isacharunderscore}NB\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   336
\ {\isachardoublequoteopen}{\isasymlbrakk}Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   337
\ \ \ A\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   338
\ \ {\isasymLongrightarrow}\ Nonce\ NB\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isachardoublequoteclose}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   339
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   340
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   341
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   342
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   343
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   344
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   345
\begin{isamarkuptxt}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   346
To prove it, we must formulate the induction properly (one of the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   347
assumptions mentions~\isa{evs}), apply induction, and simplify:%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   348
\end{isamarkuptxt}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   349
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   350
\isacommand{apply}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   351
\ {\isacharparenleft}erule\ rev{\isacharunderscore}mp{\isacharcomma}\ erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   352
\begin{isamarkuptxt}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   353
The proof states are too complicated to present in full.  
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   354
Let's examine the simplest subgoal, that for message~1.  The following
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   355
event has just occurred:
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   356
\[ 1.\quad  A'\to B'  : \comp{Na',A'}\sb{Kb'} \]
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   357
The variables above have been primed because this step
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   358
belongs to a different run from that referred to in the theorem
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   359
statement --- the theorem
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   360
refers to a past instance of message~2, while this subgoal
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   361
concerns message~1 being sent just now.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   362
In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   363
we have \isa{Ba} and~\isa{NAa}:
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   364
\begin{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   365
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}evs{\isadigit{1}}\ NAa\ Ba{\isachardot}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   366
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}A\ {\isasymnotin}\ bad{\isacharsemicolon}\ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ evs{\isadigit{1}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   367
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   368
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isasymin}\ set\ evs{\isadigit{1}}\ {\isasymlongrightarrow}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   369
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Nonce\ NB\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   370
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Nonce\ NAa\ {\isasymnotin}\ used\ evs{\isadigit{1}}{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   371
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Ba\ {\isasymin}\ bad\ {\isasymlongrightarrow}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   372
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   373
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }{\isasymin}\ set\ evs{\isadigit{1}}\ {\isasymlongrightarrow}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   374
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }NB\ {\isasymnoteq}\ NAa%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   375
\end{isabelle}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   376
The simplifier has used a 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   377
default simplification rule that does a case
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   378
analysis for each encrypted message on whether or not the decryption key
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   379
is compromised.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   380
\begin{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   381
analz\ {\isacharparenleft}insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ H{\isacharparenright}\ {\isacharequal}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   382
{\isacharparenleft}if\ Key\ {\isacharparenleft}invKey\ K{\isacharparenright}\ {\isasymin}\ analz\ H\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   383
\isaindent{{\isacharparenleft}}then\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ {\isacharparenleft}insert\ X\ H{\isacharparenright}{\isacharparenright}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   384
\isaindent{{\isacharparenleft}}else\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ H{\isacharparenright}{\isacharparenright}\rulename{analz{\isacharunderscore}Crypt{\isacharunderscore}if}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   385
\end{isabelle}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   386
The simplifier has also used \isa{Spy{\isacharunderscore}see{\isacharunderscore}priK}, proved in
27094
2cf13a72e170 updated generated file;
wenzelm
parents: 23925
diff changeset
   387
{\S}\ref{sec:regularity} above, to yield \isa{Ba\ {\isasymin}\ bad}.
23925
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   388
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   389
Recall that this subgoal concerns the case
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   390
where the last message to be sent was
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   391
\[ 1.\quad  A'\to B'  : \comp{Na',A'}\sb{Kb'}. \]
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   392
This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised,
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   393
allowing the spy to decrypt the message.  The Isabelle subgoal says
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   394
precisely this, if we allow for its choice of variable names.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   395
Proving \isa{NB\ {\isasymnoteq}\ NAa} is easy: \isa{NB} was
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   396
sent earlier, while \isa{NAa} is fresh; formally, we have
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   397
the assumption \isa{Nonce\ NAa\ {\isasymnotin}\ used\ evs{\isadigit{1}}}. 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   398
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   399
Note that our reasoning concerned \isa{B}'s participation in another
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   400
run.  Agents may engage in several runs concurrently, and some attacks work
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   401
by interleaving the messages of two runs.  With model checking, this
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   402
possibility can cause a state-space explosion, and for us it
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   403
certainly complicates proofs.  The biggest subgoal concerns message~2.  It
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   404
splits into several cases, such as whether or not the message just sent is
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   405
the very message mentioned in the theorem statement.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   406
Some of the cases are proved by unicity, others by
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   407
the induction hypothesis.  For all those complications, the proofs are
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   408
automatic by \isa{blast} with the theorem \isa{no{\isacharunderscore}nonce{\isacharunderscore}NS{\isadigit{1}}{\isacharunderscore}NS{\isadigit{2}}}.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   409
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   410
The remaining theorems about the protocol are not hard to prove.  The
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   411
following one asserts a form of \emph{authenticity}: if
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   412
\isa{B} has sent an instance of message~2 to~\isa{A} and has received the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   413
expected reply, then that reply really originated with~\isa{A}.  The
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   414
proof is a simple induction.%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   415
\end{isamarkuptxt}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   416
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   417
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   418
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   419
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   420
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   421
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   422
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   423
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   424
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   425
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   426
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   427
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   428
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   429
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   430
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   431
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   432
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   433
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   434
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   435
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   436
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   437
\isacommand{theorem}\isamarkupfalse%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   438
\ B{\isacharunderscore}trusts{\isacharunderscore}NS{\isadigit{3}}{\isacharcolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   439
\ {\isachardoublequoteopen}{\isasymlbrakk}Says\ B\ A\ \ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   440
\ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   441
\ \ \ A\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   442
\ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ evs{\isachardoublequoteclose}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   443
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   444
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   445
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   446
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   447
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   448
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   449
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   450
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   451
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   452
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   453
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   454
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   455
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   456
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   457
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   458
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   459
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   460
\isatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   461
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   462
\endisatagproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   463
{\isafoldproof}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   464
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   465
\isadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   466
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   467
\endisadelimproof
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   468
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   469
\begin{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   470
From similar assumptions, we can prove that \isa{A} started the protocol
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   471
run by sending an instance of message~1 involving the nonce~\isa{NA}\@. 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   472
For this theorem, the conclusion is 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   473
\begin{isabelle}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   474
Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   475
\end{isabelle}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   476
Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA}
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   477
remains secret and that message~2 really originates with~\isa{B}.  Even the
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   478
flawed protocol establishes these properties for~\isa{A};
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   479
the flaw only harms the second participant.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   480
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   481
\medskip
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   482
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   483
Detailed information on this protocol verification technique can be found
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   484
elsewhere~\cite{paulson-jcs}, including proofs of an Internet
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   485
protocol~\cite{paulson-tls}.  We must stress that the protocol discussed
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   486
in this chapter is trivial.  There are only three messages; no keys are
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   487
exchanged; we merely have to prove that encrypted data remains secret. 
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   488
Real world protocols are much longer and distribute many secrets to their
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   489
participants.  To be realistic, the model has to include the possibility
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   490
of keys being lost dynamically due to carelessness.  If those keys have
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   491
been used to encrypt other sensitive information, there may be cascading
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   492
losses.  We may still be able to establish a bound on the losses and to
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   493
prove that other protocol runs function
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   494
correctly~\cite{paulson-yahalom}.  Proofs of real-world protocols follow
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   495
the strategy illustrated above, but the subgoals can
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   496
be much bigger and there are more of them.
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   497
\index{protocols!security|)}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   498
\end{isamarkuptext}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   499
\isamarkuptrue%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   500
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   501
\isadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   502
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   503
\endisadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   504
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   505
\isatagtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   506
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   507
\endisatagtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   508
{\isafoldtheory}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   509
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   510
\isadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   511
%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   512
\endisadelimtheory
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   513
\end{isabellebody}%
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   514
%%% Local Variables:
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   515
%%% mode: latex
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   516
%%% TeX-master: "root"
ee98c2528a8f LaTeX code is now generated directly from theory files.
berghofe
parents:
diff changeset
   517
%%% End: