6452

1 
(* Title: HOL/Auth/KerberosIV


2 
ID: $Id$


3 
Author: Giampaolo Bella, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
The Kerberos protocol, version IV.


7 
*)


8 


9 
Pretty.setdepth 20;


10 
proof_timing:=true;


11 


12 
AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];


13 


14 


15 
(** Reversed traces **)


16 


17 
Goal "spies (evs @ [Says A B X]) = insert X (spies evs)";


18 
by (induct_tac "evs" 1);


19 
by (induct_tac "a" 2);


20 
by Auto_tac;


21 
qed "spies_Says_rev";


22 


23 
Goal "spies (evs @ [Gets A X]) = spies evs";


24 
by (induct_tac "evs" 1);


25 
by (induct_tac "a" 2);


26 
by Auto_tac;


27 
qed "spies_Gets_rev";


28 


29 
Goal "spies (evs @ [Notes A X]) = \


30 
\ (if A:bad then insert X (spies evs) else spies evs)";


31 
by (induct_tac "evs" 1);


32 
by (induct_tac "a" 2);


33 
by Auto_tac;


34 
qed "spies_Notes_rev";


35 


36 
Goal "spies evs = spies (rev evs)";


37 
by (induct_tac "evs" 1);


38 
by (induct_tac "a" 2);


39 
by (ALLGOALS


40 
(asm_simp_tac (simpset() addsimps [spies_Says_rev, spies_Gets_rev,


41 
spies_Notes_rev])));


42 
qed "spies_evs_rev";


43 
bind_thm ("parts_spies_evs_revD2", spies_evs_rev RS equalityD2 RS parts_mono);


44 


45 
Goal "spies (takeWhile P evs) <= spies evs";


46 
by (induct_tac "evs" 1);


47 
by (induct_tac "a" 2);


48 
by Auto_tac;


49 
(* Resembles "used_subset_append" in Event.ML*)


50 
qed "spies_takeWhile";


51 
bind_thm ("parts_spies_takeWhile_mono", spies_takeWhile RS parts_mono);


52 


53 
Goal "~P(x) > takeWhile P (xs @ [x]) = takeWhile P xs";


54 
by (induct_tac "xs" 1);


55 
by Auto_tac;


56 
qed "takeWhile_tail";


57 


58 


59 
(*****************LEMMAS ABOUT AuthKeys****************)


60 


61 
Goalw [AuthKeys_def] "AuthKeys [] = {}";


62 
by (Simp_tac 1);


63 
qed "AuthKeys_empty";


64 


65 
Goalw [AuthKeys_def]


66 
"(ALL A Tk akey Peer. \


67 
\ ev ~= Says Kas A (Crypt (shrK A) {akey, Agent Peer, Tk, \


68 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, akey, Tk})}))\


69 
\ ==> AuthKeys (ev # evs) = AuthKeys evs";


70 
by Auto_tac;


71 
qed "AuthKeys_not_insert";


72 


73 
Goalw [AuthKeys_def]


74 
"AuthKeys \


75 
\ (Says Kas A (Crypt (shrK A) {Key K, Agent Peer, Number Tk, \


76 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, Key K, Number Tk})}) # evs) \


77 
\ = insert K (AuthKeys evs)";


78 
by Auto_tac;


79 
qed "AuthKeys_insert";


80 


81 
Goalw [AuthKeys_def]


82 
"K : AuthKeys \


83 
\ (Says Kas A (Crypt (shrK A) {Key K', Agent Peer, Number Tk, \


84 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, Key K', Number Tk})}) # evs) \


85 
\ ==> K = K'  K : AuthKeys evs";


86 
by Auto_tac;


87 
qed "AuthKeys_simp";


88 


89 
Goalw [AuthKeys_def]


90 
"Says Kas A (Crypt (shrK A) {Key K, Agent Tgs, Number Tk, \


91 
\ (Crypt (shrK Tgs) {Agent A, Agent Tgs, Key K, Number Tk})}) : set evs \


92 
\ ==> K : AuthKeys evs";


93 
by Auto_tac;


94 
qed "AuthKeysI";


95 


96 
Goalw [AuthKeys_def] "K : AuthKeys evs ==> Key K : used evs";


97 
by (Simp_tac 1);


98 
by (blast_tac (claset() addSEs spies_partsEs) 1);


99 
qed "AuthKeys_used";


100 


101 


102 
(**** FORWARDING LEMMAS ****)


103 


104 
(*For reasoning about the encrypted portion of message K3*)


105 
Goal "Says Kas' A (Crypt KeyA {AuthKey, Peer, Tk, AuthTicket}) \


106 
\ : set evs ==> AuthTicket : parts (spies evs)";


107 
by (blast_tac (claset() addSEs spies_partsEs) 1);


108 
qed "K3_msg_in_parts_spies";


109 


110 
Goal "Says Kas A (Crypt KeyA {AuthKey, Peer, Tk, AuthTicket}) \


111 
\ : set evs ==> AuthKey : parts (spies evs)";


112 
by (blast_tac (claset() addSEs spies_partsEs) 1);


113 
qed "Oops_parts_spies1";


114 


115 
Goal "[ Says Kas A (Crypt KeyA {Key AuthKey, Peer, Tk, AuthTicket}) \


116 
\ : set evs ;\


117 
\ evs : kerberos ] ==> AuthKey ~: range shrK";


118 
by (etac rev_mp 1);


119 
by (etac kerberos.induct 1);


120 
by Auto_tac;


121 
qed "Oops_range_spies1";


122 


123 
(*For reasoning about the encrypted portion of message K5*)


124 
Goal "Says Tgs' A (Crypt AuthKey {ServKey, Agent B, Tt, ServTicket})\


125 
\ : set evs ==> ServTicket : parts (spies evs)";


126 
by (blast_tac (claset() addSEs spies_partsEs) 1);


127 
qed "K5_msg_in_parts_spies";


128 


129 
Goal "Says Tgs A (Crypt AuthKey {ServKey, Agent B, Tt, ServTicket})\


130 
\ : set evs ==> ServKey : parts (spies evs)";


131 
by (blast_tac (claset() addSEs spies_partsEs) 1);


132 
qed "Oops_parts_spies2";


133 


134 
Goal "[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket}) \


135 
\ : set evs ;\


136 
\ evs : kerberos ] ==> ServKey ~: range shrK";


137 
by (etac rev_mp 1);


138 
by (etac kerberos.induct 1);


139 
by Auto_tac;


140 
qed "Oops_range_spies2";


141 


142 
Goal "Says S A (Crypt K {SesKey, B, TimeStamp, Ticket}) : set evs \


143 
\ ==> Ticket : parts (spies evs)";


144 
by (blast_tac (claset() addSEs spies_partsEs) 1);


145 
qed "Says_ticket_in_parts_spies";


146 
(*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*)


147 


148 
fun parts_induct_tac i =


149 
etac kerberos.induct i THEN


150 
REPEAT (FIRSTGOAL analz_mono_contra_tac) THEN


151 
forward_tac [K3_msg_in_parts_spies] (i+4) THEN


152 
forward_tac [K5_msg_in_parts_spies] (i+6) THEN


153 
forward_tac [Oops_parts_spies1] (i+8) THEN


154 
forward_tac [Oops_parts_spies2] (i+9) THEN


155 
prove_simple_subgoals_tac 1;


156 


157 


158 
(*Spy never sees another agent's shared key! (unless it's lost at start)*)


159 
Goal "evs : kerberos ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";


160 
by (parts_induct_tac 1);


161 
by (Fake_parts_insert_tac 1);


162 
by (ALLGOALS Blast_tac);


163 
qed "Spy_see_shrK";


164 
Addsimps [Spy_see_shrK];


165 


166 
Goal "evs : kerberos ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";


167 
by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset()));


168 
qed "Spy_analz_shrK";


169 
Addsimps [Spy_analz_shrK];


170 


171 
Goal "[ Key (shrK A) : parts (spies evs); evs : kerberos ] ==> A:bad";


172 
by (blast_tac (claset() addDs [Spy_see_shrK]) 1);


173 
qed "Spy_see_shrK_D";


174 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);


175 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];


176 


177 
(*Nobody can have used nonexistent keys!*)


178 
Goal "evs : kerberos ==> \


179 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))";


180 
by (parts_induct_tac 1);


181 
(*Fake*)


182 
by (best_tac


183 
(claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]


184 
addIs [impOfSubs analz_subset_parts]


185 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]


186 
addss (simpset())) 1);


187 
(*Others*)


188 
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));


189 
qed_spec_mp "new_keys_not_used";


190 


191 
bind_thm ("new_keys_not_analzd",


192 
[analz_subset_parts RS keysFor_mono,


193 
new_keys_not_used] MRS contra_subsetD);


194 


195 
Addsimps [new_keys_not_used, new_keys_not_analzd];


196 


197 


198 
(*********************** REGULARITY LEMMAS ***********************)


199 
(* concerning the form of items passed in messages *)


200 
(*****************************************************************)


201 


202 
(*Describes the form of AuthKey, AuthTicket, and K sent by Kas*)


203 
Goal "[ Says Kas A (Crypt K {Key AuthKey, Agent Peer, Tk, AuthTicket}) \


204 
\ : set evs; \


205 
\ evs : kerberos ] \


206 
\ ==> AuthKey ~: range shrK & AuthKey : AuthKeys evs & \


207 
\ AuthTicket = (Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk} ) &\


208 
\ K = shrK A & Peer = Tgs";


209 
by (etac rev_mp 1);


210 
by (etac kerberos.induct 1);


211 
by (ALLGOALS (simp_tac (simpset() addsimps [AuthKeys_def, AuthKeys_insert])));


212 
by (ALLGOALS Blast_tac);


213 
qed "Says_Kas_message_form";


214 


215 
(*This lemma is essential for proving Says_Tgs_message_form:


216 


217 
the session key AuthKey


218 
supplied by Kas in the authentication ticket


219 
cannot be a longterm key!


220 


221 
Generalised to any session keys (both AuthKey and ServKey).


222 
*)


223 
Goal "[ Crypt (shrK Tgs_B) {Agent A, Agent Tgs_B, Key SesKey, Number T}\


224 
\ : parts (spies evs); Tgs_B ~: bad;\


225 
\ evs : kerberos ] \


226 
\ ==> SesKey ~: range shrK";


227 
by (etac rev_mp 1);


228 
by (parts_induct_tac 1);


229 
by (Fake_parts_insert_tac 1);


230 
qed "SesKey_is_session_key";


231 


232 
Goal "[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk} \


233 
\ : parts (spies evs); \


234 
\ evs : kerberos ] \


235 
\ ==> Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, \


236 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}}) \


237 
\ : set evs";


238 
by (etac rev_mp 1);


239 
by (parts_induct_tac 1);


240 
(*Fake*)


241 
by (Fake_parts_insert_tac 1);


242 
(*K4*)


243 
by (Blast_tac 1);


244 
qed "A_trusts_AuthTicket";


245 


246 
Goal "[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}\


247 
\ : parts (spies evs);\


248 
\ evs : kerberos ] \


249 
\ ==> AuthKey : AuthKeys evs";


250 
by (forward_tac [A_trusts_AuthTicket] 1);


251 
by (assume_tac 1);


252 
by (simp_tac (simpset() addsimps [AuthKeys_def]) 1);


253 
by (Blast_tac 1);


254 
qed "AuthTicket_crypt_AuthKey";


255 


256 
(*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*)


257 
Goal "[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\


258 
\ : set evs; \


259 
\ evs : kerberos ] \


260 
\ ==> B ~= Tgs & ServKey ~: range shrK & ServKey ~: AuthKeys evs &\


261 
\ ServTicket = (Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt} ) & \


262 
\ AuthKey ~: range shrK & AuthKey : AuthKeys evs";


263 
by (etac rev_mp 1);


264 
by (etac kerberos.induct 1);


265 
by (ALLGOALS


266 
(asm_full_simp_tac


267 
(simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert,


268 
AuthKeys_empty, AuthKeys_simp])));


269 
by (blast_tac (claset() addEs spies_partsEs) 1);


270 
by Auto_tac;


271 
by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1);


272 
by (blast_tac (claset() addSDs [SesKey_is_session_key]


273 
addEs spies_partsEs) 1);


274 
by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey]


275 
addEs spies_partsEs) 1);


276 
qed "Says_Tgs_message_form";


277 


278 
(*If a certain encrypted message appears then it originated with Kas*)


279 
Goal "[ Crypt (shrK A) {Key AuthKey, Peer, Tk, AuthTicket} \


280 
\ : parts (spies evs); \


281 
\ A ~: bad; evs : kerberos ] \


282 
\ ==> Says Kas A (Crypt (shrK A) {Key AuthKey, Peer, Tk, AuthTicket}) \


283 
\ : set evs";


284 
by (etac rev_mp 1);


285 
by (parts_induct_tac 1);


286 
(*Fake*)


287 
by (Fake_parts_insert_tac 1);


288 
(*K4*)


289 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst,


290 
A_trusts_AuthTicket RS Says_Kas_message_form])


291 
1);


292 
qed "A_trusts_AuthKey";


293 


294 


295 
(*If a certain encrypted message appears then it originated with Tgs*)


296 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \


297 
\ : parts (spies evs); \


298 
\ Key AuthKey ~: analz (spies evs); \


299 
\ AuthKey ~: range shrK; \


300 
\ evs : kerberos ] \


301 
\==> EX A. Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\


302 
\ : set evs";


303 
by (etac rev_mp 1);


304 
by (etac rev_mp 1);


305 
by (parts_induct_tac 1);


306 
(*Fake*)


307 
by (Fake_parts_insert_tac 1);


308 
(*K2*)


309 
by (Blast_tac 1);


310 
(*K4*)


311 
by Auto_tac;


312 
qed "A_trusts_K4";


313 


314 
Goal "[ Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, AuthTicket} \


315 
\ : parts (spies evs); \


316 
\ A ~: bad; \


317 
\ evs : kerberos ] \


318 
\ ==> AuthKey ~: range shrK & \


319 
\ AuthTicket = Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}";


320 
by (etac rev_mp 1);


321 
by (parts_induct_tac 1);


322 
by (Fake_parts_insert_tac 1);


323 
by (Blast_tac 1);


324 
qed "AuthTicket_form";


325 


326 
(* This form holds also over an AuthTicket, but is not needed below. *)


327 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \


328 
\ : parts (spies evs); \


329 
\ Key AuthKey ~: analz (spies evs); \


330 
\ evs : kerberos ] \


331 
\ ==> ServKey ~: range shrK & \


332 
\ (EX A. ServTicket = Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt})";


333 
by (etac rev_mp 1);


334 
by (etac rev_mp 1);


335 
by (parts_induct_tac 1);


336 
by (Fake_parts_insert_tac 1);


337 
qed "ServTicket_form";


338 


339 
Goal "[ Says Kas' A (Crypt (shrK A) \


340 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket} ) : set evs; \


341 
\ evs : kerberos ] \


342 
\ ==> AuthKey ~: range shrK & \


343 
\ AuthTicket = \


344 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}\


345 
\  AuthTicket : analz (spies evs)";


346 
by (case_tac "A : bad" 1);


347 
by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);


348 
by (forward_tac [Says_imp_spies RS parts.Inj] 1);


349 
by (blast_tac (claset() addSDs [AuthTicket_form]) 1);


350 
qed "Says_kas_message_form";


351 
(* Essentially the same as AuthTicket_form *)


352 


353 
Goal "[ Says Tgs' A (Crypt AuthKey \


354 
\ {Key ServKey, Agent B, Tt, ServTicket} ) : set evs; \


355 
\ evs : kerberos ] \


356 
\ ==> ServKey ~: range shrK & \


357 
\ (EX A. ServTicket = \


358 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}) \


359 
\  ServTicket : analz (spies evs)";


360 
by (case_tac "Key AuthKey : analz (spies evs)" 1);


361 
by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);


362 
by (forward_tac [Says_imp_spies RS parts.Inj] 1);


363 
by (blast_tac (claset() addSDs [ServTicket_form]) 1);


364 
qed "Says_tgs_message_form";


365 
(* This form MUST be used in analz_sees_tac below *)


366 


367 


368 
(*****************UNICITY THEOREMS****************)


369 


370 
(* The session key, if secure, uniquely identifies the Ticket


371 
whether AuthTicket or ServTicket. As a matter of fact, one can read


372 
also Tgs in the place of B. *)


373 
Goal "evs : kerberos ==> \


374 
\ Key SesKey ~: analz (spies evs) > \


375 
\ (EX A B T. ALL A' B' T'. \


376 
\ Crypt (shrK B') {Agent A', Agent B', Key SesKey, T'} \


377 
\ : parts (spies evs) > A'=A & B'=B & T'=T)";


378 
by (parts_induct_tac 1);


379 
by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*)


380 
THEN Fake_parts_insert_tac 1);


381 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);


382 
by (expand_case_tac "SesKey = ?y" 1);


383 
by (blast_tac (claset() addSEs spies_partsEs) 1);


384 
by (expand_case_tac "SesKey = ?y" 1);


385 
by (blast_tac (claset() addSEs spies_partsEs) 1);


386 
val lemma = result();


387 


388 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key SesKey, T} \


389 
\ : parts (spies evs); \


390 
\ Crypt (shrK B') {Agent A', Agent B', Key SesKey, T'} \


391 
\ : parts (spies evs); \


392 
\ evs : kerberos; Key SesKey ~: analz (spies evs) ] \


393 
\ ==> A=A' & B=B' & T=T'";


394 
by (prove_unique_tac lemma 1);


395 
qed "unique_CryptKey";


396 


397 
Goal "evs : kerberos \


398 
\ ==> Key SesKey ~: analz (spies evs) > \


399 
\ (EX K' B' T' Ticket'. ALL K B T Ticket. \


400 
\ Crypt K {Key SesKey, Agent B, T, Ticket} \


401 
\ : parts (spies evs) > K=K' & B=B' & T=T' & Ticket=Ticket')";


402 
by (parts_induct_tac 1);


403 
by (REPEAT (etac (exI RSN (2,exE)) 1) THEN Fake_parts_insert_tac 1);


404 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);


405 
by (expand_case_tac "SesKey = ?y" 1);


406 
by (blast_tac (claset() addSEs spies_partsEs) 1);


407 
by (expand_case_tac "SesKey = ?y" 1);


408 
by (blast_tac (claset() addSEs spies_partsEs) 1);


409 
val lemma = result();


410 


411 
(*An AuthKey is encrypted by one and only one Shared key.


412 
A ServKey is encrypted by one and only one AuthKey.


413 
*)


414 
Goal "[ Crypt K {Key SesKey, Agent B, T, Ticket} \


415 
\ : parts (spies evs); \


416 
\ Crypt K' {Key SesKey, Agent B', T', Ticket'} \


417 
\ : parts (spies evs); \


418 
\ evs : kerberos; Key SesKey ~: analz (spies evs) ] \


419 
\ ==> K=K' & B=B' & T=T' & Ticket=Ticket'";


420 
by (prove_unique_tac lemma 1);


421 
qed "Key_unique_SesKey";


422 


423 


424 
(*


425 
At reception of any message mentioning A, Kas associates shrK A with


426 
a new AuthKey. Realistic, as the user gets a new AuthKey at each login.


427 
Similarly, at reception of any message mentioning an AuthKey


428 
(a legitimate user could make several requests to Tgs  by K3), Tgs


429 
associates it with a new ServKey.


430 


431 
Therefore, a goal like


432 


433 
"evs : kerberos \


434 
\ ==> Key Kc ~: analz (spies evs) > \


435 
\ (EX K' B' T' Ticket'. ALL K B T Ticket. \


436 
\ Crypt Kc {Key K, Agent B, T, Ticket} \


437 
\ : parts (spies evs) > K=K' & B=B' & T=T' & Ticket=Ticket')";


438 


439 
would fail on the K2 and K4 cases.


440 
*)


441 


442 
(* AuthKey uniquely identifies the message from Kas *)


443 
Goal "evs : kerberos ==> \


444 
\ EX A' Ka' Tk' X'. ALL A Ka Tk X. \


445 
\ Says Kas A (Crypt Ka {Key AuthKey, Agent Tgs, Tk, X}) \


446 
\ : set evs > A=A' & Ka=Ka' & Tk=Tk' & X=X'";


447 
by (etac kerberos.induct 1);


448 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));


449 
by (Step_tac 1);


450 
(*K2: it can't be a new key*)


451 
by (expand_case_tac "AuthKey = ?y" 1);


452 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));


453 
by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*)


454 
addSEs spies_partsEs) 1);


455 
val lemma = result();


456 


457 
Goal "[ Says Kas A \


458 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Tk, X}) : set evs; \


459 
\ Says Kas A' \


460 
\ (Crypt Ka' {Key AuthKey, Agent Tgs, Tk', X'}) : set evs; \


461 
\ evs : kerberos ] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";


462 
by (prove_unique_tac lemma 1);


463 
qed "unique_AuthKeys";


464 


465 
(* ServKey uniquely identifies the message from Tgs *)


466 
Goal "evs : kerberos ==> \


467 
\ EX A' B' AuthKey' Tk' X'. ALL A B AuthKey Tk X. \


468 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tk, X}) \


469 
\ : set evs > A=A' & B=B' & AuthKey=AuthKey' & Tk=Tk' & X=X'";


470 
by (etac kerberos.induct 1);


471 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));


472 
by (Step_tac 1);


473 
(*K4: it can't be a new key*)


474 
by (expand_case_tac "ServKey = ?y" 1);


475 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));


476 
by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*)


477 
addSEs spies_partsEs) 1);


478 
val lemma = result();


479 


480 
Goal "[ Says Tgs A \


481 
\ (Crypt K {Key ServKey, Agent B, Tt, X}) : set evs; \


482 
\ Says Tgs A' \


483 
\ (Crypt K' {Key ServKey, Agent B', Tt', X'}) : set evs; \


484 
\ evs : kerberos ] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";


485 
by (prove_unique_tac lemma 1);


486 
qed "unique_ServKeys";


487 


488 


489 
(*****************LEMMAS ABOUT the predicate KeyCryptKey****************)


490 


491 
Goalw [KeyCryptKey_def] "~ KeyCryptKey AuthKey ServKey []";


492 
by (Simp_tac 1);


493 
qed "not_KeyCryptKey_Nil";


494 
AddIffs [not_KeyCryptKey_Nil];


495 


496 
Goalw [KeyCryptKey_def]


497 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, tt, X }) \


498 
\ : set evs; \


499 
\ evs : kerberos ] ==> KeyCryptKey AuthKey ServKey evs";


500 
by (forward_tac [Says_Tgs_message_form] 1);


501 
by (assume_tac 1);


502 
by (Blast_tac 1);


503 
qed "KeyCryptKeyI";


504 


505 
Goalw [KeyCryptKey_def]


506 
"KeyCryptKey AuthKey ServKey (Says S A X # evs) = \


507 
\ (Tgs = S & \


508 
\ (EX B tt. X = Crypt AuthKey \


509 
\ {Key ServKey, Agent B, tt, \


510 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, tt} }) \


511 
\  KeyCryptKey AuthKey ServKey evs)";


512 
by (Simp_tac 1);


513 
by (Blast_tac 1);


514 
qed "KeyCryptKey_Says";


515 
Addsimps [KeyCryptKey_Says];


516 


517 
(*A fresh AuthKey cannot be associated with any other


518 
(with respect to a given trace). *)


519 
Goalw [KeyCryptKey_def]


520 
"[ Key AuthKey ~: used evs; evs : kerberos ] \


521 
\ ==> ~ KeyCryptKey AuthKey ServKey evs";


522 
by (etac rev_mp 1);


523 
by (parts_induct_tac 1);


524 
by (Asm_full_simp_tac 1);


525 
by (blast_tac (claset() addSEs spies_partsEs) 1);


526 
qed "Auth_fresh_not_KeyCryptKey";


527 


528 
(*A fresh ServKey cannot be associated with any other


529 
(with respect to a given trace). *)


530 
Goalw [KeyCryptKey_def]


531 
"Key ServKey ~: used evs ==> ~ KeyCryptKey AuthKey ServKey evs";


532 
by (blast_tac (claset() addSEs spies_partsEs) 1);


533 
qed "Serv_fresh_not_KeyCryptKey";


534 


535 
Goalw [KeyCryptKey_def]


536 
"[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, tk}\


537 
\ : parts (spies evs); evs : kerberos ] \


538 
\ ==> ~ KeyCryptKey K AuthKey evs";


539 
by (etac rev_mp 1);


540 
by (parts_induct_tac 1);


541 
(*K4*)


542 
by (blast_tac (claset() addEs spies_partsEs) 3);


543 
(*K2: by freshness*)


544 
by (blast_tac (claset() addEs spies_partsEs) 2);


545 
by (Fake_parts_insert_tac 1);


546 
qed "AuthKey_not_KeyCryptKey";


547 


548 
(*A secure serverkey cannot have been used to encrypt others*)


549 
Goalw [KeyCryptKey_def]


550 
"[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, tt} \


551 
\ : parts (spies evs); \


552 
\ Key ServKey ~: analz (spies evs); \


553 
\ B ~= Tgs; evs : kerberos ] \


554 
\ ==> ~ KeyCryptKey ServKey K evs";


555 
by (etac rev_mp 1);


556 
by (etac rev_mp 1);


557 
by (parts_induct_tac 1);


558 
by (Fake_parts_insert_tac 1);


559 
(*K4 splits into distinct subcases*)


560 
by (Step_tac 1);


561 
by (ALLGOALS Asm_full_simp_tac);


562 
(*ServKey can't have been enclosed in two certificates*)


563 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]


564 
addSEs [MPair_parts]


565 
addDs [unique_CryptKey]) 4);


566 
(*ServKey is fresh and so could not have been used, by new_keys_not_used*)


567 
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,


568 
Crypt_imp_invKey_keysFor],


569 
simpset()) 2);


570 
(*Others by freshness*)


571 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));


572 
qed "ServKey_not_KeyCryptKey";


573 


574 
(*Long term keys are not issued as ServKeys*)


575 
Goalw [KeyCryptKey_def]


576 
"evs : kerberos ==> ~ KeyCryptKey K (shrK A) evs";


577 
by (parts_induct_tac 1);


578 
qed "shrK_not_KeyCryptKey";


579 


580 
(*The Tgs message associates ServKey with AuthKey and therefore not with any


581 
other key AuthKey.*)


582 
Goalw [KeyCryptKey_def]


583 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, tt, X }) \


584 
\ : set evs; \


585 
\ AuthKey' ~= AuthKey; evs : kerberos ] \


586 
\ ==> ~ KeyCryptKey AuthKey' ServKey evs";


587 
by (blast_tac (claset() addDs [unique_ServKeys]) 1);


588 
qed "Says_Tgs_KeyCryptKey";


589 


590 
Goal "[ KeyCryptKey AuthKey ServKey evs; evs : kerberos ] \


591 
\ ==> ~ KeyCryptKey ServKey K evs";


592 
by (etac rev_mp 1);


593 
by (parts_induct_tac 1);


594 
by (Step_tac 1);


595 
by (ALLGOALS Asm_full_simp_tac);


596 
(*K4 splits into subcases*)


597 
by (blast_tac (claset() addEs spies_partsEs


598 
addSDs [AuthKey_not_KeyCryptKey]) 4);


599 
(*ServKey is fresh and so could not have been used, by new_keys_not_used*)


600 
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,


601 
Crypt_imp_invKey_keysFor],


602 
simpset() addsimps [KeyCryptKey_def]) 2);


603 
(*Others by freshness*)


604 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));


605 
qed "KeyCryptKey_not_KeyCryptKey";


606 


607 
(*The only session keys that can be found with the help of session keys are


608 
those sent by Tgs in step K4. *)


609 


610 
(*We take some pains to express the property


611 
as a logical equivalence so that the simplifier can apply it.*)


612 
Goal "P > (Key K : analz (Key``KK Un H)) > (K:KK  Key K : analz H) \


613 
\ ==> \


614 
\ P > (Key K : analz (Key``KK Un H)) = (K:KK  Key K : analz H)";


615 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);


616 
qed "Key_analz_image_Key_lemma";


617 


618 
Goal "[ KeyCryptKey K K' evs; evs : kerberos ] \


619 
\ ==> Key K' : analz (insert (Key K) (spies evs))";


620 
by (full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);


621 
by (Clarify_tac 1);


622 
by (dresolve_tac [Says_imp_spies RS analz.Inj RS analz_insertI] 1);


623 
by Auto_tac;


624 
qed "KeyCryptKey_analz_insert";


625 


626 
Goal "[ K : AuthKeys evs Un range shrK; evs : kerberos ] \


627 
\ ==> ALL SK. ~ KeyCryptKey SK K evs";


628 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);


629 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);


630 
qed "AuthKeys_are_not_KeyCryptKey";


631 


632 
Goal "[ K ~: AuthKeys evs; \


633 
\ K ~: range shrK; evs : kerberos ] \


634 
\ ==> ALL SK. ~ KeyCryptKey K SK evs";


635 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);


636 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);


637 
qed "not_AuthKeys_not_KeyCryptKey";


638 


639 


640 
(*****************SECRECY THEOREMS****************)


641 


642 
(*For proofs involving analz.*)


643 
val analz_sees_tac =


644 
EVERY


645 
[REPEAT (FIRSTGOAL analz_mono_contra_tac),


646 
forward_tac [Oops_range_spies2] 10,


647 
forward_tac [Oops_range_spies1] 9,


648 
forward_tac [Says_tgs_message_form] 7,


649 
forward_tac [Says_kas_message_form] 5,


650 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]


651 
ORELSE' hyp_subst_tac)];


652 


653 
Goal "[ KK <= (range shrK); Key K : analz (spies evs); evs: kerberos ] \


654 
\ ==> Key K : analz (Key `` KK Un spies evs)";


655 
by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);


656 
qed "analz_mono_KK";


657 


658 
(* Big simplification law for keys SK that are not crypted by keys in KK *)


659 
(* It helps prove three, otherwise hard, facts about keys. These facts are *)


660 
(* exploited as simplification laws for analz, and also "limit the damage" *)


661 
(* in case of loss of a key to the spy. See ESORICS98. *)


662 
Goal "evs : kerberos ==> \


663 
\ (ALL SK KK. KK <= (range shrK) > \


664 
\ (ALL K: KK. ~ KeyCryptKey K SK evs) > \


665 
\ (Key SK : analz (Key``KK Un (spies evs))) = \


666 
\ (SK : KK  Key SK : analz (spies evs)))";


667 
by (etac kerberos.induct 1);


668 
by analz_sees_tac;


669 
by (REPEAT_FIRST (rtac allI));


670 
by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI)));


671 
by (ALLGOALS


672 
(asm_simp_tac


673 
(analz_image_freshK_ss addsimps


674 
[KeyCryptKey_Says, shrK_not_KeyCryptKey,


675 
Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey,


676 
Says_Tgs_KeyCryptKey, Spy_analz_shrK])));


677 
(*Fake*)


678 
by (spy_analz_tac 1);


679 
(* Base + K2 done by the simplifier! *)


680 
(*K3*)


681 
by (Blast_tac 1);


682 
(*K4*)


683 
by (blast_tac (claset() addEs spies_partsEs


684 
addSDs [AuthKey_not_KeyCryptKey]) 1);


685 
(*K5*)


686 
by (rtac impI 1);


687 
by (case_tac "Key ServKey : analz (spies evs5)" 1);


688 
(*If ServKey is compromised then the result follows directly...*)


689 
by (asm_simp_tac


690 
(simpset() addsimps [analz_insert_eq,


691 
impOfSubs (Un_upper2 RS analz_mono)]) 1);


692 
(*...therefore ServKey is uncompromised.*)


693 
by (case_tac "KeyCryptKey ServKey SK evs5" 1);


694 
by (asm_simp_tac analz_image_freshK_ss 2);


695 
(*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*)


696 
by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)]


697 
addEs spies_partsEs delrules [allE, ballE]) 1);


698 
(** Level 14: Oops1 and Oops2 **)


699 
by (ALLGOALS Clarify_tac);


700 
(*Oops 2*)


701 
by (case_tac "Key ServKey : analz (spies evsO2)" 2);


702 
by (ALLGOALS Asm_full_simp_tac);


703 
by (forward_tac [analz_mono_KK] 2


704 
THEN assume_tac 2


705 
THEN assume_tac 2);


706 
by (forward_tac [analz_cut] 2 THEN assume_tac 2);


707 
by (blast_tac (claset() addDs [analz_cut, impOfSubs analz_mono]) 2);


708 
by (dres_inst_tac [("x","SK")] spec 2);


709 
by (dres_inst_tac [("x","insert ServKey KK")] spec 2);


710 
by (forward_tac [Says_Tgs_message_form] 2 THEN assume_tac 2);


711 
by (Clarify_tac 2);


712 
by (forward_tac [Says_imp_spies RS parts.Inj RS parts.Body


713 
RS parts.Snd RS parts.Snd RS parts.Snd] 2);


714 
by (Asm_full_simp_tac 2);


715 
by (blast_tac (claset() addSDs [ServKey_not_KeyCryptKey]


716 
addDs [impOfSubs analz_mono]) 2);


717 
(*Level 28: Oops 1*)


718 
by (dres_inst_tac [("x","SK")] spec 1);


719 
by (dres_inst_tac [("x","insert AuthKey KK")] spec 1);


720 
by (case_tac "KeyCryptKey AuthKey SK evsO1" 1);


721 
by (ALLGOALS Asm_full_simp_tac);


722 
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);


723 
by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);


724 
qed_spec_mp "Key_analz_image_Key";


725 


726 


727 
(* First simplification law for analz: no session keys encrypt *)


728 
(* authentication keys or shared keys. *)


729 
Goal "[ evs : kerberos; K : (AuthKeys evs) Un range shrK; \


730 
\ SesKey ~: range shrK ] \


731 
\ ==> Key K : analz (insert (Key SesKey) (spies evs)) = \


732 
\ (K = SesKey  Key K : analz (spies evs))";


733 
by (forward_tac [AuthKeys_are_not_KeyCryptKey] 1 THEN assume_tac 1);


734 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);


735 
qed "analz_insert_freshK1";


736 


737 


738 
(* Second simplification law for analz: no service keys encrypt *)


739 
(* any other keys. *)


740 
Goal "[ evs : kerberos; ServKey ~: (AuthKeys evs); ServKey ~: range shrK]\


741 
\ ==> Key K : analz (insert (Key ServKey) (spies evs)) = \


742 
\ (K = ServKey  Key K : analz (spies evs))";


743 
by (forward_tac [not_AuthKeys_not_KeyCryptKey] 1


744 
THEN assume_tac 1


745 
THEN assume_tac 1);


746 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);


747 
qed "analz_insert_freshK2";


748 


749 


750 
(* Third simplification law for analz: only one authentication key *)


751 
(* encrypts a certain service key. *)


752 
Goal


753 
"[ Says Tgs A \


754 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \


755 
\ : set evs; \


756 
\ AuthKey ~= AuthKey'; AuthKey' ~: range shrK; evs : kerberos ] \


757 
\ ==> Key ServKey : analz (insert (Key AuthKey') (spies evs)) = \


758 
\ (ServKey = AuthKey'  Key ServKey : analz (spies evs))";


759 
by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);


760 
by (Blast_tac 1);


761 
by (assume_tac 1);


762 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);


763 
qed "analz_insert_freshK3";


764 


765 


766 
(*a weakness of the protocol*)


767 
Goal "[ Says Tgs A \


768 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \


769 
\ : set evs; \


770 
\ Key AuthKey : analz (spies evs); evs : kerberos ] \


771 
\ ==> Key ServKey : analz (spies evs)";


772 
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS


773 
analz.Decrypt RS analz.Fst],


774 
simpset()) 1);


775 
qed "AuthKey_compromises_ServKey";


776 


777 


778 
(********************** Guarantees for Kas *****************************)


779 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Tt, \


780 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}\


781 
\ : parts (spies evs); \


782 
\ Key ServKey ~: analz (spies evs); \


783 
\ B ~= Tgs; evs : kerberos ] \


784 
\ ==> ServKey ~: AuthKeys evs";


785 
by (etac rev_mp 1);


786 
by (etac rev_mp 1);


787 
by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);


788 
by (parts_induct_tac 1);


789 
by (Fake_parts_insert_tac 1);


790 
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));


791 
bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE));


792 
bind_thm ("ServKey_notin_AuthKeysD", result());


793 


794 


795 
(** If Spy sees the Authentication Key sent in msg K2, then


796 
the Key has expired **)


797 
Goal "[ A ~: bad; evs : kerberos ] \


798 
\ ==> Says Kas A \


799 
\ (Crypt (shrK A) \


800 
\ {Key AuthKey, Agent Tgs, Number Tk, \


801 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


802 
\ : set evs > \


803 
\ Key AuthKey : analz (spies evs) > \


804 
\ ExpirAuth Tk evs";


805 
by (etac kerberos.induct 1);


806 
by analz_sees_tac;


807 
by (ALLGOALS


808 
(asm_simp_tac


809 
(simpset() addsimps ([Says_Kas_message_form,


810 
analz_insert_eq, not_parts_not_analz,


811 
analz_insert_freshK1] @ pushes))));


812 
(*Fake*)


813 
by (spy_analz_tac 1);


814 
(*K2*)


815 
by (blast_tac (claset() addSEs spies_partsEs


816 
addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);


817 
(*K4*)


818 
by (blast_tac (claset() addSEs spies_partsEs) 1);


819 
(*Level 8: K5*)


820 
by (blast_tac (claset() addEs [ServKey_notin_AuthKeys]


821 
addDs [Says_Kas_message_form,


822 
Says_imp_spies RS parts.Inj]


823 
addIs [less_SucI]) 1);


824 
(*Oops1*)


825 
by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1);


826 
(*Oops2*)


827 
by (blast_tac (claset() addDs [Says_Tgs_message_form,


828 
Says_Kas_message_form]) 1);


829 
val lemma = result() RS mp RS mp RSN(1,rev_notE);


830 


831 


832 
Goal "[ Says Kas A \


833 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}) \


834 
\ : set evs; \


835 
\ ~ ExpirAuth Tk evs; \


836 
\ A ~: bad; evs : kerberos ] \


837 
\ ==> Key AuthKey ~: analz (spies evs)";


838 
by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1);


839 
by (blast_tac (claset() addSDs [lemma]) 1);


840 
qed "Confidentiality_Kas";


841 


842 


843 


844 


845 


846 


847 
(********************** Guarantees for Tgs *****************************)


848 


849 
(** If Spy sees the Service Key sent in msg K4, then


850 
the Key has expired **)


851 
Goal "[ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


852 
\ ==> Key AuthKey ~: analz (spies evs) > \


853 
\ Says Tgs A \


854 
\ (Crypt AuthKey \


855 
\ {Key ServKey, Agent B, Number Tt, \


856 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}})\


857 
\ : set evs > \


858 
\ Key ServKey : analz (spies evs) > \


859 
\ ExpirServ Tt evs";


860 
by (etac kerberos.induct 1);


861 
(*The Oops1 case is unusual: must simplify Authkey ~: analz (spies (ev#evs))


862 
rather than weakening it to Authkey ~: analz (spies evs), for we then


863 
conclude AuthKey ~= AuthKeya.*)


864 
by (Clarify_tac 9);


865 
by analz_sees_tac;


866 
by (rotate_tac ~1 11);


867 
by (ALLGOALS


868 
(asm_full_simp_tac


869 
(simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form,


870 
analz_insert_eq, not_parts_not_analz,


871 
analz_insert_freshK1, analz_insert_freshK2] @ pushes))));


872 
(*Fake*)


873 
by (spy_analz_tac 1);


874 
(*K2*)


875 
by (blast_tac (claset() addSEs spies_partsEs


876 
addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);


877 
(*K4*)


878 
by (case_tac "A ~= Aa" 1);


879 
by (blast_tac (claset() addSEs spies_partsEs


880 
addIs [less_SucI]) 1);


881 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst,


882 
A_trusts_AuthTicket,


883 
Confidentiality_Kas,


884 
impOfSubs analz_subset_parts]) 1);


885 
by (ALLGOALS Clarify_tac);


886 
(*Oops2*)


887 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj,


888 
Key_unique_SesKey] addIs [less_SucI]) 3);


889 
(** Level 12 **)


890 
(*Oops1*)


891 
by (forward_tac [Says_Kas_message_form] 2);


892 
by (assume_tac 2);


893 
by (blast_tac (claset() addDs [analz_insert_freshK3,


894 
Says_Kas_message_form, Says_Tgs_message_form]


895 
addIs [less_SucI]) 2);


896 
(** Level 16 **)


897 
by (thin_tac "Says Aa Tgs ?X : set ?evs" 1);


898 
by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);


899 
by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);


900 
by (rotate_tac ~1 1);


901 
by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);


902 
by (etac disjE 1);


903 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj,


904 
Key_unique_SesKey]) 1);


905 
by (blast_tac (claset() addIs [less_SucI]) 1);


906 
val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE);


907 


908 


909 
(* In the real world Tgs can't check wheter AuthKey is secure! *)


910 
Goal


911 
"[ Says Tgs A \


912 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \


913 
\ : set evs; \


914 
\ Key AuthKey ~: analz (spies evs); \


915 
\ ~ ExpirServ Tt evs; \


916 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


917 
\ ==> Key ServKey ~: analz (spies evs)";


918 
by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1);


919 
by (blast_tac (claset() addDs [lemma]) 1);


920 
qed "Confidentiality_Tgs1";


921 


922 
(* In the real world Tgs CAN check what Kas sends! *)


923 
Goal


924 
"[ Says Kas A \


925 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}) \


926 
\ : set evs; \


927 
\ Says Tgs A \


928 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \


929 
\ : set evs; \


930 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \


931 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


932 
\ ==> Key ServKey ~: analz (spies evs)";


933 
by (blast_tac (claset() addSDs [Confidentiality_Kas,


934 
Confidentiality_Tgs1]) 1);


935 
qed "Confidentiality_Tgs2";


936 


937 
(*Most general form*)


938 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2;


939 


940 


941 
(********************** Guarantees for Alice *****************************)


942 


943 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas;


944 


945 
Goal


946 
"[ Says Kas A \


947 
\ (Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, AuthTicket}) : set evs;\


948 
\ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \


949 
\ : parts (spies evs); \


950 
\ Key AuthKey ~: analz (spies evs); \


951 
\ evs : kerberos ] \


952 
\==> Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\


953 
\ : set evs";


954 
by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1);


955 
by (etac rev_mp 1);


956 
by (etac rev_mp 1);


957 
by (etac rev_mp 1);


958 
by (parts_induct_tac 1);


959 
by (Fake_parts_insert_tac 1);


960 
(*K2 and K4 remain*)


961 
by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts]


962 
addSDs [unique_CryptKey]) 2);


963 
by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form,


964 
AuthKeys_used]) 1);


965 
qed "A_trusts_K4_bis";


966 


967 


968 
Goal "[ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \


969 
\ : parts (spies evs); \


970 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


971 
\ : parts (spies evs); \


972 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \


973 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


974 
\ ==> Key ServKey ~: analz (spies evs)";


975 
by (dtac A_trusts_AuthKey 1);


976 
by (assume_tac 1);


977 
by (assume_tac 1);


978 
by (blast_tac (claset() addDs [Confidentiality_Kas,


979 
Says_Kas_message_form,


980 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1);


981 
qed "Confidentiality_Serv_A";


982 


983 


984 
(********************** Guarantees for Bob *****************************)


985 
(* Theorems for the refined model have suffix "refined" *)


986 


987 
Goal


988 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\


989 
\ : set evs; evs : kerberos] \


990 
\ ==> EX Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\


991 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


992 
\ : set evs";


993 
by (etac rev_mp 1);


994 
by (parts_induct_tac 1);


995 
by Auto_tac;


996 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS


997 
A_trusts_AuthTicket]) 1);


998 
qed "K4_imp_K2";


999 


1000 
Goal


1001 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\


1002 
\ : set evs; evs : kerberos] \


1003 
\ ==> EX Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\


1004 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


1005 
\ : set evs \


1006 
\ & ServLife + Tt <= AuthLife + Tk)";


1007 
by (etac rev_mp 1);


1008 
by (parts_induct_tac 1);


1009 
by Auto_tac;


1010 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS


1011 
A_trusts_AuthTicket]) 1);


1012 
qed "K4_imp_K2_refined";


1013 


1014 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt} \


1015 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \


1016 
\ evs : kerberos ] \


1017 
\==> EX AuthKey. \


1018 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, \


1019 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}) \


1020 
\ : set evs";


1021 
by (etac rev_mp 1);


1022 
by (parts_induct_tac 1);


1023 
by (Fake_parts_insert_tac 1);


1024 
by (Blast_tac 1);


1025 
qed "B_trusts_ServKey";


1026 


1027 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1028 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \


1029 
\ evs : kerberos ] \


1030 
\ ==> EX AuthKey Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\


1031 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


1032 
\ : set evs";


1033 
by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1);


1034 
qed "B_trusts_ServTicket_Kas";


1035 


1036 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1037 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \


1038 
\ evs : kerberos ] \


1039 
\ ==> EX AuthKey Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\


1040 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


1041 
\ : set evs \


1042 
\ & ServLife + Tt <= AuthLife + Tk)";


1043 
by (blast_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1);


1044 
qed "B_trusts_ServTicket_Kas_refined";


1045 


1046 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1047 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \


1048 
\ evs : kerberos ] \


1049 
\==> EX Tk AuthKey. \


1050 
\ Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \


1051 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


1052 
\ : set evs \


1053 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \


1054 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}}) \


1055 
\ : set evs";


1056 
by (forward_tac [B_trusts_ServKey] 1);


1057 
by (etac exE 4);


1058 
by (forward_tac [K4_imp_K2] 4);


1059 
by (Blast_tac 5);


1060 
by (ALLGOALS assume_tac);


1061 
qed "B_trusts_ServTicket";


1062 


1063 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1064 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \


1065 
\ evs : kerberos ] \


1066 
\==> EX Tk AuthKey. \


1067 
\ (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \


1068 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\


1069 
\ : set evs \


1070 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \


1071 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}}) \


1072 
\ : set evs \


1073 
\ & ServLife + Tt <= AuthLife + Tk)";


1074 
by (forward_tac [B_trusts_ServKey] 1);


1075 
by (etac exE 4);


1076 
by (forward_tac [K4_imp_K2_refined] 4);


1077 
by (Blast_tac 5);


1078 
by (ALLGOALS assume_tac);


1079 
qed "B_trusts_ServTicket_refined";


1080 


1081 


1082 
Goal "[ ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk ] \


1083 
\ ==> ~ ExpirAuth Tk evs";


1084 
by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1);


1085 
qed "NotExpirServ_NotExpirAuth_refined";


1086 


1087 


1088 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1089 
\ : parts (spies evs); \


1090 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1091 
\ : parts (spies evs); \


1092 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\


1093 
\ : parts (spies evs); \


1094 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \


1095 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1096 
\ ==> Key ServKey ~: analz (spies evs)";


1097 
by (forward_tac [A_trusts_AuthKey] 1);


1098 
by (forward_tac [Confidentiality_Kas] 3);


1099 
by (forward_tac [B_trusts_ServTicket] 6);


1100 
by (etac exE 9);


1101 
by (etac exE 9);


1102 
by (forward_tac [Says_Kas_message_form] 9);


1103 
by (blast_tac (claset() addDs [A_trusts_K4,


1104 
unique_ServKeys, unique_AuthKeys,


1105 
Confidentiality_Tgs2]) 10);


1106 
by (ALLGOALS assume_tac);


1107 
(*


1108 
The proof above executes in 8 secs. It can be done in one command in 50 secs:


1109 
by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,


1110 
Says_Kas_message_form, B_trusts_ServTicket,


1111 
unique_ServKeys, unique_AuthKeys,


1112 
Confidentiality_Kas,


1113 
Confidentiality_Tgs2]) 1);


1114 
*)


1115 
qed "Confidentiality_B";


1116 


1117 


1118 
(*Most general form  only for refined model! *)


1119 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1120 
\ : parts (spies evs); \


1121 
\ ~ ExpirServ Tt evs; \


1122 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1123 
\ ==> Key ServKey ~: analz (spies evs)";


1124 
by (blast_tac (claset() addDs [B_trusts_ServTicket_refined,


1125 
NotExpirServ_NotExpirAuth_refined,


1126 
Confidentiality_Tgs2]) 1);


1127 
qed "Confidentiality_B_refined";


1128 


1129 


1130 
(********************** Authenticity theorems *****************************)


1131 


1132 
(***1. Session Keys authenticity: they originated with servers.***)


1133 


1134 
(*Authenticity of AuthKey for A: "A_trusts_AuthKey"*)


1135 


1136 
(*Authenticity of ServKey for A: "A_trusts_ServKey"*)


1137 
Goal "[ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \


1138 
\ : parts (spies evs); \


1139 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1140 
\ : parts (spies evs); \


1141 
\ ~ ExpirAuth Tk evs; A ~: bad; evs : kerberos ] \


1142 
\==>Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\


1143 
\ : set evs";


1144 
by (forward_tac [A_trusts_AuthKey] 1 THEN assume_tac 1 THEN assume_tac 1);


1145 
by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1);


1146 
qed "A_trusts_ServKey";


1147 
(*Note: requires a temporal check*)


1148 


1149 


1150 
(*Authenticity of ServKey for B: "B_trusts_ServKey"*)


1151 


1152 
(***2. Parties authenticity: each party verifies "the identity of


1153 
another party who generated some data" (quoted from Neuman & Ts'o).***)


1154 


1155 
(*These guarantees don't assess whether two parties agree on


1156 
the same session key: sending a message containing a key


1157 
doesn't a priori state knowledge of the key.***)


1158 


1159 
(*B checks authenticity of A: theorems "A_Authenticity",


1160 
"A_authenticity_refined" *)


1161 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \


1162 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \


1163 
\ ServTicket}) : set evs; \


1164 
\ Key ServKey ~: analz (spies evs); \


1165 
\ A ~: bad; B ~: bad; evs : kerberos ] \


1166 
\==> Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} : set evs";


1167 
by (etac rev_mp 1);


1168 
by (etac rev_mp 1);


1169 
by (etac rev_mp 1);


1170 
by (etac kerberos.induct 1);


1171 
by (forward_tac [Says_ticket_in_parts_spies] 5);


1172 
by (forward_tac [Says_ticket_in_parts_spies] 7);


1173 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));


1174 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));


1175 
by (Fake_parts_insert_tac 1);


1176 
(*K3*)


1177 
by (blast_tac (claset() addEs spies_partsEs


1178 
addDs [A_trusts_AuthKey,


1179 
Says_Kas_message_form,


1180 
Says_Tgs_message_form]) 1);


1181 
(*K4*)


1182 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);


1183 
(*K5*)


1184 
by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1);


1185 
qed "Says_Auth";


1186 


1187 
(*The second assumption tells B what kind of key ServKey is.*)


1188 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \


1189 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1190 
\ : parts (spies evs); \


1191 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1192 
\ : parts (spies evs); \


1193 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \


1194 
\ : parts (spies evs); \


1195 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \


1196 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1197 
\ ==> Says A B {Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt},\


1198 
\ Crypt ServKey {Agent A, Number Ta} } : set evs";


1199 
by (forward_tac [Confidentiality_B] 1);


1200 
by (forward_tac [B_trusts_ServKey] 9);


1201 
by (etac exE 12);


1202 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]


1203 
addSIs [Says_Auth]) 12);


1204 
by (ALLGOALS assume_tac);


1205 
qed "A_Authenticity";


1206 


1207 
(*Stronger form in the refined model*)


1208 
Goal "[ Crypt ServKey {Agent A, Number Ta2} : parts (spies evs); \


1209 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1210 
\ : parts (spies evs); \


1211 
\ ~ ExpirServ Tt evs; \


1212 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1213 
\ ==> Says A B {Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt},\


1214 
\ Crypt ServKey {Agent A, Number Ta2} } : set evs";


1215 
by (forward_tac [Confidentiality_B_refined] 1);


1216 
by (forward_tac [B_trusts_ServKey] 6);


1217 
by (etac exE 9);


1218 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]


1219 
addSIs [Says_Auth]) 9);


1220 
by (ALLGOALS assume_tac);


1221 
qed "A_Authenticity_refined";


1222 


1223 


1224 
(*A checks authenticity of B: theorem "B_authenticity"*)


1225 


1226 
Goal "[ Crypt ServKey (Number Ta) : parts (spies evs); \


1227 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \


1228 
\ ServTicket}) : set evs; \


1229 
\ Key ServKey ~: analz (spies evs); \


1230 
\ A ~: bad; B ~: bad; evs : kerberos ] \


1231 
\ ==> Says B A (Crypt ServKey (Number Ta)) : set evs";


1232 
by (etac rev_mp 1);


1233 
by (etac rev_mp 1);


1234 
by (etac rev_mp 1);


1235 
by (etac kerberos.induct 1);


1236 
by (forward_tac [Says_ticket_in_parts_spies] 5);


1237 
by (forward_tac [Says_ticket_in_parts_spies] 7);


1238 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));


1239 
by (ALLGOALS Asm_simp_tac);


1240 
by (Fake_parts_insert_tac 1);


1241 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);


1242 
by (Clarify_tac 1);


1243 
by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1);


1244 
by (Clarify_tac 1); (*PROOF FAILED if omitted*)


1245 
by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1);


1246 
qed "Says_K6";


1247 


1248 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, T, ServTicket} \


1249 
\ : parts (spies evs); \


1250 
\ Key AuthKey ~: analz (spies evs); AuthKey ~: range shrK; \


1251 
\ evs : kerberos ] \


1252 
\ ==> EX A. Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, T, ServTicket})\


1253 
\ : set evs";


1254 
by (etac rev_mp 1);


1255 
by (etac rev_mp 1);


1256 
by (parts_induct_tac 1);


1257 
by (Fake_parts_insert_tac 1);


1258 
by (Blast_tac 1);


1259 
by (Blast_tac 1);


1260 
qed "K4_trustworthy";


1261 


1262 
Goal "[ Crypt ServKey (Number Ta) : parts (spies evs); \


1263 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1264 
\ : parts (spies evs); \


1265 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\


1266 
\ : parts (spies evs); \


1267 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \


1268 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1269 
\ ==> Says B A (Crypt ServKey (Number Ta)) : set evs";


1270 
by (forward_tac [A_trusts_AuthKey] 1);


1271 
by (forward_tac [Says_Kas_message_form] 3);


1272 
by (forward_tac [Confidentiality_Kas] 4);


1273 
by (forward_tac [K4_trustworthy] 7);


1274 
by (Blast_tac 8);


1275 
by (etac exE 9);


1276 
by (forward_tac [K4_imp_K2] 9);


1277 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]


1278 
addSIs [Says_K6]


1279 
addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10);


1280 
by (ALLGOALS assume_tac);


1281 
qed "B_Authenticity";


1282 


1283 


1284 
(***3. Parties' knowledge of session keys. A knows a session key if she


1285 
used it to build a cipher.***)


1286 


1287 
Goal "[ Says B A (Crypt ServKey (Number Ta)) : set evs; \


1288 
\ Key ServKey ~: analz (spies evs); \


1289 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1290 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";


1291 
by (simp_tac (simpset() addsimps [Issues_def]) 1);


1292 
by (rtac exI 1);


1293 
by (rtac conjI 1);


1294 
by (assume_tac 1);


1295 
by (Simp_tac 1);


1296 
by (etac rev_mp 1);


1297 
by (etac rev_mp 1);


1298 
by (etac kerberos.induct 1);


1299 
by (forward_tac [Says_ticket_in_parts_spies] 5);


1300 
by (forward_tac [Says_ticket_in_parts_spies] 7);


1301 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));


1302 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));


1303 
by (Fake_parts_insert_tac 1);


1304 
(*K6 requires numerous lemmas*)


1305 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);


1306 
by (blast_tac (claset() addDs [B_trusts_ServTicket,


1307 
impOfSubs parts_spies_takeWhile_mono,


1308 
impOfSubs parts_spies_evs_revD2]


1309 
addIs [Says_K6]


1310 
addEs spies_partsEs) 1);


1311 
qed "B_Knows_B_Knows_ServKey_lemma";


1312 
(*Key ServKey ~: analz (spies evs) could be relaxed by Confidentiality_B


1313 
but this is irrelevant because B knows what he knows! *)


1314 


1315 
Goal "[ Says B A (Crypt ServKey (Number Ta)) : set evs; \


1316 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}\


1317 
\ : parts (spies evs);\


1318 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}\


1319 
\ : parts (spies evs);\


1320 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\


1321 
\ : parts (spies evs); \


1322 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \


1323 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1324 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";


1325 
by (blast_tac (claset() addSDs [Confidentiality_B,


1326 
B_Knows_B_Knows_ServKey_lemma]) 1);


1327 
qed "B_Knows_B_Knows_ServKey";


1328 


1329 
Goal "[ Says B A (Crypt ServKey (Number Ta)) : set evs; \


1330 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}\


1331 
\ : parts (spies evs);\


1332 
\ ~ ExpirServ Tt evs; \


1333 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1334 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";


1335 
by (blast_tac (claset() addSDs [Confidentiality_B_refined,


1336 
B_Knows_B_Knows_ServKey_lemma]) 1);


1337 
qed "B_Knows_B_Knows_ServKey_refined";


1338 


1339 


1340 
Goal "[ Crypt ServKey (Number Ta) : parts (spies evs); \


1341 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1342 
\ : parts (spies evs); \


1343 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\


1344 
\ : parts (spies evs); \


1345 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \


1346 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \


1347 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";


1348 
by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A,


1349 
B_Knows_B_Knows_ServKey_lemma]) 1);


1350 
qed "A_Knows_B_Knows_ServKey";


1351 


1352 
Goal "[ Says A Tgs \


1353 
\ {AuthTicket, Crypt AuthKey {Agent A, Number Ta}, Agent B}\


1354 
\ : set evs; \


1355 
\ A ~: bad; evs : kerberos ] \


1356 
\ ==> EX Tk. Says Kas A (Crypt (shrK A) \


1357 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \


1358 
\ : set evs";


1359 
by (etac rev_mp 1);


1360 
by (parts_induct_tac 1);


1361 
by (Fake_parts_insert_tac 1);


1362 
by (Blast_tac 1);


1363 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS


1364 
A_trusts_AuthKey]) 1);


1365 
qed "K3_imp_K2";


1366 


1367 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1368 
\ : parts (spies evs); \


1369 
\ Says Kas A (Crypt (shrK A) \


1370 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \


1371 
\ : set evs; \


1372 
\ Key AuthKey ~: analz (spies evs); \


1373 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1374 
\ ==> Says Tgs A (Crypt AuthKey \


1375 
\ {Key ServKey, Agent B, Number Tt, ServTicket}) \


1376 
\ : set evs";


1377 
by (etac rev_mp 1);


1378 
by (etac rev_mp 1);


1379 
by (etac rev_mp 1);


1380 
by (parts_induct_tac 1);


1381 
by (Fake_parts_insert_tac 1);


1382 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);


1383 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS


1384 
A_trusts_AuthTicket, unique_AuthKeys]) 1);


1385 
qed "K4_trustworthy'";


1386 


1387 
Goal "[ Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} \


1388 
\ : set evs; \


1389 
\ Key ServKey ~: analz (spies evs); \


1390 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1391 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs";


1392 
by (simp_tac (simpset() addsimps [Issues_def]) 1);


1393 
by (rtac exI 1);


1394 
by (rtac conjI 1);


1395 
by (assume_tac 1);


1396 
by (Simp_tac 1);


1397 
by (etac rev_mp 1);


1398 
by (etac rev_mp 1);


1399 
by (etac kerberos.induct 1);


1400 
by (forward_tac [Says_ticket_in_parts_spies] 5);


1401 
by (forward_tac [Says_ticket_in_parts_spies] 7);


1402 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));


1403 
by (ALLGOALS Asm_simp_tac);


1404 
by (Clarify_tac 1);


1405 
(*K6*)


1406 
by Auto_tac;


1407 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);


1408 
(*Level 15: case study necessary because the assumption doesn't state


1409 
the form of ServTicket. The guarantee becomes stronger.*)


1410 
by (case_tac "Key AuthKey : analz (spies evs5)" 1);


1411 
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS


1412 
analz.Decrypt RS analz.Fst],


1413 
simpset()) 1);


1414 
by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy',


1415 
impOfSubs parts_spies_takeWhile_mono,


1416 
impOfSubs parts_spies_evs_revD2]


1417 
addIs [Says_Auth]


1418 
addEs spies_partsEs) 1);


1419 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);


1420 
qed "A_Knows_A_Knows_ServKey_lemma";


1421 


1422 
Goal "[ Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} \


1423 
\ : set evs; \


1424 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\


1425 
\ : parts (spies evs);\


1426 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}\


1427 
\ : parts (spies evs); \


1428 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;\


1429 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1430 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs";


1431 
by (blast_tac (claset() addSDs [Confidentiality_Serv_A,


1432 
A_Knows_A_Knows_ServKey_lemma]) 1);


1433 
qed "A_Knows_A_Knows_ServKey";


1434 


1435 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \


1436 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1437 
\ : parts (spies evs); \


1438 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \


1439 
\ : parts (spies evs); \


1440 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \


1441 
\ : parts (spies evs); \


1442 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \


1443 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1444 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs";


1445 
by (blast_tac (claset() addDs [A_Authenticity, Confidentiality_B,


1446 
A_Knows_A_Knows_ServKey_lemma]) 1);


1447 
qed "B_Knows_A_Knows_ServKey";


1448 


1449 


1450 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \


1451 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \


1452 
\ : parts (spies evs); \


1453 
\ ~ ExpirServ Tt evs; \


1454 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \


1455 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs";


1456 
by (blast_tac (claset() addDs [A_Authenticity_refined,


1457 
Confidentiality_B_refined,


1458 
A_Knows_A_Knows_ServKey_lemma]) 1);


1459 
qed "B_Knows_A_Knows_ServKey_refined";
