equal
deleted
inserted
replaced
85 apply (intro exI bexI) |
85 apply (intro exI bexI) |
86 apply (rule_tac [2] yahalom.Nil |
86 apply (rule_tac [2] yahalom.Nil |
87 [THEN yahalom.YM1, THEN yahalom.Reception, |
87 [THEN yahalom.YM1, THEN yahalom.Reception, |
88 THEN yahalom.YM2, THEN yahalom.Reception, |
88 THEN yahalom.YM2, THEN yahalom.Reception, |
89 THEN yahalom.YM3, THEN yahalom.Reception, |
89 THEN yahalom.YM3, THEN yahalom.Reception, |
90 THEN yahalom.YM4]) |
90 THEN yahalom.YM4], possibility) |
91 apply possibility |
|
92 done |
91 done |
93 |
92 |
94 lemma Gets_imp_Says: |
93 lemma Gets_imp_Says: |
95 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
94 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
96 by (erule rev_mp, erule yahalom.induct, auto) |
95 by (erule rev_mp, erule yahalom.induct, auto) |
122 |
121 |
123 (*Spy never sees a good agent's shared key!*) |
122 (*Spy never sees a good agent's shared key!*) |
124 lemma Spy_see_shrK [simp]: |
123 lemma Spy_see_shrK [simp]: |
125 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
124 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
126 apply (erule yahalom.induct, force, |
125 apply (erule yahalom.induct, force, |
127 drule_tac [6] YM4_parts_knows_Spy, simp_all) |
126 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) |
128 apply blast+ |
|
129 done |
127 done |
130 |
128 |
131 lemma Spy_analz_shrK [simp]: |
129 lemma Spy_analz_shrK [simp]: |
132 "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
130 "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
133 by auto |
131 by auto |
170 "evs \<in> yahalom ==> |
168 "evs \<in> yahalom ==> |
171 \<forall>K KK. KK <= - (range shrK) --> |
169 \<forall>K KK. KK <= - (range shrK) --> |
172 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
170 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
173 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
171 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
174 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, |
172 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, |
175 drule_tac [6] YM4_analz_knows_Spy) |
173 drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz) |
176 apply analz_freshK |
|
177 apply spy_analz |
|
178 done |
174 done |
179 |
175 |
180 lemma analz_insert_freshK: |
176 lemma analz_insert_freshK: |
181 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
177 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
182 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
178 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
210 \<in> set evs --> |
206 \<in> set evs --> |
211 Notes Spy {|na, nb, Key K|} \<notin> set evs --> |
207 Notes Spy {|na, nb, Key K|} \<notin> set evs --> |
212 Key K \<notin> analz (knows Spy evs)" |
208 Key K \<notin> analz (knows Spy evs)" |
213 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, |
209 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, |
214 drule_tac [6] YM4_analz_knows_Spy) |
210 drule_tac [6] YM4_analz_knows_Spy) |
215 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) |
211 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*) |
216 apply spy_analz (*Fake*) |
|
217 apply (blast dest: unique_session_keys)+ (*YM3, Oops*) |
212 apply (blast dest: unique_session_keys)+ (*YM3, Oops*) |
218 done |
213 done |
219 |
214 |
220 |
215 |
221 (*Final version*) |
216 (*Final version*) |