|
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 |
|
13 open Kerberos_BAN; |
|
14 |
|
15 (* |
|
16 Confidentiality (secrecy) and authentication properties rely on |
|
17 temporal checks: strong guarantees in a little abstracted - but |
|
18 very realistic - model (see .thy). |
|
19 |
|
20 Total execution time: 158s |
|
21 *) |
|
22 |
|
23 proof_timing:=true; |
|
24 HOL_quantifiers := false; |
|
25 |
|
26 AddEs spies_partsEs; |
|
27 AddDs [impOfSubs analz_subset_parts]; |
|
28 AddDs [impOfSubs Fake_parts_insert]; |
|
29 |
|
30 AddSIs [SesKeyLife_LB, AutLife_LB]; |
|
31 |
|
32 Addsimps [SesKeyLife_LB, AutLife_LB]; |
|
33 |
|
34 |
|
35 (*A "possibility property": there are traces that reach the end.*) |
|
36 goal thy |
|
37 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
|
38 \ ==> EX Timestamp K. EX evs: kerberos_ban. \ |
|
39 \ Says B A (Crypt K (Number Timestamp)) \ |
|
40 \ : set evs"; |
|
41 by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
42 by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS |
|
43 kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); |
|
44 by possibility_tac; |
|
45 by (ALLGOALS (simp_tac (simpset() addsimps [leD]))); (*from NatDef.ML!!!!*) |
|
46 by (cut_facts_tac [SesKeyLife_LB] 1); |
|
47 by (trans_tac 1); |
|
48 result(); |
|
49 |
|
50 |
|
51 |
|
52 (**** Inductive proofs about kerberos_ban ****) |
|
53 |
|
54 (*Nobody sends themselves messages*) |
|
55 goal thy "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs"; |
|
56 by (etac kerberos_ban.induct 1); |
|
57 by Auto_tac; |
|
58 qed_spec_mp "not_Says_to_self"; |
|
59 Addsimps [not_Says_to_self]; |
|
60 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
61 |
|
62 |
|
63 (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*) |
|
64 goal thy "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \ |
|
65 \ ==> X : parts (spies evs)"; |
|
66 by (Blast_tac 1); |
|
67 qed "Kb3_msg_in_parts_spies"; |
|
68 |
|
69 goal thy |
|
70 "!!evs. Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \ |
|
71 \ ==> K : parts (spies evs)"; |
|
72 by (Blast_tac 1); |
|
73 qed "Oops_parts_spies"; |
|
74 |
|
75 (*For proving the easier theorems about X ~: parts (spies evs).*) |
|
76 fun parts_induct_tac i = |
|
77 etac kerberos_ban.induct i THEN |
|
78 forward_tac [Oops_parts_spies] (i+6) THEN |
|
79 forward_tac [Kb3_msg_in_parts_spies] (i+4) THEN |
|
80 prove_simple_subgoals_tac i; |
|
81 |
|
82 |
|
83 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
|
84 goal thy |
|
85 "!!evs. evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
|
86 by (parts_induct_tac 1); |
|
87 by (ALLGOALS Blast_tac); |
|
88 qed "Spy_see_shrK"; |
|
89 Addsimps [Spy_see_shrK]; |
|
90 |
|
91 |
|
92 goal thy |
|
93 "!!evs. evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
|
94 by Auto_tac; |
|
95 qed "Spy_analz_shrK"; |
|
96 Addsimps [Spy_analz_shrK]; |
|
97 |
|
98 goal thy "!!A. [| Key (shrK A) : parts (spies evs); \ |
|
99 \ evs : kerberos_ban |] ==> A:bad"; |
|
100 by (blast_tac (claset() addDs [Spy_see_shrK]) 1); |
|
101 qed "Spy_see_shrK_D"; |
|
102 |
|
103 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
|
104 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
|
105 |
|
106 |
|
107 (*Nobody can have used non-existent keys!*) |
|
108 goal thy "!!evs. evs : kerberos_ban ==> \ |
|
109 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
|
110 by (parts_induct_tac 1); |
|
111 (*Fake*) |
|
112 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
|
113 (*Kb2, Kb3, Kb4*) |
|
114 by (ALLGOALS Blast_tac); |
|
115 qed_spec_mp "new_keys_not_used"; |
|
116 |
|
117 bind_thm ("new_keys_not_analzd", |
|
118 [analz_subset_parts RS keysFor_mono, |
|
119 new_keys_not_used] MRS contra_subsetD); |
|
120 |
|
121 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
|
122 |
|
123 |
|
124 (** Lemmas concerning the form of items passed in messages **) |
|
125 |
|
126 (*Describes the form of K, X and K' when the Server sends this message.*) |
|
127 goal thy |
|
128 "!!evs. [| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \ |
|
129 \ : set evs; evs : kerberos_ban |] \ |
|
130 \ ==> K ~: range shrK & \ |
|
131 \ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \ |
|
132 \ K' = shrK A"; |
|
133 by (etac rev_mp 1); |
|
134 by (etac kerberos_ban.induct 1); |
|
135 by Auto_tac; |
|
136 qed "Says_Server_message_form"; |
|
137 |
|
138 |
|
139 (*If the encrypted message appears then it originated with the Server |
|
140 PROVIDED that A is NOT compromised! |
|
141 |
|
142 This shows implicitly the FRESHNESS OF THE SESSION KEY to A |
|
143 *) |
|
144 goal thy |
|
145 "!!evs. [| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ |
|
146 \ : parts (spies evs); \ |
|
147 \ A ~: bad; evs : kerberos_ban |] \ |
|
148 \ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
149 \ : set evs"; |
|
150 by (etac rev_mp 1); |
|
151 by (parts_induct_tac 1); |
|
152 by (Blast_tac 1); |
|
153 qed "A_trusts_K_by_Kb2"; |
|
154 |
|
155 |
|
156 (*If the TICKET appears then it originated with the Server*) |
|
157 (*FRESHNESS OF THE SESSION KEY to B*) |
|
158 goal thy |
|
159 "!!evs. [| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \ |
|
160 \ B ~: bad; evs : kerberos_ban |] \ |
|
161 \ ==> Says Server A \ |
|
162 \ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ |
|
163 \ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \ |
|
164 \ : set evs"; |
|
165 by (etac rev_mp 1); |
|
166 by (parts_induct_tac 1); |
|
167 by (Blast_tac 1); |
|
168 qed "B_trusts_K_by_Kb3"; |
|
169 |
|
170 |
|
171 (*EITHER describes the form of X when the following message is sent, |
|
172 OR reduces it to the Fake case. |
|
173 Use Says_Server_message_form if applicable.*) |
|
174 goal thy |
|
175 "!!evs. [| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
176 \ : set evs; \ |
|
177 \ evs : kerberos_ban |] \ |
|
178 \ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\ |
|
179 \ | X : analz (spies evs)"; |
|
180 by (case_tac "A : bad" 1); |
|
181 by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] |
|
182 addss (simpset())) 1); |
|
183 by (forward_tac [Says_imp_spies RS parts.Inj] 1); |
|
184 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, |
|
185 Says_Server_message_form]) 1); |
|
186 qed "Says_S_message_form"; |
|
187 |
|
188 |
|
189 (*For proofs involving analz.*) |
|
190 val analz_spies_tac = |
|
191 forward_tac [Says_Server_message_form] 7 THEN |
|
192 forward_tac [Says_S_message_form] 5 THEN |
|
193 REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); |
|
194 |
|
195 |
|
196 (**** |
|
197 The following is to prove theorems of the form |
|
198 |
|
199 Key K : analz (insert (Key KAB) (spies evs)) ==> |
|
200 Key K : analz (spies evs) |
|
201 |
|
202 A more general formula must be proved inductively. |
|
203 |
|
204 ****) |
|
205 |
|
206 |
|
207 (** Session keys are not used to encrypt other session keys **) |
|
208 |
|
209 goal thy |
|
210 "!!evs. evs : kerberos_ban ==> \ |
|
211 \ ALL K KK. KK <= Compl (range shrK) --> \ |
|
212 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
|
213 \ (K : KK | Key K : analz (spies evs))"; |
|
214 by (etac kerberos_ban.induct 1); |
|
215 by analz_spies_tac; |
|
216 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
|
217 by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
|
218 (*Takes 5 secs*) |
|
219 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
|
220 (*Fake*) |
|
221 by (spy_analz_tac 1); |
|
222 qed_spec_mp "analz_image_freshK"; |
|
223 |
|
224 |
|
225 goal thy |
|
226 "!!evs. [| evs : kerberos_ban; KAB ~: range shrK |] ==> \ |
|
227 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
|
228 \ (K = KAB | Key K : analz (spies evs))"; |
|
229 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
|
230 qed "analz_insert_freshK"; |
|
231 |
|
232 |
|
233 (** The session key K uniquely identifies the message **) |
|
234 |
|
235 goal thy |
|
236 "!!evs. evs : kerberos_ban ==> \ |
|
237 \ EX A' Ts' B' X'. ALL A Ts B X. \ |
|
238 \ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
239 \ : set evs \ |
|
240 \ --> A=A' & Ts=Ts' & B=B' & X=X'"; |
|
241 by (etac kerberos_ban.induct 1); |
|
242 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
243 by Safe_tac; |
|
244 (*Kb2: it can't be a new key*) |
|
245 by (expand_case_tac "K = ?y" 1); |
|
246 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
|
247 by (blast_tac (claset() delrules [conjI]) 1); |
|
248 val lemma = result(); |
|
249 |
|
250 (*In messages of this form, the session key uniquely identifies the rest*) |
|
251 goal thy |
|
252 "!!evs. [| Says Server A \ |
|
253 \ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ |
|
254 \ Says Server A' \ |
|
255 \ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\ |
|
256 \ evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"; |
|
257 by (prove_unique_tac lemma 1); |
|
258 qed "unique_session_keys"; |
|
259 |
|
260 |
|
261 (** Lemma: the session key sent in msg Kb2 would be EXPIRED |
|
262 if the spy could see it! |
|
263 **) |
|
264 |
|
265 goal thy |
|
266 "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] \ |
|
267 \ ==> Says Server A \ |
|
268 \ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ |
|
269 \ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ |
|
270 \ : set evs --> \ |
|
271 \ Key K : analz (spies evs) --> Expired Ts evs"; |
|
272 by (etac kerberos_ban.induct 1); |
|
273 by analz_spies_tac; |
|
274 by (ALLGOALS |
|
275 (asm_simp_tac (simpset() |
|
276 addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes @ split_ifs)))); |
|
277 (*Oops*) |
|
278 by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4); |
|
279 (*Kb2*) |
|
280 by (fast_tac (claset() addIs [parts_insertI, less_SucI]) 2); |
|
281 (*Fake*) |
|
282 by (spy_analz_tac 1); |
|
283 (**LEVEL 6 **) |
|
284 by (clarify_tac (claset() delrules [impCE]) 1); |
|
285 by (case_tac "Ba : bad" 1); |
|
286 by (blast_tac (claset() addIs [less_SucI]) 2); |
|
287 (**LEVEL 9**) |
|
288 by (rotate_tac 10 1); |
|
289 by (forward_tac [mp] 1 THEN assume_tac 1); |
|
290 by (etac disjE 1); |
|
291 by (blast_tac (claset() addIs [less_SucI]) 2); |
|
292 (**LEVEL 13**) |
|
293 by (Clarify_tac 1); |
|
294 by (case_tac "Aa : bad" 1); |
|
295 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, |
|
296 A_trusts_K_by_Kb2, unique_session_keys]) 2); |
|
297 (**LEVEL 16**) |
|
298 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS |
|
299 Crypt_Spy_analz_bad RS analz.Snd RS |
|
300 analz.Snd RS analz.Fst] |
|
301 addIs [less_SucI]) 1); |
|
302 val lemma = result() RS mp RS mp RSN(1,rev_notE); |
|
303 |
|
304 |
|
305 (** CONFIDENTIALITY for the SERVER: |
|
306 Spy does not see the keys sent in msg Kb2 |
|
307 as long as they have NOT EXPIRED |
|
308 **) |
|
309 goal thy |
|
310 "!!evs. [| Says Server A \ |
|
311 \ (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs; \ |
|
312 \ ~ Expired T evs; \ |
|
313 \ A ~: bad; B ~: bad; evs : kerberos_ban \ |
|
314 \ |] ==> Key K ~: analz (spies evs)"; |
|
315 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
|
316 by (Clarify_tac 1); |
|
317 by (rtac ccontr 1); |
|
318 by (blast_tac (claset() addSEs [lemma]) 1); |
|
319 qed "Confidentiality_S"; |
|
320 |
|
321 (**** THE COUNTERPART OF CONFIDENTIALITY |
|
322 [|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs) |
|
323 WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) |
|
324 |
|
325 |
|
326 (** CONFIDENTIALITY for ALICE: **) |
|
327 (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **) |
|
328 goal thy |
|
329 "!!evs. [| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\ |
|
330 \ ~ Expired T evs; \ |
|
331 \ A ~: bad; B ~: bad; evs : kerberos_ban \ |
|
332 \ |] ==> Key K ~: analz (spies evs)"; |
|
333 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, |
|
334 Confidentiality_S]) 1); |
|
335 qed "Confidentiality_A"; |
|
336 |
|
337 |
|
338 (** CONFIDENTIALITY for BOB: **) |
|
339 (** Also B_trusts_K_by_Kb3 RS Confidentiality_S **) |
|
340 goal thy |
|
341 "!!evs. [| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \ |
|
342 \ : parts (spies evs); \ |
|
343 \ ~ Expired Tk evs; \ |
|
344 \ A ~: bad; B ~: bad; evs : kerberos_ban \ |
|
345 \ |] ==> Key K ~: analz (spies evs)"; |
|
346 by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, |
|
347 Confidentiality_S]) 1); |
|
348 qed "Confidentiality_B"; |
|
349 |
|
350 |
|
351 goal thy |
|
352 "!!evs. [| B ~: bad; evs : kerberos_ban |] \ |
|
353 \ ==> Key K ~: analz (spies evs) --> \ |
|
354 \ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
355 \ : set evs --> \ |
|
356 \ Crypt K (Number Ta) : parts (spies evs) --> \ |
|
357 \ Says B A (Crypt K (Number Ta)) : set evs"; |
|
358 by (etac kerberos_ban.induct 1); |
|
359 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
360 by (dtac Kb3_msg_in_parts_spies 5); |
|
361 by (forward_tac [Oops_parts_spies] 7); |
|
362 by (TRYALL (rtac impI)); |
|
363 by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD))); |
|
364 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
365 (**LEVEL 7**) |
|
366 by (Blast_tac 1); |
|
367 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); |
|
368 (* |
|
369 Subgoal 1: contradiction from the assumptions |
|
370 Key K ~: used evs2 and Crypt K (Number Ta) : parts (spies evs2) |
|
371 *) |
|
372 by (dtac Crypt_imp_invKey_keysFor 1); |
|
373 by (Asm_full_simp_tac 1); |
|
374 (* the two tactics above detectthe contradiction*) |
|
375 by (rtac disjI1 1); |
|
376 by (thin_tac "?PP-->?QQ" 1); (*deletes the matching assumptions*) |
|
377 by (case_tac "Ba : bad" 1); (*splits up the subgoal by the stated case*) |
|
378 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS |
|
379 B_trusts_K_by_Kb3, |
|
380 unique_session_keys]) 2); |
|
381 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS |
|
382 Crypt_Spy_analz_bad]) 1); |
|
383 val lemma_B = result(); |
|
384 |
|
385 |
|
386 (*AUTHENTICATION OF B TO A*) |
|
387 goal thy |
|
388 "!!evs. [| Crypt K (Number Ta) : parts (spies evs); \ |
|
389 \ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ |
|
390 \ : parts (spies evs); \ |
|
391 \ ~ Expired Ts evs; \ |
|
392 \ A ~: bad; B ~: bad; evs : kerberos_ban |] \ |
|
393 \ ==> Says B A (Crypt K (Number Ta)) : set evs"; |
|
394 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2] |
|
395 addSIs [lemma_B RS mp RS mp RS mp] |
|
396 addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); |
|
397 qed "Authentication_B"; |
|
398 |
|
399 |
|
400 goal thy |
|
401 "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] ==> \ |
|
402 \ Key K ~: analz (spies evs) --> \ |
|
403 \ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
|
404 \ : set evs --> \ |
|
405 \ Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\ |
|
406 \ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \ |
|
407 \ : set evs"; |
|
408 by (etac kerberos_ban.induct 1); |
|
409 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
410 by (forward_tac [Kb3_msg_in_parts_spies] 5); |
|
411 by (forward_tac [Oops_parts_spies] 7); |
|
412 by (TRYALL (rtac impI)); |
|
413 by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD))); |
|
414 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
415 (**LEVEL 7**) |
|
416 by (Blast_tac 1); |
|
417 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); |
|
418 by (dtac Crypt_imp_invKey_keysFor 1); |
|
419 by (Asm_full_simp_tac 1); |
|
420 by (rtac disjI1 1); |
|
421 (*Last Subgoal! ...to be refined...*) |
|
422 by (thin_tac "Says ?A Server ?X : set evs3" 1); |
|
423 by (dresolve_tac [Says_imp_spies RS parts.Inj] 1); |
|
424 by (dresolve_tac [Says_imp_spies RS parts.Inj] 1); |
|
425 by (dtac A_trusts_K_by_Kb2 1); |
|
426 by (assume_tac 1); |
|
427 by (assume_tac 1); |
|
428 by (dtac A_trusts_K_by_Kb2 1); |
|
429 by (assume_tac 1); |
|
430 by (assume_tac 1); |
|
431 by (dtac unique_session_keys 1); |
|
432 by (assume_tac 1); |
|
433 by (assume_tac 1); |
|
434 by (Blast_tac 1); |
|
435 val lemma_A = result(); |
|
436 |
|
437 |
|
438 (*AUTHENTICATION OF A TO B*) |
|
439 goal thy |
|
440 "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \ |
|
441 \ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ |
|
442 \ : parts (spies evs); \ |
|
443 \ ~ Expired Ts evs; \ |
|
444 \ A ~: bad; B ~: bad; evs : kerberos_ban |] \ |
|
445 \ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \ |
|
446 \ Crypt K {|Agent A, Number Ta|}|} : set evs"; |
|
447 by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3] |
|
448 addSIs [lemma_A RS mp RS mp RS mp] |
|
449 addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); |
|
450 qed "Authentication_A"; |