1 (* Title: HOL/Auth/Kerberos_BAN |
|
2 ID: $Id$ |
|
3 Author: Giampaolo Bella, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 The Kerberos protocol, BAN version. |
|
7 |
|
8 From page 251 of |
|
9 Burrows, Abadi and Needham. A Logic of Authentication. |
|
10 Proc. Royal Soc. 426 (1989) |
|
11 |
|
12 Confidentiality (secrecy) and authentication properties rely on |
|
13 temporal checks: strong guarantees in a little abstracted - but |
|
14 very realistic - model (see .thy). |
|
15 |
|
16 Tidied by lcp. |
|
17 *) |
|
18 |
|
19 AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
|
20 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
|
21 |
|
22 AddIffs [SesKeyLife_LB, AutLife_LB]; |
|
23 |
|
24 |
|
25 (*A "possibility property": there are traces that reach the end.*) |
|
26 Goal "\\<exists>Timestamp K. \\<exists>evs \\<in> kerberos_ban. \ |
|
27 \ Says B A (Crypt K (Number Timestamp)) \ |
|
28 \ \\<in> set evs"; |
|
29 by (cut_facts_tac [SesKeyLife_LB] 1); |
|
30 by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
31 by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS |
|
32 kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); |
|
33 by possibility_tac; |
|
34 by (ALLGOALS Asm_simp_tac); |
|
35 result(); |
|
36 |
|
37 |
|
38 |
|
39 (**** Inductive proofs about kerberos_ban ****) |
|
40 |
|
41 (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*) |
|
42 Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) \\<in> set evs \ |
|
43 \ ==> X \\<in> parts (spies evs)"; |
|
44 by (Blast_tac 1); |
|
45 qed "Kb3_msg_in_parts_spies"; |
|
46 |
|
47 Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \\<in> set evs \ |
|
48 \ ==> K \\<in> parts (spies evs)"; |
|
49 by (Blast_tac 1); |
|
50 qed "Oops_parts_spies"; |
|
51 |
|
52 (*For proving the easier theorems about X \\<notin> parts (spies evs).*) |
|
53 fun parts_induct_tac i = |
|
54 etac kerberos_ban.induct i THEN |
|
55 ftac Oops_parts_spies (i+6) THEN |
|
56 ftac Kb3_msg_in_parts_spies (i+4) THEN |
|
57 prove_simple_subgoals_tac i; |
|
58 |
|
59 |
|
60 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
|
61 Goal "evs \\<in> kerberos_ban ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"; |
|
62 by (parts_induct_tac 1); |
|
63 by (ALLGOALS Blast_tac); |
|
64 qed "Spy_see_shrK"; |
|
65 Addsimps [Spy_see_shrK]; |
|
66 |
|
67 |
|
68 Goal "evs \\<in> kerberos_ban ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"; |
|
69 by Auto_tac; |
|
70 qed "Spy_analz_shrK"; |
|
71 Addsimps [Spy_analz_shrK]; |
|
72 |
|
73 Goal "[| Key (shrK A) \\<in> parts (spies evs); \ |
|
74 \ evs \\<in> kerberos_ban |] ==> A:bad"; |
|
75 by (blast_tac (claset() addDs [Spy_see_shrK]) 1); |
|
76 qed "Spy_see_shrK_D"; |
|
77 |
|
78 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
|
79 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
|
80 |
|
81 |
|
82 (*Nobody can have used non-existent keys!*) |
|
83 Goal "evs \\<in> kerberos_ban ==> \ |
|
84 \ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))"; |
|
85 by (parts_induct_tac 1); |
|
86 (*Fake*) |
|
87 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
|
88 (*Kb2, Kb3, Kb4*) |
|
89 by (ALLGOALS Blast_tac); |
|
90 qed_spec_mp "new_keys_not_used"; |
|
91 Addsimps [new_keys_not_used]; |
|
92 |
|
93 (** Lemmas concerning the form of items passed in messages **) |
|
94 |
|
95 (*Describes the form of K, X and K' when the Server sends this message.*) |
|
96 Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \ |
|
97 \ \\<in> set evs; evs \\<in> kerberos_ban |] \ |
|
98 \ ==> K \\<notin> range shrK & \ |
|
99 \ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \ |
|
100 \ K' = shrK A"; |
|
101 by (etac rev_mp 1); |
|
102 by (etac kerberos_ban.induct 1); |
|
103 by Auto_tac; |
|
104 qed "Says_Server_message_form"; |
|
105 |
|
106 |
|
107 (*If the encrypted message appears then it originated with the Server |
|
108 PROVIDED that A is NOT compromised! |
|
109 |
|
110 This shows implicitly the FRESHNESS OF THE SESSION KEY to A |
|
111 *) |
|
112 Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ |
|
113 \ \\<in> parts (spies evs); \ |
|
114 \ A \\<notin> bad; evs \\<in> kerberos_ban |] \ |
|
115 \ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
116 \ \\<in> set evs"; |
|
117 by (etac rev_mp 1); |
|
118 by (parts_induct_tac 1); |
|
119 by (Blast_tac 1); |
|
120 qed "A_trusts_K_by_Kb2"; |
|
121 |
|
122 |
|
123 (*If the TICKET appears then it originated with the Server*) |
|
124 (*FRESHNESS OF THE SESSION KEY to B*) |
|
125 Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \\<in> parts (spies evs); \ |
|
126 \ B \\<notin> bad; evs \\<in> kerberos_ban |] \ |
|
127 \ ==> Says Server A \ |
|
128 \ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ |
|
129 \ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \ |
|
130 \ \\<in> set evs"; |
|
131 by (etac rev_mp 1); |
|
132 by (parts_induct_tac 1); |
|
133 by (Blast_tac 1); |
|
134 qed "B_trusts_K_by_Kb3"; |
|
135 |
|
136 |
|
137 (*EITHER describes the form of X when the following message is sent, |
|
138 OR reduces it to the Fake case. |
|
139 Use Says_Server_message_form if applicable.*) |
|
140 Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
141 \ \\<in> set evs; \ |
|
142 \ evs \\<in> kerberos_ban |] \ |
|
143 \==> (K \\<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\ |
|
144 \ | X \\<in> analz (spies evs)"; |
|
145 by (case_tac "A \\<in> bad" 1); |
|
146 by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] |
|
147 addss (simpset())) 1); |
|
148 by (forward_tac [Says_imp_spies RS parts.Inj] 1); |
|
149 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, |
|
150 Says_Server_message_form]) 1); |
|
151 qed "Says_S_message_form"; |
|
152 |
|
153 |
|
154 (*For proofs involving analz.*) |
|
155 val analz_spies_tac = |
|
156 ftac Says_Server_message_form 7 THEN |
|
157 ftac Says_S_message_form 5 THEN |
|
158 REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); |
|
159 |
|
160 |
|
161 (**** |
|
162 The following is to prove theorems of the form |
|
163 |
|
164 Key K \\<in> analz (insert (Key KAB) (spies evs)) ==> |
|
165 Key K \\<in> analz (spies evs) |
|
166 |
|
167 A more general formula must be proved inductively. |
|
168 |
|
169 ****) |
|
170 |
|
171 |
|
172 (** Session keys are not used to encrypt other session keys **) |
|
173 |
|
174 Goal "evs \\<in> kerberos_ban ==> \ |
|
175 \ \\<forall>K KK. KK <= - (range shrK) --> \ |
|
176 \ (Key K \\<in> analz (Key`KK Un (spies evs))) = \ |
|
177 \ (K \\<in> KK | Key K \\<in> analz (spies evs))"; |
|
178 by (etac kerberos_ban.induct 1); |
|
179 by analz_spies_tac; |
|
180 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
|
181 by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
|
182 (*Takes 5 secs*) |
|
183 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
|
184 (*Fake*) |
|
185 by (spy_analz_tac 1); |
|
186 qed_spec_mp "analz_image_freshK"; |
|
187 |
|
188 |
|
189 Goal "[| evs \\<in> kerberos_ban; KAB \\<notin> range shrK |] ==> \ |
|
190 \ (Key K \\<in> analz (insert (Key KAB) (spies evs))) = \ |
|
191 \ (K = KAB | Key K \\<in> analz (spies evs))"; |
|
192 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
|
193 qed "analz_insert_freshK"; |
|
194 |
|
195 |
|
196 (** The session key K uniquely identifies the message **) |
|
197 |
|
198 Goal "[| Says Server A \ |
|
199 \ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \\<in> set evs; \ |
|
200 \ Says Server A' \ |
|
201 \ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \\<in> set evs;\ |
|
202 \ evs \\<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"; |
|
203 by (etac rev_mp 1); |
|
204 by (etac rev_mp 1); |
|
205 by (parts_induct_tac 1); |
|
206 (*Kb2: it can't be a new key*) |
|
207 by (Blast_tac 1); |
|
208 qed "unique_session_keys"; |
|
209 |
|
210 |
|
211 (** Lemma: the session key sent in msg Kb2 would be EXPIRED |
|
212 if the spy could see it! |
|
213 **) |
|
214 |
|
215 Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] \ |
|
216 \ ==> Says Server A \ |
|
217 \ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ |
|
218 \ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ |
|
219 \ \\<in> set evs --> \ |
|
220 \ Key K \\<in> analz (spies evs) --> Expired Ts evs"; |
|
221 by (etac kerberos_ban.induct 1); |
|
222 by analz_spies_tac; |
|
223 by (ALLGOALS |
|
224 (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq, |
|
225 analz_insert_freshK] @ pushes))); |
|
226 (*Oops: PROOF FAILED if addIs below*) |
|
227 by (blast_tac (claset() addDs [unique_session_keys] addSIs [less_SucI]) 4); |
|
228 (*Kb2*) |
|
229 by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2); |
|
230 (*Fake*) |
|
231 by (spy_analz_tac 1); |
|
232 (**LEVEL 6 **) |
|
233 (*Kb3*) |
|
234 by (case_tac "Aa \\<in> bad" 1); |
|
235 by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2); |
|
236 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, |
|
237 Crypt_Spy_analz_bad, analz.Fst, analz.Snd] |
|
238 addIs [less_SucI]) 1); |
|
239 qed_spec_mp "lemma2"; |
|
240 |
|
241 |
|
242 (** CONFIDENTIALITY for the SERVER: |
|
243 Spy does not see the keys sent in msg Kb2 |
|
244 as long as they have NOT EXPIRED |
|
245 **) |
|
246 Goal "[| Says Server A \ |
|
247 \ (Crypt K' {|Number T, Agent B, Key K, X|}) \\<in> set evs; \ |
|
248 \ ~ Expired T evs; \ |
|
249 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban \ |
|
250 \ |] ==> Key K \\<notin> analz (spies evs)"; |
|
251 by (ftac Says_Server_message_form 1 THEN assume_tac 1); |
|
252 by (blast_tac (claset() addIs [lemma2]) 1); |
|
253 qed "Confidentiality_S"; |
|
254 |
|
255 (**** THE COUNTERPART OF CONFIDENTIALITY |
|
256 [|...; Expired Ts evs; ...|] ==> Key K \\<in> analz (spies evs) |
|
257 WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) |
|
258 |
|
259 |
|
260 (** CONFIDENTIALITY for ALICE: **) |
|
261 (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **) |
|
262 Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \\<in> parts (spies evs);\ |
|
263 \ ~ Expired T evs; \ |
|
264 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban \ |
|
265 \ |] ==> Key K \\<notin> analz (spies evs)"; |
|
266 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1); |
|
267 qed "Confidentiality_A"; |
|
268 |
|
269 |
|
270 (** CONFIDENTIALITY for BOB: **) |
|
271 (** Also B_trusts_K_by_Kb3 RS Confidentiality_S **) |
|
272 Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \ |
|
273 \ \\<in> parts (spies evs); \ |
|
274 \ ~ Expired Tk evs; \ |
|
275 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban \ |
|
276 \ |] ==> Key K \\<notin> analz (spies evs)"; |
|
277 by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, |
|
278 Confidentiality_S]) 1); |
|
279 qed "Confidentiality_B"; |
|
280 |
|
281 |
|
282 Goal "[| B \\<notin> bad; evs \\<in> kerberos_ban |] \ |
|
283 \ ==> Key K \\<notin> analz (spies evs) --> \ |
|
284 \ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
285 \ \\<in> set evs --> \ |
|
286 \ Crypt K (Number Ta) \\<in> parts (spies evs) --> \ |
|
287 \ Says B A (Crypt K (Number Ta)) \\<in> set evs"; |
|
288 by (etac kerberos_ban.induct 1); |
|
289 by (ftac Says_S_message_form 5 THEN assume_tac 5); |
|
290 by (dtac Kb3_msg_in_parts_spies 5); |
|
291 by (ftac Oops_parts_spies 7); |
|
292 by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); |
|
293 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
294 (**LEVEL 6**) |
|
295 by (Blast_tac 1); |
|
296 by (Clarify_tac 1); |
|
297 (* |
|
298 Subgoal 1: contradiction from the assumptions |
|
299 Key K \\<notin> used evs2 and Crypt K (Number Ta) \\<in> parts (spies evs2) |
|
300 *) |
|
301 by (dtac Crypt_imp_invKey_keysFor 1); |
|
302 by (Asm_full_simp_tac 1); |
|
303 (* the two tactics above detect the contradiction*) |
|
304 by (case_tac "Ba \\<in> bad" 1); (*splits up the subgoal by the stated case*) |
|
305 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS |
|
306 B_trusts_K_by_Kb3, |
|
307 unique_session_keys]) 2); |
|
308 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS |
|
309 Crypt_Spy_analz_bad]) 1); |
|
310 val lemma_B = result(); |
|
311 |
|
312 |
|
313 (*AUTHENTICATION OF B TO A*) |
|
314 Goal "[| Crypt K (Number Ta) \\<in> parts (spies evs); \ |
|
315 \ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ |
|
316 \ \\<in> parts (spies evs); \ |
|
317 \ ~ Expired Ts evs; \ |
|
318 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] \ |
|
319 \ ==> Says B A (Crypt K (Number Ta)) \\<in> set evs"; |
|
320 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2] |
|
321 addSIs [lemma_B RS mp RS mp RS mp] |
|
322 addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); |
|
323 qed "Authentication_B"; |
|
324 |
|
325 |
|
326 Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] ==> \ |
|
327 \ Key K \\<notin> analz (spies evs) --> \ |
|
328 \ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
329 \ \\<in> set evs --> \ |
|
330 \ Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs) -->\ |
|
331 \ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \ |
|
332 \ \\<in> set evs"; |
|
333 by (etac kerberos_ban.induct 1); |
|
334 by (ftac Says_S_message_form 5 THEN assume_tac 5); |
|
335 by (ftac Kb3_msg_in_parts_spies 5); |
|
336 by (ftac Oops_parts_spies 7); |
|
337 by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); |
|
338 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
339 (**LEVEL 6**) |
|
340 by (Blast_tac 1); |
|
341 by (Clarify_tac 1); |
|
342 by (dtac Crypt_imp_invKey_keysFor 1); |
|
343 by (Asm_full_simp_tac 1); |
|
344 by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1); |
|
345 val lemma_A = result(); |
|
346 |
|
347 |
|
348 (*AUTHENTICATION OF A TO B*) |
|
349 Goal "[| Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs); \ |
|
350 \ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ |
|
351 \ \\<in> parts (spies evs); \ |
|
352 \ ~ Expired Ts evs; \ |
|
353 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] \ |
|
354 \ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \ |
|
355 \ Crypt K {|Agent A, Number Ta|}|} \\<in> set evs"; |
|
356 by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3] |
|
357 addSIs [lemma_A RS mp RS mp RS mp] |
|
358 addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); |
|
359 qed "Authentication_A"; |
|