equal
deleted
inserted
replaced
86 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
86 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
87 goal thy |
87 goal thy |
88 "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
88 "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
89 by (parts_induct_tac 1); |
89 by (parts_induct_tac 1); |
90 by (Fake_parts_insert_tac 1); |
90 by (Fake_parts_insert_tac 1); |
91 by (Blast_tac 1); |
91 by (ALLGOALS Blast_tac); |
92 qed "Spy_see_shrK"; |
92 qed "Spy_see_shrK"; |
93 Addsimps [Spy_see_shrK]; |
93 Addsimps [Spy_see_shrK]; |
94 |
94 |
95 goal thy |
95 goal thy |
96 "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
96 "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
110 goal thy "!!evs. evs : otway ==> \ |
110 goal thy "!!evs. evs : otway ==> \ |
111 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
111 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
112 by (parts_induct_tac 1); |
112 by (parts_induct_tac 1); |
113 (*Fake*) |
113 (*Fake*) |
114 by (best_tac |
114 by (best_tac |
115 (!claset addIs [impOfSubs analz_subset_parts] |
115 (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
116 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
116 addIs [impOfSubs analz_subset_parts] |
117 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
117 addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] |
118 addss (!simpset)) 1); |
118 addss (!simpset)) 1); |
119 (*OR1-3*) |
119 (*OR1-3*) |
120 by (ALLGOALS Blast_tac); |
120 by (ALLGOALS Blast_tac); |
121 qed_spec_mp "new_keys_not_used"; |
121 qed_spec_mp "new_keys_not_used"; |
122 |
122 |
123 bind_thm ("new_keys_not_analzd", |
123 bind_thm ("new_keys_not_analzd", |
229 by (etac otway.induct 1); |
229 by (etac otway.induct 1); |
230 by analz_spies_tac; |
230 by analz_spies_tac; |
231 by (ALLGOALS |
231 by (ALLGOALS |
232 (asm_simp_tac (!simpset addcongs [conj_cong] |
232 (asm_simp_tac (!simpset addcongs [conj_cong] |
233 addsimps [analz_insert_eq, analz_insert_freshK] |
233 addsimps [analz_insert_eq, analz_insert_freshK] |
234 addsplits [expand_if]))); |
234 addsimps (pushes@expand_ifs)))); |
235 (*Oops*) |
235 (*Oops*) |
236 by (blast_tac (!claset addSDs [unique_session_keys]) 4); |
236 by (blast_tac (!claset addSDs [unique_session_keys]) 4); |
237 (*OR4*) |
237 (*OR4*) |
238 by (Blast_tac 3); |
238 by (Blast_tac 3); |
239 (*OR3*) |
239 (*OR3*) |