27 \ ==> EX K. EX NA. EX evs: otway. \ |
27 \ ==> EX K. EX NA. EX evs: otway. \ |
28 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
28 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
29 \ : set_of_list evs"; |
29 \ : set_of_list evs"; |
30 by (REPEAT (resolve_tac [exI,bexI] 1)); |
30 by (REPEAT (resolve_tac [exI,bexI] 1)); |
31 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); |
31 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); |
32 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); |
32 by possibility_tac; |
33 by (REPEAT_FIRST (resolve_tac [refl, conjI])); |
|
34 by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver)))); |
|
35 result(); |
33 result(); |
36 |
34 |
37 |
35 |
38 (**** Inductive proofs about otway ****) |
36 (**** Inductive proofs about otway ****) |
39 |
|
40 (*The Spy can see more than anybody else, except for their initial state*) |
|
41 goal thy |
|
42 "!!evs. evs : otway ==> \ |
|
43 \ sees lost A evs <= initState lost A Un sees lost Spy evs"; |
|
44 by (etac otway.induct 1); |
|
45 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
|
46 addss (!simpset)))); |
|
47 qed "sees_agent_subset_sees_Spy"; |
|
48 |
|
49 |
37 |
50 (*Nobody sends themselves messages*) |
38 (*Nobody sends themselves messages*) |
51 goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs"; |
39 goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs"; |
52 by (etac otway.induct 1); |
40 by (etac otway.induct 1); |
53 by (Auto_tac()); |
41 by (Auto_tac()); |
61 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \ |
49 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \ |
62 \ X : analz (sees lost Spy evs)"; |
50 \ X : analz (sees lost Spy evs)"; |
63 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
51 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
64 qed "OR2_analz_sees_Spy"; |
52 qed "OR2_analz_sees_Spy"; |
65 |
53 |
66 goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \ |
54 goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \ |
67 \ X : analz (sees lost Spy evs)"; |
55 \ X : analz (sees lost Spy evs)"; |
68 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
56 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
69 qed "OR4_analz_sees_Spy"; |
57 qed "OR4_analz_sees_Spy"; |
70 |
58 |
71 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ |
59 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ |
72 \ ==> K : parts (sees lost Spy evs)"; |
60 \ ==> K : parts (sees lost Spy evs)"; |
73 by (fast_tac (!claset addSEs partsEs |
61 by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); |
74 addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
|
75 qed "Oops_parts_sees_Spy"; |
62 qed "Oops_parts_sees_Spy"; |
76 |
63 |
77 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
78 argument as for the Fake case. This is possible for most, but not all, |
65 argument as for the Fake case. This is possible for most, but not all, |
79 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
66 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
90 forward_tac [Oops_parts_sees_Spy] 7; |
77 forward_tac [Oops_parts_sees_Spy] 7; |
91 |
78 |
92 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
79 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
93 fun parts_induct_tac i = SELECT_GOAL |
80 fun parts_induct_tac i = SELECT_GOAL |
94 (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN |
81 (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN |
95 (*Fake message*) |
82 (*Fake message*) |
96 TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
83 TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
97 impOfSubs Fake_parts_insert] |
84 impOfSubs Fake_parts_insert] |
98 addss (!simpset)) 2)) THEN |
85 addss (!simpset)) 2)) THEN |
99 (*Base case*) |
86 (*Base case*) |
100 fast_tac (!claset addss (!simpset)) 1 THEN |
87 fast_tac (!claset addss (!simpset)) 1 THEN |
101 ALLGOALS Asm_simp_tac) i; |
88 ALLGOALS Asm_simp_tac) i; |
102 |
89 |
127 |
114 |
128 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
115 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
129 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
116 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
130 |
117 |
131 |
118 |
132 (*** Future keys can't be seen or used! ***) |
119 (*Nobody can have used non-existent keys!*) |
133 |
120 goal thy "!!evs. evs : otway ==> \ |
134 (*Nobody can have SEEN keys that will be generated in the future. *) |
121 \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; |
135 goal thy "!!i. evs : otway ==> \ |
|
136 \ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)"; |
|
137 by (parts_induct_tac 1); |
122 by (parts_induct_tac 1); |
138 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] |
123 (*Fake*) |
139 addDs [impOfSubs analz_subset_parts, |
124 by (best_tac |
140 impOfSubs parts_insert_subset_Un, |
125 (!claset addIs [impOfSubs analz_subset_parts] |
141 Suc_leD] |
126 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
142 addss (!simpset)))); |
127 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
143 qed_spec_mp "new_keys_not_seen"; |
128 addss (!simpset)) 1); |
144 Addsimps [new_keys_not_seen]; |
129 (*OR1-3*) |
145 |
130 by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); |
146 (*Variant: old messages must contain old keys!*) |
|
147 goal thy |
|
148 "!!evs. [| Says A B X : set_of_list evs; \ |
|
149 \ Key (newK i) : parts {X}; \ |
|
150 \ evs : otway \ |
|
151 \ |] ==> i < length evs"; |
|
152 by (rtac ccontr 1); |
|
153 by (dtac leI 1); |
|
154 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] |
|
155 addIs [impOfSubs parts_mono]) 1); |
|
156 qed "Says_imp_old_keys"; |
|
157 |
|
158 |
|
159 (*** Future nonces can't be seen or used! ***) |
|
160 |
|
161 goal thy "!!i. evs : otway ==> \ |
|
162 \ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)"; |
|
163 by (parts_induct_tac 1); |
|
164 by (REPEAT_FIRST |
|
165 (fast_tac (!claset addSEs partsEs |
|
166 addSDs [Says_imp_sees_Spy RS parts.Inj] |
|
167 addEs [leD RS notE] |
|
168 addDs [impOfSubs analz_subset_parts, |
|
169 impOfSubs parts_insert_subset_Un, Suc_leD] |
|
170 addss (!simpset)))); |
|
171 qed_spec_mp "new_nonces_not_seen"; |
|
172 Addsimps [new_nonces_not_seen]; |
|
173 |
|
174 (*Variant: old messages must contain old nonces!*) |
|
175 goal thy |
|
176 "!!evs. [| Says A B X : set_of_list evs; \ |
|
177 \ Nonce (newN i) : parts {X}; \ |
|
178 \ evs : otway \ |
|
179 \ |] ==> i < length evs"; |
|
180 by (rtac ccontr 1); |
|
181 by (dtac leI 1); |
|
182 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] |
|
183 addIs [impOfSubs parts_mono]) 1); |
|
184 qed "Says_imp_old_nonces"; |
|
185 |
|
186 |
|
187 (*Nobody can have USED keys that will be generated in the future. |
|
188 ...very like new_keys_not_seen*) |
|
189 goal thy "!!i. evs : otway ==> \ |
|
190 \ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))"; |
|
191 by (parts_induct_tac 1); |
|
192 (*OR1 and OR3*) |
|
193 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); |
|
194 (*Fake, OR2, OR4: these messages send unknown (X) components*) |
|
195 by (REPEAT |
|
196 (best_tac |
|
197 (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
|
198 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
|
199 Suc_leD] |
|
200 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] |
|
201 addss (!simpset)) 1)); |
|
202 qed_spec_mp "new_keys_not_used"; |
131 qed_spec_mp "new_keys_not_used"; |
203 |
132 |
204 bind_thm ("new_keys_not_analzd", |
133 bind_thm ("new_keys_not_analzd", |
205 [analz_subset_parts RS keysFor_mono, |
134 [analz_subset_parts RS keysFor_mono, |
206 new_keys_not_used] MRS contra_subsetD); |
135 new_keys_not_used] MRS contra_subsetD); |
212 (*** Proofs involving analz ***) |
141 (*** Proofs involving analz ***) |
213 |
142 |
214 (*Describes the form of K and NA when the Server sends this message. Also |
143 (*Describes the form of K and NA when the Server sends this message. Also |
215 for Oops case.*) |
144 for Oops case.*) |
216 goal thy |
145 goal thy |
217 "!!evs. [| Says Server B \ |
146 "!!evs. [| Says Server B \ |
218 \ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ |
147 \ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
219 \ evs : otway |] \ |
148 \ evs : otway |] \ |
220 \ ==> (EX n. K = Key(newK n)) & \ |
149 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
221 \ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
|
222 by (etac rev_mp 1); |
150 by (etac rev_mp 1); |
223 by (etac otway.induct 1); |
151 by (etac otway.induct 1); |
224 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
152 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
225 qed "Says_Server_message_form"; |
153 qed "Says_Server_message_form"; |
226 |
154 |
227 |
155 |
228 (*For proofs involving analz.*) |
156 (*For proofs involving analz.*) |
229 val analz_Fake_tac = |
157 val analz_Fake_tac = |
230 dtac OR2_analz_sees_Spy 4 THEN |
158 dtac OR2_analz_sees_Spy 4 THEN |
231 dtac OR4_analz_sees_Spy 6 THEN |
159 dtac OR4_analz_sees_Spy 6 THEN |
232 forward_tac [Says_Server_message_form] 7 THEN |
160 forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN |
233 assume_tac 7 THEN Full_simp_tac 7 THEN |
|
234 REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); |
161 REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); |
235 |
162 |
236 |
163 |
237 (**** |
164 (**** |
238 The following is to prove theorems of the form |
165 The following is to prove theorems of the form |
239 |
166 |
240 Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> |
167 Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> |
241 Key K : analz (sees lost Spy evs) |
168 Key K : analz (sees lost Spy evs) |
242 |
169 |
243 A more general formula must be proved inductively. |
170 A more general formula must be proved inductively. |
244 |
|
245 ****) |
171 ****) |
246 |
172 |
247 |
173 |
248 (** Session keys are not used to encrypt other session keys **) |
174 (** Session keys are not used to encrypt other session keys **) |
249 |
|
250 (*Lemma for the trivial direction of the if-and-only-if*) |
|
251 goal thy |
|
252 "!!evs. (Key K : analz (Key``nE Un sEe)) --> \ |
|
253 \ (K : nE | Key K : analz sEe) ==> \ |
|
254 \ (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)"; |
|
255 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); |
|
256 val lemma = result(); |
|
257 |
|
258 |
175 |
259 (*The equality makes the induction hypothesis easier to apply*) |
176 (*The equality makes the induction hypothesis easier to apply*) |
260 goal thy |
177 goal thy |
261 "!!evs. evs : otway ==> \ |
178 "!!evs. evs : otway ==> \ |
262 \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ |
179 \ ALL K KK. KK <= Compl (range shrK) --> \ |
263 \ (K : newK``E | Key K : analz (sees lost Spy evs))"; |
180 \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ |
|
181 \ (K : KK | Key K : analz (sees lost Spy evs))"; |
264 by (etac otway.induct 1); |
182 by (etac otway.induct 1); |
265 by analz_Fake_tac; |
183 by analz_Fake_tac; |
266 by (REPEAT_FIRST (ares_tac [allI, lemma])); |
184 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
267 by (ALLGOALS (*Takes 18 secs*) |
185 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
268 (asm_simp_tac |
186 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
269 (!simpset addsimps [Un_assoc RS sym, |
187 (*Base*) |
270 insert_Key_singleton, insert_Key_image, pushKey_newK] |
188 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
271 setloop split_tac [expand_if]))); |
189 (*Fake, OR2, OR4*) |
272 (*OR4, OR2, Fake*) |
190 by (REPEAT (spy_analz_tac 1)); |
273 by (EVERY (map spy_analz_tac [5,3,2])); |
191 qed_spec_mp "analz_image_freshK"; |
274 (*Oops, OR3, Base*) |
|
275 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); |
|
276 qed_spec_mp "analz_image_newK"; |
|
277 |
192 |
278 |
193 |
279 goal thy |
194 goal thy |
280 "!!evs. evs : otway ==> \ |
195 "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \ |
281 \ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \ |
196 \ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ |
282 \ (K = newK i | Key K : analz (sees lost Spy evs))"; |
197 \ (K = KAB | Key K : analz (sees lost Spy evs))"; |
283 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
198 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
284 insert_Key_singleton]) 1); |
199 qed "analz_insert_freshK"; |
285 by (Fast_tac 1); |
|
286 qed "analz_insert_Key_newK"; |
|
287 |
200 |
288 |
201 |
289 (*** The Key K uniquely identifies the Server's message. **) |
202 (*** The Key K uniquely identifies the Server's message. **) |
290 |
203 |
291 goal thy |
204 goal thy |
299 (*Remaining cases: OR3 and OR4*) |
212 (*Remaining cases: OR3 and OR4*) |
300 by (ex_strip_tac 2); |
213 by (ex_strip_tac 2); |
301 by (Fast_tac 2); |
214 by (Fast_tac 2); |
302 by (expand_case_tac "K = ?y" 1); |
215 by (expand_case_tac "K = ?y" 1); |
303 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
216 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
304 (*...we assume X is a very new message, and handle this case by contradiction*) |
217 (*...we assume X is a recent message, and handle this case by contradiction*) |
305 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] |
218 by (fast_tac (!claset addSEs sees_Spy_partsEs |
306 delrules [conjI] (*prevent split-up into 4 subgoals*) |
219 delrules [conjI] (*prevent split-up into 4 subgoals*) |
307 addss (!simpset addsimps [parts_insertI])) 1); |
220 addss (!simpset addsimps [parts_insertI])) 1); |
308 val lemma = result(); |
221 val lemma = result(); |
309 |
222 |
310 goal thy |
223 goal thy |
326 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ |
239 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ |
327 \ Key K ~: analz (sees lost Spy evs)"; |
240 \ Key K ~: analz (sees lost Spy evs)"; |
328 by (etac otway.induct 1); |
241 by (etac otway.induct 1); |
329 by analz_Fake_tac; |
242 by analz_Fake_tac; |
330 by (ALLGOALS |
243 by (ALLGOALS |
331 (asm_simp_tac (!simpset addsimps [not_parts_not_analz, |
244 (asm_simp_tac (!simpset addcongs [conj_cong] |
332 analz_insert_Key_newK] |
245 addsimps [not_parts_not_analz, analz_insert_freshK] |
333 setloop split_tac [expand_if]))); |
246 setloop split_tac [expand_if]))); |
334 (*OR3*) |
247 (*OR3*) |
335 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] |
248 by (fast_tac (!claset delrules [impCE] |
|
249 addSEs sees_Spy_partsEs |
|
250 addIs [impOfSubs analz_subset_parts] |
336 addss (!simpset addsimps [parts_insert2])) 3); |
251 addss (!simpset addsimps [parts_insert2])) 3); |
337 (*OR4, OR2, Fake*) |
252 (*OR4, OR2, Fake*) |
338 by (REPEAT_FIRST spy_analz_tac); |
253 by (REPEAT_FIRST spy_analz_tac); |
339 (*Oops*) (** LEVEL 5 **) |
254 (*Oops*) (** LEVEL 5 **) |
340 by (fast_tac (!claset delrules [disjE] |
255 by (fast_tac (!claset delrules [disjE] |
341 addDs [unique_session_keys] addss (!simpset)) 1); |
256 addDs [unique_session_keys] addss (!simpset)) 1); |
342 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
257 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
343 |
258 |
344 |
259 goal thy |
345 goal thy |
260 "!!evs. [| Says Server B \ |
346 "!!evs. [| Says Server B \ |
261 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
347 \ {|NA, Crypt (shrK A) {|NA, K|}, \ |
262 \ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ |
348 \ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ |
263 \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
349 \ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ |
|
350 \ A ~: lost; B ~: lost; evs : otway |] \ |
264 \ A ~: lost; B ~: lost; evs : otway |] \ |
351 \ ==> K ~: analz (sees lost Spy evs)"; |
265 \ ==> Key K ~: analz (sees lost Spy evs)"; |
352 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
266 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
353 by (fast_tac (!claset addSEs [lemma]) 1); |
267 by (fast_tac (!claset addSEs [lemma]) 1); |
354 qed "Spy_not_see_encrypted_key"; |
268 qed "Spy_not_see_encrypted_key"; |
355 |
269 |
356 |
270 |
357 (*** Attempting to prove stronger properties ***) |
271 (*** Attempting to prove stronger properties ***) |
358 |
272 |
359 (*Only OR1 can have caused such a part of a message to appear. |
273 (*Only OR1 can have caused such a part of a message to appear. |
360 I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. |
274 I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. |
361 Perhaps it's because OR2 has two similar-looking encrypted messages in |
275 Perhaps it's because OR2 has two similar-looking encrypted messages in |
362 this version.*) |
276 this version.*) |
363 goal thy |
277 goal thy |
364 "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ |
278 "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ |
365 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
279 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
366 \ : parts (sees lost Spy evs) --> \ |
280 \ : parts (sees lost Spy evs) --> \ |
367 \ Says A B {|NA, Agent A, Agent B, \ |
281 \ Says A B {|NA, Agent A, Agent B, \ |
368 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
282 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
369 \ : set_of_list evs"; |
283 \ : set_of_list evs"; |
388 \ Crypt (shrK B) {|NB, Key K|}|} \ |
302 \ Crypt (shrK B) {|NB, Key K|}|} \ |
389 \ : set_of_list evs)"; |
303 \ : set_of_list evs)"; |
390 by (parts_induct_tac 1); |
304 by (parts_induct_tac 1); |
391 (*OR1: it cannot be a new Nonce, contradiction.*) |
305 (*OR1: it cannot be a new Nonce, contradiction.*) |
392 by (fast_tac (!claset addSIs [parts_insertI] |
306 by (fast_tac (!claset addSIs [parts_insertI] |
393 addSEs partsEs |
307 addSEs sees_Spy_partsEs |
394 addEs [Says_imp_old_nonces RS less_irrefl] |
|
395 addss (!simpset)) 1); |
308 addss (!simpset)) 1); |
396 (*OR4*) |
309 (*OR4*) |
397 by (REPEAT (Safe_step_tac 2)); |
310 by (REPEAT (Safe_step_tac 2)); |
398 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); |
311 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); |
399 by (fast_tac (!claset addSIs [Crypt_imp_OR1] |
312 by (fast_tac (!claset addSIs [Crypt_imp_OR1] |
400 addEs partsEs |
313 addEs sees_Spy_partsEs) 2); |
401 addDs [Says_imp_sees_Spy RS parts.Inj]) 2); |
|
402 (*OR3*) (** LEVEL 5 **) |
314 (*OR3*) (** LEVEL 5 **) |
403 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
315 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
404 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
316 by (step_tac (!claset delrules [disjCI, impCE]) 1); |
405 (*The hypotheses at this point suggest an attack in which nonce NA is used |
317 (*The hypotheses at this point suggest an attack in which nonce NA is used |
406 in two different roles: |
318 in two different roles: |