168 Spy_analz_shrK RSN (2, rev_iffD1)]; |
168 Spy_analz_shrK RSN (2, rev_iffD1)]; |
169 |
169 |
170 |
170 |
171 (** Nobody can have used non-existent keys! **) |
171 (** Nobody can have used non-existent keys! **) |
172 |
172 |
173 goal thy |
173 (*The special case of H={} has the same proof*) |
174 "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \ |
174 goal thy |
175 \ ==> K : range shrK"; |
175 "!!evs. [| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \ |
|
176 \ ==> K : range shrK | K : keysFor (parts H)"; |
176 by (etac rev_mp 1); |
177 by (etac rev_mp 1); |
177 by (etac (respond_imp_responses RS responses.induct) 1); |
178 by (etac (respond_imp_responses RS responses.induct) 1); |
178 by Auto_tac; |
179 by Auto_tac; |
179 qed_spec_mp "Key_in_keysFor_parts"; |
180 qed_spec_mp "Key_in_keysFor_parts"; |
180 |
181 |
181 |
182 |
182 goal thy "!!evs. evs : recur ==> \ |
183 goal thy "!!evs. evs : recur ==> \ |
183 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
184 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
184 by (parts_induct_tac 1); |
185 by (parts_induct_tac 1); |
185 (*RA3*) |
186 (*RA3*) |
186 by (best_tac (claset() addDs [Key_in_keysFor_parts] |
187 by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2); |
187 addss (simpset() addsimps [parts_insert_spies])) 2); |
|
188 (*Fake*) |
188 (*Fake*) |
189 by (best_tac |
189 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
190 (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
|
191 addIs [impOfSubs analz_subset_parts] |
|
192 addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] |
|
193 addss (simpset())) 1); |
|
194 qed_spec_mp "new_keys_not_used"; |
190 qed_spec_mp "new_keys_not_used"; |
195 |
191 |
196 |
192 |
197 bind_thm ("new_keys_not_analzd", |
193 bind_thm ("new_keys_not_analzd", |
198 [analz_subset_parts RS keysFor_mono, |
194 [analz_subset_parts RS keysFor_mono, |