equal
deleted
inserted
replaced
114 "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
114 "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
115 ==> X \<in> analz (knows Spy evs)" |
115 ==> X \<in> analz (knows Spy evs)" |
116 by blast |
116 by blast |
117 |
117 |
118 lemmas YM4_parts_knows_Spy = |
118 lemmas YM4_parts_knows_Spy = |
119 YM4_analz_knows_Spy [THEN analz_into_parts, standard] |
119 YM4_analz_knows_Spy [THEN analz_into_parts] |
120 |
120 |
121 |
121 |
122 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
122 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
123 sends messages containing X! **) |
123 sends messages containing X! **) |
124 |
124 |