equal
deleted
inserted
replaced
134 (*Nobody can have SEEN keys that will be generated in the future. *) |
134 (*Nobody can have SEEN keys that will be generated in the future. *) |
135 goal thy "!!evs. evs : otway ==> \ |
135 goal thy "!!evs. evs : otway ==> \ |
136 \ length evs <= length evs' --> \ |
136 \ length evs <= length evs' --> \ |
137 \ Key (newK evs') ~: parts (sees lost Spy evs)"; |
137 \ Key (newK evs') ~: parts (sees lost Spy evs)"; |
138 by (parts_induct_tac 1); |
138 by (parts_induct_tac 1); |
139 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
139 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] |
|
140 addDs [impOfSubs analz_subset_parts, |
140 impOfSubs parts_insert_subset_Un, |
141 impOfSubs parts_insert_subset_Un, |
141 Suc_leD] |
142 Suc_leD] |
142 addss (!simpset)))); |
143 addss (!simpset)))); |
143 qed_spec_mp "new_keys_not_seen"; |
144 qed_spec_mp "new_keys_not_seen"; |
144 Addsimps [new_keys_not_seen]; |
145 Addsimps [new_keys_not_seen]; |
163 \ Nonce (newN evs') ~: parts (sees lost Spy evs)"; |
164 \ Nonce (newN evs') ~: parts (sees lost Spy evs)"; |
164 by (parts_induct_tac 1); |
165 by (parts_induct_tac 1); |
165 by (REPEAT_FIRST |
166 by (REPEAT_FIRST |
166 (fast_tac (!claset addSEs partsEs |
167 (fast_tac (!claset addSEs partsEs |
167 addSDs [Says_imp_sees_Spy RS parts.Inj] |
168 addSDs [Says_imp_sees_Spy RS parts.Inj] |
|
169 addEs [leD RS notE] |
168 addDs [impOfSubs analz_subset_parts, |
170 addDs [impOfSubs analz_subset_parts, |
169 impOfSubs parts_insert_subset_Un, Suc_leD] |
171 impOfSubs parts_insert_subset_Un, Suc_leD] |
170 addss (!simpset)))); |
172 addss (!simpset)))); |
171 qed_spec_mp "new_nonces_not_seen"; |
173 qed_spec_mp "new_nonces_not_seen"; |
172 Addsimps [new_nonces_not_seen]; |
174 Addsimps [new_nonces_not_seen]; |