176 |
176 |
177 Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy]; |
177 Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy]; |
178 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
178 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
179 |
179 |
180 |
180 |
181 goal thy "!!K. newK evs = invKey K ==> newK evs = K"; |
181 (** Power of the Spy **) |
182 by (rtac (invKey_eq RS iffD1) 1); |
182 |
183 by (Simp_tac 1); |
183 (*The Spy can see more than anybody else, except for their initial state*) |
184 val newK_invKey = result(); |
184 goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs"; |
185 |
185 by (list.induct_tac "evs" 1); |
186 AddSDs [newK_invKey]; |
186 by (event.induct_tac "a" 2); |
|
187 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
|
188 addss (!simpset)))); |
|
189 qed "sees_agent_subset_sees_Spy"; |
|
190 |
|
191 (*The Spy can see more than anybody else who's lost their key!*) |
|
192 goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs"; |
|
193 by (list.induct_tac "evs" 1); |
|
194 by (event.induct_tac "a" 2); |
|
195 by (agent.induct_tac "A" 1); |
|
196 by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset))); |
|
197 qed_spec_mp "sees_lost_agent_subset_sees_Spy"; |
|
198 |
187 |
199 |
188 (** Rewrites to push in Key and Crypt messages, so that other messages can |
200 (** Rewrites to push in Key and Crypt messages, so that other messages can |
189 be pulled out using the analz_insert rules **) |
201 be pulled out using the analz_insert rules **) |
190 |
202 |
191 fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] |
203 fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] |
233 parts_insert |> read_instantiate_sg (sign_of thy) |
245 parts_insert |> read_instantiate_sg (sign_of thy) |
234 [("H", "sees lost A evs")] |
246 [("H", "sees lost A evs")] |
235 |> standard; |
247 |> standard; |
236 |
248 |
237 |
249 |
238 (** Specialized rewriting for **) |
250 (*** Specialized rewriting for analz_insert_Key_newK ***) |
|
251 |
|
252 goal thy "!!K. newK evs = invKey K ==> newK evs = K"; |
|
253 by (rtac (invKey_eq RS iffD1) 1); |
|
254 by (Simp_tac 1); |
|
255 val newK_invKey = result(); |
|
256 |
|
257 AddSDs [newK_invKey]; |
239 |
258 |
240 Delsimps [image_insert]; |
259 Delsimps [image_insert]; |
241 Addsimps [image_insert RS sym]; |
260 Addsimps [image_insert RS sym]; |
242 |
261 |
243 Delsimps [image_Un]; |
262 Delsimps [image_Un]; |