20 Nil: "[] \<in> yahalom" |
20 Nil: "[] \<in> yahalom" |
21 |
21 |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
23 invent new nonces here, but he can also use NS1. Common to |
23 invent new nonces here, but he can also use NS1. Common to |
24 all similar protocols.*) |
24 all similar protocols.*) |
25 | Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] |
25 | Fake: "\<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf))\<rbrakk> |
26 ==> Says Spy B X # evsf \<in> yahalom" |
26 \<Longrightarrow> Says Spy B X # evsf \<in> yahalom" |
27 |
27 |
28 (*A message that has been sent can be received by the |
28 (*A message that has been sent can be received by the |
29 intended recipient.*) |
29 intended recipient.*) |
30 | Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] |
30 | Reception: "\<lbrakk>evsr \<in> yahalom; Says A B X \<in> set evsr\<rbrakk> |
31 ==> Gets B X # evsr \<in> yahalom" |
31 \<Longrightarrow> Gets B X # evsr \<in> yahalom" |
32 |
32 |
33 (*Alice initiates a protocol run*) |
33 (*Alice initiates a protocol run*) |
34 | YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] |
34 | YM1: "\<lbrakk>evs1 \<in> yahalom; Nonce NA \<notin> used evs1\<rbrakk> |
35 ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" |
35 \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" |
36 |
36 |
37 (*Bob's response to Alice's message.*) |
37 (*Bob's response to Alice's message.*) |
38 | YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
38 | YM2: "\<lbrakk>evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
39 Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |] |
39 Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> |
40 ==> Says B Server |
40 \<Longrightarrow> Says B Server |
41 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
41 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
42 # evs2 \<in> yahalom" |
42 # evs2 \<in> yahalom" |
43 |
43 |
44 (*The Server receives Bob's message. He responds by sending a |
44 (*The Server receives Bob's message. He responds by sending a |
45 new session key to Alice, with a packet for forwarding to Bob.*) |
45 new session key to Alice, with a packet for forwarding to Bob.*) |
46 | YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; |
46 | YM3: "\<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; |
47 Gets Server |
47 Gets Server |
48 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
48 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
49 \<in> set evs3 |] |
49 \<in> set evs3\<rbrakk> |
50 ==> Says Server A |
50 \<Longrightarrow> Says Server A |
51 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>, |
51 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>, |
52 Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace> |
52 Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace> |
53 # evs3 \<in> yahalom" |
53 # evs3 \<in> yahalom" |
54 |
54 |
55 | YM4: |
55 | YM4: |
56 \<comment>\<open>Alice receives the Server's (?) message, checks her Nonce, and |
56 \<comment>\<open>Alice receives the Server's (?) message, checks her Nonce, and |
57 uses the new session key to send Bob his Nonce. The premise |
57 uses the new session key to send Bob his Nonce. The premise |
58 @{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>. |
58 @{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>. |
59 Alice can check that K is symmetric by its length.\<close> |
59 Alice can check that K is symmetric by its length.\<close> |
60 "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; |
60 "\<lbrakk>evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; |
61 Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace> |
61 Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace> |
62 \<in> set evs4; |
62 \<in> set evs4; |
63 Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |] |
63 Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> |
64 ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" |
64 \<Longrightarrow> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" |
65 |
65 |
66 (*This message models possible leaks of session keys. The Nonces |
66 (*This message models possible leaks of session keys. The Nonces |
67 identify the protocol run. Quoting Server here ensures they are |
67 identify the protocol run. Quoting Server here ensures they are |
68 correct.*) |
68 correct.*) |
69 | Oops: "[| evso \<in> yahalom; |
69 | Oops: "\<lbrakk>evso \<in> yahalom; |
70 Says Server A \<lbrace>Crypt (shrK A) |
70 Says Server A \<lbrace>Crypt (shrK A) |
71 \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, |
71 \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, |
72 X\<rbrace> \<in> set evso |] |
72 X\<rbrace> \<in> set evso\<rbrakk> |
73 ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom" |
73 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom" |
74 |
74 |
75 |
75 |
76 definition KeyWithNonce :: "[key, nat, event list] => bool" where |
76 definition KeyWithNonce :: "[key, nat, event list] => bool" where |
77 "KeyWithNonce K NB evs == |
77 "KeyWithNonce K NB evs == |
78 \<exists>A B na X. |
78 \<exists>A B na X. |
100 |
100 |
101 |
101 |
102 subsection\<open>Regularity Lemmas for Yahalom\<close> |
102 subsection\<open>Regularity Lemmas for Yahalom\<close> |
103 |
103 |
104 lemma Gets_imp_Says: |
104 lemma Gets_imp_Says: |
105 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
105 "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" |
106 by (erule rev_mp, erule yahalom.induct, auto) |
106 by (erule rev_mp, erule yahalom.induct, auto) |
107 |
107 |
108 text\<open>Must be proved separately for each protocol\<close> |
108 text\<open>Must be proved separately for each protocol\<close> |
109 lemma Gets_imp_knows_Spy: |
109 lemma Gets_imp_knows_Spy: |
110 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" |
110 "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" |
111 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
111 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
112 |
112 |
113 lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj] |
113 lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj] |
114 declare Gets_imp_analz_Spy [dest] |
114 declare Gets_imp_analz_Spy [dest] |
115 |
115 |
116 |
116 |
117 text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close> |
117 text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close> |
118 lemma YM4_analz_knows_Spy: |
118 lemma YM4_analz_knows_Spy: |
119 "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom |] |
119 "\<lbrakk>Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom\<rbrakk> |
120 ==> X \<in> analz (knows Spy evs)" |
120 \<Longrightarrow> 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] |
124 YM4_analz_knows_Spy [THEN analz_into_parts] |
125 |
125 |
126 text\<open>For Oops\<close> |
126 text\<open>For Oops\<close> |
127 lemma YM4_Key_parts_knows_Spy: |
127 lemma YM4_Key_parts_knows_Spy: |
128 "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs |
128 "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs |
129 ==> K \<in> parts (knows Spy evs)" |
129 \<Longrightarrow> K \<in> parts (knows Spy evs)" |
130 by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) |
130 by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) |
131 |
131 |
132 text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply |
132 text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply |
133 that NOBODY sends messages containing X!\<close> |
133 that NOBODY sends messages containing X!\<close> |
134 |
134 |
135 text\<open>Spy never sees a good agent's shared key!\<close> |
135 text\<open>Spy never sees a good agent's shared key!\<close> |
136 lemma Spy_see_shrK [simp]: |
136 lemma Spy_see_shrK [simp]: |
137 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
137 "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
138 by (erule yahalom.induct, force, |
138 by (erule yahalom.induct, force, |
139 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) |
139 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) |
140 |
140 |
141 lemma Spy_analz_shrK [simp]: |
141 lemma Spy_analz_shrK [simp]: |
142 "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
142 "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
143 by auto |
143 by auto |
144 |
144 |
145 lemma Spy_see_shrK_D [dest!]: |
145 lemma Spy_see_shrK_D [dest!]: |
146 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
146 "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom\<rbrakk> \<Longrightarrow> A \<in> bad" |
147 by (blast dest: Spy_see_shrK) |
147 by (blast dest: Spy_see_shrK) |
148 |
148 |
149 text\<open>Nobody can have used non-existent keys! |
149 text\<open>Nobody can have used non-existent keys! |
150 Needed to apply \<open>analz_insert_Key\<close>\<close> |
150 Needed to apply \<open>analz_insert_Key\<close>\<close> |
151 lemma new_keys_not_used [simp]: |
151 lemma new_keys_not_used [simp]: |
152 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|] |
152 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk> |
153 ==> K \<notin> keysFor (parts (spies evs))" |
153 \<Longrightarrow> K \<notin> keysFor (parts (spies evs))" |
154 apply (erule rev_mp) |
154 apply (erule rev_mp) |
155 apply (erule yahalom.induct, force, |
155 apply (erule yahalom.induct, force, |
156 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
156 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
157 txt\<open>Fake\<close> |
157 txt\<open>Fake\<close> |
158 apply (force dest!: keysFor_parts_insert, auto) |
158 apply (force dest!: keysFor_parts_insert, auto) |
160 |
160 |
161 |
161 |
162 text\<open>Earlier, all protocol proofs declared this theorem. |
162 text\<open>Earlier, all protocol proofs declared this theorem. |
163 But only a few proofs need it, e.g. Yahalom and Kerberos IV.\<close> |
163 But only a few proofs need it, e.g. Yahalom and Kerberos IV.\<close> |
164 lemma new_keys_not_analzd: |
164 lemma new_keys_not_analzd: |
165 "[|K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs|] |
165 "\<lbrakk>K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs\<rbrakk> |
166 ==> K \<notin> keysFor (analz (knows Spy evs))" |
166 \<Longrightarrow> K \<notin> keysFor (analz (knows Spy evs))" |
167 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) |
167 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) |
168 |
168 |
169 |
169 |
170 text\<open>Describes the form of K when the Server sends this message. Useful for |
170 text\<open>Describes the form of K when the Server sends this message. Useful for |
171 Oops as well as main secrecy property.\<close> |
171 Oops as well as main secrecy property.\<close> |
172 lemma Says_Server_not_range [simp]: |
172 lemma Says_Server_not_range [simp]: |
173 "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> |
173 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> |
174 \<in> set evs; evs \<in> yahalom |] |
174 \<in> set evs; evs \<in> yahalom\<rbrakk> |
175 ==> K \<notin> range shrK" |
175 \<Longrightarrow> K \<notin> range shrK" |
176 by (erule rev_mp, erule yahalom.induct, simp_all) |
176 by (erule rev_mp, erule yahalom.induct, simp_all) |
177 |
177 |
178 |
178 |
179 subsection\<open>Secrecy Theorems\<close> |
179 subsection\<open>Secrecy Theorems\<close> |
180 |
180 |
181 (**** |
181 (**** |
182 The following is to prove theorems of the form |
182 The following is to prove theorems of the form |
183 |
183 |
184 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
184 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> |
185 Key K \<in> analz (knows Spy evs) |
185 Key K \<in> analz (knows Spy evs) |
186 |
186 |
187 A more general formula must be proved inductively. |
187 A more general formula must be proved inductively. |
188 ****) |
188 ****) |
189 |
189 |
190 text\<open>Session keys are not used to encrypt other session keys\<close> |
190 text\<open>Session keys are not used to encrypt other session keys\<close> |
191 |
191 |
192 lemma analz_image_freshK [rule_format]: |
192 lemma analz_image_freshK [rule_format]: |
193 "evs \<in> yahalom ==> |
193 "evs \<in> yahalom \<Longrightarrow> |
194 \<forall>K KK. KK <= - (range shrK) --> |
194 \<forall>K KK. KK <= - (range shrK) --> |
195 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
195 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
196 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
196 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
197 apply (erule yahalom.induct, |
197 apply (erule yahalom.induct, |
198 drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) |
198 drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) |
199 apply (simp only: Says_Server_not_range analz_image_freshK_simps) |
199 apply (simp only: Says_Server_not_range analz_image_freshK_simps) |
200 apply safe |
200 apply safe |
201 done |
201 done |
202 |
202 |
203 lemma analz_insert_freshK: |
203 lemma analz_insert_freshK: |
204 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
204 "\<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> |
205 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
205 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
206 (K = KAB | Key K \<in> analz (knows Spy evs))" |
206 (K = KAB | Key K \<in> analz (knows Spy evs))" |
207 by (simp only: analz_image_freshK analz_image_freshK_simps) |
207 by (simp only: analz_image_freshK analz_image_freshK_simps) |
208 |
208 |
209 |
209 |
210 text\<open>The Key K uniquely identifies the Server's message.\<close> |
210 text\<open>The Key K uniquely identifies the Server's message.\<close> |
211 lemma unique_session_keys: |
211 lemma unique_session_keys: |
212 "[| Says Server A |
212 "\<lbrakk>Says Server A |
213 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs; |
213 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs; |
214 Says Server A' |
214 Says Server A' |
215 \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs; |
215 \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs; |
216 evs \<in> yahalom |] |
216 evs \<in> yahalom\<rbrakk> |
217 ==> A=A' & B=B' & na=na' & nb=nb'" |
217 \<Longrightarrow> A=A' & B=B' & na=na' & nb=nb'" |
218 apply (erule rev_mp, erule rev_mp) |
218 apply (erule rev_mp, erule rev_mp) |
219 apply (erule yahalom.induct, simp_all) |
219 apply (erule yahalom.induct, simp_all) |
220 txt\<open>YM3, by freshness, and YM4\<close> |
220 txt\<open>YM3, by freshness, and YM4\<close> |
221 apply blast+ |
221 apply blast+ |
222 done |
222 done |
223 |
223 |
224 |
224 |
225 text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close> |
225 text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close> |
226 lemma secrecy_lemma: |
226 lemma secrecy_lemma: |
227 "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
227 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
228 ==> Says Server A |
228 \<Longrightarrow> Says Server A |
229 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, |
229 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, |
230 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
230 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
231 \<in> set evs --> |
231 \<in> set evs --> |
232 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs --> |
232 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs --> |
233 Key K \<notin> analz (knows Spy evs)" |
233 Key K \<notin> analz (knows Spy evs)" |
234 apply (erule yahalom.induct, force, |
234 apply (erule yahalom.induct, force, |
235 drule_tac [6] YM4_analz_knows_Spy) |
235 drule_tac [6] YM4_analz_knows_Spy) |
236 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) \<comment>\<open>Fake\<close> |
236 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) |
237 apply (blast dest: unique_session_keys)+ \<comment>\<open>YM3, Oops\<close> |
237 subgoal --\<open>Fake\<close> by spy_analz |
|
238 subgoal --\<open>YM3\<close> by blast |
|
239 subgoal --\<open>Oops\<close> by (blast dest: unique_session_keys) |
238 done |
240 done |
239 |
241 |
240 text\<open>Final version\<close> |
242 text\<open>Final version\<close> |
241 lemma Spy_not_see_encrypted_key: |
243 lemma Spy_not_see_encrypted_key: |
242 "[| Says Server A |
244 "\<lbrakk>Says Server A |
243 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, |
245 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, |
244 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
246 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
245 \<in> set evs; |
247 \<in> set evs; |
246 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; |
248 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; |
247 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
249 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
248 ==> Key K \<notin> analz (knows Spy evs)" |
250 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
249 by (blast dest: secrecy_lemma) |
251 by (blast dest: secrecy_lemma) |
250 |
252 |
251 |
253 |
252 subsubsection\<open>Security Guarantee for A upon receiving YM3\<close> |
254 subsubsection\<open>Security Guarantee for A upon receiving YM3\<close> |
253 |
255 |
254 text\<open>If the encrypted message appears then it originated with the Server\<close> |
256 text\<open>If the encrypted message appears then it originated with the Server\<close> |
255 lemma A_trusts_YM3: |
257 lemma A_trusts_YM3: |
256 "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); |
258 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); |
257 A \<notin> bad; evs \<in> yahalom |] |
259 A \<notin> bad; evs \<in> yahalom\<rbrakk> |
258 ==> Says Server A |
260 \<Longrightarrow> Says Server A |
259 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, |
261 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, |
260 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
262 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
261 \<in> set evs" |
263 \<in> set evs" |
262 apply (erule rev_mp) |
264 apply (erule rev_mp) |
263 apply (erule yahalom.induct, force, |
265 apply (erule yahalom.induct, force, |
267 done |
269 done |
268 |
270 |
269 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with |
271 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with |
270 \<open>Spy_not_see_encrypted_key\<close>\<close> |
272 \<open>Spy_not_see_encrypted_key\<close>\<close> |
271 lemma A_gets_good_key: |
273 lemma A_gets_good_key: |
272 "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); |
274 "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); |
273 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; |
275 Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; |
274 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
276 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
275 ==> Key K \<notin> analz (knows Spy evs)" |
277 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
276 by (metis A_trusts_YM3 secrecy_lemma) |
278 by (metis A_trusts_YM3 secrecy_lemma) |
277 |
279 |
278 |
280 |
279 subsubsection\<open>Security Guarantees for B upon receiving YM4\<close> |
281 subsubsection\<open>Security Guarantees for B upon receiving YM4\<close> |
280 |
282 |
281 text\<open>B knows, by the first part of A's message, that the Server distributed |
283 text\<open>B knows, by the first part of A's message, that the Server distributed |
282 the key for A and B. But this part says nothing about nonces.\<close> |
284 the key for A and B. But this part says nothing about nonces.\<close> |
283 lemma B_trusts_YM4_shrK: |
285 lemma B_trusts_YM4_shrK: |
284 "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); |
286 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); |
285 B \<notin> bad; evs \<in> yahalom |] |
287 B \<notin> bad; evs \<in> yahalom\<rbrakk> |
286 ==> \<exists>NA NB. Says Server A |
288 \<Longrightarrow> \<exists>NA NB. Says Server A |
287 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, |
289 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, |
288 Nonce NA, Nonce NB\<rbrace>, |
290 Nonce NA, Nonce NB\<rbrace>, |
289 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
291 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
290 \<in> set evs" |
292 \<in> set evs" |
291 apply (erule rev_mp) |
293 apply (erule rev_mp) |
300 agent names. Secrecy of NB is crucial. Note that @{term "Nonce NB |
302 agent names. Secrecy of NB is crucial. Note that @{term "Nonce NB |
301 \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the |
303 \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the |
302 induction formula.\<close> |
304 induction formula.\<close> |
303 |
305 |
304 lemma B_trusts_YM4_newK [rule_format]: |
306 lemma B_trusts_YM4_newK [rule_format]: |
305 "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs); |
307 "\<lbrakk>Crypt K (Nonce NB) \<in> parts (knows Spy evs); |
306 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
308 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> |
307 ==> \<exists>A B NA. Says Server A |
309 \<Longrightarrow> \<exists>A B NA. Says Server A |
308 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, |
310 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, |
309 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
311 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
310 \<in> set evs" |
312 \<in> set evs" |
311 apply (erule rev_mp, erule rev_mp) |
313 apply (erule rev_mp, erule rev_mp) |
312 apply (erule yahalom.induct, force, |
314 apply (erule yahalom.induct, force, |
313 frule_tac [6] YM4_parts_knows_Spy) |
315 frule_tac [6] YM4_parts_knows_Spy) |
314 apply (analz_mono_contra, simp_all) |
316 apply (analz_mono_contra, simp_all) |
315 txt\<open>Fake, YM3\<close> |
317 subgoal --\<open>Fake\<close> by blast |
316 apply blast |
318 subgoal --\<open>YM3\<close> by blast |
317 apply blast |
|
318 txt\<open>YM4. A is uncompromised because NB is secure |
319 txt\<open>YM4. A is uncompromised because NB is secure |
319 A's certificate guarantees the existence of the Server message\<close> |
320 A's certificate guarantees the existence of the Server message\<close> |
320 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
321 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
321 dest: Says_imp_spies |
322 dest: Says_imp_spies |
322 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
323 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
394 Says_Server_KeyWithNonce) |
395 Says_Server_KeyWithNonce) |
395 txt\<open>For Oops, simplification proves @{prop "NBa\<noteq>NB"}. By |
396 txt\<open>For Oops, simplification proves @{prop "NBa\<noteq>NB"}. By |
396 @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB |
397 @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB |
397 evs"}; then simplification can apply the induction hypothesis with |
398 evs"}; then simplification can apply the induction hypothesis with |
398 @{term "KK = {K}"}.\<close> |
399 @{term "KK = {K}"}.\<close> |
399 txt\<open>Fake\<close> |
400 subgoal --\<open>Fake\<close> by spy_analz |
400 apply spy_analz |
401 subgoal --\<open>YM2\<close> by blast |
401 txt\<open>YM2\<close> |
402 subgoal --\<open>YM3\<close> by blast |
402 apply blast |
403 subgoal --\<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close> |
403 txt\<open>YM3\<close> |
404 by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def |
404 apply blast |
405 Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) |
405 txt\<open>YM4\<close> |
|
406 apply (erule_tac V = "\<forall>KK. P KK" for P in thin_rl, clarify) |
|
407 txt\<open>If @{prop "A \<in> bad"} then @{term NBa} is known, therefore |
|
408 @{prop "NBa \<noteq> NB"}. Previous two steps make the next step |
|
409 faster.\<close> |
|
410 apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def |
|
411 Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) |
|
412 done |
406 done |
413 |
407 |
414 |
408 |
415 text\<open>Version required below: if NB can be decrypted using a session key then |
409 text\<open>Version required below: if NB can be decrypted using a session key then |
416 it was distributed with that key. The more general form above is required |
410 it was distributed with that key. The more general form above is required |
417 for the induction to carry through.\<close> |
411 for the induction to carry through.\<close> |
418 lemma single_Nonce_secrecy: |
412 lemma single_Nonce_secrecy: |
419 "[| Says Server A |
413 "\<lbrakk>Says Server A |
420 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace> |
414 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace> |
421 \<in> set evs; |
415 \<in> set evs; |
422 NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |] |
416 NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom\<rbrakk> |
423 ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = |
417 \<Longrightarrow> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = |
424 (Nonce NB \<in> analz (knows Spy evs))" |
418 (Nonce NB \<in> analz (knows Spy evs))" |
425 by (simp_all del: image_insert image_Un imp_disjL |
419 by (simp_all del: image_insert image_Un imp_disjL |
426 add: analz_image_freshK_simps split_ifs |
420 add: analz_image_freshK_simps split_ifs |
427 Nonce_secrecy Says_Server_KeyWithNonce) |
421 Nonce_secrecy Says_Server_KeyWithNonce) |
428 |
422 |
429 |
423 |
430 subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close> |
424 subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close> |
431 |
425 |
432 lemma unique_NB: |
426 lemma unique_NB: |
433 "[| Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); |
427 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); |
434 Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs); |
428 Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs); |
435 evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |] |
429 evs \<in> yahalom; B \<notin> bad; B' \<notin> bad\<rbrakk> |
436 ==> NA' = NA & A' = A & B' = B" |
430 \<Longrightarrow> NA' = NA & A' = A & B' = B" |
437 apply (erule rev_mp, erule rev_mp) |
431 apply (erule rev_mp, erule rev_mp) |
438 apply (erule yahalom.induct, force, |
432 apply (erule yahalom.induct, force, |
439 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
433 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
440 txt\<open>Fake, and YM2 by freshness\<close> |
434 txt\<open>Fake, and YM2 by freshness\<close> |
441 apply blast+ |
435 apply blast+ |
443 |
437 |
444 |
438 |
445 text\<open>Variant useful for proving secrecy of NB. Because nb is assumed to be |
439 text\<open>Variant useful for proving secrecy of NB. Because nb is assumed to be |
446 secret, we no longer must assume B, B' not bad.\<close> |
440 secret, we no longer must assume B, B' not bad.\<close> |
447 lemma Says_unique_NB: |
441 lemma Says_unique_NB: |
448 "[| Says C S \<lbrace>X, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
442 "\<lbrakk>Says C S \<lbrace>X, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
449 \<in> set evs; |
443 \<in> set evs; |
450 Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace> |
444 Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace> |
451 \<in> set evs; |
445 \<in> set evs; |
452 nb \<notin> analz (knows Spy evs); evs \<in> yahalom |] |
446 nb \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> |
453 ==> NA' = NA & A' = A & B' = B" |
447 \<Longrightarrow> NA' = NA & A' = A & B' = B" |
454 by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
448 by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
455 dest: Says_imp_spies unique_NB parts.Inj analz.Inj) |
449 dest: Says_imp_spies unique_NB parts.Inj analz.Inj) |
456 |
450 |
457 |
451 |
458 subsubsection\<open>A nonce value is never used both as NA and as NB\<close> |
452 subsubsection\<open>A nonce value is never used both as NA and as NB\<close> |
459 |
453 |
460 lemma no_nonce_YM1_YM2: |
454 lemma no_nonce_YM1_YM2: |
461 "[|Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs); |
455 "\<lbrakk>Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs); |
462 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
456 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> |
463 ==> Crypt (shrK B) \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)" |
457 \<Longrightarrow> Crypt (shrK B) \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)" |
464 apply (erule rev_mp, erule rev_mp) |
458 apply (erule rev_mp, erule rev_mp) |
465 apply (erule yahalom.induct, force, |
459 apply (erule yahalom.induct, force, |
466 frule_tac [6] YM4_parts_knows_Spy) |
460 frule_tac [6] YM4_parts_knows_Spy) |
467 apply (analz_mono_contra, simp_all) |
461 apply (analz_mono_contra, simp_all) |
468 txt\<open>Fake, YM2\<close> |
462 txt\<open>Fake, YM2\<close> |
469 apply blast+ |
463 apply blast+ |
470 done |
464 done |
471 |
465 |
472 text\<open>The Server sends YM3 only in response to YM2.\<close> |
466 text\<open>The Server sends YM3 only in response to YM2.\<close> |
473 lemma Says_Server_imp_YM2: |
467 lemma Says_Server_imp_YM2: |
474 "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs; |
468 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs; |
475 evs \<in> yahalom |] |
469 evs \<in> yahalom\<rbrakk> |
476 ==> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace> |
470 \<Longrightarrow> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace> |
477 \<in> set evs" |
471 \<in> set evs" |
478 by (erule rev_mp, erule yahalom.induct, auto) |
472 by (erule rev_mp, erule yahalom.induct, auto) |
479 |
473 |
480 text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close> |
474 text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close> |
481 lemma Spy_not_see_NB : |
475 theorem Spy_not_see_NB : |
482 "[| Says B Server |
476 "\<lbrakk>Says B Server |
483 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
477 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
484 \<in> set evs; |
478 \<in> set evs; |
485 (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); |
479 (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); |
486 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
480 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
487 ==> Nonce NB \<notin> analz (knows Spy evs)" |
481 \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)" |
488 apply (erule rev_mp, erule rev_mp) |
482 apply (erule rev_mp, erule rev_mp) |
489 apply (erule yahalom.induct, force, |
483 apply (erule yahalom.induct, force, |
490 frule_tac [6] YM4_analz_knows_Spy) |
484 frule_tac [6] YM4_analz_knows_Spy) |
491 apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq |
485 apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq |
492 analz_insert_freshK) |
486 analz_insert_freshK) |
493 txt\<open>Fake\<close> |
487 subgoal --\<open>Fake\<close> by spy_analz |
494 apply spy_analz |
488 subgoal --\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast |
495 txt\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> |
489 subgoal --\<open>YM2\<close> by blast |
496 apply blast |
490 subgoal --\<open>YM3: because no NB can also be an NA\<close> |
497 txt\<open>YM2\<close> |
491 by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) |
498 apply blast |
492 subgoal --\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close> |
499 txt\<open>Prove YM3 by showing that no NB can also be an NA\<close> |
493 --\<open>Case analysis on whether Aa is bad; |
500 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) |
494 use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close> |
501 txt\<open>LEVEL 7: YM4 and Oops remain\<close> |
495 apply clarify |
502 apply (clarify, simp add: all_conj_distrib) |
496 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt |
503 txt\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close> |
497 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] |
504 txt\<open>Case analysis on Aa:bad; PROOF FAILED problems |
498 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 |
505 use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close> |
499 Spy_not_see_encrypted_key) |
506 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt |
500 done |
507 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] |
501 subgoal --\<open>Oops case: if the nonce is betrayed now, show that the Oops event is |
508 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 |
502 covered by the quantified Oops assumption.\<close> |
509 Spy_not_see_encrypted_key) |
503 apply clarsimp |
510 txt\<open>Oops case: if the nonce is betrayed now, show that the Oops event is |
504 apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) |
511 covered by the quantified Oops assumption.\<close> |
505 done |
512 apply (clarify, simp add: all_conj_distrib) |
506 done |
513 apply (frule Says_Server_imp_YM2, assumption) |
|
514 apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) |
|
515 done |
|
516 |
|
517 |
507 |
518 text\<open>B's session key guarantee from YM4. The two certificates contribute to a |
508 text\<open>B's session key guarantee from YM4. The two certificates contribute to a |
519 single conclusion about the Server's message. Note that the "Notes Spy" |
509 single conclusion about the Server's message. Note that the "Notes Spy" |
520 assumption must quantify over \<open>\<forall>\<close> POSSIBLE keys instead of our particular K. |
510 assumption must quantify over \<open>\<forall>\<close> POSSIBLE keys instead of our particular K. |
521 If this run is broken and the spy substitutes a certificate containing an |
511 If this run is broken and the spy substitutes a certificate containing an |
522 old key, B has no means of telling.\<close> |
512 old key, B has no means of telling.\<close> |
523 lemma B_trusts_YM4: |
513 lemma B_trusts_YM4: |
524 "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, |
514 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, |
525 Crypt K (Nonce NB)\<rbrace> \<in> set evs; |
515 Crypt K (Nonce NB)\<rbrace> \<in> set evs; |
526 Says B Server |
516 Says B Server |
527 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
517 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
528 \<in> set evs; |
518 \<in> set evs; |
529 \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; |
519 \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; |
530 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
520 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
531 ==> Says Server A |
521 \<Longrightarrow> Says Server A |
532 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, |
522 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, |
533 Nonce NA, Nonce NB\<rbrace>, |
523 Nonce NA, Nonce NB\<rbrace>, |
534 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
524 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> |
535 \<in> set evs" |
525 \<in> set evs" |
536 by (blast dest: Spy_not_see_NB Says_unique_NB |
526 by (blast dest: Spy_not_see_NB Says_unique_NB |
539 |
529 |
540 |
530 |
541 text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with |
531 text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with |
542 \<open>Spy_not_see_encrypted_key\<close>\<close> |
532 \<open>Spy_not_see_encrypted_key\<close>\<close> |
543 lemma B_gets_good_key: |
533 lemma B_gets_good_key: |
544 "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, |
534 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, |
545 Crypt K (Nonce NB)\<rbrace> \<in> set evs; |
535 Crypt K (Nonce NB)\<rbrace> \<in> set evs; |
546 Says B Server |
536 Says B Server |
547 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
537 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
548 \<in> set evs; |
538 \<in> set evs; |
549 \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; |
539 \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; |
550 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
540 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
551 ==> Key K \<notin> analz (knows Spy evs)" |
541 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
552 by (metis B_trusts_YM4 Spy_not_see_encrypted_key) |
542 by (metis B_trusts_YM4 Spy_not_see_encrypted_key) |
553 |
543 |
554 |
544 |
555 subsection\<open>Authenticating B to A\<close> |
545 subsection\<open>Authenticating B to A\<close> |
556 |
546 |
557 text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> |
547 text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> |
558 lemma B_Said_YM2 [rule_format]: |
548 lemma B_Said_YM2 [rule_format]: |
559 "[|Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); |
549 "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); |
560 evs \<in> yahalom|] |
550 evs \<in> yahalom\<rbrakk> |
561 ==> B \<notin> bad --> |
551 \<Longrightarrow> B \<notin> bad --> |
562 Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
552 Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
563 \<in> set evs" |
553 \<in> set evs" |
564 apply (erule rev_mp, erule yahalom.induct, force, |
554 apply (erule rev_mp, erule yahalom.induct, force, |
565 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
555 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
566 txt\<open>Fake\<close> |
556 txt\<open>Fake\<close> |
567 apply blast |
557 apply blast |
568 done |
558 done |
569 |
559 |
570 text\<open>If the server sends YM3 then B sent YM2\<close> |
560 text\<open>If the server sends YM3 then B sent YM2\<close> |
571 lemma YM3_auth_B_to_A_lemma: |
561 lemma YM3_auth_B_to_A_lemma: |
572 "[|Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> |
562 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> |
573 \<in> set evs; evs \<in> yahalom|] |
563 \<in> set evs; evs \<in> yahalom\<rbrakk> |
574 ==> B \<notin> bad --> |
564 \<Longrightarrow> B \<notin> bad --> |
575 Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
565 Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
576 \<in> set evs" |
566 \<in> set evs" |
577 apply (erule rev_mp, erule yahalom.induct, simp_all) |
567 apply (erule rev_mp, erule yahalom.induct, simp_all) |
578 txt\<open>YM3, YM4\<close> |
568 txt\<open>YM3, YM4\<close> |
579 apply (blast dest!: B_Said_YM2)+ |
569 apply (blast dest!: B_Said_YM2)+ |
580 done |
570 done |
581 |
571 |
582 text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> |
572 text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> |
583 lemma YM3_auth_B_to_A: |
573 theorem YM3_auth_B_to_A: |
584 "[| Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> |
574 "\<lbrakk>Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> |
585 \<in> set evs; |
575 \<in> set evs; |
586 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
576 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
587 ==> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
577 \<Longrightarrow> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> |
588 \<in> set evs" |
578 \<in> set evs" |
589 by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst |
579 by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst |
590 not_parts_not_analz) |
580 not_parts_not_analz) |
591 |
581 |
592 |
582 |
594 @{term "Crypt K (Nonce NB)"}\<close> |
584 @{term "Crypt K (Nonce NB)"}\<close> |
595 |
585 |
596 text\<open>Assuming the session key is secure, if both certificates are present then |
586 text\<open>Assuming the session key is secure, if both certificates are present then |
597 A has said NB. We can't be sure about the rest of A's message, but only |
587 A has said NB. We can't be sure about the rest of A's message, but only |
598 NB matters for freshness.\<close> |
588 NB matters for freshness.\<close> |
599 lemma A_Said_YM3_lemma [rule_format]: |
589 theorem A_Said_YM3_lemma [rule_format]: |
600 "evs \<in> yahalom |
590 "evs \<in> yahalom |
601 ==> Key K \<notin> analz (knows Spy evs) --> |
591 \<Longrightarrow> Key K \<notin> analz (knows Spy evs) --> |
602 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
592 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
603 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) --> |
593 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) --> |
604 B \<notin> bad --> |
594 B \<notin> bad --> |
605 (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" |
595 (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" |
606 apply (erule yahalom.induct, force, |
596 apply (erule yahalom.induct, force, |
607 frule_tac [6] YM4_parts_knows_Spy) |
597 frule_tac [6] YM4_parts_knows_Spy) |
608 apply (analz_mono_contra, simp_all) |
598 apply (analz_mono_contra, simp_all) |
609 txt\<open>Fake\<close> |
599 subgoal --\<open>Fake\<close> by blast |
610 apply blast |
600 subgoal --\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close> |
611 txt\<open>YM3: by \<open>new_keys_not_used\<close>, the message |
601 by (force dest!: Crypt_imp_keysFor) |
612 @{term "Crypt K (Nonce NB)"} could not exist\<close> |
602 subgoal --\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis, |
613 apply (force dest!: Crypt_imp_keysFor) |
603 otherwise by unicity of session keys\<close> |
614 txt\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? |
604 by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad |
615 If not, use the induction hypothesis\<close> |
|
616 apply (simp add: ex_disj_distrib) |
|
617 txt\<open>yes: apply unicity of session keys\<close> |
|
618 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK |
|
619 Crypt_Spy_analz_bad |
|
620 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
605 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
621 done |
606 done |
622 |
607 |
623 text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). |
608 text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). |
624 Moreover, A associates K with NB (thus is talking about the same run). |
609 Moreover, A associates K with NB (thus is talking about the same run). |
625 Other premises guarantee secrecy of K.\<close> |
610 Other premises guarantee secrecy of K.\<close> |
626 lemma YM4_imp_A_Said_YM3 [rule_format]: |
611 theorem YM4_imp_A_Said_YM3 [rule_format]: |
627 "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, |
612 "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, |
628 Crypt K (Nonce NB)\<rbrace> \<in> set evs; |
613 Crypt K (Nonce NB)\<rbrace> \<in> set evs; |
629 Says B Server |
614 Says B Server |
630 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
615 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> |
631 \<in> set evs; |
616 \<in> set evs; |
632 (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); |
617 (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); |
633 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
618 A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> |
634 ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" |
619 \<Longrightarrow> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" |
635 by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz) |
620 by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz) |
|
621 |
636 end |
622 end |