author | wenzelm |
Mon, 08 Nov 2010 00:00:47 +0100 | |
changeset 40406 | 313a24b66a8d |
parent 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}% |
40406 | 3 |
\def\isabellecontext{NS{\isaliteral{5F}{\isacharunderscore}}Public}% |
23925
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} |
40406 | 24 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
25 |
\ ns{\isaliteral{5F}{\isacharunderscore}}public\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}event\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23925
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 |
40406 | 28 |
\ \ \ Nil{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
23925
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 |
40406 | 31 |
\ {\isaliteral{7C}{\isacharbar}}\ Fake{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evsf\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\ \ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
32 |
\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ Spy\ B\ X\ \ {\isaliteral{23}{\isacharhash}}\ evsf\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23925
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 |
40406 | 35 |
\ {\isaliteral{7C}{\isacharbar}}\ NS{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evs{\isadigit{1}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\ \ Nonce\ NA\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{1}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
36 |
\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
37 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{23}{\isacharhash}}\ evs{\isadigit{1}}\ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ \ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23925
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 |
40406 | 40 |
\ {\isaliteral{7C}{\isacharbar}}\ NS{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evs{\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\ \ Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
41 |
\ \ \ \ \ \ \ \ \ \ \ Says\ A{\isaliteral{27}{\isacharprime}}\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{2}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
42 |
\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
43 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{23}{\isacharhash}}\ evs{\isadigit{2}}\ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ \ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23925
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 |
40406 | 46 |
\ {\isaliteral{7C}{\isacharbar}}\ NS{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evs{\isadigit{3}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
47 |
\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
48 |
\ \ \ \ \ \ \ \ \ \ \ Says\ B{\isaliteral{27}{\isacharprime}}\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
49 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{3}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
50 |
\ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Nonce\ NB{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ evs{\isadigit{3}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23925
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 |
40406 | 68 |
\isa{ns{\isaliteral{5F}{\isacharunderscore}}public} to be a set of such traces. |
23925
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}% |
40406 | 81 |
\ \ \ \ \ Says\ A{\isaliteral{27}{\isacharprime}}\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}% |
23925
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}% |
40406 | 85 |
\ \ \ \ \ Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}% |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset
|
86 |
\end{isabelle} |
40406 | 87 |
where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{2}}}. |
88 |
Writing the sender as \isa{A{\isaliteral{27}{\isacharprime}}} indicates that \isa{B} does not |
|
23925
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 |
40406 | 120 |
\isa{X\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}}. The difficulty arises from |
23925
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% |
40406 | 135 |
\ Spy{\isaliteral{5F}{\isacharunderscore}}see{\isaliteral{5F}{\isacharunderscore}}priK\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
136 |
\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public\isanewline |
|
137 |
\ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Key\ {\isaliteral{28}{\isacharparenleft}}priK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23925
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% |
40406 | 145 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% |
23925
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 |
40406 | 148 |
\isa{ns{\isaliteral{5F}{\isacharunderscore}}public}. The idea is to prove that the protocol property holds initially |
23925
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}% |
40406 | 157 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}evsf\ X{\isaliteral{2E}{\isachardot}}\isanewline |
158 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}evsf\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
159 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }{\isaliteral{28}{\isacharparenleft}}Key\ {\isaliteral{28}{\isacharparenleft}}priK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
160 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
161 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Key\ {\isaliteral{28}{\isacharparenleft}}priK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}insert\ X\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evsf{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
162 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad{\isaliteral{29}{\isacharparenright}}% |
|
23925
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 |
40406 | 202 |
\isa{rev{\isaliteral{5F}{\isacharunderscore}}mp} to prepare the induction by moving two assumptions into the |
23925
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% |
40406 | 207 |
\ no{\isaliteral{5F}{\isacharunderscore}}nonce{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
208 |
\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}NA{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ D{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
209 |
\ \ \ \ \ \ Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
210 |
\ \ \ \ \ \ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
211 |
\ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Nonce\ NA\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23925
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% |
40406 | 219 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ rev{\isaliteral{5F}{\isacharunderscore}}mp{\isaliteral{2C}{\isacharcomma}}\ erule\ rev{\isaliteral{5F}{\isacharunderscore}}mp{\isaliteral{29}{\isacharparenright}}\isanewline |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset
|
220 |
\isacommand{apply}\isamarkupfalse% |
40406 | 221 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset
|
222 |
\isacommand{apply}\isamarkupfalse% |
40406 | 223 |
\ {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ analz{\isaliteral{5F}{\isacharunderscore}}insertI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2B}{\isacharplus}}\isanewline |
23925
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% |
40406 | 240 |
\ unique{\isaliteral{5F}{\isacharunderscore}}NA{\isaliteral{3A}{\isacharcolon}}\isanewline |
241 |
\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Crypt{\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A\ {\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts{\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
242 |
\ \ \ \ \ \ \ Crypt{\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts{\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
243 |
\ \ \ \ \ \ \ Nonce\ NA\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
244 |
\ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{3D}{\isacharequal}}A{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{3D}{\isacharequal}}B{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23925
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% |
40406 | 335 |
\ Spy{\isaliteral{5F}{\isacharunderscore}}not{\isaliteral{5F}{\isacharunderscore}}see{\isaliteral{5F}{\isacharunderscore}}NB\ {\isaliteral{5B}{\isacharbrackleft}}dest{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
336 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
337 |
\ \ \ A\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ B\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
338 |
\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23925
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% |
40406 | 351 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ rev{\isaliteral{5F}{\isacharunderscore}}mp{\isaliteral{2C}{\isacharcomma}}\ erule\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% |
23925
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}% |
40406 | 365 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}evs{\isadigit{1}}\ NAa\ Ba{\isaliteral{2E}{\isachardot}}\isanewline |
366 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ B\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ evs{\isadigit{1}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
367 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
368 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }{\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
369 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }Nonce\ NB\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
370 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }Nonce\ NAa\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{1}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
371 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Ba\ {\isaliteral{5C3C696E3E}{\isasymin}}\ bad\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
372 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }Says\ B\ A\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
373 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }{\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
374 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }NB\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ NAa% |
|
23925
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}% |
40406 | 381 |
analz\ {\isaliteral{28}{\isacharparenleft}}insert\ {\isaliteral{28}{\isacharparenleft}}Crypt\ K\ X{\isaliteral{29}{\isacharparenright}}\ H{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
382 |
{\isaliteral{28}{\isacharparenleft}}if\ Key\ {\isaliteral{28}{\isacharparenleft}}invKey\ K{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H\isanewline |
|
383 |
\isaindent{{\isaliteral{28}{\isacharparenleft}}}then\ insert\ {\isaliteral{28}{\isacharparenleft}}Crypt\ K\ X{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}insert\ X\ H{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
384 |
\isaindent{{\isaliteral{28}{\isacharparenleft}}}else\ insert\ {\isaliteral{28}{\isacharparenleft}}Crypt\ K\ X{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}analz\ H{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\rulename{analz{\isaliteral{5F}{\isacharunderscore}}Crypt{\isaliteral{5F}{\isacharunderscore}}if}% |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset
|
385 |
\end{isabelle} |
40406 | 386 |
The simplifier has also used \isa{Spy{\isaliteral{5F}{\isacharunderscore}}see{\isaliteral{5F}{\isacharunderscore}}priK}, proved in |
387 |
{\S}\ref{sec:regularity} above, to yield \isa{Ba\ {\isaliteral{5C3C696E3E}{\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. |
40406 | 395 |
Proving \isa{NB\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ NAa} is easy: \isa{NB} was |
23925
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 |
40406 | 397 |
the assumption \isa{Nonce\ NAa\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ used\ evs{\isadigit{1}}}. |
23925
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 |
40406 | 408 |
automatic by \isa{blast} with the theorem \isa{no{\isaliteral{5F}{\isacharunderscore}}nonce{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{2}}}. |
23925
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% |
40406 | 438 |
\ B{\isaliteral{5F}{\isacharunderscore}}trusts{\isaliteral{5F}{\isacharunderscore}}NS{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
439 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Says\ B\ A\ \ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Nonce\ NB{\isaliteral{2C}{\isacharcomma}}\ Agent\ B{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
440 |
\ \ \ Says\ A{\isaliteral{27}{\isacharprime}}\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Nonce\ NB{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
441 |
\ \ \ A\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ B\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ bad{\isaliteral{3B}{\isacharsemicolon}}\ \ evs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ ns{\isaliteral{5F}{\isacharunderscore}}public{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
442 |
\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Nonce\ NB{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23925
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}% |
40406 | 474 |
Says\ A\ B\ {\isaliteral{28}{\isacharparenleft}}Crypt\ {\isaliteral{28}{\isacharparenleft}}pubK\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}Nonce\ NA{\isaliteral{2C}{\isacharcomma}}\ Agent\ A{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ evs% |
23925
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: |