equal
deleted
inserted
replaced
174 Oops as well as main secrecy property.*} |
174 Oops as well as main secrecy property.*} |
175 lemma Says_Server_not_range [simp]: |
175 lemma Says_Server_not_range [simp]: |
176 "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} |
176 "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} |
177 \<in> set evs; evs \<in> yahalom |] |
177 \<in> set evs; evs \<in> yahalom |] |
178 ==> K \<notin> range shrK" |
178 ==> K \<notin> range shrK" |
179 by (erule rev_mp, erule yahalom.induct, simp_all, blast) |
179 by (erule rev_mp, erule yahalom.induct, simp_all) |
180 |
180 |
181 |
181 |
182 subsection{*Secrecy Theorems*} |
182 subsection{*Secrecy Theorems*} |
183 |
183 |
184 (**** |
184 (**** |