equal
deleted
inserted
replaced
81 \<exists>A B na X. |
81 \<exists>A B na X. |
82 Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
82 Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
83 \<in> set evs" |
83 \<in> set evs" |
84 |
84 |
85 |
85 |
86 declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
86 declare Says_imp_analz_Spy [dest] |
87 declare parts.Body [dest] |
87 declare parts.Body [dest] |
88 declare Fake_parts_insert_in_Un [dest] |
88 declare Fake_parts_insert_in_Un [dest] |
89 declare analz_into_parts [dest] |
89 declare analz_into_parts [dest] |
90 |
90 |
91 text{*A "possibility property": there are traces that reach the end*} |
91 text{*A "possibility property": there are traces that reach the end*} |
111 text{*Must be proved separately for each protocol*} |
111 text{*Must be proved separately for each protocol*} |
112 lemma Gets_imp_knows_Spy: |
112 lemma Gets_imp_knows_Spy: |
113 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" |
113 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" |
114 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
114 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
115 |
115 |
116 declare Gets_imp_knows_Spy [THEN analz.Inj, dest] |
116 lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj] |
|
117 declare Gets_imp_analz_Spy [dest] |
117 |
118 |
118 |
119 |
119 text{*Lets us treat YM4 using a similar argument as for the Fake case.*} |
120 text{*Lets us treat YM4 using a similar argument as for the Fake case.*} |
120 lemma YM4_analz_knows_Spy: |
121 lemma YM4_analz_knows_Spy: |
121 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
122 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |