34 |
31 |
35 |
32 |
36 (**** Inductive proofs about otway ****) |
33 (**** Inductive proofs about otway ****) |
37 |
34 |
38 (*Nobody sends themselves messages*) |
35 (*Nobody sends themselves messages*) |
39 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs"; |
36 goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; |
40 by (etac otway.induct 1); |
37 by (etac otway.induct 1); |
41 by (Auto_tac()); |
38 by (Auto_tac()); |
42 qed_spec_mp "not_Says_to_self"; |
39 qed_spec_mp "not_Says_to_self"; |
43 Addsimps [not_Says_to_self]; |
40 Addsimps [not_Says_to_self]; |
44 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
41 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
45 |
42 |
46 |
43 |
47 (** For reasoning about the encrypted portion of messages **) |
44 (** For reasoning about the encrypted portion of messages **) |
48 |
45 |
49 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \ |
46 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \ |
50 \ ==> X : analz (sees lost Spy evs)"; |
47 \ ==> X : analz (sees Spy evs)"; |
51 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); |
48 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
52 qed "OR2_analz_sees_Spy"; |
49 qed "OR2_analz_sees_Spy"; |
53 |
50 |
54 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ |
51 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ |
55 \ ==> X : analz (sees lost Spy evs)"; |
52 \ ==> X : analz (sees Spy evs)"; |
56 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); |
53 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
57 qed "OR4_analz_sees_Spy"; |
54 qed "OR4_analz_sees_Spy"; |
58 |
55 |
59 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
56 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
60 \ ==> K : parts (sees lost Spy evs)"; |
57 \ ==> K : parts (sees Spy evs)"; |
61 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
58 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
62 qed "Oops_parts_sees_Spy"; |
59 qed "Oops_parts_sees_Spy"; |
63 |
60 |
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
61 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
65 argument as for the Fake case. This is possible for most, but not all, |
62 argument as for the Fake case. This is possible for most, but not all, |
69 bind_thm ("OR2_parts_sees_Spy", |
66 bind_thm ("OR2_parts_sees_Spy", |
70 OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
67 OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
71 bind_thm ("OR4_parts_sees_Spy", |
68 bind_thm ("OR4_parts_sees_Spy", |
72 OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
69 OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
73 |
70 |
74 (*For proving the easier theorems about X ~: parts (sees lost Spy evs). |
71 (*For proving the easier theorems about X ~: parts (sees Spy evs).*) |
75 We instantiate the variable to "lost" since leaving it as a Var would |
72 fun parts_induct_tac i = |
76 interfere with simplification.*) |
73 etac otway.induct i THEN |
77 val parts_induct_tac = |
74 forward_tac [Oops_parts_sees_Spy] (i+6) THEN |
78 let val tac = forw_inst_tac [("lost","lost")] |
75 forward_tac [OR4_parts_sees_Spy] (i+5) THEN |
79 in etac otway.induct 1 THEN |
76 forward_tac [OR2_parts_sees_Spy] (i+3) THEN |
80 tac OR2_parts_sees_Spy 4 THEN |
77 prove_simple_subgoals_tac i; |
81 tac OR4_parts_sees_Spy 6 THEN |
78 |
82 tac Oops_parts_sees_Spy 7 THEN |
79 |
83 prove_simple_subgoals_tac 1 |
80 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY |
84 end; |
|
85 |
|
86 |
|
87 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
|
88 sends messages containing X! **) |
81 sends messages containing X! **) |
89 |
82 |
90 |
83 |
91 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
84 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
92 goal thy |
85 goal thy |
93 "!!evs. evs : otway lost \ |
86 "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)"; |
94 \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
87 by (parts_induct_tac 1); |
95 by parts_induct_tac; |
|
96 by (Fake_parts_insert_tac 1); |
88 by (Fake_parts_insert_tac 1); |
97 by (Blast_tac 1); |
89 by (Blast_tac 1); |
98 qed "Spy_see_shrK"; |
90 qed "Spy_see_shrK"; |
99 Addsimps [Spy_see_shrK]; |
91 Addsimps [Spy_see_shrK]; |
100 |
92 |
101 goal thy |
93 goal thy |
102 "!!evs. evs : otway lost \ |
94 "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)"; |
103 \ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
|
104 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
95 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
105 qed "Spy_analz_shrK"; |
96 qed "Spy_analz_shrK"; |
106 Addsimps [Spy_analz_shrK]; |
97 Addsimps [Spy_analz_shrK]; |
107 |
98 |
108 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
99 goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \ |
109 \ evs : otway lost |] ==> A:lost"; |
100 \ evs : otway |] ==> A:lost"; |
110 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
101 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
111 qed "Spy_see_shrK_D"; |
102 qed "Spy_see_shrK_D"; |
112 |
103 |
113 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
104 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
114 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
105 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
115 |
106 |
116 |
107 |
117 (*Nobody can have used non-existent keys!*) |
108 (*Nobody can have used non-existent keys!*) |
118 goal thy "!!evs. evs : otway lost ==> \ |
109 goal thy "!!evs. evs : otway ==> \ |
119 \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; |
110 \ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))"; |
120 by parts_induct_tac; |
111 by (parts_induct_tac 1); |
121 (*Fake*) |
112 (*Fake*) |
122 by (best_tac |
113 by (best_tac |
123 (!claset addIs [impOfSubs analz_subset_parts] |
114 (!claset addIs [impOfSubs analz_subset_parts] |
124 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
115 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
125 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
116 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
138 (*** Proofs involving analz ***) |
129 (*** Proofs involving analz ***) |
139 |
130 |
140 (*Describes the form of K and NA when the Server sends this message. Also |
131 (*Describes the form of K and NA when the Server sends this message. Also |
141 for Oops case.*) |
132 for Oops case.*) |
142 goal thy |
133 goal thy |
143 "!!evs. [| Says Server B \ |
134 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
144 \ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
135 \ evs : otway |] \ |
145 \ evs : otway lost |] \ |
|
146 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
136 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
147 by (etac rev_mp 1); |
137 by (etac rev_mp 1); |
148 by (etac otway.induct 1); |
138 by (etac otway.induct 1); |
149 by (ALLGOALS Simp_tac); |
139 by (ALLGOALS Simp_tac); |
150 by (ALLGOALS Blast_tac); |
140 by (ALLGOALS Blast_tac); |
151 qed "Says_Server_message_form"; |
141 qed "Says_Server_message_form"; |
152 |
142 |
153 |
143 |
154 (*For proofs involving analz. We again instantiate the variable to "lost".*) |
144 (*For proofs involving analz.*) |
155 val analz_sees_tac = |
145 val analz_sees_tac = |
156 dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN |
146 dtac OR2_analz_sees_Spy 4 THEN |
157 dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN |
147 dtac OR4_analz_sees_Spy 6 THEN |
158 forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN |
148 forward_tac [Says_Server_message_form] 7 THEN |
159 assume_tac 7 THEN |
149 assume_tac 7 THEN |
160 REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); |
150 REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); |
161 |
151 |
162 |
152 |
163 (**** |
153 (**** |
164 The following is to prove theorems of the form |
154 The following is to prove theorems of the form |
165 |
155 |
166 Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> |
156 Key K : analz (insert (Key KAB) (sees Spy evs)) ==> |
167 Key K : analz (sees lost Spy evs) |
157 Key K : analz (sees Spy evs) |
168 |
158 |
169 A more general formula must be proved inductively. |
159 A more general formula must be proved inductively. |
170 ****) |
160 ****) |
171 |
161 |
172 |
162 |
173 (** Session keys are not used to encrypt other session keys **) |
163 (** Session keys are not used to encrypt other session keys **) |
174 |
164 |
175 (*The equality makes the induction hypothesis easier to apply*) |
165 (*The equality makes the induction hypothesis easier to apply*) |
176 goal thy |
166 goal thy |
177 "!!evs. evs : otway lost ==> \ |
167 "!!evs. evs : otway ==> \ |
178 \ ALL K KK. KK <= Compl (range shrK) --> \ |
168 \ ALL K KK. KK <= Compl (range shrK) --> \ |
179 \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ |
169 \ (Key K : analz (Key``KK Un (sees Spy evs))) = \ |
180 \ (K : KK | Key K : analz (sees lost Spy evs))"; |
170 \ (K : KK | Key K : analz (sees Spy evs))"; |
181 by (etac otway.induct 1); |
171 by (etac otway.induct 1); |
182 by analz_sees_tac; |
172 by analz_sees_tac; |
183 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
173 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
184 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
174 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
185 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
175 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
221 goal thy |
211 goal thy |
222 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \ |
212 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \ |
223 \ : set evs; \ |
213 \ : set evs; \ |
224 \ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \ |
214 \ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \ |
225 \ : set evs; \ |
215 \ : set evs; \ |
226 \ evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; |
216 \ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; |
227 by (prove_unique_tac lemma 1); |
217 by (prove_unique_tac lemma 1); |
228 qed "unique_session_keys"; |
218 qed "unique_session_keys"; |
229 |
219 |
230 |
220 |
231 |
221 |
232 (**** Authenticity properties relating to NA ****) |
222 (**** Authenticity properties relating to NA ****) |
233 |
223 |
234 (*Only OR1 can have caused such a part of a message to appear.*) |
224 (*Only OR1 can have caused such a part of a message to appear.*) |
235 goal thy |
225 goal thy |
236 "!!evs. [| A ~: lost; evs : otway lost |] \ |
226 "!!evs. [| A ~: lost; evs : otway |] \ |
237 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
227 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
238 \ : parts (sees lost Spy evs) --> \ |
228 \ : parts (sees Spy evs) --> \ |
239 \ Says A B {|NA, Agent A, Agent B, \ |
229 \ Says A B {|NA, Agent A, Agent B, \ |
240 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
230 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
241 \ : set evs"; |
231 \ : set evs"; |
242 by parts_induct_tac; |
232 by (parts_induct_tac 1); |
243 by (Fake_parts_insert_tac 1); |
233 by (Fake_parts_insert_tac 1); |
244 qed_spec_mp "Crypt_imp_OR1"; |
234 qed_spec_mp "Crypt_imp_OR1"; |
245 |
235 |
246 |
236 |
247 (** The Nonce NA uniquely identifies A's message. **) |
237 (** The Nonce NA uniquely identifies A's message. **) |
248 |
238 |
249 goal thy |
239 goal thy |
250 "!!evs. [| evs : otway lost; A ~: lost |] \ |
240 "!!evs. [| evs : otway; A ~: lost |] \ |
251 \ ==> EX B'. ALL B. \ |
241 \ ==> EX B'. ALL B. \ |
252 \ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \ |
242 \ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \ |
253 \ --> B = B'"; |
243 \ --> B = B'"; |
254 by parts_induct_tac; |
244 by (parts_induct_tac 1); |
255 by (Fake_parts_insert_tac 1); |
245 by (Fake_parts_insert_tac 1); |
256 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
246 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
257 (*OR1: creation of new Nonce. Move assertion into global context*) |
247 (*OR1: creation of new Nonce. Move assertion into global context*) |
258 by (expand_case_tac "NA = ?y" 1); |
248 by (expand_case_tac "NA = ?y" 1); |
259 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
249 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
260 val lemma = result(); |
250 val lemma = result(); |
261 |
251 |
262 goal thy |
252 goal thy |
263 "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \ |
253 "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \ |
264 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \ |
254 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \ |
265 \ evs : otway lost; A ~: lost |] \ |
255 \ evs : otway; A ~: lost |] \ |
266 \ ==> B = C"; |
256 \ ==> B = C"; |
267 by (prove_unique_tac lemma 1); |
257 by (prove_unique_tac lemma 1); |
268 qed "unique_NA"; |
258 qed "unique_NA"; |
269 |
259 |
270 |
260 |
271 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
261 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
272 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
262 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
273 over-simplified version of this protocol: see OtwayRees_Bad.*) |
263 over-simplified version of this protocol: see OtwayRees_Bad.*) |
274 goal thy |
264 goal thy |
275 "!!evs. [| A ~: lost; evs : otway lost |] \ |
265 "!!evs. [| A ~: lost; evs : otway |] \ |
276 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
266 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
277 \ : parts (sees lost Spy evs) --> \ |
267 \ : parts (sees Spy evs) --> \ |
278 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
268 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
279 \ ~: parts (sees lost Spy evs)"; |
269 \ ~: parts (sees Spy evs)"; |
280 by parts_induct_tac; |
270 by (parts_induct_tac 1); |
281 by (Fake_parts_insert_tac 1); |
271 by (Fake_parts_insert_tac 1); |
282 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs |
272 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs |
283 addSDs [impOfSubs parts_insert_subset_Un]) 1)); |
273 addSDs [impOfSubs parts_insert_subset_Un]) 1)); |
284 qed_spec_mp"no_nonce_OR1_OR2"; |
274 qed_spec_mp"no_nonce_OR1_OR2"; |
285 |
275 |
286 |
276 |
287 (*Crucial property: If the encrypted message appears, and A has used NA |
277 (*Crucial property: If the encrypted message appears, and A has used NA |
288 to start a run, then it originated with the Server!*) |
278 to start a run, then it originated with the Server!*) |
289 goal thy |
279 goal thy |
290 "!!evs. [| A ~: lost; A ~= Spy; evs : otway lost |] \ |
280 "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \ |
291 \ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) \ |
281 \ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) \ |
292 \ --> Says A B {|NA, Agent A, Agent B, \ |
282 \ --> Says A B {|NA, Agent A, Agent B, \ |
293 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
283 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
294 \ : set evs --> \ |
284 \ : set evs --> \ |
295 \ (EX NB. Says Server B \ |
285 \ (EX NB. Says Server B \ |
296 \ {|NA, \ |
286 \ {|NA, \ |
297 \ Crypt (shrK A) {|NA, Key K|}, \ |
287 \ Crypt (shrK A) {|NA, Key K|}, \ |
298 \ Crypt (shrK B) {|NB, Key K|}|} \ |
288 \ Crypt (shrK B) {|NB, Key K|}|} \ |
299 \ : set evs)"; |
289 \ : set evs)"; |
300 by parts_induct_tac; |
290 by (parts_induct_tac 1); |
301 by (Fake_parts_insert_tac 1); |
291 by (Fake_parts_insert_tac 1); |
302 (*OR1: it cannot be a new Nonce, contradiction.*) |
292 (*OR1: it cannot be a new Nonce, contradiction.*) |
303 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); |
293 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); |
304 (*OR3 and OR4*) |
294 (*OR3 and OR4*) |
305 (*OR4*) |
295 (*OR4*) |
369 (*Fake*) |
359 (*Fake*) |
370 by (spy_analz_tac 1); |
360 by (spy_analz_tac 1); |
371 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
361 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
372 |
362 |
373 goal thy |
363 goal thy |
374 "!!evs. [| Says Server B \ |
364 "!!evs. [| Says Server B \ |
375 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
365 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
376 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
366 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
377 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
367 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
378 \ A ~: lost; B ~: lost; evs : otway lost |] \ |
368 \ A ~: lost; B ~: lost; evs : otway |] \ |
379 \ ==> Key K ~: analz (sees lost Spy evs)"; |
369 \ ==> Key K ~: analz (sees Spy evs)"; |
380 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
370 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
381 by (blast_tac (!claset addSEs [lemma]) 1); |
371 by (blast_tac (!claset addSEs [lemma]) 1); |
382 qed "Spy_not_see_encrypted_key"; |
372 qed "Spy_not_see_encrypted_key"; |
383 |
373 |
384 |
374 |
385 (**** Authenticity properties relating to NB ****) |
375 (**** Authenticity properties relating to NB ****) |
386 |
376 |
387 (*Only OR2 can have caused such a part of a message to appear. We do not |
377 (*Only OR2 can have caused such a part of a message to appear. We do not |
388 know anything about X: it does NOT have to have the right form.*) |
378 know anything about X: it does NOT have to have the right form.*) |
389 goal thy |
379 goal thy |
390 "!!evs. [| B ~: lost; evs : otway lost |] \ |
380 "!!evs. [| B ~: lost; evs : otway |] \ |
391 \ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
381 \ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
392 \ : parts (sees lost Spy evs) --> \ |
382 \ : parts (sees Spy evs) --> \ |
393 \ (EX X. Says B Server \ |
383 \ (EX X. Says B Server \ |
394 \ {|NA, Agent A, Agent B, X, \ |
384 \ {|NA, Agent A, Agent B, X, \ |
395 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
385 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
396 \ : set evs)"; |
386 \ : set evs)"; |
397 by parts_induct_tac; |
387 by (parts_induct_tac 1); |
398 by (Fake_parts_insert_tac 1); |
388 by (Fake_parts_insert_tac 1); |
399 by (ALLGOALS Blast_tac); |
389 by (ALLGOALS Blast_tac); |
400 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); |
390 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); |
401 |
391 |
402 |
392 |
403 (** The Nonce NB uniquely identifies B's message. **) |
393 (** The Nonce NB uniquely identifies B's message. **) |
404 |
394 |
405 goal thy |
395 goal thy |
406 "!!evs. [| evs : otway lost; B ~: lost |] \ |
396 "!!evs. [| evs : otway; B ~: lost |] \ |
407 \ ==> EX NA' A'. ALL NA A. \ |
397 \ ==> EX NA' A'. ALL NA A. \ |
408 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \ |
398 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \ |
409 \ --> NA = NA' & A = A'"; |
399 \ --> NA = NA' & A = A'"; |
410 by parts_induct_tac; |
400 by (parts_induct_tac 1); |
411 by (Fake_parts_insert_tac 1); |
401 by (Fake_parts_insert_tac 1); |
412 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
402 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
413 (*OR2: creation of new Nonce. Move assertion into global context*) |
403 (*OR2: creation of new Nonce. Move assertion into global context*) |
414 by (expand_case_tac "NB = ?y" 1); |
404 by (expand_case_tac "NB = ?y" 1); |
415 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
405 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
416 val lemma = result(); |
406 val lemma = result(); |
417 |
407 |
418 goal thy |
408 goal thy |
419 "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
409 "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
420 \ : parts(sees lost Spy evs); \ |
410 \ : parts(sees Spy evs); \ |
421 \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \ |
411 \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \ |
422 \ : parts(sees lost Spy evs); \ |
412 \ : parts(sees Spy evs); \ |
423 \ evs : otway lost; B ~: lost |] \ |
413 \ evs : otway; B ~: lost |] \ |
424 \ ==> NC = NA & C = A"; |
414 \ ==> NC = NA & C = A"; |
425 by (prove_unique_tac lemma 1); |
415 by (prove_unique_tac lemma 1); |
426 qed "unique_NB"; |
416 qed "unique_NB"; |
427 |
417 |
428 |
418 |
429 (*If the encrypted message appears, and B has used Nonce NB, |
419 (*If the encrypted message appears, and B has used Nonce NB, |
430 then it originated with the Server!*) |
420 then it originated with the Server!*) |
431 goal thy |
421 goal thy |
432 "!!evs. [| B ~: lost; B ~= Spy; evs : otway lost |] \ |
422 "!!evs. [| B ~: lost; B ~= Spy; evs : otway |] \ |
433 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs) \ |
423 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs) \ |
434 \ --> (ALL X'. Says B Server \ |
424 \ --> (ALL X'. Says B Server \ |
435 \ {|NA, Agent A, Agent B, X', \ |
425 \ {|NA, Agent A, Agent B, X', \ |
436 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
426 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
437 \ : set evs \ |
427 \ : set evs \ |
438 \ --> Says Server B \ |
428 \ --> Says Server B \ |
439 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
429 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
440 \ Crypt (shrK B) {|NB, Key K|}|} \ |
430 \ Crypt (shrK B) {|NB, Key K|}|} \ |
441 \ : set evs)"; |
431 \ : set evs)"; |
442 by parts_induct_tac; |
432 by (parts_induct_tac 1); |
443 by (Fake_parts_insert_tac 1); |
433 by (Fake_parts_insert_tac 1); |
444 (*OR1: it cannot be a new Nonce, contradiction.*) |
434 (*OR1: it cannot be a new Nonce, contradiction.*) |
445 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); |
435 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); |
446 (*OR4*) |
436 (*OR4*) |
447 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); |
437 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); |
448 (*OR3*) |
438 (*OR3*) |
449 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
439 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
450 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); |
440 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); |
451 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
441 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] |
452 addSEs [MPair_parts] |
442 addSEs [MPair_parts] |
453 addDs [unique_NB]) 2); |
443 addDs [unique_NB]) 2); |
454 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)] |
444 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)] |
455 addSDs [Says_imp_sees_Spy' RS parts.Inj] |
445 addSDs [Says_imp_sees_Spy RS parts.Inj] |
456 delrules [conjI, impCE] (*stop split-up*)) 1); |
446 delrules [conjI, impCE] (*stop split-up*)) 1); |
457 qed_spec_mp "NB_Crypt_imp_Server_msg"; |
447 qed_spec_mp "NB_Crypt_imp_Server_msg"; |
458 |
448 |
459 |
449 |
460 (*Guarantee for B: if it gets a message with matching NB then the Server |
450 (*Guarantee for B: if it gets a message with matching NB then the Server |
461 has sent the correct message.*) |
451 has sent the correct message.*) |
462 goal thy |
452 goal thy |
463 "!!evs. [| B ~: lost; B ~= Spy; evs : otway lost; \ |
453 "!!evs. [| B ~: lost; B ~= Spy; evs : otway; \ |
464 \ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \ |
454 \ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \ |
465 \ : set evs; \ |
455 \ : set evs; \ |
466 \ Says B Server {|NA, Agent A, Agent B, X', \ |
456 \ Says B Server {|NA, Agent A, Agent B, X', \ |
467 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
457 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
468 \ : set evs |] \ |
458 \ : set evs |] \ |