14 open NS_Public_Bad; |
14 open NS_Public_Bad; |
15 |
15 |
16 proof_timing:=true; |
16 proof_timing:=true; |
17 HOL_quantifiers := false; |
17 HOL_quantifiers := false; |
18 |
18 |
19 val op addss = op unsafe_addss; |
|
20 |
|
21 AddIffs [Spy_in_lost]; |
19 AddIffs [Spy_in_lost]; |
22 |
20 |
23 (*Replacing the variable by a constant improves search speed by 50%!*) |
21 (*Replacing the variable by a constant improves search speed by 50%!*) |
24 val Says_imp_sees_Spy' = |
22 val Says_imp_sees_Spy' = |
25 read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; |
23 read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; |
26 |
|
27 |
24 |
28 (*A "possibility property": there are traces that reach the end*) |
25 (*A "possibility property": there are traces that reach the end*) |
29 goal thy |
26 goal thy |
30 "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ |
27 "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ |
31 \ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; |
28 \ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; |
44 qed_spec_mp "not_Says_to_self"; |
41 qed_spec_mp "not_Says_to_self"; |
45 Addsimps [not_Says_to_self]; |
42 Addsimps [not_Says_to_self]; |
46 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
43 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
47 |
44 |
48 |
45 |
49 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
|
50 fun parts_induct_tac i = SELECT_GOAL |
|
51 (DETERM (etac ns_public.induct 1 THEN |
|
52 (*Fake message*) |
|
53 TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
|
54 impOfSubs Fake_parts_insert] |
|
55 addss (!simpset)) 2)) THEN |
|
56 (*Base case*) |
|
57 fast_tac (!claset addss (!simpset)) 1 THEN |
|
58 ALLGOALS Asm_simp_tac) i; |
|
59 |
|
60 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
46 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
61 sends messages containing X! **) |
47 sends messages containing X! **) |
62 |
48 |
63 (*Spy never sees another agent's private key! (unless it's lost at start)*) |
49 (*Spy never sees another agent's private key! (unless it's lost at start)*) |
64 goal thy |
50 goal thy |
65 "!!evs. evs : ns_public \ |
51 "!!evs. evs : ns_public \ |
66 \ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; |
52 \ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; |
67 by (parts_induct_tac 1); |
53 by (etac ns_public.induct 1); |
68 by (Auto_tac()); |
54 by (prove_simple_subgoals_tac 1); |
|
55 by (Fake_parts_insert_tac 1); |
69 qed "Spy_see_priK"; |
56 qed "Spy_see_priK"; |
70 Addsimps [Spy_see_priK]; |
57 Addsimps [Spy_see_priK]; |
71 |
58 |
72 goal thy |
59 goal thy |
73 "!!evs. evs : ns_public \ |
60 "!!evs. evs : ns_public \ |
76 qed "Spy_analz_priK"; |
63 qed "Spy_analz_priK"; |
77 Addsimps [Spy_analz_priK]; |
64 Addsimps [Spy_analz_priK]; |
78 |
65 |
79 goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ |
66 goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ |
80 \ evs : ns_public |] ==> A:lost"; |
67 \ evs : ns_public |] ==> A:lost"; |
81 by (fast_tac (!claset addDs [Spy_see_priK]) 1); |
68 by (blast_tac (!claset addDs [Spy_see_priK]) 1); |
82 qed "Spy_see_priK_D"; |
69 qed "Spy_see_priK_D"; |
83 |
70 |
84 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); |
71 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); |
85 AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; |
72 AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; |
86 |
73 |
87 |
74 |
88 fun analz_induct_tac i = |
75 fun analz_induct_tac i = |
89 etac ns_public.induct i THEN |
76 etac ns_public.induct i THEN |
90 ALLGOALS (asm_simp_tac |
77 ALLGOALS (asm_simp_tac |
91 (!simpset addsimps [not_parts_not_analz] |
78 (!simpset addsimps [not_parts_not_analz] |
92 setloop split_tac [expand_if])); |
79 setloop split_tac [expand_if])); |
93 |
80 |
94 |
81 |
103 \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)"; |
90 \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)"; |
104 by (etac rev_mp 1); |
91 by (etac rev_mp 1); |
105 by (etac rev_mp 1); |
92 by (etac rev_mp 1); |
106 by (analz_induct_tac 1); |
93 by (analz_induct_tac 1); |
107 (*NS3*) |
94 (*NS3*) |
108 by (fast_tac (!claset addSEs partsEs) 4); |
95 by (blast_tac (!claset addSEs partsEs) 4); |
109 (*NS2*) |
96 (*NS2*) |
110 by (fast_tac (!claset addSEs partsEs) 3); |
97 by (blast_tac (!claset addSEs partsEs) 3); |
111 (*Fake*) |
98 (*Fake*) |
112 by (deepen_tac (!claset addSIs [analz_insertI] |
99 by (blast_tac (!claset addSIs [analz_insertI] |
113 addDs [impOfSubs analz_subset_parts, |
100 addDs [impOfSubs analz_subset_parts, |
114 impOfSubs Fake_parts_insert] |
101 impOfSubs Fake_parts_insert]) 2); |
115 addss (!simpset)) 0 2); |
|
116 (*Base*) |
102 (*Base*) |
117 by (fast_tac (!claset addss (!simpset)) 1); |
103 by (Blast_tac 1); |
118 qed "no_nonce_NS1_NS2"; |
104 qed "no_nonce_NS1_NS2"; |
119 |
105 |
120 |
106 |
121 (*Unicity for NS1: nonce NA identifies agents A and B*) |
107 (*Unicity for NS1: nonce NA identifies agents A and B*) |
122 goal thy |
108 goal thy |
127 by (etac rev_mp 1); |
113 by (etac rev_mp 1); |
128 by (analz_induct_tac 1); |
114 by (analz_induct_tac 1); |
129 (*NS1*) |
115 (*NS1*) |
130 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
116 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
131 by (expand_case_tac "NA = ?y" 3 THEN |
117 by (expand_case_tac "NA = ?y" 3 THEN |
132 REPEAT (fast_tac (!claset addSEs partsEs) 3)); |
118 REPEAT (blast_tac (!claset addSEs partsEs) 3)); |
133 (*Base*) |
119 (*Base*) |
134 by (fast_tac (!claset addss (!simpset)) 1); |
120 by (Blast_tac 1); |
135 (*Fake*) |
121 (*Fake*) |
136 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); |
122 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); |
137 by (step_tac (!claset addSIs [analz_insertI]) 1); |
123 by (step_tac (!claset addSIs [analz_insertI]) 1); |
138 by (ex_strip_tac 1); |
124 by (ex_strip_tac 1); |
139 by (best_tac (!claset delrules [conjI] |
125 by (blast_tac (!claset delrules [conjI] |
140 addSDs [impOfSubs Fake_parts_insert] |
126 addSDs [impOfSubs Fake_parts_insert] |
141 addDs [impOfSubs analz_subset_parts] |
127 addDs [impOfSubs analz_subset_parts]) 1); |
142 addss (!simpset)) 1); |
|
143 val lemma = result(); |
128 val lemma = result(); |
144 |
129 |
145 goal thy |
130 goal thy |
146 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \ |
131 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \ |
147 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \ |
132 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \ |
158 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
143 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
159 \ ==> Nonce NA ~: analz (sees lost Spy evs)"; |
144 \ ==> Nonce NA ~: analz (sees lost Spy evs)"; |
160 by (etac rev_mp 1); |
145 by (etac rev_mp 1); |
161 by (analz_induct_tac 1); |
146 by (analz_induct_tac 1); |
162 (*NS3*) |
147 (*NS3*) |
163 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
148 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] |
164 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
149 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
165 (*NS2*) |
150 (*NS2*) |
166 by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
151 by (blast_tac (!claset addSEs [MPair_parts] |
167 addSEs [MPair_parts] |
152 addDs [Says_imp_sees_Spy' RS parts.Inj, |
168 addDs [parts.Body, unique_NA]) 0 3); |
153 parts.Body, unique_NA]) 3); |
169 (*NS1*) |
154 (*NS1*) |
170 by (fast_tac (!claset addSEs sees_Spy_partsEs |
155 by (blast_tac (!claset addSEs sees_Spy_partsEs |
171 addIs [impOfSubs analz_subset_parts]) 2); |
156 addIs [impOfSubs analz_subset_parts]) 2); |
172 (*Fake*) |
157 (*Fake*) |
173 by (spy_analz_tac 1); |
158 by (spy_analz_tac 1); |
174 qed "Spy_not_see_NA"; |
159 qed "Spy_not_see_NA"; |
175 |
160 |
176 |
161 |
185 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) |
170 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) |
186 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); |
171 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); |
187 by (etac ns_public.induct 1); |
172 by (etac ns_public.induct 1); |
188 by (ALLGOALS Asm_simp_tac); |
173 by (ALLGOALS Asm_simp_tac); |
189 (*NS1*) |
174 (*NS1*) |
190 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
175 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); |
191 (*Fake*) |
176 (*Fake*) |
192 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
177 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
193 by (fast_tac (!claset addss (!simpset)) 1); |
178 addDs [Spy_not_see_NA, |
194 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
179 impOfSubs analz_subset_parts]) 1); |
195 by (best_tac (!claset addSIs [disjI2] |
180 (*NS2; not clear why blast_tac needs to be preceeded by Step_tac*) |
196 addSDs [impOfSubs Fake_parts_insert] |
|
197 addDs [impOfSubs analz_subset_parts] |
|
198 addss (!simpset)) 1); |
|
199 (*NS2*) |
|
200 by (Step_tac 1); |
181 by (Step_tac 1); |
201 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
182 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, |
202 by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
183 Spy_not_see_NA, unique_NA]) 1); |
203 addDs [unique_NA]) 1 1); |
|
204 qed "A_trusts_NS2"; |
184 qed "A_trusts_NS2"; |
205 |
185 |
206 (*If the encrypted message appears then it originated with Alice in NS1*) |
186 (*If the encrypted message appears then it originated with Alice in NS1*) |
207 goal thy |
187 goal thy |
208 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \ |
188 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \ |
211 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
191 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
212 by (etac rev_mp 1); |
192 by (etac rev_mp 1); |
213 by (etac rev_mp 1); |
193 by (etac rev_mp 1); |
214 by (analz_induct_tac 1); |
194 by (analz_induct_tac 1); |
215 (*Fake*) |
195 (*Fake*) |
216 by (best_tac (!claset addSIs [disjI2] |
196 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
217 addSDs [impOfSubs Fake_parts_insert] |
197 addIs [analz_insertI] |
218 addIs [analz_insertI] |
198 addDs [impOfSubs analz_subset_parts]) 2); |
219 addDs [impOfSubs analz_subset_parts] |
|
220 addss (!simpset)) 2); |
|
221 (*Base*) |
199 (*Base*) |
222 by (fast_tac (!claset addss (!simpset)) 1); |
200 by (Blast_tac 1); |
223 qed_spec_mp "B_trusts_NS1"; |
201 qed "B_trusts_NS1"; |
224 |
202 |
225 |
203 |
226 |
204 |
227 (**** Authenticity properties obtained from NS2 ****) |
205 (**** Authenticity properties obtained from NS2 ****) |
228 |
206 |
236 by (etac rev_mp 1); |
214 by (etac rev_mp 1); |
237 by (analz_induct_tac 1); |
215 by (analz_induct_tac 1); |
238 (*NS2*) |
216 (*NS2*) |
239 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
217 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
240 by (expand_case_tac "NB = ?y" 3 THEN |
218 by (expand_case_tac "NB = ?y" 3 THEN |
241 REPEAT (fast_tac (!claset addSEs partsEs) 3)); |
219 REPEAT (blast_tac (!claset addSEs partsEs) 3)); |
242 (*Base*) |
220 (*Base*) |
243 by (fast_tac (!claset addss (!simpset)) 1); |
221 by (Blast_tac 1); |
244 (*Fake*) |
222 (*Fake*) |
245 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); |
223 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); |
246 by (step_tac (!claset addSIs [analz_insertI]) 1); |
224 by (step_tac (!claset addSIs [analz_insertI]) 1); |
247 by (ex_strip_tac 1); |
225 by (ex_strip_tac 1); |
248 by (best_tac (!claset delrules [conjI] |
226 by (blast_tac (!claset delrules [conjI] |
249 addSDs [impOfSubs Fake_parts_insert] |
227 addSDs [impOfSubs Fake_parts_insert] |
250 addDs [impOfSubs analz_subset_parts] |
228 addDs [impOfSubs analz_subset_parts]) 1); |
251 addss (!simpset)) 1); |
|
252 val lemma = result(); |
229 val lemma = result(); |
253 |
230 |
254 goal thy |
231 goal thy |
255 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(sees lost Spy evs); \ |
232 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(sees lost Spy evs); \ |
256 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \ |
233 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \ |
269 \ ==> Nonce NB ~: analz (sees lost Spy evs)"; |
246 \ ==> Nonce NB ~: analz (sees lost Spy evs)"; |
270 by (etac rev_mp 1); |
247 by (etac rev_mp 1); |
271 by (etac rev_mp 1); |
248 by (etac rev_mp 1); |
272 by (analz_induct_tac 1); |
249 by (analz_induct_tac 1); |
273 (*NS1*) |
250 (*NS1*) |
274 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
251 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); |
275 (*Fake*) |
252 (*Fake*) |
276 by (spy_analz_tac 1); |
253 by (spy_analz_tac 1); |
277 (*NS2 and NS3*) |
254 (*NS2 and NS3*) |
278 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
255 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
279 by (step_tac (!claset delrules [allI]) 1); |
256 by (step_tac (!claset delrules [allI]) 1); |
280 by (Fast_tac 5); |
257 by (Blast_tac 5); |
281 by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); |
|
282 (*NS2*) |
|
283 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
|
284 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
285 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
|
286 (*NS3*) |
258 (*NS3*) |
287 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 |
259 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, |
288 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); |
260 Spy_not_see_NB, unique_NB]) 4); |
289 by (Fast_tac 1); |
261 (*NS2*) |
|
262 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); |
|
263 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
264 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); |
|
265 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); |
290 qed "Spy_not_see_NB"; |
266 qed "Spy_not_see_NB"; |
291 |
267 |
292 |
268 |
293 |
269 |
294 (*Authentication for B: if he receives message 3 and has used NB |
270 (*Authentication for B: if he receives message 3 and has used NB |
303 (*prepare induction over Crypt (pubK B) NB : parts H*) |
279 (*prepare induction over Crypt (pubK B) NB : parts H*) |
304 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); |
280 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); |
305 by (analz_induct_tac 1); |
281 by (analz_induct_tac 1); |
306 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
282 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
307 (*NS1*) |
283 (*NS1*) |
308 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
284 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); |
309 (*Fake*) |
285 (*Fake*) |
310 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
286 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
311 by (fast_tac (!claset addss (!simpset)) 1); |
287 addDs [Spy_not_see_NB, |
312 by (rtac (ccontr RS disjI2) 1); |
288 impOfSubs analz_subset_parts]) 1); |
313 by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) |
289 (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) |
314 THEN Fast_tac 1); |
|
315 by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
|
316 addDs [impOfSubs analz_subset_parts] |
|
317 addss (!simpset)) 1); |
|
318 (*NS3*) |
|
319 by (Step_tac 1); |
290 by (Step_tac 1); |
320 by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) |
291 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, |
321 THEN Fast_tac 1); |
292 Spy_not_see_NB, unique_NB]) 1); |
322 by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
323 addDs [unique_NB]) 1); |
|
324 qed "B_trusts_NS3"; |
293 qed "B_trusts_NS3"; |
325 |
294 |
326 |
295 |
327 (*Can we strengthen the secrecy theorem? NO*) |
296 (*Can we strengthen the secrecy theorem? NO*) |
328 goal thy |
297 goal thy |
329 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
298 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
330 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \ |
299 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \ |
331 \ --> Nonce NB ~: analz (sees lost Spy evs)"; |
300 \ --> Nonce NB ~: analz (sees lost Spy evs)"; |
332 by (analz_induct_tac 1); |
301 by (analz_induct_tac 1); |
333 (*NS1*) |
302 (*NS1*) |
334 by (fast_tac (!claset addSEs partsEs |
303 by (blast_tac (!claset addSEs partsEs |
335 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
304 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
336 (*Fake*) |
305 (*Fake*) |
337 by (spy_analz_tac 1); |
306 by (spy_analz_tac 1); |
338 (*NS2 and NS3*) |
307 (*NS2 and NS3*) |
339 by (Step_tac 1); |
308 by (Step_tac 1); |
340 by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); |
309 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); |
341 (*NS2*) |
310 (*NS2*) |
342 by (fast_tac (!claset addSEs partsEs |
311 by (blast_tac (!claset addSEs partsEs |
343 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
312 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
344 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
313 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
345 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
314 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
346 (*NS3*) |
315 (*NS3*) |
347 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 |
316 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 |
348 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); |
317 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); |
349 by (Step_tac 1); |
318 by (Step_tac 1); |
350 |
319 |