75 qed "Spy_sees_lost"; |
75 qed "Spy_sees_lost"; |
76 |
76 |
77 AddIffs [sees_pubK]; |
77 AddIffs [sees_pubK]; |
78 AddSIs [sees_own_priK, Spy_sees_lost]; |
78 AddSIs [sees_own_priK, Spy_sees_lost]; |
79 |
79 |
80 (*Added for Yahalom/lost_tac*) |
|
81 goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \ |
|
82 \ ==> X : analz (sees lost Spy evs)"; |
|
83 by (blast_tac (!claset addSDs [analz.Decrypt]) 1); |
|
84 qed "Crypt_Spy_analz_lost"; |
|
85 |
80 |
86 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) |
81 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) |
87 |
82 |
88 goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)"; |
83 goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)"; |
89 by (Simp_tac 1); |
84 by (Simp_tac 1); |
131 |
126 |
132 (*Use with addSEs to derive contradictions from old Says events containing |
127 (*Use with addSEs to derive contradictions from old Says events containing |
133 items known to be fresh*) |
128 items known to be fresh*) |
134 val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs; |
129 val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs; |
135 |
130 |
136 goal thy |
131 (*For not_lost_tac*) |
137 "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; C : lost |] \ |
132 goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \ |
138 \ ==> X : analz (sees lost Spy evs)"; |
133 \ ==> X : analz (sees lost Spy evs)"; |
139 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
134 by (blast_tac (!claset addSDs [analz.Decrypt]) 1); |
140 qed "Says_Crypt_lost"; |
135 qed "Crypt_Spy_analz_lost"; |
141 |
136 |
142 goal thy |
137 (*Prove that the agent is uncompromised by the confidentiality of |
143 "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; \ |
138 a component of a message she's said.*) |
144 \ X ~: analz (sees lost Spy evs) |] \ |
139 fun not_lost_tac s = |
145 \ ==> C ~: lost"; |
140 case_tac ("(" ^ s ^ ") : lost") THEN' |
146 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
141 SELECT_GOAL |
147 qed "Says_Crypt_not_lost"; |
142 (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN |
|
143 REPEAT_DETERM (etac MPair_analz 1) THEN |
|
144 THEN_BEST_FIRST |
|
145 (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1) |
|
146 (has_fewer_prems 1, size_of_thm) |
|
147 (Step_tac 1)); |
148 |
148 |
149 Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; |
149 Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; |
150 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
150 Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
151 |
151 |
152 |
152 |