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 lost ==> \ |
135 goal thy "!!evs. evs : otway lost ==> \ |
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 evt) ~: parts (sees lost Spy evs)"; |
164 \ Nonce (newN evt) ~: parts (sees lost Spy evs)"; |
164 by (parts_induct_tac 1); |
165 by (parts_induct_tac 1); |
165 by (REPEAT_FIRST (fast_tac (!claset |
166 by (REPEAT_FIRST (fast_tac (!claset |
166 addSEs partsEs |
167 addSEs partsEs |
167 addSDs [Says_imp_sees_Spy RS parts.Inj] |
168 addSDs [Says_imp_sees_Spy RS parts.Inj] |
168 addDs [impOfSubs analz_subset_parts, |
169 addEs [leD RS notE] |
|
170 addDs [impOfSubs analz_subset_parts, |
169 impOfSubs parts_insert_subset_Un, |
171 impOfSubs parts_insert_subset_Un, |
170 Suc_leD] |
172 Suc_leD] |
171 addss (!simpset)))); |
173 addss (!simpset)))); |
172 qed_spec_mp "new_nonces_not_seen"; |
174 qed_spec_mp "new_nonces_not_seen"; |
173 Addsimps [new_nonces_not_seen]; |
175 Addsimps [new_nonces_not_seen]; |