6 Inductive relation "yahalom" for the Yahalom protocol. |
6 Inductive relation "yahalom" for the Yahalom protocol. |
7 |
7 |
8 From page 257 of |
8 From page 257 of |
9 Burrows, Abadi and Needham. A Logic of Authentication. |
9 Burrows, Abadi and Needham. A Logic of Authentication. |
10 Proc. Royal Soc. 426 (1989) |
10 Proc. Royal Soc. 426 (1989) |
|
11 |
|
12 This theory has the prototypical example of a secrecy relation, KeyCryptNonce. |
11 *) |
13 *) |
12 |
14 |
13 Yahalom = Shared + |
15 theory Yahalom = Shared: |
14 |
16 |
15 consts yahalom :: event list set |
17 consts yahalom :: "event list set" |
16 inductive "yahalom" |
18 inductive "yahalom" |
17 intrs |
19 intros |
18 (*Initial trace is empty*) |
20 (*Initial trace is empty*) |
19 Nil "[] \\<in> yahalom" |
21 Nil: "[] \<in> yahalom" |
20 |
22 |
21 (*The spy MAY say anything he CAN say. We do not expect him to |
23 (*The spy MAY say anything he CAN say. We do not expect him to |
22 invent new nonces here, but he can also use NS1. Common to |
24 invent new nonces here, but he can also use NS1. Common to |
23 all similar protocols.*) |
25 all similar protocols.*) |
24 Fake "[| evsf \\<in> yahalom; X \\<in> synth (analz (knows Spy evsf)) |] |
26 Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] |
25 ==> Says Spy B X # evsf \\<in> yahalom" |
27 ==> Says Spy B X # evsf \<in> yahalom" |
26 |
28 |
27 (*A message that has been sent can be received by the |
29 (*A message that has been sent can be received by the |
28 intended recipient.*) |
30 intended recipient.*) |
29 Reception "[| evsr \\<in> yahalom; Says A B X \\<in> set evsr |] |
31 Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] |
30 ==> Gets B X # evsr \\<in> yahalom" |
32 ==> Gets B X # evsr \<in> yahalom" |
31 |
33 |
32 (*Alice initiates a protocol run*) |
34 (*Alice initiates a protocol run*) |
33 YM1 "[| evs1 \\<in> yahalom; Nonce NA \\<notin> used evs1 |] |
35 YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] |
34 ==> Says A B {|Agent A, Nonce NA|} # evs1 \\<in> yahalom" |
36 ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom" |
35 |
37 |
36 (*Bob's response to Alice's message.*) |
38 (*Bob's response to Alice's message.*) |
37 YM2 "[| evs2 \\<in> yahalom; Nonce NB \\<notin> used evs2; |
39 YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
38 Gets B {|Agent A, Nonce NA|} \\<in> set evs2 |] |
40 Gets B {|Agent A, Nonce NA|} \<in> set evs2 |] |
39 ==> Says B Server |
41 ==> Says B Server |
40 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
42 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
41 # evs2 \\<in> yahalom" |
43 # evs2 \<in> yahalom" |
42 |
44 |
43 (*The Server receives Bob's message. He responds by sending a |
45 (*The Server receives Bob's message. He responds by sending a |
44 new session key to Alice, with a packet for forwarding to Bob.*) |
46 new session key to Alice, with a packet for forwarding to Bob.*) |
45 YM3 "[| evs3 \\<in> yahalom; Key KAB \\<notin> used evs3; |
47 YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; |
46 Gets Server |
48 Gets Server |
47 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
49 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
48 \\<in> set evs3 |] |
50 \<in> set evs3 |] |
49 ==> Says Server A |
51 ==> Says Server A |
50 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
52 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
51 Crypt (shrK B) {|Agent A, Key KAB|}|} |
53 Crypt (shrK B) {|Agent A, Key KAB|}|} |
52 # evs3 \\<in> yahalom" |
54 # evs3 \<in> yahalom" |
53 |
55 |
54 (*Alice receives the Server's (?) message, checks her Nonce, and |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
55 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 |
56 A \\<noteq> Server is needed to prove Says_Server_not_range.*) |
58 A \<noteq> Server is needed to prove Says_Server_not_range.*) |
57 YM4 "[| evs4 \\<in> yahalom; A \\<noteq> Server; |
59 YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; |
58 Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
60 Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
59 \\<in> set evs4; |
61 \<in> set evs4; |
60 Says A B {|Agent A, Nonce NA|} \\<in> set evs4 |] |
62 Says A B {|Agent A, Nonce NA|} \<in> set evs4 |] |
61 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\<in> yahalom" |
63 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom" |
62 |
64 |
63 (*This message models possible leaks of session keys. The Nonces |
65 (*This message models possible leaks of session keys. The Nonces |
64 identify the protocol run. Quoting Server here ensures they are |
66 identify the protocol run. Quoting Server here ensures they are |
65 correct.*) |
67 correct.*) |
66 Oops "[| evso \\<in> yahalom; |
68 Oops: "[| evso \<in> yahalom; |
67 Says Server A {|Crypt (shrK A) |
69 Says Server A {|Crypt (shrK A) |
68 {|Agent B, Key K, Nonce NA, Nonce NB|}, |
70 {|Agent B, Key K, Nonce NA, Nonce NB|}, |
69 X|} \\<in> set evso |] |
71 X|} \<in> set evso |] |
70 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> yahalom" |
72 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom" |
71 |
73 |
72 |
74 |
73 constdefs |
75 constdefs |
74 KeyWithNonce :: [key, nat, event list] => bool |
76 KeyWithNonce :: "[key, nat, event list] => bool" |
75 "KeyWithNonce K NB evs == |
77 "KeyWithNonce K NB evs == |
76 \\<exists>A B na X. |
78 \<exists>A B na X. |
77 Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
79 Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
78 \\<in> set evs" |
80 \<in> set evs" |
|
81 |
|
82 |
|
83 declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
84 declare parts.Body [dest] |
|
85 declare Fake_parts_insert_in_Un [dest] |
|
86 declare analz_into_parts [dest] |
|
87 |
|
88 (*A "possibility property": there are traces that reach the end*) |
|
89 lemma "A \<noteq> Server |
|
90 ==> \<exists>X NB K. \<exists>evs \<in> yahalom. |
|
91 Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
|
92 apply (intro exI bexI) |
|
93 apply (rule_tac [2] yahalom.Nil |
|
94 [THEN yahalom.YM1, THEN yahalom.Reception, |
|
95 THEN yahalom.YM2, THEN yahalom.Reception, |
|
96 THEN yahalom.YM3, THEN yahalom.Reception, |
|
97 THEN yahalom.YM4]) |
|
98 apply possibility |
|
99 done |
|
100 |
|
101 lemma Gets_imp_Says: |
|
102 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" |
|
103 by (erule rev_mp, erule yahalom.induct, auto) |
|
104 |
|
105 (*Must be proved separately for each protocol*) |
|
106 lemma Gets_imp_knows_Spy: |
|
107 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" |
|
108 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
|
109 |
|
110 declare Gets_imp_knows_Spy [THEN analz.Inj, dest] |
|
111 |
|
112 |
|
113 (**** Inductive proofs about yahalom ****) |
|
114 |
|
115 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
|
116 lemma YM4_analz_knows_Spy: |
|
117 "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |] |
|
118 ==> X \<in> analz (knows Spy evs)" |
|
119 by blast |
|
120 |
|
121 lemmas YM4_parts_knows_Spy = |
|
122 YM4_analz_knows_Spy [THEN analz_into_parts, standard] |
|
123 |
|
124 (*For Oops*) |
|
125 lemma YM4_Key_parts_knows_Spy: |
|
126 "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs |
|
127 ==> K \<in> parts (knows Spy evs)" |
|
128 by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj]) |
|
129 |
|
130 |
|
131 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
|
132 sends messages containing X! **) |
|
133 |
|
134 (*Spy never sees a good agent's shared key!*) |
|
135 lemma Spy_see_shrK [simp]: |
|
136 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
137 apply (erule yahalom.induct, force, |
|
138 drule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
139 apply blast+ |
|
140 done |
|
141 |
|
142 lemma Spy_analz_shrK [simp]: |
|
143 "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
144 by auto |
|
145 |
|
146 lemma Spy_see_shrK_D [dest!]: |
|
147 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" |
|
148 by (blast dest: Spy_see_shrK) |
|
149 |
|
150 (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) |
|
151 lemma new_keys_not_used [rule_format, simp]: |
|
152 "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))" |
|
153 apply (erule yahalom.induct, force, |
|
154 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
155 (*Fake, YM3, YM4*) |
|
156 apply (blast dest!: keysFor_parts_insert)+ |
|
157 done |
|
158 |
|
159 |
|
160 (*Earlier, all protocol proofs declared this theorem. |
|
161 But only a few proofs need it, e.g. Yahalom and Kerberos IV.*) |
|
162 lemma new_keys_not_analzd: |
|
163 "[|evs \<in> yahalom; Key K \<notin> used evs|] ==> K \<notin> keysFor (analz (knows Spy evs))" |
|
164 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) |
|
165 |
|
166 |
|
167 (*Describes the form of K when the Server sends this message. Useful for |
|
168 Oops as well as main secrecy property.*) |
|
169 lemma Says_Server_not_range [simp]: |
|
170 "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} |
|
171 \<in> set evs; evs \<in> yahalom |] |
|
172 ==> K \<notin> range shrK" |
|
173 apply (erule rev_mp, erule yahalom.induct, simp_all) |
|
174 apply blast |
|
175 done |
|
176 |
|
177 |
|
178 (*For proofs involving analz. |
|
179 val analz_knows_Spy_tac = |
|
180 ftac YM4_analz_knows_Spy 7 THEN assume_tac 7 |
|
181 *) |
|
182 |
|
183 (**** |
|
184 The following is to prove theorems of the form |
|
185 |
|
186 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
187 Key K \<in> analz (knows Spy evs) |
|
188 |
|
189 A more general formula must be proved inductively. |
|
190 ****) |
|
191 |
|
192 (** Session keys are not used to encrypt other session keys **) |
|
193 |
|
194 lemma analz_image_freshK [rule_format]: |
|
195 "evs \<in> yahalom ==> |
|
196 \<forall>K KK. KK <= - (range shrK) --> |
|
197 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
198 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
199 apply (erule yahalom.induct, force, |
|
200 drule_tac [6] YM4_analz_knows_Spy) |
|
201 apply analz_freshK |
|
202 apply spy_analz |
|
203 apply (simp only: Says_Server_not_range analz_image_freshK_simps) |
|
204 done |
|
205 |
|
206 lemma analz_insert_freshK: |
|
207 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> |
|
208 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) = |
|
209 (K = KAB | Key K \<in> analz (knows Spy evs))" |
|
210 by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
211 |
|
212 |
|
213 (*** The Key K uniquely identifies the Server's message. **) |
|
214 |
|
215 lemma unique_session_keys: |
|
216 "[| Says Server A |
|
217 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs; |
|
218 Says Server A' |
|
219 {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs; |
|
220 evs \<in> yahalom |] |
|
221 ==> A=A' & B=B' & na=na' & nb=nb'" |
|
222 apply (erule rev_mp, erule rev_mp) |
|
223 apply (erule yahalom.induct, simp_all) |
|
224 (*YM3, by freshness, and YM4*) |
|
225 apply blast+ |
|
226 done |
|
227 |
|
228 |
|
229 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
|
230 |
|
231 lemma secrecy_lemma: |
|
232 "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
233 ==> Says Server A |
|
234 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
235 Crypt (shrK B) {|Agent A, Key K|}|} |
|
236 \<in> set evs --> |
|
237 Notes Spy {|na, nb, Key K|} \<notin> set evs --> |
|
238 Key K \<notin> analz (knows Spy evs)" |
|
239 apply (erule yahalom.induct, force, |
|
240 drule_tac [6] YM4_analz_knows_Spy) |
|
241 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) |
|
242 apply spy_analz (*Fake*) |
|
243 apply (blast dest: unique_session_keys)+ (*YM3, Oops*) |
|
244 done |
|
245 |
|
246 (*Final version*) |
|
247 lemma Spy_not_see_encrypted_key: |
|
248 "[| Says Server A |
|
249 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
250 Crypt (shrK B) {|Agent A, Key K|}|} |
|
251 \<in> set evs; |
|
252 Notes Spy {|na, nb, Key K|} \<notin> set evs; |
|
253 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
254 ==> Key K \<notin> analz (knows Spy evs)" |
|
255 by (blast dest: secrecy_lemma) |
|
256 |
|
257 |
|
258 (** Security Guarantee for A upon receiving YM3 **) |
|
259 |
|
260 (*If the encrypted message appears then it originated with the Server*) |
|
261 lemma A_trusts_YM3: |
|
262 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
|
263 A \<notin> bad; evs \<in> yahalom |] |
|
264 ==> Says Server A |
|
265 {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, |
|
266 Crypt (shrK B) {|Agent A, Key K|}|} |
|
267 \<in> set evs" |
|
268 apply (erule rev_mp) |
|
269 apply (erule yahalom.induct, force, |
|
270 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
271 (*Fake, YM3*) |
|
272 apply blast+ |
|
273 done |
|
274 |
|
275 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) |
|
276 lemma A_gets_good_key: |
|
277 "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs); |
|
278 Notes Spy {|na, nb, Key K|} \<notin> set evs; |
|
279 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
280 ==> Key K \<notin> analz (knows Spy evs)" |
|
281 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) |
|
282 |
|
283 (** Security Guarantees for B upon receiving YM4 **) |
|
284 |
|
285 (*B knows, by the first part of A's message, that the Server distributed |
|
286 the key for A and B. But this part says nothing about nonces.*) |
|
287 lemma B_trusts_YM4_shrK: |
|
288 "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs); |
|
289 B \<notin> bad; evs \<in> yahalom |] |
|
290 ==> \<exists>NA NB. Says Server A |
|
291 {|Crypt (shrK A) {|Agent B, Key K, |
|
292 Nonce NA, Nonce NB|}, |
|
293 Crypt (shrK B) {|Agent A, Key K|}|} |
|
294 \<in> set evs" |
|
295 apply (erule rev_mp) |
|
296 apply (erule yahalom.induct, force, |
|
297 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
298 (*Fake, YM3*) |
|
299 apply blast+ |
|
300 done |
|
301 |
|
302 (*B knows, by the second part of A's message, that the Server distributed |
|
303 the key quoting nonce NB. This part says nothing about agent names. |
|
304 Secrecy of NB is crucial. Note that Nonce NB \<notin> analz(knows Spy evs) must |
|
305 be the FIRST antecedent of the induction formula.*) |
|
306 lemma B_trusts_YM4_newK[rule_format]: |
|
307 "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs); |
|
308 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
|
309 ==> \<exists>A B NA. Says Server A |
|
310 {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
|
311 Crypt (shrK B) {|Agent A, Key K|}|} |
|
312 \<in> set evs" |
|
313 apply (erule rev_mp, erule rev_mp) |
|
314 apply (erule yahalom.induct, force, |
|
315 frule_tac [6] YM4_parts_knows_Spy) |
|
316 apply (analz_mono_contra, simp_all) |
|
317 (*Fake, YM3*) |
|
318 apply blast |
|
319 apply blast |
|
320 (*YM4*) |
|
321 (*A is uncompromised because NB is secure |
|
322 A's certificate guarantees the existence of the Server message*) |
|
323 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
|
324 dest: Says_imp_spies |
|
325 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) |
|
326 done |
|
327 |
|
328 |
|
329 (**** Towards proving secrecy of Nonce NB ****) |
|
330 |
|
331 (** Lemmas about the predicate KeyWithNonce **) |
|
332 |
|
333 lemma KeyWithNonceI: |
|
334 "Says Server A |
|
335 {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} |
|
336 \<in> set evs ==> KeyWithNonce K NB evs" |
|
337 by (unfold KeyWithNonce_def, blast) |
|
338 |
|
339 lemma KeyWithNonce_Says [simp]: |
|
340 "KeyWithNonce K NB (Says S A X # evs) = |
|
341 (Server = S & |
|
342 (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) |
|
343 | KeyWithNonce K NB evs)" |
|
344 by (simp add: KeyWithNonce_def, blast) |
|
345 |
|
346 |
|
347 lemma KeyWithNonce_Notes [simp]: |
|
348 "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs" |
|
349 by (simp add: KeyWithNonce_def) |
|
350 |
|
351 lemma KeyWithNonce_Gets [simp]: |
|
352 "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" |
|
353 by (simp add: KeyWithNonce_def) |
|
354 |
|
355 (*A fresh key cannot be associated with any nonce |
|
356 (with respect to a given trace). *) |
|
357 lemma fresh_not_KeyWithNonce: |
|
358 "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs" |
|
359 by (unfold KeyWithNonce_def, blast) |
|
360 |
|
361 (*The Server message associates K with NB' and therefore not with any |
|
362 other nonce NB.*) |
|
363 lemma Says_Server_KeyWithNonce: |
|
364 "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} |
|
365 \<in> set evs; |
|
366 NB \<noteq> NB'; evs \<in> yahalom |] |
|
367 ==> ~ KeyWithNonce K NB evs" |
|
368 by (unfold KeyWithNonce_def, blast dest: unique_session_keys) |
|
369 |
|
370 |
|
371 (*The only nonces that can be found with the help of session keys are |
|
372 those distributed as nonce NB by the Server. The form of the theorem |
|
373 recalls analz_image_freshK, but it is much more complicated.*) |
|
374 |
|
375 |
|
376 (*As with analz_image_freshK, we take some pains to express the property |
|
377 as a logical equivalence so that the simplifier can apply it.*) |
|
378 lemma Nonce_secrecy_lemma: |
|
379 "P --> (X \<in> analz (G Un H)) --> (X \<in> analz H) ==> |
|
380 P --> (X \<in> analz (G Un H)) = (X \<in> analz H)" |
|
381 by (blast intro: analz_mono [THEN subsetD]) |
|
382 |
|
383 lemma Nonce_secrecy: |
|
384 "evs \<in> yahalom ==> |
|
385 (\<forall>KK. KK <= - (range shrK) --> |
|
386 (\<forall>K \<in> KK. ~ KeyWithNonce K NB evs) --> |
|
387 (Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) = |
|
388 (Nonce NB \<in> analz (knows Spy evs)))" |
|
389 apply (erule yahalom.induct, force, |
|
390 frule_tac [6] YM4_analz_knows_Spy) |
|
391 apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI]) |
|
392 apply (simp_all del: image_insert image_Un |
|
393 add: analz_image_freshK_simps split_ifs |
|
394 all_conj_distrib ball_conj_distrib |
|
395 analz_image_freshK fresh_not_KeyWithNonce |
|
396 imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) |
|
397 Says_Server_KeyWithNonce) |
|
398 (*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce, |
|
399 we get (~ KeyWithNonce K NB evs); then simplification can apply the |
|
400 induction hypothesis with KK = {K}.*) |
|
401 (*Fake*) |
|
402 apply spy_analz |
|
403 (*YM4*) (** LEVEL 6 **) |
|
404 apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl) |
|
405 apply clarify |
|
406 (*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps make |
|
407 the next step faster.*) |
|
408 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad |
|
409 dest: analz.Inj |
|
410 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI]) |
|
411 done |
|
412 |
|
413 |
|
414 (*Version required below: if NB can be decrypted using a session key then it |
|
415 was distributed with that key. The more general form above is required |
|
416 for the induction to carry through.*) |
|
417 lemma single_Nonce_secrecy: |
|
418 "[| Says Server A |
|
419 {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} |
|
420 \<in> set evs; |
|
421 NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |] |
|
422 ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = |
|
423 (Nonce NB \<in> analz (knows Spy evs))" |
|
424 by (simp_all del: image_insert image_Un imp_disjL |
|
425 add: analz_image_freshK_simps split_ifs |
|
426 Nonce_secrecy Says_Server_KeyWithNonce); |
|
427 |
|
428 |
|
429 (*** The Nonce NB uniquely identifies B's message. ***) |
|
430 |
|
431 lemma unique_NB: |
|
432 "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs); |
|
433 Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs); |
|
434 evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |] |
|
435 ==> NA' = NA & A' = A & B' = B" |
|
436 apply (erule rev_mp, erule rev_mp) |
|
437 apply (erule yahalom.induct, force, |
|
438 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
439 (*Fake, and YM2 by freshness*) |
|
440 apply blast+ |
|
441 done |
|
442 |
|
443 |
|
444 (*Variant useful for proving secrecy of NB. Because nb is assumed to be |
|
445 secret, we no longer must assume B, B' not bad.*) |
|
446 lemma Says_unique_NB: |
|
447 "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
448 \<in> set evs; |
|
449 Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} |
|
450 \<in> set evs; |
|
451 nb \<notin> analz (knows Spy evs); evs \<in> yahalom |] |
|
452 ==> NA' = NA & A' = A & B' = B" |
|
453 by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad |
|
454 dest: Says_imp_spies unique_NB parts.Inj analz.Inj) |
|
455 |
|
456 |
|
457 (** A nonce value is never used both as NA and as NB **) |
|
458 |
|
459 lemma no_nonce_YM1_YM2: |
|
460 "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs); |
|
461 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
|
462 ==> Crypt (shrK B) {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)" |
|
463 apply (erule rev_mp, erule rev_mp) |
|
464 apply (erule yahalom.induct, force, |
|
465 frule_tac [6] YM4_parts_knows_Spy) |
|
466 apply (analz_mono_contra, simp_all) |
|
467 (*Fake, YM2*) |
|
468 apply blast+ |
|
469 done |
|
470 |
|
471 (*The Server sends YM3 only in response to YM2.*) |
|
472 lemma Says_Server_imp_YM2: |
|
473 "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs; |
|
474 evs \<in> yahalom |] |
|
475 ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} |
|
476 \<in> set evs" |
|
477 apply (erule rev_mp, erule yahalom.induct) |
|
478 apply auto |
|
479 done |
|
480 |
|
481 |
|
482 (*A vital theorem for B, that nonce NB remains secure from the Spy.*) |
|
483 lemma Spy_not_see_NB : |
|
484 "[| Says B Server |
|
485 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
486 \<in> set evs; |
|
487 (\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs); |
|
488 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
489 ==> Nonce NB \<notin> analz (knows Spy evs)" |
|
490 apply (erule rev_mp, erule rev_mp) |
|
491 apply (erule yahalom.induct, force, |
|
492 frule_tac [6] YM4_analz_knows_Spy) |
|
493 apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq |
|
494 analz_insert_freshK) |
|
495 (*Fake*) |
|
496 apply spy_analz |
|
497 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) |
|
498 apply blast |
|
499 (*YM2*) |
|
500 apply blast |
|
501 (*Prove YM3 by showing that no NB can also be an NA*) |
|
502 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) |
|
503 (** LEVEL 7: YM4 and Oops remain **) |
|
504 apply (clarify, simp add: all_conj_distrib) |
|
505 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) |
|
506 (*Case analysis on Aa:bad; PROOF FAILED problems |
|
507 use Says_unique_NB to identify message components: Aa=A, Ba=B*) |
|
508 apply (blast dest!: Says_unique_NB |
|
509 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] |
|
510 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 |
|
511 Spy_not_see_encrypted_key) |
|
512 (*Oops case: if the nonce is betrayed now, show that the Oops event is |
|
513 covered by the quantified Oops assumption.*) |
|
514 apply (clarify, simp add: all_conj_distrib) |
|
515 apply (frule Says_Server_imp_YM2, assumption) |
|
516 apply (case_tac "NB = NBa") |
|
517 (*If NB=NBa then all other components of the Oops message agree*) |
|
518 apply (blast dest: Says_unique_NB) |
|
519 (*case NB \<noteq> NBa*) |
|
520 apply (simp add: single_Nonce_secrecy) |
|
521 apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*)) |
|
522 done |
|
523 |
|
524 |
|
525 (*B's session key guarantee from YM4. The two certificates contribute to a |
|
526 single conclusion about the Server's message. Note that the "Notes Spy" |
|
527 assumption must quantify over \<forall>POSSIBLE keys instead of our particular K. |
|
528 If this run is broken and the spy substitutes a certificate containing an |
|
529 old key, B has no means of telling.*) |
|
530 lemma B_trusts_YM4: |
|
531 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
532 Crypt K (Nonce NB)|} \<in> set evs; |
|
533 Says B Server |
|
534 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
535 \<in> set evs; |
|
536 \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs; |
|
537 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
538 ==> Says Server A |
|
539 {|Crypt (shrK A) {|Agent B, Key K, |
|
540 Nonce NA, Nonce NB|}, |
|
541 Crypt (shrK B) {|Agent A, Key K|}|} |
|
542 \<in> set evs" |
|
543 by (blast dest: Spy_not_see_NB Says_unique_NB |
|
544 Says_Server_imp_YM2 B_trusts_YM4_newK) |
|
545 |
|
546 |
|
547 |
|
548 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) |
|
549 lemma B_gets_good_key: |
|
550 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
551 Crypt K (Nonce NB)|} \<in> set evs; |
|
552 Says B Server |
|
553 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
554 \<in> set evs; |
|
555 \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs; |
|
556 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
557 ==> Key K \<notin> analz (knows Spy evs)" |
|
558 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) |
|
559 |
|
560 |
|
561 (*** Authenticating B to A ***) |
|
562 |
|
563 (*The encryption in message YM2 tells us it cannot be faked.*) |
|
564 lemma B_Said_YM2 [rule_format]: |
|
565 "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs); |
|
566 evs \<in> yahalom|] |
|
567 ==> B \<notin> bad --> |
|
568 Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
569 \<in> set evs" |
|
570 apply (erule rev_mp, erule yahalom.induct, force, |
|
571 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
|
572 (*Fake*) |
|
573 apply blast |
|
574 done |
|
575 |
|
576 (*If the server sends YM3 then B sent YM2*) |
|
577 lemma YM3_auth_B_to_A_lemma: |
|
578 "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} |
|
579 \<in> set evs; evs \<in> yahalom|] |
|
580 ==> B \<notin> bad --> |
|
581 Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
582 \<in> set evs" |
|
583 apply (erule rev_mp, erule yahalom.induct, simp_all) |
|
584 (*YM3, YM4*) |
|
585 apply (blast dest!: B_Said_YM2)+ |
|
586 done |
|
587 |
|
588 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) |
|
589 lemma YM3_auth_B_to_A: |
|
590 "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} |
|
591 \<in> set evs; |
|
592 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
593 ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} |
|
594 \<in> set evs" |
|
595 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs) |
|
596 |
|
597 |
|
598 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
|
599 |
|
600 (*Assuming the session key is secure, if both certificates are present then |
|
601 A has said NB. We can't be sure about the rest of A's message, but only |
|
602 NB matters for freshness.*) |
|
603 lemma A_Said_YM3_lemma [rule_format]: |
|
604 "evs \<in> yahalom |
|
605 ==> Key K \<notin> analz (knows Spy evs) --> |
|
606 Crypt K (Nonce NB) \<in> parts (knows Spy evs) --> |
|
607 Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) --> |
|
608 B \<notin> bad --> |
|
609 (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)" |
|
610 apply (erule yahalom.induct, force, |
|
611 frule_tac [6] YM4_parts_knows_Spy) |
|
612 apply (analz_mono_contra, simp_all) |
|
613 (*Fake*) |
|
614 apply blast |
|
615 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) |
|
616 apply (force dest!: Crypt_imp_keysFor) |
|
617 (*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) |
|
618 apply (simp add: ex_disj_distrib) |
|
619 (*yes: apply unicity of session keys*) |
|
620 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK |
|
621 Crypt_Spy_analz_bad |
|
622 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) |
|
623 done |
|
624 |
|
625 (*If B receives YM4 then A has used nonce NB (and therefore is alive). |
|
626 Moreover, A associates K with NB (thus is talking about the same run). |
|
627 Other premises guarantee secrecy of K.*) |
|
628 lemma YM4_imp_A_Said_YM3 [rule_format]: |
|
629 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
|
630 Crypt K (Nonce NB)|} \<in> set evs; |
|
631 Says B Server |
|
632 {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} |
|
633 \<in> set evs; |
|
634 (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs); |
|
635 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] |
|
636 ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs" |
|
637 by (blast intro!: A_Said_YM3_lemma |
|
638 dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) |
79 |
639 |
80 end |
640 end |