equal
deleted
inserted
replaced
119 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
119 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
120 ==> X \<in> analz (knows Spy evs)" |
120 ==> X \<in> analz (knows Spy evs)" |
121 by blast |
121 by blast |
122 |
122 |
123 lemmas YM4_parts_knows_Spy = |
123 lemmas YM4_parts_knows_Spy = |
124 YM4_analz_knows_Spy [THEN analz_into_parts, standard] |
124 YM4_analz_knows_Spy [THEN analz_into_parts] |
125 |
125 |
126 text{*For Oops*} |
126 text{*For Oops*} |
127 lemma YM4_Key_parts_knows_Spy: |
127 lemma YM4_Key_parts_knows_Spy: |
128 "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs |
128 "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs |
129 ==> K \<in> parts (knows Spy evs)" |
129 ==> K \<in> parts (knows Spy evs)" |