author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 42637 | doc-src/TutorialI/Protocol/NS_Public.thy@381fdcab0f36 |
child 49322 | fbb320d02420 |
permissions | -rw-r--r-- |
11250 | 1 |
(* Title: HOL/Auth/NS_Public |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1996 University of Cambridge |
|
4 |
||
5 |
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. |
|
6 |
Version incorporating Lowe's fix (inclusion of B's identity in round 2). |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
7 |
*)(*<*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
8 |
theory NS_Public imports Public begin(*>*) |
11250 | 9 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
10 |
section{* Modelling the Protocol \label{sec:modelling} *} |
11250 | 11 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
12 |
text_raw {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
13 |
\begin{figure} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
14 |
\begin{isabelle} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
15 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
16 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
17 |
inductive_set ns_public :: "event list set" |
23733 | 18 |
where |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
19 |
|
11250 | 20 |
Nil: "[] \<in> ns_public" |
21 |
||
22 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
23 |
| Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (knows Spy evsf))\<rbrakk> |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
24 |
\<Longrightarrow> Says Spy B X # evsf \<in> ns_public" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
25 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
26 |
|
23733 | 27 |
| NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
11250 | 28 |
\<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
29 |
# evs1 \<in> ns_public" |
|
30 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
31 |
|
23733 | 32 |
| NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
11250 | 33 |
Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
34 |
\<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
|
35 |
# evs2 \<in> ns_public" |
|
36 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
37 |
|
23733 | 38 |
| NS3: "\<lbrakk>evs3 \<in> ns_public; |
11250 | 39 |
Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
40 |
Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
|
41 |
\<in> set evs3\<rbrakk> |
|
42 |
\<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public" |
|
43 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
44 |
text_raw {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
45 |
\end{isabelle} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
46 |
\caption{An Inductive Protocol Definition}\label{fig:ns_public} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
47 |
\end{figure} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
48 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
49 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
50 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
51 |
Let us formalize the Needham-Schroeder public-key protocol, as corrected by |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
52 |
Lowe: |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
53 |
\begin{alignat*% |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
54 |
}{2} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
55 |
&1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
56 |
&2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
57 |
&3.&\quad A\to B &: \comp{Nb}\sb{Kb} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
58 |
\end{alignat*% |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
59 |
} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
60 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
61 |
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:
23733
diff
changeset
|
62 |
event trace has type @{text "event list"}, so we declare the constant |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
63 |
@{text ns_public} to be a set of such traces. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
64 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
65 |
Figure~\ref{fig:ns_public} presents the inductive definition. The |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
66 |
@{text Nil} rule introduces the empty trace. The @{text Fake} rule models the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
67 |
adversary's sending a message built from components taken from past |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
68 |
traffic, expressed using the functions @{text synth} and |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
69 |
@{text analz}. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
70 |
The next three rules model how honest agents would perform the three |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
71 |
protocol steps. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
72 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
73 |
Here is a detailed explanation of rule @{text NS2}. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
74 |
A trace containing an event of the form |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
75 |
@{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
76 |
may be extended by an event of the form |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
77 |
@{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"} |
35503 | 78 |
where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}. |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
79 |
Writing the sender as @{text A'} indicates that @{text B} does not |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
80 |
know who sent the message. Calling the trace variable @{text evs2} rather |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
81 |
than simply @{text evs} helps us know where we are in a proof after many |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
82 |
case-splits: every subgoal mentioning @{text evs2} involves message~2 of the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
83 |
protocol. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
84 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
85 |
Benefits of this approach are simplicity and clarity. The semantic model |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
86 |
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:
23733
diff
changeset
|
87 |
notation to the inductive rules is straightforward. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
88 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
89 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
90 |
section{* Proving Elementary Properties \label{sec:regularity} *} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
91 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
92 |
(*<*) |
11250 | 93 |
declare knows_Spy_partsEs [elim] |
94 |
declare analz_subset_parts [THEN subsetD, dest] |
|
95 |
declare Fake_parts_insert [THEN subsetD, dest] |
|
96 |
declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |
|
97 |
||
98 |
(*A "possibility property": there are traces that reach the end*) |
|
99 |
lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
|
100 |
apply (intro exI bexI) |
|
11269 | 101 |
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, |
11250 | 102 |
THEN ns_public.NS3]) |
103 |
by possibility |
|
104 |
||
105 |
||
106 |
(**** Inductive proofs about ns_public ****) |
|
107 |
||
11269 | 108 |
(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
11250 | 109 |
sends messages containing X! **) |
110 |
||
111 |
(*Spy never sees another agent's private key! (unless it's bad at start)*) |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
112 |
(*>*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
113 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
114 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
115 |
Secrecy properties can be hard to prove. The conclusion of a typical |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
116 |
secrecy theorem is |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
117 |
@{term "X \<notin> analz (knows Spy evs)"}. The difficulty arises from |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
118 |
having to reason about @{text analz}, or less formally, showing that the spy |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
119 |
can never learn~@{text X}. Much easier is to prove that @{text X} can never |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
120 |
occur at all. Such \emph{regularity} properties are typically expressed |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
121 |
using @{text parts} rather than @{text analz}. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
122 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
123 |
The following lemma states that @{text A}'s private key is potentially |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
124 |
known to the spy if and only if @{text A} belongs to the set @{text bad} of |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
125 |
compromised agents. The statement uses @{text parts}: the very presence of |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
126 |
@{text A}'s private key in a message, whether protected by encryption or |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
127 |
not, is enough to confirm that @{text A} is compromised. The proof, like |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
128 |
nearly all protocol proofs, is by induction over traces. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
129 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
130 |
|
11269 | 131 |
lemma Spy_see_priK [simp]: |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
132 |
"evs \<in> ns_public |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
133 |
\<Longrightarrow> (Key (priK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
134 |
apply (erule ns_public.induct, simp_all) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
135 |
txt {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
136 |
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:
23733
diff
changeset
|
137 |
@{text ns_public}. The idea is to prove that the protocol property holds initially |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
138 |
(rule @{text Nil}), is preserved by each of the legitimate protocol steps (rules |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
139 |
@{text NS1}--@{text 3}), and even is preserved in the face of anything the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
140 |
spy can do (rule @{text Fake}). |
11250 | 141 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
142 |
The proof is trivial. No legitimate protocol rule sends any keys |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
143 |
at all, so only @{text Fake} is relevant. Indeed, simplification leaves |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
144 |
only the @{text Fake} case, as indicated by the variable name @{text evsf}: |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
145 |
@{subgoals[display,indent=0,margin=65]} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
146 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
147 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
148 |
(*<*) |
11269 | 149 |
lemma Spy_analz_priK [simp]: |
150 |
"evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
11250 | 151 |
by auto |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
152 |
(*>*) |
11250 | 153 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
154 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
155 |
The @{text Fake} case is proved automatically. If |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
156 |
@{term "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:
23733
diff
changeset
|
157 |
original trace or (2) it was |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
158 |
generated by the spy, who must have known this key already. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
159 |
Either way, the induction hypothesis applies. |
11250 | 160 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
161 |
\emph{Unicity} lemmas are regularity lemmas stating that specified items |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
162 |
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:
23733
diff
changeset
|
163 |
cannot be used both as $Na$ and as $Nb$ unless |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
164 |
it is known to the spy. Intuitively, it holds because honest agents |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
165 |
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:
23733
diff
changeset
|
166 |
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:
23733
diff
changeset
|
167 |
induction, simplification, @{text blast}. The first line uses the rule |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
168 |
@{text rev_mp} to prepare the induction by moving two assumptions into the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
169 |
induction formula. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
170 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
171 |
|
11269 | 172 |
lemma no_nonce_NS1_NS2: |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
173 |
"\<lbrakk>Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (knows Spy evs); |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
174 |
Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs); |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
175 |
evs \<in> ns_public\<rbrakk> |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
176 |
\<Longrightarrow> Nonce NA \<in> analz (knows Spy evs)" |
11269 | 177 |
apply (erule rev_mp, erule rev_mp) |
11250 | 178 |
apply (erule ns_public.induct, simp_all) |
179 |
apply (blast intro: analz_insertI)+ |
|
180 |
done |
|
181 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
182 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
183 |
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:
23733
diff
changeset
|
184 |
appearance in any instance of message~1 determines the other components. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
185 |
The proof is similar to the previous one. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
186 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
187 |
|
11269 | 188 |
lemma unique_NA: |
189 |
"\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(knows Spy evs); |
|
190 |
Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(knows Spy evs); |
|
191 |
Nonce NA \<notin> analz (knows Spy evs); evs \<in> ns_public\<rbrakk> |
|
11250 | 192 |
\<Longrightarrow> A=A' \<and> B=B'" |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
193 |
(*<*) |
11269 | 194 |
apply (erule rev_mp, erule rev_mp, erule rev_mp) |
11250 | 195 |
apply (erule ns_public.induct, simp_all) |
196 |
(*Fake, NS1*) |
|
197 |
apply (blast intro: analz_insertI)+ |
|
198 |
done |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
199 |
(*>*) |
11250 | 200 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
201 |
section{* Proving Secrecy Theorems \label{sec:secrecy} *} |
11250 | 202 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
203 |
(*<*) |
11250 | 204 |
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure |
205 |
The major premise "Says A B ..." makes it a dest-rule, so we use |
|
206 |
(erule rev_mp) rather than rule_format. *) |
|
11269 | 207 |
theorem Spy_not_see_NA: |
11250 | 208 |
"\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
11269 | 209 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
210 |
\<Longrightarrow> Nonce NA \<notin> analz (knows Spy evs)" |
|
211 |
apply (erule rev_mp) |
|
11250 | 212 |
apply (erule ns_public.induct, simp_all) |
213 |
apply spy_analz |
|
214 |
apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ |
|
215 |
done |
|
216 |
||
217 |
||
218 |
(*Authentication for A: if she receives message 2 and has used NA |
|
219 |
to start a run, then B has sent message 2.*) |
|
11269 | 220 |
lemma A_trusts_NS2_lemma [rule_format]: |
221 |
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
222 |
\<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32891
diff
changeset
|
223 |
Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32891
diff
changeset
|
224 |
Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs" |
11250 | 225 |
apply (erule ns_public.induct, simp_all) |
226 |
(*Fake, NS1*) |
|
227 |
apply (blast dest: Spy_not_see_NA)+ |
|
228 |
done |
|
229 |
||
11269 | 230 |
theorem A_trusts_NS2: |
231 |
"\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
|
11250 | 232 |
Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
11269 | 233 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
11250 | 234 |
\<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs" |
235 |
by (blast intro: A_trusts_NS2_lemma) |
|
236 |
||
237 |
||
238 |
(*If the encrypted message appears then it originated with Alice in NS1*) |
|
239 |
lemma B_trusts_NS1 [rule_format]: |
|
11269 | 240 |
"evs \<in> ns_public |
241 |
\<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32891
diff
changeset
|
242 |
Nonce NA \<notin> analz (knows Spy evs) \<longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32891
diff
changeset
|
243 |
Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" |
11250 | 244 |
apply (erule ns_public.induct, simp_all) |
245 |
(*Fake*) |
|
246 |
apply (blast intro!: analz_insertI) |
|
247 |
done |
|
248 |
||
249 |
||
250 |
||
251 |
(*** Authenticity properties obtained from NS2 ***) |
|
252 |
||
11269 | 253 |
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
11250 | 254 |
[unicity of B makes Lowe's fix work] |
255 |
[proof closely follows that for unique_NA] *) |
|
256 |
||
11269 | 257 |
lemma unique_NB [dest]: |
258 |
"\<lbrakk>Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(knows Spy evs); |
|
259 |
Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(knows Spy evs); |
|
260 |
Nonce NB \<notin> analz (knows Spy evs); evs \<in> ns_public\<rbrakk> |
|
11250 | 261 |
\<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'" |
11269 | 262 |
apply (erule rev_mp, erule rev_mp, erule rev_mp) |
11250 | 263 |
apply (erule ns_public.induct, simp_all) |
264 |
(*Fake, NS2*) |
|
265 |
apply (blast intro: analz_insertI)+ |
|
266 |
done |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
267 |
(*>*) |
11269 | 268 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
269 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
270 |
The secrecy theorems for Bob (the second participant) are especially |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
271 |
important because they fail for the original protocol. The following |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
272 |
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:
23733
diff
changeset
|
273 |
uncompromised, then Bob's nonce will never reach the spy. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
274 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
275 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
276 |
theorem Spy_not_see_NB [dest]: |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
277 |
"\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
278 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
279 |
\<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
280 |
txt {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
281 |
To prove it, we must formulate the induction properly (one of the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
282 |
assumptions mentions~@{text evs}), apply induction, and simplify: |
11269 | 283 |
*} |
284 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
285 |
apply (erule rev_mp, erule ns_public.induct, simp_all) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
286 |
(*<*) |
11250 | 287 |
apply spy_analz |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
288 |
defer |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
289 |
apply (blast intro: no_nonce_NS1_NS2) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
290 |
apply (blast intro: no_nonce_NS1_NS2) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
291 |
(*>*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
292 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
293 |
txt {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
294 |
The proof states are too complicated to present in full. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
295 |
Let's examine the simplest subgoal, that for message~1. The following |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
296 |
event has just occurred: |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
297 |
\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \] |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
298 |
The variables above have been primed because this step |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
299 |
belongs to a different run from that referred to in the theorem |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
300 |
statement --- the theorem |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
301 |
refers to a past instance of message~2, while this subgoal |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
302 |
concerns message~1 being sent just now. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
303 |
In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$ |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
304 |
we have @{text Ba} and~@{text NAa}: |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
305 |
@{subgoals[display,indent=0]} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
306 |
The simplifier has used a |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
307 |
default simplification rule that does a case |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
308 |
analysis for each encrypted message on whether or not the decryption key |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
309 |
is compromised. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
310 |
@{named_thms [display,indent=0,margin=50] analz_Crypt_if [no_vars] (analz_Crypt_if)} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
311 |
The simplifier has also used @{text Spy_see_priK}, proved in |
27093 | 312 |
{\S}\ref{sec:regularity} above, to yield @{term "Ba \<in> bad"}. |
11250 | 313 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
314 |
Recall that this subgoal concerns the case |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
315 |
where the last message to be sent was |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
316 |
\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \] |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
317 |
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:
23733
diff
changeset
|
318 |
allowing the spy to decrypt the message. The Isabelle subgoal says |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
319 |
precisely this, if we allow for its choice of variable names. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
320 |
Proving @{term "NB \<noteq> NAa"} is easy: @{text NB} was |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
321 |
sent earlier, while @{text NAa} is fresh; formally, we have |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
322 |
the assumption @{term "Nonce NAa \<notin> used evs1"}. |
11250 | 323 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
324 |
Note that our reasoning concerned @{text B}'s participation in another |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
325 |
run. Agents may engage in several runs concurrently, and some attacks work |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
326 |
by interleaving the messages of two runs. With model checking, this |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
327 |
possibility can cause a state-space explosion, and for us it |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
328 |
certainly complicates proofs. The biggest subgoal concerns message~2. It |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
329 |
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:
23733
diff
changeset
|
330 |
the very message mentioned in the theorem statement. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
331 |
Some of the cases are proved by unicity, others by |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
332 |
the induction hypothesis. For all those complications, the proofs are |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
333 |
automatic by @{text blast} with the theorem @{text no_nonce_NS1_NS2}. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
334 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
335 |
The remaining theorems about the protocol are not hard to prove. The |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
336 |
following one asserts a form of \emph{authenticity}: if |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
337 |
@{text B} has sent an instance of message~2 to~@{text A} and has received the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
338 |
expected reply, then that reply really originated with~@{text A}. The |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
339 |
proof is a simple induction. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
340 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
341 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
342 |
(*<*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
343 |
by (blast intro: no_nonce_NS1_NS2) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
344 |
|
11250 | 345 |
lemma B_trusts_NS3_lemma [rule_format]: |
346 |
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> |
|
11269 | 347 |
Crypt (pubK B) (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> |
11250 | 348 |
Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow> |
349 |
Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
|
350 |
by (erule ns_public.induct, auto) |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
351 |
(*>*) |
11250 | 352 |
theorem B_trusts_NS3: |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
353 |
"\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
354 |
Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs; |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
355 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
356 |
\<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
357 |
(*<*) |
11250 | 358 |
by (blast intro: B_trusts_NS3_lemma) |
359 |
||
360 |
(*** Overall guarantee for B ***) |
|
361 |
||
362 |
||
363 |
(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with |
|
364 |
NA, then A initiated the run using NA.*) |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
365 |
theorem B_trusts_protocol [rule_format]: |
11250 | 366 |
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> |
11269 | 367 |
Crypt (pubK B) (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> |
11250 | 368 |
Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow> |
369 |
Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" |
|
370 |
by (erule ns_public.induct, auto) |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
371 |
(*>*) |
11250 | 372 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
373 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
374 |
From similar assumptions, we can prove that @{text A} started the protocol |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
375 |
run by sending an instance of message~1 involving the nonce~@{text NA}\@. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
376 |
For this theorem, the conclusion is |
32891 | 377 |
@{thm [display] (concl) B_trusts_protocol [no_vars]} |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
378 |
Analogous theorems can be proved for~@{text A}, stating that nonce~@{text NA} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
379 |
remains secret and that message~2 really originates with~@{text B}. Even the |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
380 |
flawed protocol establishes these properties for~@{text A}; |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
381 |
the flaw only harms the second participant. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
382 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
383 |
\medskip |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
384 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
385 |
Detailed information on this protocol verification technique can be found |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
386 |
elsewhere~\cite{paulson-jcs}, including proofs of an Internet |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
387 |
protocol~\cite{paulson-tls}. We must stress that the protocol discussed |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
388 |
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:
23733
diff
changeset
|
389 |
exchanged; we merely have to prove that encrypted data remains secret. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
390 |
Real world protocols are much longer and distribute many secrets to their |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
391 |
participants. To be realistic, the model has to include the possibility |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
392 |
of keys being lost dynamically due to carelessness. If those keys have |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
393 |
been used to encrypt other sensitive information, there may be cascading |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
394 |
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:
23733
diff
changeset
|
395 |
prove that other protocol runs function |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
396 |
correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
397 |
the strategy illustrated above, but the subgoals can |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
398 |
be much bigger and there are more of them. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
399 |
\index{protocols!security|)} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
400 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
401 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
23733
diff
changeset
|
402 |
(*<*)end(*>*) |