author | wenzelm |
Sun, 08 Jun 2008 14:31:06 +0200 | |
changeset 27094 | 2cf13a72e170 |
parent 23925 | ee98c2528a8f |
child 35503 | 7bba12c3b7b6 |
permissions | -rw-r--r-- |
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} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset
|
87 |
where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}. |
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 | 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: |