112 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
112 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
113 \ Crypt (pubK C) {|X, Nonce NA, Agent D|} ~: parts (sees lost Spy evs)"; |
113 \ Crypt (pubK C) {|X, Nonce NA, Agent D|} ~: parts (sees lost Spy evs)"; |
114 by (etac ns_public.induct 1); |
114 by (etac ns_public.induct 1); |
115 by (ALLGOALS |
115 by (ALLGOALS |
116 (asm_simp_tac |
116 (asm_simp_tac |
117 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
117 (!simpset addsimps ([not_parts_not_analz] @ pushes) |
118 setloop split_tac [expand_if]))); |
118 setloop split_tac [expand_if]))); |
119 (*NS3*) |
119 (*NS3*) |
120 by (fast_tac (!claset addSEs partsEs |
120 by (fast_tac (!claset addSEs partsEs |
121 addEs [nonce_not_seen_now]) 4); |
121 addEs [nonce_not_seen_now]) 4); |
122 (*NS2*) |
122 (*NS2*) |
123 by (fast_tac (!claset addSEs partsEs |
123 by (fast_tac (!claset addSEs partsEs |
124 addEs [nonce_not_seen_now]) 3); |
124 addEs [nonce_not_seen_now]) 3); |
125 (*Fake*) |
125 (*Fake*) |
126 by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)] |
126 by (best_tac (!claset addIs [analz_insertI] |
127 addDs [impOfSubs analz_subset_parts, |
127 addDs [impOfSubs analz_subset_parts, |
128 impOfSubs Fake_parts_insert] |
128 impOfSubs Fake_parts_insert] |
129 addss (!simpset)) 2); |
129 addss (!simpset)) 2); |
130 (*Base*) |
130 (*Base*) |
131 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] |
131 by (fast_tac (!claset addss (!simpset)) 1); |
132 addss (!simpset)) 1); |
|
133 bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); |
132 bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); |
134 |
133 |
135 |
134 |
136 (*Uniqueness for NS1: nonce NA identifies agents A and B*) |
135 (*Uniqueness for NS1: nonce NA identifies agents A and B*) |
137 goal thy |
136 goal thy |
141 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
140 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
142 \ A=A' & B=B')"; |
141 \ A=A' & B=B')"; |
143 by (etac ns_public.induct 1); |
142 by (etac ns_public.induct 1); |
144 by (ALLGOALS |
143 by (ALLGOALS |
145 (asm_simp_tac |
144 (asm_simp_tac |
146 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
145 (!simpset addsimps ([not_parts_not_analz] @ pushes) |
147 setloop split_tac [expand_if]))); |
146 setloop split_tac [expand_if]))); |
148 (*NS1*) |
147 (*NS1*) |
149 by (expand_case_tac "NA = ?y" 3 THEN |
148 by (expand_case_tac "NA = ?y" 3 THEN |
150 REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); |
149 REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); |
151 (*Base*) |
150 (*Base*) |
152 by (fast_tac (!claset addss (!simpset)) 1); |
151 by (fast_tac (!claset addss (!simpset)) 1); |
153 (*Fake*) |
152 (*Fake*) |
154 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); |
153 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); |
155 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); |
154 by (step_tac (!claset addSIs [analz_insertI]) 1); |
156 by (ex_strip_tac 1); |
155 by (ex_strip_tac 1); |
157 by (best_tac (!claset delrules [conjI] |
156 by (best_tac (!claset delrules [conjI] |
158 addSDs [impOfSubs Fake_parts_insert] |
157 addSDs [impOfSubs Fake_parts_insert] |
159 addDs [impOfSubs analz_subset_parts] |
158 addDs [impOfSubs analz_subset_parts] |
160 addss (!simpset)) 1); |
159 addss (!simpset)) 1); |
181 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ |
180 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ |
182 \ --> Nonce NA ~: analz (sees lost Spy evs)"; |
181 \ --> Nonce NA ~: analz (sees lost Spy evs)"; |
183 by (etac ns_public.induct 1); |
182 by (etac ns_public.induct 1); |
184 by (ALLGOALS |
183 by (ALLGOALS |
185 (asm_simp_tac |
184 (asm_simp_tac |
186 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
185 (!simpset addsimps ([not_parts_not_analz] @ pushes) |
187 setloop split_tac [expand_if]))); |
186 setloop split_tac [expand_if]))); |
188 (*NS3*) |
187 (*NS3*) |
189 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
188 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
190 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
189 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
191 (*NS1*) |
190 (*NS1*) |
192 by (fast_tac (!claset addSEs partsEs |
191 by (fast_tac (!claset addSEs partsEs |
193 addSDs [new_nonces_not_seen, |
192 addSDs [new_nonces_not_seen, |
194 Says_imp_sees_Spy' RS parts.Inj]) 2); |
193 Says_imp_sees_Spy' RS parts.Inj]) 2); |
195 (*Fake*) |
194 (*Fake*) |
196 by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); |
195 by (REPEAT_FIRST spy_analz_tac); |
197 (*NS2*) |
196 (*NS2*) |
198 by (Step_tac 1); |
197 by (Step_tac 1); |
199 by (fast_tac (!claset addSEs partsEs |
198 by (fast_tac (!claset addSEs partsEs |
200 addSDs [new_nonces_not_seen, |
199 addSDs [new_nonces_not_seen, |
201 Says_imp_sees_Spy' RS parts.Inj]) 2); |
200 Says_imp_sees_Spy' RS parts.Inj]) 2); |
250 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
249 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
251 \ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
250 \ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
252 by (etac ns_public.induct 1); |
251 by (etac ns_public.induct 1); |
253 by (ALLGOALS |
252 by (ALLGOALS |
254 (asm_simp_tac |
253 (asm_simp_tac |
255 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
254 (!simpset addsimps ([not_parts_not_analz] @ pushes) |
256 setloop split_tac [expand_if]))); |
255 setloop split_tac [expand_if]))); |
257 (*Fake*) |
256 (*Fake*) |
258 by (best_tac (!claset addSIs [disjI2] |
257 by (best_tac (!claset addSIs [disjI2] |
259 addSDs [impOfSubs Fake_parts_insert] |
258 addSDs [impOfSubs Fake_parts_insert] |
260 addIs [impOfSubs (subset_insertI RS analz_mono)] |
259 addIs [analz_insertI] |
261 addDs [impOfSubs analz_subset_parts] |
260 addDs [impOfSubs analz_subset_parts] |
262 addss (!simpset)) 2); |
261 addss (!simpset)) 2); |
263 (*Base*) |
262 (*Base*) |
264 by (fast_tac (!claset addss (!simpset)) 1); |
263 by (fast_tac (!claset addss (!simpset)) 1); |
265 qed_spec_mp "B_trusts_NS1"; |
264 qed_spec_mp "B_trusts_NS1"; |
278 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
277 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
279 \ : parts (sees lost Spy evs) --> A=A' & NA=NA' & B=B')"; |
278 \ : parts (sees lost Spy evs) --> A=A' & NA=NA' & B=B')"; |
280 by (etac ns_public.induct 1); |
279 by (etac ns_public.induct 1); |
281 by (ALLGOALS |
280 by (ALLGOALS |
282 (asm_simp_tac |
281 (asm_simp_tac |
283 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
282 (!simpset addsimps ([not_parts_not_analz] @ pushes) |
284 setloop split_tac [expand_if]))); |
283 setloop split_tac [expand_if]))); |
285 (*NS2*) |
284 (*NS2*) |
286 by (expand_case_tac "NB = ?y" 3 THEN |
285 by (expand_case_tac "NB = ?y" 3 THEN |
287 REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); |
286 REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); |
288 (*Base*) |
287 (*Base*) |
289 by (fast_tac (!claset addss (!simpset)) 1); |
288 by (fast_tac (!claset addss (!simpset)) 1); |
290 (*Fake*) |
289 (*Fake*) |
291 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); |
290 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); |
292 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); |
291 by (step_tac (!claset addSIs [analz_insertI]) 1); |
293 by (ex_strip_tac 1); |
292 by (ex_strip_tac 1); |
294 by (best_tac (!claset delrules [conjI] |
293 by (best_tac (!claset delrules [conjI] |
295 addSDs [impOfSubs Fake_parts_insert] |
294 addSDs [impOfSubs Fake_parts_insert] |
296 addDs [impOfSubs analz_subset_parts] |
295 addDs [impOfSubs analz_subset_parts] |
297 addss (!simpset)) 1); |
296 addss (!simpset)) 1); |
321 \ : set_of_list evs \ |
320 \ : set_of_list evs \ |
322 \ --> Nonce NB ~: analz (sees lost Spy evs)"; |
321 \ --> Nonce NB ~: analz (sees lost Spy evs)"; |
323 by (etac ns_public.induct 1); |
322 by (etac ns_public.induct 1); |
324 by (ALLGOALS |
323 by (ALLGOALS |
325 (asm_simp_tac |
324 (asm_simp_tac |
326 (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) |
325 (!simpset addsimps ([not_parts_not_analz] @ pushes) |
327 setloop split_tac [expand_if]))); |
326 setloop split_tac [expand_if]))); |
328 (*NS3*) |
327 (*NS3*) |
329 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
328 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
330 addDs [unique_NB]) 4); |
329 addDs [unique_NB]) 4); |
331 (*NS1*) |
330 (*NS1*) |
332 by (fast_tac (!claset addSEs partsEs |
331 by (fast_tac (!claset addSEs partsEs |
333 addSDs [new_nonces_not_seen, |
332 addSDs [new_nonces_not_seen, |
334 Says_imp_sees_Spy' RS parts.Inj]) 2); |
333 Says_imp_sees_Spy' RS parts.Inj]) 2); |
335 (*Fake*) |
334 (*Fake*) |
336 by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); |
335 by (REPEAT_FIRST spy_analz_tac); |
337 (*NS2*) |
336 (*NS2*) |
338 by (Step_tac 1); |
337 by (Step_tac 1); |
339 by (fast_tac (!claset addSEs partsEs |
338 by (fast_tac (!claset addSEs partsEs |
340 addSDs [new_nonces_not_seen, |
339 addSDs [new_nonces_not_seen, |
341 Says_imp_sees_Spy' RS parts.Inj]) 2); |
340 Says_imp_sees_Spy' RS parts.Inj]) 2); |