equal
deleted
inserted
replaced
89 |
89 |
90 (*** Shared keys are not betrayed ***) |
90 (*** Shared keys are not betrayed ***) |
91 |
91 |
92 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*) |
92 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*) |
93 goal thy |
93 goal thy |
94 "!!evs. [| evs : otway; A ~: bad |] ==> \ |
94 "!!evs. [| evs : otway; A ~: bad |] \ |
95 \ Key (shrK A) ~: parts (sees Enemy evs)"; |
95 \ ==> Key (shrK A) ~: parts (sees Enemy evs)"; |
96 be otway.induct 1; |
96 be otway.induct 1; |
97 by OR2_OR4_tac; |
97 by OR2_OR4_tac; |
98 by (Auto_tac()); |
98 by (Auto_tac()); |
99 (*Deals with Fake message*) |
99 (*Deals with Fake message*) |
100 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
100 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
146 addss (!simpset)))); |
146 addss (!simpset)))); |
147 val lemma = result(); |
147 val lemma = result(); |
148 |
148 |
149 (*Variant needed for the main theorem below*) |
149 (*Variant needed for the main theorem below*) |
150 goal thy |
150 goal thy |
151 "!!evs. [| evs : otway; length evs <= length evs' |] ==> \ |
151 "!!evs. [| evs : otway; length evs <= length evs' |] \ |
152 \ Key (newK evs') ~: parts (sees C evs)"; |
152 \ ==> Key (newK evs') ~: parts (sees C evs)"; |
153 by (fast_tac (!claset addDs [lemma]) 1); |
153 by (fast_tac (!claset addDs [lemma]) 1); |
154 qed "new_keys_not_seen"; |
154 qed "new_keys_not_seen"; |
155 Addsimps [new_keys_not_seen]; |
155 Addsimps [new_keys_not_seen]; |
156 |
156 |
157 (*Another variant: old messages must contain old keys!*) |
157 (*Another variant: old messages must contain old keys!*) |
192 addIs [less_SucI, impOfSubs keysFor_mono] |
192 addIs [less_SucI, impOfSubs keysFor_mono] |
193 addss (!simpset addsimps [le_def])) 1); |
193 addss (!simpset addsimps [le_def])) 1); |
194 val lemma = result(); |
194 val lemma = result(); |
195 |
195 |
196 goal thy |
196 goal thy |
197 "!!evs. [| evs : otway; length evs <= length evs' |] ==> \ |
197 "!!evs. [| evs : otway; length evs <= length evs' |] \ |
198 \ newK evs' ~: keysFor (parts (sees C evs))"; |
198 \ ==> newK evs' ~: keysFor (parts (sees C evs))"; |
199 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
199 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
200 qed "new_keys_not_used"; |
200 qed "new_keys_not_used"; |
201 |
201 |
202 bind_thm ("new_keys_not_analzd", |
202 bind_thm ("new_keys_not_analzd", |
203 [analz_subset_parts RS keysFor_mono, |
203 [analz_subset_parts RS keysFor_mono, |