equal
deleted
inserted
replaced
118 qed "Spy_sees_lost"; |
118 qed "Spy_sees_lost"; |
119 |
119 |
120 AddSIs [sees_own_shrK, Spy_sees_lost]; |
120 AddSIs [sees_own_shrK, Spy_sees_lost]; |
121 |
121 |
122 (*Added for Yahalom/lost_tac*) |
122 (*Added for Yahalom/lost_tac*) |
123 goal thy "!!A. [| Crypt X (shrK A) : analz (sees lost Spy evs); A: lost |] \ |
123 goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs); A: lost |] \ |
124 \ ==> X : analz (sees lost Spy evs)"; |
124 \ ==> X : analz (sees lost Spy evs)"; |
125 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); |
125 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); |
126 qed "Crypt_Spy_analz_lost"; |
126 qed "Crypt_Spy_analz_lost"; |
127 |
127 |
128 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) |
128 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) |
170 by (list.induct_tac "evs" 1); |
170 by (list.induct_tac "evs" 1); |
171 by (Auto_tac ()); |
171 by (Auto_tac ()); |
172 qed_spec_mp "Says_imp_sees_Spy"; |
172 qed_spec_mp "Says_imp_sees_Spy"; |
173 |
173 |
174 goal thy |
174 goal thy |
175 "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs; C : lost |] \ |
175 "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost |] \ |
176 \ ==> X : analz (sees lost Spy evs)"; |
176 \ ==> X : analz (sees lost Spy evs)"; |
177 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] |
177 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] |
178 addss (!simpset)) 1); |
178 addss (!simpset)) 1); |
179 qed "Says_Crypt_lost"; |
179 qed "Says_Crypt_lost"; |
180 |
180 |
181 goal thy |
181 goal thy |
182 "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs; \ |
182 "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; \ |
183 \ X ~: analz (sees lost Spy evs) |] \ |
183 \ X ~: analz (sees lost Spy evs) |] \ |
184 \ ==> C ~: lost"; |
184 \ ==> C ~: lost"; |
185 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] |
185 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] |
186 addss (!simpset)) 1); |
186 addss (!simpset)) 1); |
187 qed "Says_Crypt_not_lost"; |
187 qed "Says_Crypt_not_lost"; |