92 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
92 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
93 |
93 |
94 declare Gets_imp_knows_Spy [THEN analz.Inj, dest] |
94 declare Gets_imp_knows_Spy [THEN analz.Inj, dest] |
95 |
95 |
96 |
96 |
97 subsection{* For reasoning about the encrypted portion of messages *} |
97 subsection\<open>For reasoning about the encrypted portion of messages\<close> |
98 |
98 |
99 text{*Lets us treat YM4 using a similar argument as for the Fake case.*} |
99 text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close> |
100 lemma YM4_analz_knows_Spy: |
100 lemma YM4_analz_knows_Spy: |
101 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
101 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
102 ==> X \<in> analz (knows Spy evs)" |
102 ==> X \<in> analz (knows Spy evs)" |
103 by blast |
103 by blast |
104 |
104 |
105 lemmas YM4_parts_knows_Spy = |
105 lemmas YM4_parts_knows_Spy = |
106 YM4_analz_knows_Spy [THEN analz_into_parts] |
106 YM4_analz_knows_Spy [THEN analz_into_parts] |
107 |
107 |
108 |
108 |
109 text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply |
109 text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply |
110 that NOBODY sends messages containing X!*} |
110 that NOBODY sends messages containing X!\<close> |
111 |
111 |
112 text{*Spy never sees a good agent's shared key!*} |
112 text\<open>Spy never sees a good agent's shared key!\<close> |
113 lemma Spy_see_shrK [simp]: |
113 lemma Spy_see_shrK [simp]: |
114 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
114 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
115 apply (erule yahalom.induct, force, |
115 apply (erule yahalom.induct, force, |
116 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) |
116 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) |
117 done |
117 done |
122 |
122 |
123 lemma Spy_see_shrK_D [dest!]: |
123 lemma Spy_see_shrK_D [dest!]: |
124 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
124 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
125 by (blast dest: Spy_see_shrK) |
125 by (blast dest: Spy_see_shrK) |
126 |
126 |
127 text{*Nobody can have used non-existent keys! |
127 text\<open>Nobody can have used non-existent keys! |
128 Needed to apply @{text analz_insert_Key}*} |
128 Needed to apply \<open>analz_insert_Key\<close>\<close> |
129 lemma new_keys_not_used [simp]: |
129 lemma new_keys_not_used [simp]: |
130 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|] |
130 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|] |
131 ==> K \<notin> keysFor (parts (spies evs))" |
131 ==> K \<notin> keysFor (parts (spies evs))" |
132 apply (erule rev_mp) |
132 apply (erule rev_mp) |
133 apply (erule yahalom.induct, force, |
133 apply (erule yahalom.induct, force, |
134 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
134 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
135 txt{*Fake*} |
135 txt\<open>Fake\<close> |
136 apply (force dest!: keysFor_parts_insert, auto) |
136 apply (force dest!: keysFor_parts_insert, auto) |
137 done |
137 done |
138 |
138 |
139 |
139 |
140 subsection{*Secrecy Theorems*} |
140 subsection\<open>Secrecy Theorems\<close> |
141 |
141 |
142 (**** |
142 (**** |
143 The following is to prove theorems of the form |
143 The following is to prove theorems of the form |
144 |
144 |
145 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
145 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
146 Key K \<in> analz (knows Spy evs) |
146 Key K \<in> analz (knows Spy evs) |
147 |
147 |
148 A more general formula must be proved inductively. |
148 A more general formula must be proved inductively. |
149 ****) |
149 ****) |
150 |
150 |
151 subsection{* Session keys are not used to encrypt other session keys *} |
151 subsection\<open>Session keys are not used to encrypt other session keys\<close> |
152 |
152 |
153 lemma analz_image_freshK [rule_format]: |
153 lemma analz_image_freshK [rule_format]: |
154 "evs \<in> yahalom ==> |
154 "evs \<in> yahalom ==> |
155 \<forall>K KK. KK <= - (range shrK) --> |
155 \<forall>K KK. KK <= - (range shrK) --> |
156 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
156 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
163 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
163 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
164 (K = KAB | Key K \<in> analz (knows Spy evs))" |
164 (K = KAB | Key K \<in> analz (knows Spy evs))" |
165 by (simp only: analz_image_freshK analz_image_freshK_simps) |
165 by (simp only: analz_image_freshK analz_image_freshK_simps) |
166 |
166 |
167 |
167 |
168 text{*The Key K uniquely identifies the Server's message.*} |
168 text\<open>The Key K uniquely identifies the Server's message.\<close> |
169 lemma unique_session_keys: |
169 lemma unique_session_keys: |
170 "[| Says Server A |
170 "[| Says Server A |
171 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs; |
171 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs; |
172 Says Server A' |
172 Says Server A' |
173 {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs; |
173 {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs; |
174 evs \<in> yahalom |] |
174 evs \<in> yahalom |] |
175 ==> A=A' & B=B' & na=na' & nb=nb'" |
175 ==> A=A' & B=B' & na=na' & nb=nb'" |
176 apply (erule rev_mp, erule rev_mp) |
176 apply (erule rev_mp, erule rev_mp) |
177 apply (erule yahalom.induct, simp_all) |
177 apply (erule yahalom.induct, simp_all) |
178 txt{*YM3, by freshness, and YM4*} |
178 txt\<open>YM3, by freshness, and YM4\<close> |
179 apply blast+ |
179 apply blast+ |
180 done |
180 done |
181 |
181 |
182 |
182 |
183 text{* Crucial secrecy property: Spy does not see the keys sent in msg YM3 *} |
183 text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close> |
184 lemma secrecy_lemma: |
184 lemma secrecy_lemma: |
185 "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
185 "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
186 ==> Says Server A |
186 ==> Says Server A |
187 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
187 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
188 Crypt (shrK B) {|Agent A, Key K|}|} |
188 Crypt (shrK B) {|Agent A, Key K|}|} |
191 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy) |
191 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy) |
192 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*) |
192 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*) |
193 apply (blast dest: unique_session_keys) (*YM3*) |
193 apply (blast dest: unique_session_keys) (*YM3*) |
194 done |
194 done |
195 |
195 |
196 text{*Final version*} |
196 text\<open>Final version\<close> |
197 lemma Spy_not_see_encrypted_key: |
197 lemma Spy_not_see_encrypted_key: |
198 "[| Says Server A |
198 "[| Says Server A |
199 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
199 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
200 Crypt (shrK B) {|Agent A, Key K|}|} |
200 Crypt (shrK B) {|Agent A, Key K|}|} |
201 \<in> set evs; |
201 \<in> set evs; |
202 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
202 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
203 ==> Key K \<notin> analz (knows Spy evs)" |
203 ==> Key K \<notin> analz (knows Spy evs)" |
204 by (blast dest: secrecy_lemma) |
204 by (blast dest: secrecy_lemma) |
205 |
205 |
206 |
206 |
207 subsection{* Security Guarantee for A upon receiving YM3 *} |
207 subsection\<open>Security Guarantee for A upon receiving YM3\<close> |
208 |
208 |
209 text{*If the encrypted message appears then it originated with the Server*} |
209 text\<open>If the encrypted message appears then it originated with the Server\<close> |
210 lemma A_trusts_YM3: |
210 lemma A_trusts_YM3: |
211 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
211 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
212 A \<notin> bad; evs \<in> yahalom |] |
212 A \<notin> bad; evs \<in> yahalom |] |
213 ==> Says Server A |
213 ==> Says Server A |
214 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
214 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
215 Crypt (shrK B) {|Agent A, Key K|}|} |
215 Crypt (shrK B) {|Agent A, Key K|}|} |
216 \<in> set evs" |
216 \<in> set evs" |
217 apply (erule rev_mp) |
217 apply (erule rev_mp) |
218 apply (erule yahalom.induct, force, |
218 apply (erule yahalom.induct, force, |
219 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
219 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
220 txt{*Fake, YM3*} |
220 txt\<open>Fake, YM3\<close> |
221 apply blast+ |
221 apply blast+ |
222 done |
222 done |
223 |
223 |
224 text{*The obvious combination of @{text A_trusts_YM3} with |
224 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with |
225 @{text Spy_not_see_encrypted_key}*} |
225 \<open>Spy_not_see_encrypted_key\<close>\<close> |
226 lemma A_gets_good_key: |
226 lemma A_gets_good_key: |
227 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
227 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
228 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
228 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
229 ==> Key K \<notin> analz (knows Spy evs)" |
229 ==> Key K \<notin> analz (knows Spy evs)" |
230 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
230 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
231 |
231 |
232 subsection{* Security Guarantees for B upon receiving YM4 *} |
232 subsection\<open>Security Guarantees for B upon receiving YM4\<close> |
233 |
233 |
234 text{*B knows, by the first part of A's message, that the Server distributed |
234 text\<open>B knows, by the first part of A's message, that the Server distributed |
235 the key for A and B. But this part says nothing about nonces.*} |
235 the key for A and B. But this part says nothing about nonces.\<close> |
236 lemma B_trusts_YM4_shrK: |
236 lemma B_trusts_YM4_shrK: |
237 "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs); |
237 "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs); |
238 B \<notin> bad; evs \<in> yahalom |] |
238 B \<notin> bad; evs \<in> yahalom |] |
239 ==> \<exists>NA NB. Says Server A |
239 ==> \<exists>NA NB. Says Server A |
240 {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
240 {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
241 Crypt (shrK B) {|Agent A, Key K|}|} |
241 Crypt (shrK B) {|Agent A, Key K|}|} |
242 \<in> set evs" |
242 \<in> set evs" |
243 apply (erule rev_mp) |
243 apply (erule rev_mp) |
244 apply (erule yahalom.induct, force, |
244 apply (erule yahalom.induct, force, |
245 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
245 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
246 txt{*Fake, YM3*} |
246 txt\<open>Fake, YM3\<close> |
247 apply blast+ |
247 apply blast+ |
248 done |
248 done |
249 |
249 |
250 subsection{*The Flaw in the Model*} |
250 subsection\<open>The Flaw in the Model\<close> |
251 |
251 |
252 text{* Up to now, the reasoning is similar to standard Yahalom. Now the |
252 text\<open>Up to now, the reasoning is similar to standard Yahalom. Now the |
253 doubtful reasoning occurs. We should not be assuming that an unknown |
253 doubtful reasoning occurs. We should not be assuming that an unknown |
254 key is secure, but the model allows us to: there is no Oops rule to |
254 key is secure, but the model allows us to: there is no Oops rule to |
255 let session keys become compromised.*} |
255 let session keys become compromised.\<close> |
256 |
256 |
257 text{*B knows, by the second part of A's message, that the Server distributed |
257 text\<open>B knows, by the second part of A's message, that the Server distributed |
258 the key quoting nonce NB. This part says nothing about agent names. |
258 the key quoting nonce NB. This part says nothing about agent names. |
259 Secrecy of K is assumed; the valid Yahalom proof uses (and later proves) |
259 Secrecy of K is assumed; the valid Yahalom proof uses (and later proves) |
260 the secrecy of NB.*} |
260 the secrecy of NB.\<close> |
261 lemma B_trusts_YM4_newK [rule_format]: |
261 lemma B_trusts_YM4_newK [rule_format]: |
262 "[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
262 "[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
263 ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
263 ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
264 (\<exists>A B NA. Says Server A |
264 (\<exists>A B NA. Says Server A |
265 {|Crypt (shrK A) {|Agent B, Key K, |
265 {|Crypt (shrK A) {|Agent B, Key K, |
268 \<in> set evs)" |
268 \<in> set evs)" |
269 apply (erule rev_mp) |
269 apply (erule rev_mp) |
270 apply (erule yahalom.induct, force, |
270 apply (erule yahalom.induct, force, |
271 frule_tac [6] YM4_parts_knows_Spy) |
271 frule_tac [6] YM4_parts_knows_Spy) |
272 apply (analz_mono_contra, simp_all) |
272 apply (analz_mono_contra, simp_all) |
273 txt{*Fake*} |
273 txt\<open>Fake\<close> |
274 apply blast |
274 apply blast |
275 txt{*YM3*} |
275 txt\<open>YM3\<close> |
276 apply blast |
276 apply blast |
277 txt{*A is uncompromised because NB is secure |
277 txt\<open>A is uncompromised because NB is secure |
278 A's certificate guarantees the existence of the Server message*} |
278 A's certificate guarantees the existence of the Server message\<close> |
279 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
279 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
280 dest: Says_imp_spies |
280 dest: Says_imp_spies |
281 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
281 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
282 done |
282 done |
283 |
283 |
284 |
284 |
285 text{*B's session key guarantee from YM4. The two certificates contribute to a |
285 text\<open>B's session key guarantee from YM4. The two certificates contribute to a |
286 single conclusion about the Server's message. *} |
286 single conclusion about the Server's message.\<close> |
287 lemma B_trusts_YM4: |
287 lemma B_trusts_YM4: |
288 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
288 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
289 Crypt K (Nonce NB)|} \<in> set evs; |
289 Crypt K (Nonce NB)|} \<in> set evs; |
290 Says B Server |
290 Says B Server |
291 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
291 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
316 They are irrelevant to showing the need for Oops. ***) |
316 They are irrelevant to showing the need for Oops. ***) |
317 |
317 |
318 |
318 |
319 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
319 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
320 |
320 |
321 text{*Assuming the session key is secure, if both certificates are present then |
321 text\<open>Assuming the session key is secure, if both certificates are present then |
322 A has said NB. We can't be sure about the rest of A's message, but only |
322 A has said NB. We can't be sure about the rest of A's message, but only |
323 NB matters for freshness.*} |
323 NB matters for freshness.\<close> |
324 lemma A_Said_YM3_lemma [rule_format]: |
324 lemma A_Said_YM3_lemma [rule_format]: |
325 "evs \<in> yahalom |
325 "evs \<in> yahalom |
326 ==> Key K \<notin> analz (knows Spy evs) --> |
326 ==> Key K \<notin> analz (knows Spy evs) --> |
327 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
327 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
328 Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) --> |
328 Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) --> |
329 B \<notin> bad --> |
329 B \<notin> bad --> |
330 (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
330 (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
331 apply (erule yahalom.induct, force, |
331 apply (erule yahalom.induct, force, |
332 frule_tac [6] YM4_parts_knows_Spy) |
332 frule_tac [6] YM4_parts_knows_Spy) |
333 apply (analz_mono_contra, simp_all) |
333 apply (analz_mono_contra, simp_all) |
334 txt{*Fake*} |
334 txt\<open>Fake\<close> |
335 apply blast |
335 apply blast |
336 txt{*YM3: by @{text new_keys_not_used}, the message |
336 txt\<open>YM3: by \<open>new_keys_not_used\<close>, the message |
337 @{term "Crypt K (Nonce NB)"} could not exist*} |
337 @{term "Crypt K (Nonce NB)"} could not exist\<close> |
338 apply (force dest!: Crypt_imp_keysFor) |
338 apply (force dest!: Crypt_imp_keysFor) |
339 txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message? |
339 txt\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? |
340 If not, use the induction hypothesis*} |
340 If not, use the induction hypothesis\<close> |
341 apply (simp add: ex_disj_distrib) |
341 apply (simp add: ex_disj_distrib) |
342 txt{*yes: apply unicity of session keys*} |
342 txt\<open>yes: apply unicity of session keys\<close> |
343 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK |
343 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK |
344 Crypt_Spy_analz_bad |
344 Crypt_Spy_analz_bad |
345 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
345 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
346 done |
346 done |
347 |
347 |
348 text{*If B receives YM4 then A has used nonce NB (and therefore is alive). |
348 text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). |
349 Moreover, A associates K with NB (thus is talking about the same run). |
349 Moreover, A associates K with NB (thus is talking about the same run). |
350 Other premises guarantee secrecy of K.*} |
350 Other premises guarantee secrecy of K.\<close> |
351 lemma YM4_imp_A_Said_YM3 [rule_format]: |
351 lemma YM4_imp_A_Said_YM3 [rule_format]: |
352 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
352 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
353 Crypt K (Nonce NB)|} \<in> set evs; |
353 Crypt K (Nonce NB)|} \<in> set evs; |
354 Says B Server |
354 Says B Server |
355 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
355 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |