addition of Kerberos IV example
authorpaulson
Tue Apr 20 14:33:48 1999 +0200 (1999-04-20)
changeset 64526a1b393ccdc0
parent 6451 bc943acc5fda
child 6453 c97d80581572
addition of Kerberos IV example
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/README.html
src/HOL/Auth/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/KerberosIV.ML	Tue Apr 20 14:33:48 1999 +0200
     1.3 @@ -0,0 +1,1460 @@
     1.4 +(*  Title:      HOL/Auth/KerberosIV
     1.5 +    ID:         $Id$
     1.6 +    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +The Kerberos protocol, version IV.
    1.10 +*)
    1.11 +
    1.12 +Pretty.setdepth 20;
    1.13 +proof_timing:=true;
    1.14 +HOL_quantifiers := false;
    1.15 +
    1.16 +AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
    1.17 +
    1.18 +
    1.19 +(** Reversed traces **)
    1.20 +
    1.21 +Goal "spies (evs @ [Says A B X]) = insert X (spies evs)";
    1.22 +by (induct_tac "evs" 1);
    1.23 +by (induct_tac "a" 2);
    1.24 +by Auto_tac;
    1.25 +qed "spies_Says_rev";
    1.26 +
    1.27 +Goal "spies (evs @ [Gets A X]) = spies evs";
    1.28 +by (induct_tac "evs" 1);
    1.29 +by (induct_tac "a" 2);
    1.30 +by Auto_tac;
    1.31 +qed "spies_Gets_rev";
    1.32 +
    1.33 +Goal "spies (evs @ [Notes A X]) = \
    1.34 +\         (if A:bad then insert X (spies evs) else spies evs)";
    1.35 +by (induct_tac "evs" 1);
    1.36 +by (induct_tac "a" 2);
    1.37 +by Auto_tac;
    1.38 +qed "spies_Notes_rev";
    1.39 +
    1.40 +Goal "spies evs = spies (rev evs)";
    1.41 +by (induct_tac "evs" 1);
    1.42 +by (induct_tac "a" 2);
    1.43 +by (ALLGOALS 
    1.44 +    (asm_simp_tac (simpset() addsimps [spies_Says_rev, spies_Gets_rev, 
    1.45 +				       spies_Notes_rev])));
    1.46 +qed "spies_evs_rev";
    1.47 +bind_thm ("parts_spies_evs_revD2", spies_evs_rev RS equalityD2 RS parts_mono);
    1.48 +
    1.49 +Goal "spies (takeWhile P evs)  <=  spies evs";
    1.50 +by (induct_tac "evs" 1);
    1.51 +by (induct_tac "a" 2);
    1.52 +by Auto_tac;
    1.53 +(* Resembles "used_subset_append" in Event.ML*)
    1.54 +qed "spies_takeWhile";
    1.55 +bind_thm ("parts_spies_takeWhile_mono", spies_takeWhile RS parts_mono);
    1.56 +
    1.57 +Goal "~P(x) --> takeWhile P (xs @ [x]) = takeWhile P xs";
    1.58 +by (induct_tac "xs" 1);
    1.59 +by Auto_tac;
    1.60 +qed "takeWhile_tail";
    1.61 +
    1.62 +
    1.63 +(*****************LEMMAS ABOUT AuthKeys****************)
    1.64 +
    1.65 +Goalw [AuthKeys_def] "AuthKeys [] = {}";
    1.66 +by (Simp_tac 1);
    1.67 +qed "AuthKeys_empty";
    1.68 +
    1.69 +Goalw [AuthKeys_def] 
    1.70 + "(ALL A Tk akey Peer.              \
    1.71 +\  ev ~= Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,      \
    1.72 +\             (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))\ 
    1.73 +\      ==> AuthKeys (ev # evs) = AuthKeys evs";
    1.74 +by Auto_tac;
    1.75 +qed "AuthKeys_not_insert";
    1.76 +
    1.77 +Goalw [AuthKeys_def] 
    1.78 +  "AuthKeys \
    1.79 +\    (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk, \
    1.80 +\     (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs) \
    1.81 +\      = insert K (AuthKeys evs)";
    1.82 +by Auto_tac;
    1.83 +qed "AuthKeys_insert";
    1.84 +
    1.85 +Goalw [AuthKeys_def] 
    1.86 +   "K : AuthKeys \
    1.87 +\   (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk, \
    1.88 +\    (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs) \
    1.89 +\       ==> K = K' | K : AuthKeys evs";
    1.90 +by Auto_tac;
    1.91 +qed "AuthKeys_simp";
    1.92 +
    1.93 +Goalw [AuthKeys_def]  
    1.94 +   "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk, \
    1.95 +\    (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) : set evs \
    1.96 +\       ==> K : AuthKeys evs";
    1.97 +by Auto_tac;
    1.98 +qed "AuthKeysI";
    1.99 +
   1.100 +Goalw [AuthKeys_def] "K : AuthKeys evs ==> Key K : used evs";
   1.101 +by (Simp_tac 1);
   1.102 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.103 +qed "AuthKeys_used";
   1.104 +
   1.105 +
   1.106 +(**** FORWARDING LEMMAS ****)
   1.107 +
   1.108 +(*--For reasoning about the encrypted portion of message K3--*)
   1.109 +Goal "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
   1.110 +\              : set evs ==> AuthTicket : parts (spies evs)";
   1.111 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.112 +qed "K3_msg_in_parts_spies";
   1.113 +
   1.114 +Goal "Says Kas A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
   1.115 +\              : set evs ==> AuthKey : parts (spies evs)";
   1.116 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.117 +qed "Oops_parts_spies1";
   1.118 +                              
   1.119 +Goal "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|}) \
   1.120 +\          : set evs ;\
   1.121 +\        evs : kerberos |] ==> AuthKey ~: range shrK";
   1.122 +by (etac rev_mp 1);
   1.123 +by (etac kerberos.induct 1);
   1.124 +by Auto_tac;
   1.125 +qed "Oops_range_spies1";
   1.126 +
   1.127 +(*--For reasoning about the encrypted portion of message K5--*)
   1.128 +Goal "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
   1.129 + \             : set evs ==> ServTicket : parts (spies evs)";
   1.130 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.131 +qed "K5_msg_in_parts_spies";
   1.132 +
   1.133 +Goal "Says Tgs A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
   1.134 +\                  : set evs ==> ServKey : parts (spies evs)";
   1.135 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.136 +qed "Oops_parts_spies2";
   1.137 +
   1.138 +Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) \
   1.139 +\          : set evs ;\
   1.140 +\        evs : kerberos |] ==> ServKey ~: range shrK";
   1.141 +by (etac rev_mp 1);
   1.142 +by (etac kerberos.induct 1);
   1.143 +by Auto_tac;
   1.144 +qed "Oops_range_spies2";
   1.145 +
   1.146 +Goal "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) : set evs \
   1.147 +\     ==> Ticket : parts (spies evs)";
   1.148 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.149 +qed "Says_ticket_in_parts_spies";
   1.150 +(*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*)
   1.151 +
   1.152 +fun parts_induct_tac i = 
   1.153 +    etac kerberos.induct i  THEN 
   1.154 +    REPEAT (FIRSTGOAL analz_mono_contra_tac)  THEN
   1.155 +    forward_tac [K3_msg_in_parts_spies] (i+4)  THEN
   1.156 +    forward_tac [K5_msg_in_parts_spies] (i+6)  THEN
   1.157 +    forward_tac [Oops_parts_spies1] (i+8)  THEN
   1.158 +    forward_tac [Oops_parts_spies2] (i+9) THEN
   1.159 +    prove_simple_subgoals_tac 1;
   1.160 +
   1.161 +
   1.162 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   1.163 +Goal "evs : kerberos ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   1.164 +by (parts_induct_tac 1);
   1.165 +by (Fake_parts_insert_tac 1);
   1.166 +by (ALLGOALS Blast_tac);
   1.167 +qed "Spy_see_shrK";
   1.168 +Addsimps [Spy_see_shrK];
   1.169 +
   1.170 +Goal "evs : kerberos ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   1.171 +by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset()));
   1.172 +qed "Spy_analz_shrK";
   1.173 +Addsimps [Spy_analz_shrK];
   1.174 +
   1.175 +Goal "[| Key (shrK A) : parts (spies evs);  evs : kerberos |] ==> A:bad";
   1.176 +by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
   1.177 +qed "Spy_see_shrK_D";
   1.178 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   1.179 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   1.180 +
   1.181 +(*Nobody can have used non-existent keys!*)
   1.182 +Goal "evs : kerberos ==>      \
   1.183 +\     Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   1.184 +by (parts_induct_tac 1);
   1.185 +(*Fake*)
   1.186 +by (best_tac
   1.187 +      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   1.188 +               addIs  [impOfSubs analz_subset_parts]
   1.189 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
   1.190 +               addss  (simpset())) 1);
   1.191 +(*Others*)
   1.192 +by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
   1.193 +qed_spec_mp "new_keys_not_used";
   1.194 +
   1.195 +bind_thm ("new_keys_not_analzd",
   1.196 +          [analz_subset_parts RS keysFor_mono,
   1.197 +           new_keys_not_used] MRS contra_subsetD);
   1.198 +
   1.199 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.200 +
   1.201 +
   1.202 +(*********************** REGULARITY LEMMAS ***********************)
   1.203 +(*       concerning the form of items passed in messages         *)
   1.204 +(*****************************************************************)
   1.205 +
   1.206 +(*Describes the form of AuthKey, AuthTicket, and K sent by Kas*)
   1.207 +Goal "[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|}) \
   1.208 +\          : set evs;                 \
   1.209 +\        evs : kerberos |]             \
   1.210 +\     ==> AuthKey ~: range shrK & AuthKey : AuthKeys evs & \
   1.211 +\ AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|} ) &\
   1.212 +\            K = shrK A  & Peer = Tgs";
   1.213 +by (etac rev_mp 1);
   1.214 +by (etac kerberos.induct 1);
   1.215 +by (ALLGOALS (simp_tac (simpset() addsimps [AuthKeys_def, AuthKeys_insert])));
   1.216 +by (ALLGOALS Blast_tac);
   1.217 +qed "Says_Kas_message_form";
   1.218 +
   1.219 +(*This lemma is essential for proving Says_Tgs_message_form: 
   1.220 +  
   1.221 +  the session key AuthKey
   1.222 +  supplied by Kas in the authentication ticket
   1.223 +  cannot be a long-term key!
   1.224 +
   1.225 +  Generalised to any session keys (both AuthKey and ServKey).
   1.226 +*)
   1.227 +Goal "[| Crypt (shrK Tgs_B) {|Agent A, Agent Tgs_B, Key SesKey, Number T|}\
   1.228 +\           : parts (spies evs); Tgs_B ~: bad;\
   1.229 +\        evs : kerberos |]    \
   1.230 +\     ==> SesKey ~: range shrK";
   1.231 +by (etac rev_mp 1);
   1.232 +by (parts_induct_tac 1);
   1.233 +by (Fake_parts_insert_tac 1);
   1.234 +qed "SesKey_is_session_key";
   1.235 +
   1.236 +Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}  \
   1.237 +\          : parts (spies evs);                              \
   1.238 +\        evs : kerberos |]                          \
   1.239 +\     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, \
   1.240 +\                Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})  \
   1.241 +\           : set evs";
   1.242 +by (etac rev_mp 1);
   1.243 +by (parts_induct_tac 1);
   1.244 +(*Fake*)
   1.245 +by (Fake_parts_insert_tac 1);
   1.246 +(*K4*)
   1.247 +by (Blast_tac 1);
   1.248 +qed "A_trusts_AuthTicket";
   1.249 +
   1.250 +Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}\
   1.251 +\          : parts (spies evs);\
   1.252 +\        evs : kerberos |]    \
   1.253 +\     ==> AuthKey : AuthKeys evs";
   1.254 +by (forward_tac [A_trusts_AuthTicket] 1);
   1.255 +by (assume_tac 1);
   1.256 +by (simp_tac (simpset() addsimps [AuthKeys_def]) 1);
   1.257 +by (Blast_tac 1);
   1.258 +qed "AuthTicket_crypt_AuthKey";
   1.259 +
   1.260 +(*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*)
   1.261 +Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
   1.262 +\          : set evs; \
   1.263 +\        evs : kerberos |]    \
   1.264 +\  ==> B ~= Tgs & ServKey ~: range shrK & ServKey ~: AuthKeys evs &\
   1.265 +\      ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|} ) & \
   1.266 +\      AuthKey ~: range shrK & AuthKey : AuthKeys evs";
   1.267 +by (etac rev_mp 1);
   1.268 +by (etac kerberos.induct 1);
   1.269 +by (ALLGOALS
   1.270 +    (asm_full_simp_tac
   1.271 +     (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert,
   1.272 +			  AuthKeys_empty, AuthKeys_simp])));
   1.273 +by (blast_tac (claset() addEs  spies_partsEs) 1);
   1.274 +by Auto_tac;
   1.275 +by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1);
   1.276 +by (blast_tac (claset() addSDs [SesKey_is_session_key]
   1.277 +                        addEs spies_partsEs) 1);
   1.278 +by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey] 
   1.279 +                        addEs spies_partsEs) 1);
   1.280 +qed "Says_Tgs_message_form";
   1.281 +
   1.282 +(*If a certain encrypted message appears then it originated with Kas*)
   1.283 +Goal "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}  \
   1.284 +\          : parts (spies evs);                              \
   1.285 +\        A ~: bad;  evs : kerberos |]                        \
   1.286 +\     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})  \
   1.287 +\           : set evs";
   1.288 +by (etac rev_mp 1);
   1.289 +by (parts_induct_tac 1);
   1.290 +(*Fake*)
   1.291 +by (Fake_parts_insert_tac 1);
   1.292 +(*K4*)
   1.293 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst,
   1.294 +			       A_trusts_AuthTicket RS Says_Kas_message_form])
   1.295 +    1);
   1.296 +qed "A_trusts_AuthKey";
   1.297 +
   1.298 +
   1.299 +(*If a certain encrypted message appears then it originated with Tgs*)
   1.300 +Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}     \
   1.301 +\          : parts (spies evs);                                     \
   1.302 +\        Key AuthKey ~: analz (spies evs);           \
   1.303 +\        AuthKey ~: range shrK;                      \
   1.304 +\        evs : kerberos |]         \
   1.305 +\==> EX A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
   1.306 +\      : set evs";
   1.307 +by (etac rev_mp 1);
   1.308 +by (etac rev_mp 1);
   1.309 +by (parts_induct_tac 1);
   1.310 +(*Fake*)
   1.311 +by (Fake_parts_insert_tac 1);
   1.312 +(*K2*)
   1.313 +by (Blast_tac 1);
   1.314 +(*K4*)
   1.315 +by Auto_tac;
   1.316 +qed "A_trusts_K4";
   1.317 +
   1.318 +Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} \
   1.319 +\          : parts (spies evs);          \
   1.320 +\        A ~: bad;                       \
   1.321 +\        evs : kerberos |]                \
   1.322 +\   ==> AuthKey ~: range shrK &               \
   1.323 +\       AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}";
   1.324 +by (etac rev_mp 1);
   1.325 +by (parts_induct_tac 1);
   1.326 +by (Fake_parts_insert_tac 1);
   1.327 +by (Blast_tac 1);
   1.328 +qed "AuthTicket_form";
   1.329 +
   1.330 +(* This form holds also over an AuthTicket, but is not needed below.     *)
   1.331 +Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|} \
   1.332 +\             : parts (spies evs); \
   1.333 +\           Key AuthKey ~: analz (spies evs);  \
   1.334 +\           evs : kerberos |]                                       \
   1.335 +\        ==> ServKey ~: range shrK &  \
   1.336 +\   (EX A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})";
   1.337 +by (etac rev_mp 1);
   1.338 +by (etac rev_mp 1);
   1.339 +by (parts_induct_tac 1);
   1.340 +by (Fake_parts_insert_tac 1);
   1.341 +qed "ServTicket_form";
   1.342 +
   1.343 +Goal "[| Says Kas' A (Crypt (shrK A) \
   1.344 +\             {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} ) : set evs; \
   1.345 +\        evs : kerberos |]    \
   1.346 +\     ==> AuthKey ~: range shrK & \
   1.347 +\         AuthTicket = \
   1.348 +\                 Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}\
   1.349 +\         | AuthTicket : analz (spies evs)";
   1.350 +by (case_tac "A : bad" 1);
   1.351 +by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);
   1.352 +by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   1.353 +by (blast_tac (claset() addSDs [AuthTicket_form]) 1);
   1.354 +qed "Says_kas_message_form";
   1.355 +(* Essentially the same as AuthTicket_form *)
   1.356 +
   1.357 +Goal "[| Says Tgs' A (Crypt AuthKey \
   1.358 +\             {|Key ServKey, Agent B, Tt, ServTicket|} ) : set evs; \
   1.359 +\        evs : kerberos |]    \
   1.360 +\     ==> ServKey ~: range shrK & \
   1.361 +\         (EX A. ServTicket = \
   1.362 +\                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})  \
   1.363 +\          | ServTicket : analz (spies evs)";
   1.364 +by (case_tac "Key AuthKey : analz (spies evs)" 1);
   1.365 +by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);
   1.366 +by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   1.367 +by (blast_tac (claset() addSDs [ServTicket_form]) 1);
   1.368 +qed "Says_tgs_message_form";
   1.369 +(* This form MUST be used in analz_sees_tac below *)
   1.370 +
   1.371 +
   1.372 +(*****************UNICITY THEOREMS****************)
   1.373 +
   1.374 +(* The session key, if secure, uniquely identifies the Ticket
   1.375 +   whether AuthTicket or ServTicket. As a matter of fact, one can read
   1.376 +   also Tgs in the place of B.                                     *)
   1.377 +Goal "evs : kerberos ==>                                        \
   1.378 +\     Key SesKey ~: analz (spies evs) -->   \
   1.379 +\     (EX A B T. ALL A' B' T'.                          \
   1.380 +\      Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}    \
   1.381 +\        : parts (spies evs) --> A'=A & B'=B & T'=T)";
   1.382 +by (parts_induct_tac 1);
   1.383 +by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   1.384 +    THEN Fake_parts_insert_tac 1);
   1.385 +by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   1.386 +by (expand_case_tac "SesKey = ?y" 1);
   1.387 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.388 +by (expand_case_tac "SesKey = ?y" 1);
   1.389 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.390 +val lemma = result();
   1.391 +
   1.392 +Goal "[| Crypt (shrK B)  {|Agent A,  Agent B,  Key SesKey, T|}        \
   1.393 +\          : parts (spies evs);            \
   1.394 +\        Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}     \
   1.395 +\          : parts (spies evs);            \
   1.396 +\        evs : kerberos;  Key SesKey ~: analz (spies evs) |]  \
   1.397 +\     ==> A=A' & B=B' & T=T'";
   1.398 +by (prove_unique_tac lemma 1);
   1.399 +qed "unique_CryptKey";
   1.400 +
   1.401 +Goal "evs : kerberos \
   1.402 +\     ==> Key SesKey ~: analz (spies evs) -->   \
   1.403 +\         (EX K' B' T' Ticket'. ALL K B T Ticket.                          \
   1.404 +\          Crypt K {|Key SesKey, Agent B, T, Ticket|}    \
   1.405 +\            : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
   1.406 +by (parts_induct_tac 1);
   1.407 +by (REPEAT (etac (exI RSN (2,exE)) 1) THEN Fake_parts_insert_tac 1);
   1.408 +by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   1.409 +by (expand_case_tac "SesKey = ?y" 1);
   1.410 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.411 +by (expand_case_tac "SesKey = ?y" 1);
   1.412 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.413 +val lemma = result();
   1.414 +
   1.415 +(*An AuthKey is encrypted by one and only one Shared key.
   1.416 +  A ServKey is encrypted by one and only one AuthKey.
   1.417 +*)
   1.418 +Goal "[| Crypt K  {|Key SesKey,  Agent B, T, Ticket|}        \
   1.419 +\          : parts (spies evs);            \
   1.420 +\        Crypt K' {|Key SesKey,  Agent B', T', Ticket'|}     \
   1.421 +\          : parts (spies evs);            \
   1.422 +\        evs : kerberos;  Key SesKey ~: analz (spies evs) |]  \
   1.423 +\     ==> K=K' & B=B' & T=T' & Ticket=Ticket'";
   1.424 +by (prove_unique_tac lemma 1);
   1.425 +qed "Key_unique_SesKey";
   1.426 +
   1.427 +
   1.428 +(*
   1.429 +  At reception of any message mentioning A, Kas associates shrK A with
   1.430 +  a new AuthKey. Realistic, as the user gets a new AuthKey at each login.
   1.431 +  Similarly, at reception of any message mentioning an AuthKey
   1.432 +  (a legitimate user could make several requests to Tgs - by K3), Tgs 
   1.433 +  associates it with a new ServKey.
   1.434 +
   1.435 +  Therefore, a goal like
   1.436 +
   1.437 +   "evs : kerberos \
   1.438 +  \  ==> Key Kc ~: analz (spies evs) -->   \
   1.439 +  \        (EX K' B' T' Ticket'. ALL K B T Ticket.                          \
   1.440 +  \         Crypt Kc {|Key K, Agent B, T, Ticket|}    \
   1.441 +  \          : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
   1.442 +
   1.443 +  would fail on the K2 and K4 cases.
   1.444 +*)
   1.445 +
   1.446 +(* AuthKey uniquely identifies the message from Kas *)
   1.447 +Goal "evs : kerberos ==>                                        \
   1.448 +\      EX A' Ka' Tk' X'. ALL A Ka Tk X.                          \
   1.449 +\        Says Kas A (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|})  \
   1.450 +\          : set evs --> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
   1.451 +by (etac kerberos.induct 1);
   1.452 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.453 +by (Step_tac 1);
   1.454 +(*K2: it can't be a new key*)
   1.455 +by (expand_case_tac "AuthKey = ?y" 1);
   1.456 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.457 +by (blast_tac (claset() delrules [conjI]   (*prevent split-up into 4 subgoals*)
   1.458 +                      addSEs spies_partsEs) 1);
   1.459 +val lemma = result();
   1.460 +
   1.461 +Goal "[| Says Kas A                                          \
   1.462 +\             (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) : set evs;     \ 
   1.463 +\        Says Kas A'                                         \
   1.464 +\             (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) : set evs;   \
   1.465 +\        evs : kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
   1.466 +by (prove_unique_tac lemma 1);
   1.467 +qed "unique_AuthKeys";
   1.468 +
   1.469 +(* ServKey uniquely identifies the message from Tgs *)
   1.470 +Goal "evs : kerberos ==>                                        \
   1.471 +\      EX A' B' AuthKey' Tk' X'. ALL A B AuthKey Tk X.                     \
   1.472 +\        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tk, X|})  \
   1.473 +\          : set evs --> A=A' & B=B' & AuthKey=AuthKey' & Tk=Tk' & X=X'";
   1.474 +by (etac kerberos.induct 1);
   1.475 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.476 +by (Step_tac 1);
   1.477 +(*K4: it can't be a new key*)
   1.478 +by (expand_case_tac "ServKey = ?y" 1);
   1.479 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.480 +by (blast_tac (claset() delrules [conjI]   (*prevent split-up into 4 subgoals*)
   1.481 +                      addSEs spies_partsEs) 1);
   1.482 +val lemma = result();
   1.483 +
   1.484 +Goal "[| Says Tgs A                                             \
   1.485 +\             (Crypt K {|Key ServKey, Agent B, Tt, X|}) : set evs; \ 
   1.486 +\        Says Tgs A'                                                 \
   1.487 +\             (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) : set evs; \
   1.488 +\        evs : kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
   1.489 +by (prove_unique_tac lemma 1);
   1.490 +qed "unique_ServKeys";
   1.491 +
   1.492 +
   1.493 +(*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
   1.494 +
   1.495 +Goalw [KeyCryptKey_def] "~ KeyCryptKey AuthKey ServKey []";
   1.496 +by (Simp_tac 1);
   1.497 +qed "not_KeyCryptKey_Nil";
   1.498 +AddIffs [not_KeyCryptKey_Nil];
   1.499 +
   1.500 +Goalw [KeyCryptKey_def]
   1.501 + "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
   1.502 +\             : set evs;    \
   1.503 +\           evs : kerberos |] ==> KeyCryptKey AuthKey ServKey evs";
   1.504 +by (forward_tac [Says_Tgs_message_form] 1);
   1.505 +by (assume_tac 1);
   1.506 +by (Blast_tac 1);
   1.507 +qed "KeyCryptKeyI";
   1.508 +
   1.509 +Goalw [KeyCryptKey_def]
   1.510 +   "KeyCryptKey AuthKey ServKey (Says S A X # evs) =                       \
   1.511 +\    (Tgs = S &                                                            \
   1.512 +\     (EX B tt. X = Crypt AuthKey        \
   1.513 +\               {|Key ServKey, Agent B, tt,  \
   1.514 +\                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |}) \
   1.515 +\    | KeyCryptKey AuthKey ServKey evs)";
   1.516 +by (Simp_tac 1);
   1.517 +by (Blast_tac 1);
   1.518 +qed "KeyCryptKey_Says";
   1.519 +Addsimps [KeyCryptKey_Says];
   1.520 +
   1.521 +(*A fresh AuthKey cannot be associated with any other
   1.522 +  (with respect to a given trace). *)
   1.523 +Goalw [KeyCryptKey_def]
   1.524 + "[| Key AuthKey ~: used evs; evs : kerberos |] \
   1.525 +\        ==> ~ KeyCryptKey AuthKey ServKey evs";
   1.526 +by (etac rev_mp 1);
   1.527 +by (parts_induct_tac 1);
   1.528 +by (Asm_full_simp_tac 1);
   1.529 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.530 +qed "Auth_fresh_not_KeyCryptKey";
   1.531 +
   1.532 +(*A fresh ServKey cannot be associated with any other
   1.533 +  (with respect to a given trace). *)
   1.534 +Goalw [KeyCryptKey_def]
   1.535 + "Key ServKey ~: used evs ==> ~ KeyCryptKey AuthKey ServKey evs";
   1.536 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.537 +qed "Serv_fresh_not_KeyCryptKey";
   1.538 +
   1.539 +Goalw [KeyCryptKey_def]
   1.540 + "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
   1.541 +\             : parts (spies evs);  evs : kerberos |] \
   1.542 +\        ==> ~ KeyCryptKey K AuthKey evs";
   1.543 +by (etac rev_mp 1);
   1.544 +by (parts_induct_tac 1);
   1.545 +(*K4*)
   1.546 +by (blast_tac (claset() addEs spies_partsEs) 3);
   1.547 +(*K2: by freshness*)
   1.548 +by (blast_tac (claset() addEs spies_partsEs) 2);
   1.549 +by (Fake_parts_insert_tac 1);
   1.550 +qed "AuthKey_not_KeyCryptKey";
   1.551 +
   1.552 +(*A secure serverkey cannot have been used to encrypt others*)
   1.553 +Goalw [KeyCryptKey_def]
   1.554 + "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} \
   1.555 +\             : parts (spies evs);                     \
   1.556 +\           Key ServKey ~: analz (spies evs);             \
   1.557 +\           B ~= Tgs;  evs : kerberos |] \
   1.558 +\        ==> ~ KeyCryptKey ServKey K evs";
   1.559 +by (etac rev_mp 1);
   1.560 +by (etac rev_mp 1);
   1.561 +by (parts_induct_tac 1);
   1.562 +by (Fake_parts_insert_tac 1);
   1.563 +(*K4 splits into distinct subcases*)
   1.564 +by (Step_tac 1);
   1.565 +by (ALLGOALS Asm_full_simp_tac);
   1.566 +(*ServKey can't have been enclosed in two certificates*)
   1.567 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   1.568 +                       addSEs [MPair_parts]
   1.569 +                       addDs  [unique_CryptKey]) 4);
   1.570 +(*ServKey is fresh and so could not have been used, by new_keys_not_used*)
   1.571 +by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
   1.572 +				Crypt_imp_invKey_keysFor],
   1.573 +	       simpset()) 2); 
   1.574 +(*Others by freshness*)
   1.575 +by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
   1.576 +qed "ServKey_not_KeyCryptKey";
   1.577 +
   1.578 +(*Long term keys are not issued as ServKeys*)
   1.579 +Goalw [KeyCryptKey_def]
   1.580 + "evs : kerberos ==> ~ KeyCryptKey K (shrK A) evs";
   1.581 +by (parts_induct_tac 1);
   1.582 +qed "shrK_not_KeyCryptKey";
   1.583 +
   1.584 +(*The Tgs message associates ServKey with AuthKey and therefore not with any 
   1.585 +  other key AuthKey.*)
   1.586 +Goalw [KeyCryptKey_def]
   1.587 + "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
   1.588 +\      : set evs;                                         \
   1.589 +\    AuthKey' ~= AuthKey;  evs : kerberos |]                      \
   1.590 +\ ==> ~ KeyCryptKey AuthKey' ServKey evs";
   1.591 +by (blast_tac (claset() addDs [unique_ServKeys]) 1);
   1.592 +qed "Says_Tgs_KeyCryptKey";
   1.593 +
   1.594 +Goal "[| KeyCryptKey AuthKey ServKey evs;  evs : kerberos |] \
   1.595 +\     ==> ~ KeyCryptKey ServKey K evs";
   1.596 +by (etac rev_mp 1);
   1.597 +by (parts_induct_tac 1);
   1.598 +by (Step_tac 1);
   1.599 +by (ALLGOALS Asm_full_simp_tac);
   1.600 +(*K4 splits into subcases*)
   1.601 +by (blast_tac (claset() addEs spies_partsEs 
   1.602 +                       addSDs [AuthKey_not_KeyCryptKey]) 4);
   1.603 +(*ServKey is fresh and so could not have been used, by new_keys_not_used*)
   1.604 +by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
   1.605 +				Crypt_imp_invKey_keysFor],
   1.606 +                      simpset() addsimps [KeyCryptKey_def]) 2); 
   1.607 +(*Others by freshness*)
   1.608 +by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
   1.609 +qed "KeyCryptKey_not_KeyCryptKey";
   1.610 +
   1.611 +(*The only session keys that can be found with the help of session keys are
   1.612 +  those sent by Tgs in step K4.  *)
   1.613 +
   1.614 +(*We take some pains to express the property
   1.615 +  as a logical equivalence so that the simplifier can apply it.*)
   1.616 +Goal "P --> (Key K : analz (Key``KK Un H)) --> (K:KK | Key K : analz H)  \
   1.617 +\     ==>       \
   1.618 +\     P --> (Key K : analz (Key``KK Un H)) = (K:KK | Key K : analz H)";
   1.619 +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   1.620 +qed "Key_analz_image_Key_lemma";
   1.621 +
   1.622 +Goal "[| KeyCryptKey K K' evs; evs : kerberos |] \
   1.623 +\     ==> Key K' : analz (insert (Key K) (spies evs))";
   1.624 +by (full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
   1.625 +by (Clarify_tac 1);
   1.626 +by (dresolve_tac [Says_imp_spies RS analz.Inj RS analz_insertI] 1);
   1.627 +by Auto_tac;
   1.628 +qed "KeyCryptKey_analz_insert";
   1.629 +
   1.630 +Goal "[| K : AuthKeys evs Un range shrK;  evs : kerberos |]  \
   1.631 +\     ==> ALL SK. ~ KeyCryptKey SK K evs";
   1.632 +by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
   1.633 +by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
   1.634 +qed "AuthKeys_are_not_KeyCryptKey";
   1.635 +
   1.636 +Goal "[| K ~: AuthKeys evs; \
   1.637 +\        K ~: range shrK; evs : kerberos |]  \
   1.638 +\     ==> ALL SK. ~ KeyCryptKey K SK evs";
   1.639 +by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
   1.640 +by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
   1.641 +qed "not_AuthKeys_not_KeyCryptKey";
   1.642 +
   1.643 +
   1.644 +(*****************SECRECY THEOREMS****************)
   1.645 +
   1.646 +(*For proofs involving analz.*)
   1.647 +val analz_sees_tac = 
   1.648 +  EVERY 
   1.649 +   [REPEAT (FIRSTGOAL analz_mono_contra_tac),
   1.650 +    forward_tac [Oops_range_spies2] 10, 
   1.651 +    forward_tac [Oops_range_spies1] 9, 
   1.652 +    forward_tac [Says_tgs_message_form] 7,
   1.653 +    forward_tac [Says_kas_message_form] 5, 
   1.654 +    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
   1.655 +		  ORELSE' hyp_subst_tac)];
   1.656 +
   1.657 +Goal "[| KK <= -(range shrK); Key K : analz (spies evs); evs: kerberos |]   \
   1.658 +\     ==> Key K : analz (Key `` KK Un spies evs)";
   1.659 +by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
   1.660 +qed "analz_mono_KK";
   1.661 +
   1.662 +(* Big simplification law for keys SK that are not crypted by keys in KK   *)
   1.663 +(* It helps prove three, otherwise hard, facts about keys. These facts are *)
   1.664 +(* exploited as simplification laws for analz, and also "limit the damage" *)
   1.665 +(* in case of loss of a key to the spy. See ESORICS98.                     *)
   1.666 +Goal "evs : kerberos ==>                                         \
   1.667 +\     (ALL SK KK. KK <= -(range shrK) -->                   \
   1.668 +\     (ALL K: KK. ~ KeyCryptKey K SK evs)   -->           \
   1.669 +\     (Key SK : analz (Key``KK Un (spies evs))) =        \
   1.670 +\     (SK : KK | Key SK : analz (spies evs)))";
   1.671 +by (etac kerberos.induct 1);
   1.672 +by analz_sees_tac;
   1.673 +by (REPEAT_FIRST (rtac allI));
   1.674 +by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI)));
   1.675 +by (ALLGOALS  
   1.676 +    (asm_simp_tac 
   1.677 +     (analz_image_freshK_ss addsimps
   1.678 +        [KeyCryptKey_Says, shrK_not_KeyCryptKey, 
   1.679 +	 Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 
   1.680 +	 Says_Tgs_KeyCryptKey, Spy_analz_shrK])));
   1.681 +(*Fake*) 
   1.682 +by (spy_analz_tac 1);
   1.683 +(* Base + K2 done by the simplifier! *)
   1.684 +(*K3*)
   1.685 +by (Blast_tac 1);
   1.686 +(*K4*)
   1.687 +by (blast_tac (claset() addEs spies_partsEs 
   1.688 +                        addSDs [AuthKey_not_KeyCryptKey]) 1);
   1.689 +(*K5*)
   1.690 +by (rtac impI 1);
   1.691 +by (case_tac "Key ServKey : analz (spies evs5)" 1);
   1.692 +(*If ServKey is compromised then the result follows directly...*)
   1.693 +by (asm_simp_tac 
   1.694 +     (simpset() addsimps [analz_insert_eq, 
   1.695 +			 impOfSubs (Un_upper2 RS analz_mono)]) 1);
   1.696 +(*...therefore ServKey is uncompromised.*)
   1.697 +by (case_tac "KeyCryptKey ServKey SK evs5" 1);
   1.698 +by (asm_simp_tac analz_image_freshK_ss 2);
   1.699 +(*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*)
   1.700 +by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)]
   1.701 +		        addEs spies_partsEs delrules [allE, ballE]) 1);
   1.702 +(** Level 14: Oops1 and Oops2 **)
   1.703 +by (ALLGOALS Clarify_tac);
   1.704 +(*Oops 2*)
   1.705 +by (case_tac "Key ServKey : analz (spies evsO2)" 2);
   1.706 +by (ALLGOALS Asm_full_simp_tac);
   1.707 +by (forward_tac [analz_mono_KK] 2
   1.708 +    THEN assume_tac 2
   1.709 +    THEN assume_tac 2);
   1.710 +by (forward_tac [analz_cut] 2 THEN assume_tac 2);
   1.711 +by (blast_tac (claset() addDs [analz_cut, impOfSubs analz_mono]) 2);
   1.712 +by (dres_inst_tac [("x","SK")] spec 2);
   1.713 +by (dres_inst_tac [("x","insert ServKey KK")] spec 2);
   1.714 +by (forward_tac [Says_Tgs_message_form] 2 THEN assume_tac 2);
   1.715 +by (Clarify_tac 2);
   1.716 +by (forward_tac [Says_imp_spies RS parts.Inj RS parts.Body 
   1.717 +                 RS parts.Snd RS parts.Snd RS parts.Snd] 2);
   1.718 +by (Asm_full_simp_tac 2);
   1.719 +by (blast_tac (claset() addSDs [ServKey_not_KeyCryptKey] 
   1.720 +                        addDs [impOfSubs analz_mono]) 2);
   1.721 +(*Level 28: Oops 1*)
   1.722 +by (dres_inst_tac [("x","SK")] spec 1);
   1.723 +by (dres_inst_tac [("x","insert AuthKey KK")] spec 1);
   1.724 +by (case_tac "KeyCryptKey AuthKey SK evsO1" 1);
   1.725 +by (ALLGOALS Asm_full_simp_tac);
   1.726 +by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
   1.727 +by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
   1.728 +qed_spec_mp "Key_analz_image_Key";
   1.729 +
   1.730 +
   1.731 +(* First simplification law for analz: no session keys encrypt  *)
   1.732 +(* authentication keys or shared keys.                          *)
   1.733 +Goal "[| evs : kerberos;  K : (AuthKeys evs) Un range shrK;      \
   1.734 +\        SesKey ~: range shrK |]                                 \
   1.735 +\     ==> Key K : analz (insert (Key SesKey) (spies evs)) = \
   1.736 +\         (K = SesKey | Key K : analz (spies evs))";
   1.737 +by (forward_tac [AuthKeys_are_not_KeyCryptKey] 1 THEN assume_tac 1);
   1.738 +by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
   1.739 +qed "analz_insert_freshK1";
   1.740 +
   1.741 +
   1.742 +(* Second simplification law for analz: no service keys encrypt *)
   1.743 +(* any other keys.					        *)
   1.744 +Goal "[| evs : kerberos;  ServKey ~: (AuthKeys evs); ServKey ~: range shrK|]\
   1.745 +\     ==> Key K : analz (insert (Key ServKey) (spies evs)) = \
   1.746 +\         (K = ServKey | Key K : analz (spies evs))";
   1.747 +by (forward_tac [not_AuthKeys_not_KeyCryptKey] 1 
   1.748 +    THEN assume_tac 1
   1.749 +    THEN assume_tac 1);
   1.750 +by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
   1.751 +qed "analz_insert_freshK2";
   1.752 +
   1.753 +
   1.754 +(* Third simplification law for analz: only one authentication key *)
   1.755 +(* encrypts a certain service key.                                 *)
   1.756 +Goal  
   1.757 + "[| Says Tgs A    \
   1.758 +\           (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   1.759 +\             : set evs;          \ 
   1.760 +\           AuthKey ~= AuthKey'; AuthKey' ~: range shrK; evs : kerberos |]    \
   1.761 +\       ==> Key ServKey : analz (insert (Key AuthKey') (spies evs)) =  \
   1.762 +\               (ServKey = AuthKey' | Key ServKey : analz (spies evs))";
   1.763 +by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);
   1.764 +by (Blast_tac 1);
   1.765 +by (assume_tac 1);
   1.766 +by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
   1.767 +qed "analz_insert_freshK3";
   1.768 +
   1.769 +
   1.770 +(*a weakness of the protocol*)
   1.771 +Goal "[| Says Tgs A    \
   1.772 +\             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   1.773 +\          : set evs;          \ 
   1.774 +\        Key AuthKey : analz (spies evs); evs : kerberos |]    \
   1.775 +\     ==> Key ServKey : analz (spies evs)";
   1.776 +by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
   1.777 +			       analz.Decrypt RS analz.Fst],
   1.778 +	       simpset()) 1);
   1.779 +qed "AuthKey_compromises_ServKey";
   1.780 +
   1.781 +
   1.782 +(********************** Guarantees for Kas *****************************)
   1.783 +Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, \
   1.784 +\                     Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}\
   1.785 +\          : parts (spies evs); \
   1.786 +\        Key ServKey ~: analz (spies evs);                          \
   1.787 +\        B ~= Tgs; evs : kerberos |]                            \
   1.788 +\     ==> ServKey ~: AuthKeys evs";
   1.789 +by (etac rev_mp 1);
   1.790 +by (etac rev_mp 1);
   1.791 +by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);
   1.792 +by (parts_induct_tac 1);
   1.793 +by (Fake_parts_insert_tac 1);
   1.794 +by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
   1.795 +bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE));
   1.796 +bind_thm ("ServKey_notin_AuthKeysD", result());
   1.797 +
   1.798 +
   1.799 +(** If Spy sees the Authentication Key sent in msg K2, then 
   1.800 +    the Key has expired  **)
   1.801 +Goal "[| A ~: bad;  evs : kerberos |]           \
   1.802 +\     ==> Says Kas A                             \
   1.803 +\              (Crypt (shrK A)                      \
   1.804 +\                 {|Key AuthKey, Agent Tgs, Number Tk,     \
   1.805 +\         Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
   1.806 +\           : set evs -->                 \
   1.807 +\         Key AuthKey : analz (spies evs) -->                       \
   1.808 +\         ExpirAuth Tk evs";
   1.809 +by (etac kerberos.induct 1);
   1.810 +by analz_sees_tac;
   1.811 +by (ALLGOALS 
   1.812 +    (asm_simp_tac 
   1.813 +     (simpset() addsimps ([Says_Kas_message_form, 
   1.814 +			   analz_insert_eq, not_parts_not_analz, 
   1.815 +			   analz_insert_freshK1] @ pushes))));
   1.816 +(*Fake*) 
   1.817 +by (spy_analz_tac 1);
   1.818 +(*K2*)
   1.819 +by (blast_tac (claset() addSEs spies_partsEs
   1.820 +            addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);
   1.821 +(*K4*)
   1.822 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.823 +(*Level 8: K5*)
   1.824 +by (blast_tac (claset() addEs [ServKey_notin_AuthKeys]
   1.825 +                        addDs [Says_Kas_message_form, 
   1.826 +	       		       Says_imp_spies RS parts.Inj]
   1.827 +                        addIs [less_SucI]) 1);
   1.828 +(*Oops1*)
   1.829 +by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1);
   1.830 +(*Oops2*)
   1.831 +by (blast_tac (claset() addDs [Says_Tgs_message_form,
   1.832 +                               Says_Kas_message_form]) 1);
   1.833 +val lemma = result() RS mp RS mp RSN(1,rev_notE);
   1.834 +
   1.835 +
   1.836 +Goal "[| Says Kas A                                             \
   1.837 +\             (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
   1.838 +\          : set evs;                                \
   1.839 +\        ~ ExpirAuth Tk evs;                         \
   1.840 +\        A ~: bad;  evs : kerberos |]            \
   1.841 +\     ==> Key AuthKey ~: analz (spies evs)";
   1.842 +by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1);
   1.843 +by (blast_tac (claset() addSDs [lemma]) 1);
   1.844 +qed "Confidentiality_Kas";
   1.845 +
   1.846 +
   1.847 +
   1.848 +
   1.849 +
   1.850 +
   1.851 +(********************** Guarantees for Tgs *****************************)
   1.852 +
   1.853 +(** If Spy sees the Service Key sent in msg K4, then 
   1.854 +    the Key has expired  **)
   1.855 +Goal "[| A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]           \
   1.856 +\  ==> Key AuthKey ~: analz (spies evs) --> \
   1.857 +\      Says Tgs A            \
   1.858 +\        (Crypt AuthKey                      \
   1.859 +\           {|Key ServKey, Agent B, Number Tt,     \
   1.860 +\             Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})\
   1.861 +\        : set evs -->                 \
   1.862 +\      Key ServKey : analz (spies evs) -->                       \
   1.863 +\      ExpirServ Tt evs";
   1.864 +by (etac kerberos.induct 1);
   1.865 +(*The Oops1 case is unusual: must simplify Authkey ~: analz (spies (ev#evs))
   1.866 +  rather than weakening it to Authkey ~: analz (spies evs), for we then
   1.867 +  conclude AuthKey ~= AuthKeya.*)
   1.868 +by (Clarify_tac 9);
   1.869 +by analz_sees_tac;
   1.870 +by (rotate_tac ~1 11);
   1.871 +by (ALLGOALS 
   1.872 +    (asm_full_simp_tac 
   1.873 +     (simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form,
   1.874 +			   analz_insert_eq, not_parts_not_analz, 
   1.875 +			   analz_insert_freshK1, analz_insert_freshK2] @ pushes))));
   1.876 +(*Fake*) 
   1.877 +by (spy_analz_tac 1);
   1.878 +(*K2*)
   1.879 +by (blast_tac (claset() addSEs spies_partsEs
   1.880 +            addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);
   1.881 +(*K4*)
   1.882 +by (case_tac "A ~= Aa" 1);
   1.883 +by (blast_tac (claset() addSEs spies_partsEs
   1.884 +                        addIs [less_SucI]) 1);
   1.885 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst, 
   1.886 +                               A_trusts_AuthTicket, 
   1.887 +                               Confidentiality_Kas,
   1.888 +                               impOfSubs analz_subset_parts]) 1);
   1.889 +by (ALLGOALS Clarify_tac);
   1.890 +(*Oops2*)
   1.891 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   1.892 +                               Key_unique_SesKey] addIs [less_SucI]) 3);
   1.893 +(** Level 12 **)
   1.894 +(*Oops1*)
   1.895 +by (forward_tac [Says_Kas_message_form] 2);
   1.896 +by (assume_tac 2);
   1.897 +by (blast_tac (claset() addDs [analz_insert_freshK3,
   1.898 +			       Says_Kas_message_form, Says_Tgs_message_form] 
   1.899 +                        addIs  [less_SucI]) 2);
   1.900 +(** Level 16 **)
   1.901 +by (thin_tac "Says Aa Tgs ?X : set ?evs" 1);
   1.902 +by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
   1.903 +by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
   1.904 +by (rotate_tac ~1 1);
   1.905 +by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
   1.906 +by (etac disjE 1);
   1.907 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   1.908 +                               Key_unique_SesKey]) 1);
   1.909 +by (blast_tac (claset() addIs [less_SucI]) 1);
   1.910 +val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE);
   1.911 +
   1.912 +
   1.913 +(* In the real world Tgs can't check wheter AuthKey is secure! *)
   1.914 +Goal 
   1.915 + "[| Says Tgs A      \
   1.916 +\             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   1.917 +\             : set evs;              \
   1.918 +\           Key AuthKey ~: analz (spies evs);        \
   1.919 +\           ~ ExpirServ Tt evs;                         \
   1.920 +\           A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   1.921 +\        ==> Key ServKey ~: analz (spies evs)";
   1.922 +by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1);
   1.923 +by (blast_tac (claset() addDs [lemma]) 1);
   1.924 +qed "Confidentiality_Tgs1";
   1.925 +
   1.926 +(* In the real world Tgs CAN check what Kas sends! *)
   1.927 +Goal 
   1.928 + "[| Says Kas A                                             \
   1.929 +\              (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
   1.930 +\             : set evs;                                \
   1.931 +\           Says Tgs A      \
   1.932 +\             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   1.933 +\             : set evs;              \
   1.934 +\           ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
   1.935 +\           A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   1.936 +\        ==> Key ServKey ~: analz (spies evs)";
   1.937 +by (blast_tac (claset() addSDs [Confidentiality_Kas,
   1.938 +                                Confidentiality_Tgs1]) 1);
   1.939 +qed "Confidentiality_Tgs2";
   1.940 +
   1.941 +(*Most general form*)
   1.942 +val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2;
   1.943 +
   1.944 +
   1.945 +(********************** Guarantees for Alice *****************************)
   1.946 +
   1.947 +val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas;
   1.948 +
   1.949 +Goal
   1.950 + "[| Says Kas A \
   1.951 +\      (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) : set evs;\
   1.952 +\    Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}     \
   1.953 +\      : parts (spies evs);                                       \
   1.954 +\    Key AuthKey ~: analz (spies evs);            \
   1.955 +\    evs : kerberos |]         \
   1.956 +\==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
   1.957 +\      : set evs";
   1.958 +by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1);
   1.959 +by (etac rev_mp 1);
   1.960 +by (etac rev_mp 1);
   1.961 +by (etac rev_mp 1);
   1.962 +by (parts_induct_tac 1);
   1.963 +by (Fake_parts_insert_tac 1);
   1.964 +(*K2 and K4 remain*)
   1.965 +by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts] 
   1.966 +                        addSDs [unique_CryptKey]) 2);
   1.967 +by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 
   1.968 +				AuthKeys_used]) 1);
   1.969 +qed "A_trusts_K4_bis";
   1.970 +
   1.971 +
   1.972 +Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
   1.973 +\          : parts (spies evs);                              \
   1.974 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}     \
   1.975 +\          : parts (spies evs);                                       \
   1.976 +\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
   1.977 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   1.978 +\     ==> Key ServKey ~: analz (spies evs)";
   1.979 +by (dtac A_trusts_AuthKey 1);
   1.980 +by (assume_tac 1);
   1.981 +by (assume_tac 1);
   1.982 +by (blast_tac (claset() addDs [Confidentiality_Kas, 
   1.983 +                               Says_Kas_message_form,
   1.984 +                               A_trusts_K4_bis, Confidentiality_Tgs2]) 1);
   1.985 +qed "Confidentiality_Serv_A";
   1.986 +
   1.987 +
   1.988 +(********************** Guarantees for Bob *****************************)
   1.989 +(* Theorems for the refined model have suffix "refined"                *)
   1.990 +
   1.991 +Goal
   1.992 +"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
   1.993 +\            : set evs; evs : kerberos|]  \
   1.994 +\  ==> EX Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
   1.995 +\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
   1.996 +\            : set evs";
   1.997 +by (etac rev_mp 1);
   1.998 +by (parts_induct_tac 1);
   1.999 +by Auto_tac;
  1.1000 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1.1001 +                               A_trusts_AuthTicket]) 1);
  1.1002 +qed "K4_imp_K2";
  1.1003 +
  1.1004 +Goal
  1.1005 +"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
  1.1006 +\     : set evs; evs : kerberos|]  \
  1.1007 +\  ==> EX Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
  1.1008 +\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1.1009 +\            : set evs   \
  1.1010 +\         & ServLife + Tt <= AuthLife + Tk)";
  1.1011 +by (etac rev_mp 1);
  1.1012 +by (parts_induct_tac 1);
  1.1013 +by Auto_tac;
  1.1014 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1.1015 +                               A_trusts_AuthTicket]) 1);
  1.1016 +qed "K4_imp_K2_refined";
  1.1017 +
  1.1018 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}  \
  1.1019 +\          : parts (spies evs);  B ~= Tgs;  B ~: bad;       \
  1.1020 +\        evs : kerberos |]                        \
  1.1021 +\==> EX AuthKey. \
  1.1022 +\      Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,  \
  1.1023 +\                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}) \
  1.1024 +\      : set evs";
  1.1025 +by (etac rev_mp 1);
  1.1026 +by (parts_induct_tac 1);
  1.1027 +by (Fake_parts_insert_tac 1);
  1.1028 +by (Blast_tac 1);
  1.1029 +qed "B_trusts_ServKey";
  1.1030 +
  1.1031 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1.1032 +\          : parts (spies evs);  B ~= Tgs;  B ~: bad;       \
  1.1033 +\        evs : kerberos |]                        \
  1.1034 +\  ==> EX AuthKey Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
  1.1035 +\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1.1036 +\            : set evs";
  1.1037 +by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1);
  1.1038 +qed "B_trusts_ServTicket_Kas";
  1.1039 +
  1.1040 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1.1041 +\          : parts (spies evs); B ~= Tgs; B ~: bad;       \
  1.1042 +\        evs : kerberos |]                        \
  1.1043 +\  ==> EX AuthKey Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
  1.1044 +\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1.1045 +\            : set evs            \
  1.1046 +\          & ServLife + Tt <= AuthLife + Tk)";
  1.1047 +by (blast_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1);
  1.1048 +qed "B_trusts_ServTicket_Kas_refined";
  1.1049 +
  1.1050 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1.1051 +\          : parts (spies evs); B ~= Tgs; B ~: bad;        \
  1.1052 +\        evs : kerberos |]                        \
  1.1053 +\==> EX Tk AuthKey.        \
  1.1054 +\    Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \
  1.1055 +\                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1.1056 +\      : set evs         \ 
  1.1057 +\    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
  1.1058 +\                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
  1.1059 +\      : set evs";
  1.1060 +by (forward_tac [B_trusts_ServKey] 1);
  1.1061 +by (etac exE 4);
  1.1062 +by (forward_tac [K4_imp_K2] 4);
  1.1063 +by (Blast_tac 5);
  1.1064 +by (ALLGOALS assume_tac);
  1.1065 +qed "B_trusts_ServTicket";
  1.1066 +
  1.1067 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1.1068 +\          : parts (spies evs); B ~= Tgs; B ~: bad;        \
  1.1069 +\        evs : kerberos |]                        \
  1.1070 +\==> EX Tk AuthKey.        \
  1.1071 +\    (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \
  1.1072 +\                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1.1073 +\      : set evs         \ 
  1.1074 +\    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
  1.1075 +\                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
  1.1076 +\      : set evs         \
  1.1077 +\    & ServLife + Tt <= AuthLife + Tk)";
  1.1078 +by (forward_tac [B_trusts_ServKey] 1);
  1.1079 +by (etac exE 4);
  1.1080 +by (forward_tac [K4_imp_K2_refined] 4);
  1.1081 +by (Blast_tac 5);
  1.1082 +by (ALLGOALS assume_tac);
  1.1083 +qed "B_trusts_ServTicket_refined";
  1.1084 +
  1.1085 +
  1.1086 +Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]        \
  1.1087 +\  ==> ~ ExpirAuth Tk evs";
  1.1088 +by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1);
  1.1089 +qed "NotExpirServ_NotExpirAuth_refined";
  1.1090 +
  1.1091 +
  1.1092 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \
  1.1093 +\          : parts (spies evs);                                        \
  1.1094 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
  1.1095 +\          : parts (spies evs);                                         \
  1.1096 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1.1097 +\          : parts (spies evs);                     \
  1.1098 +\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;     \
  1.1099 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1100 +\     ==> Key ServKey ~: analz (spies evs)";
  1.1101 +by (forward_tac [A_trusts_AuthKey] 1);
  1.1102 +by (forward_tac [Confidentiality_Kas] 3);
  1.1103 +by (forward_tac [B_trusts_ServTicket] 6);
  1.1104 +by (etac exE 9);
  1.1105 +by (etac exE 9);
  1.1106 +by (forward_tac [Says_Kas_message_form] 9);
  1.1107 +by (blast_tac (claset() addDs [A_trusts_K4, 
  1.1108 +                               unique_ServKeys, unique_AuthKeys,
  1.1109 +                               Confidentiality_Tgs2]) 10);
  1.1110 +by (ALLGOALS assume_tac);
  1.1111 +(*
  1.1112 +The proof above executes in 8 secs. It can be done in one command in 50 secs:
  1.1113 +by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,
  1.1114 +                               Says_Kas_message_form, B_trusts_ServTicket,
  1.1115 +                               unique_ServKeys, unique_AuthKeys,
  1.1116 +                               Confidentiality_Kas, 
  1.1117 +                               Confidentiality_Tgs2]) 1);
  1.1118 +*)
  1.1119 +qed "Confidentiality_B";
  1.1120 +
  1.1121 +
  1.1122 +(*Most general form -- only for refined model! *)
  1.1123 +Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1.1124 +\          : parts (spies evs);                      \
  1.1125 +\        ~ ExpirServ Tt evs;                         \
  1.1126 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1127 +\     ==> Key ServKey ~: analz (spies evs)";
  1.1128 +by (blast_tac (claset() addDs [B_trusts_ServTicket_refined,
  1.1129 +			       NotExpirServ_NotExpirAuth_refined, 
  1.1130 +                               Confidentiality_Tgs2]) 1);
  1.1131 +qed "Confidentiality_B_refined";
  1.1132 +
  1.1133 +
  1.1134 +(********************** Authenticity theorems *****************************)
  1.1135 +
  1.1136 +(***1. Session Keys authenticity: they originated with servers.***)
  1.1137 +
  1.1138 +(*Authenticity of AuthKey for A: "A_trusts_AuthKey"*)
  1.1139 +
  1.1140 +(*Authenticity of ServKey for A: "A_trusts_ServKey"*)
  1.1141 +Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|} \
  1.1142 +\          : parts (spies evs);                                     \
  1.1143 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
  1.1144 +\          : parts (spies evs);                                        \
  1.1145 +\        ~ ExpirAuth Tk evs; A ~: bad; evs : kerberos |]         \
  1.1146 +\==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
  1.1147 +\      : set evs";
  1.1148 +by (forward_tac [A_trusts_AuthKey] 1 THEN assume_tac 1 THEN assume_tac 1);
  1.1149 +by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1);
  1.1150 +qed "A_trusts_ServKey"; 
  1.1151 +(*Note: requires a temporal check*)
  1.1152 +
  1.1153 +
  1.1154 +(*Authenticity of ServKey for B: "B_trusts_ServKey"*)
  1.1155 +
  1.1156 +(***2. Parties authenticity: each party verifies "the identity of
  1.1157 +       another party who generated some data" (quoted from Neuman & Ts'o).***)
  1.1158 +       
  1.1159 +       (*These guarantees don't assess whether two parties agree on 
  1.1160 +         the same session key: sending a message containing a key
  1.1161 +         doesn't a priori state knowledge of the key.***)
  1.1162 +
  1.1163 +(*B checks authenticity of A: theorems "A_Authenticity", 
  1.1164 +                                       "A_authenticity_refined" *)
  1.1165 +Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);  \
  1.1166 +\        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \
  1.1167 +\                                    ServTicket|}) : set evs;       \
  1.1168 +\        Key ServKey ~: analz (spies evs);                \
  1.1169 +\        A ~: bad; B ~: bad; evs : kerberos |]   \
  1.1170 +\==> Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} : set evs";
  1.1171 +by (etac rev_mp 1);
  1.1172 +by (etac rev_mp 1);
  1.1173 +by (etac rev_mp 1);
  1.1174 +by (etac kerberos.induct 1);
  1.1175 +by (forward_tac [Says_ticket_in_parts_spies] 5);
  1.1176 +by (forward_tac [Says_ticket_in_parts_spies] 7);
  1.1177 +by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1.1178 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1.1179 +by (Fake_parts_insert_tac 1);
  1.1180 +(*K3*)
  1.1181 +by (blast_tac (claset() addEs spies_partsEs
  1.1182 +                        addDs [A_trusts_AuthKey,
  1.1183 +                               Says_Kas_message_form, 
  1.1184 +                               Says_Tgs_message_form]) 1);
  1.1185 +(*K4*)
  1.1186 +by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1.1187 +(*K5*)
  1.1188 +by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1);
  1.1189 +qed "Says_Auth";
  1.1190 +
  1.1191 +(*The second assumption tells B what kind of key ServKey is.*)
  1.1192 +Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);     \
  1.1193 +\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1.1194 +\          : parts (spies evs);                                         \
  1.1195 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}  \ 
  1.1196 +\          : parts (spies evs);                                          \
  1.1197 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
  1.1198 +\          : parts (spies evs);                                            \
  1.1199 +\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
  1.1200 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1201 +\  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1.1202 +\                 Crypt ServKey {|Agent A, Number Ta|} |} : set evs";
  1.1203 +by (forward_tac [Confidentiality_B] 1);
  1.1204 +by (forward_tac [B_trusts_ServKey] 9);
  1.1205 +by (etac exE 12);
  1.1206 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1.1207 +                        addSIs [Says_Auth]) 12);
  1.1208 +by (ALLGOALS assume_tac);
  1.1209 +qed "A_Authenticity";
  1.1210 +
  1.1211 +(*Stronger form in the refined model*)
  1.1212 +Goal "[| Crypt ServKey {|Agent A, Number Ta2|} : parts (spies evs);     \
  1.1213 +\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1.1214 +\          : parts (spies evs);                                         \
  1.1215 +\        ~ ExpirServ Tt evs;                                        \
  1.1216 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1217 +\  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1.1218 +\                 Crypt ServKey {|Agent A, Number Ta2|} |} : set evs";
  1.1219 +by (forward_tac [Confidentiality_B_refined] 1);
  1.1220 +by (forward_tac [B_trusts_ServKey] 6);
  1.1221 +by (etac exE 9);
  1.1222 +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1.1223 +                        addSIs [Says_Auth]) 9);
  1.1224 +by (ALLGOALS assume_tac);
  1.1225 +qed "A_Authenticity_refined";
  1.1226 +
  1.1227 +
  1.1228 +(*A checks authenticity of B: theorem "B_authenticity"*)
  1.1229 +
  1.1230 +Goal "[| Crypt ServKey (Number Ta) : parts (spies evs);  \
  1.1231 +\        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \
  1.1232 +\                                    ServTicket|}) : set evs;       \
  1.1233 +\        Key ServKey ~: analz (spies evs);                \
  1.1234 +\        A ~: bad; B ~: bad; evs : kerberos |]   \
  1.1235 +\     ==> Says B A (Crypt ServKey (Number Ta)) : set evs";
  1.1236 +by (etac rev_mp 1);
  1.1237 +by (etac rev_mp 1);
  1.1238 +by (etac rev_mp 1);
  1.1239 +by (etac kerberos.induct 1);
  1.1240 +by (forward_tac [Says_ticket_in_parts_spies] 5);
  1.1241 +by (forward_tac [Says_ticket_in_parts_spies] 7);
  1.1242 +by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1.1243 +by (ALLGOALS Asm_simp_tac);
  1.1244 +by (Fake_parts_insert_tac 1);
  1.1245 +by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1.1246 +by (Clarify_tac 1);
  1.1247 +by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1);
  1.1248 +by (Clarify_tac 1);  (*PROOF FAILED if omitted*)
  1.1249 +by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1);
  1.1250 +qed "Says_K6";
  1.1251 +
  1.1252 +Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|}   \
  1.1253 +\          : parts (spies evs);    \
  1.1254 +\        Key AuthKey ~: analz (spies evs); AuthKey ~: range shrK;  \
  1.1255 +\        evs : kerberos |]              \
  1.1256 +\ ==> EX A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})\
  1.1257 +\             : set evs";
  1.1258 +by (etac rev_mp 1);
  1.1259 +by (etac rev_mp 1);
  1.1260 +by (parts_induct_tac 1);
  1.1261 +by (Fake_parts_insert_tac 1);
  1.1262 +by (Blast_tac 1);
  1.1263 +by (Blast_tac 1);
  1.1264 +qed "K4_trustworthy";
  1.1265 +
  1.1266 +Goal "[| Crypt ServKey (Number Ta) : parts (spies evs);           \
  1.1267 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
  1.1268 +\          : parts (spies evs);                                        \ 
  1.1269 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1.1270 +\          : parts (spies evs);                                          \
  1.1271 +\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
  1.1272 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1273 +\     ==> Says B A (Crypt ServKey (Number Ta)) : set evs";
  1.1274 +by (forward_tac [A_trusts_AuthKey] 1);
  1.1275 +by (forward_tac [Says_Kas_message_form] 3);
  1.1276 +by (forward_tac [Confidentiality_Kas] 4);
  1.1277 +by (forward_tac [K4_trustworthy] 7);
  1.1278 +by (Blast_tac 8);
  1.1279 +by (etac exE 9);
  1.1280 +by (forward_tac [K4_imp_K2] 9);
  1.1281 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1.1282 +                        addSIs [Says_K6]
  1.1283 +                        addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10);
  1.1284 +by (ALLGOALS assume_tac);
  1.1285 +qed "B_Authenticity";
  1.1286 +
  1.1287 +
  1.1288 +(***3. Parties' knowledge of session keys. A knows a session key if she
  1.1289 +       used it to build a cipher.***)
  1.1290 +
  1.1291 +Goal "[| Says B A (Crypt ServKey (Number Ta)) : set evs;           \
  1.1292 +\        Key ServKey ~: analz (spies evs);                          \
  1.1293 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1294 +\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1.1295 +by (simp_tac (simpset() addsimps [Issues_def]) 1);
  1.1296 +by (rtac exI 1);
  1.1297 +by (rtac conjI 1);
  1.1298 +by (assume_tac 1);
  1.1299 +by (Simp_tac 1);
  1.1300 +by (etac rev_mp 1);
  1.1301 +by (etac rev_mp 1);
  1.1302 +by (etac kerberos.induct 1);
  1.1303 +by (forward_tac [Says_ticket_in_parts_spies] 5);
  1.1304 +by (forward_tac [Says_ticket_in_parts_spies] 7);
  1.1305 +by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1.1306 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1.1307 +by (Fake_parts_insert_tac 1);
  1.1308 +(*K6 requires numerous lemmas*)
  1.1309 +by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1.1310 +by (blast_tac (claset() addDs [B_trusts_ServTicket,
  1.1311 +                               impOfSubs parts_spies_takeWhile_mono,
  1.1312 +                               impOfSubs parts_spies_evs_revD2]
  1.1313 +                        addIs [Says_K6]
  1.1314 +                        addEs spies_partsEs) 1);
  1.1315 +qed "B_Knows_B_Knows_ServKey_lemma";
  1.1316 +(*Key ServKey ~: analz (spies evs) could be relaxed by Confidentiality_B
  1.1317 +  but this is irrelevant because B knows what he knows!                  *)
  1.1318 +
  1.1319 +Goal "[| Says B A (Crypt ServKey (Number Ta)) : set evs;           \
  1.1320 +\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
  1.1321 +\           : parts (spies evs);\
  1.1322 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}\
  1.1323 +\           : parts (spies evs);\
  1.1324 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1.1325 +\          : parts (spies evs);     \
  1.1326 +\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;              \
  1.1327 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1328 +\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1.1329 +by (blast_tac (claset() addSDs [Confidentiality_B,
  1.1330 +	                       B_Knows_B_Knows_ServKey_lemma]) 1);
  1.1331 +qed "B_Knows_B_Knows_ServKey";
  1.1332 +
  1.1333 +Goal "[| Says B A (Crypt ServKey (Number Ta)) : set evs;           \
  1.1334 +\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
  1.1335 +\           : parts (spies evs);\
  1.1336 +\        ~ ExpirServ Tt evs;            \
  1.1337 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1338 +\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1.1339 +by (blast_tac (claset() addSDs [Confidentiality_B_refined,
  1.1340 +	                       B_Knows_B_Knows_ServKey_lemma]) 1);
  1.1341 +qed "B_Knows_B_Knows_ServKey_refined";
  1.1342 +
  1.1343 +
  1.1344 +Goal "[| Crypt ServKey (Number Ta) : parts (spies evs);           \
  1.1345 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
  1.1346 +\          : parts (spies evs);                                        \ 
  1.1347 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1.1348 +\          : parts (spies evs);                                          \
  1.1349 +\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
  1.1350 +\        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1.1351 +\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1.1352 +by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A,
  1.1353 +                                B_Knows_B_Knows_ServKey_lemma]) 1);
  1.1354 +qed "A_Knows_B_Knows_ServKey";
  1.1355 +
  1.1356 +Goal "[| Says A Tgs     \
  1.1357 +\            {|AuthTicket, Crypt AuthKey {|Agent A, Number Ta|}, Agent B|}\
  1.1358 +\          : set evs;      \
  1.1359 +\        A ~: bad;  evs : kerberos |]         \
  1.1360 +\     ==> EX Tk. Says Kas A (Crypt (shrK A) \
  1.1361 +\                     {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
  1.1362 +\                  : set evs";
  1.1363 +by (etac rev_mp 1);
  1.1364 +by (parts_induct_tac 1);
  1.1365 +by (Fake_parts_insert_tac 1);
  1.1366 +by (Blast_tac 1);
  1.1367 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 
  1.1368 +			       A_trusts_AuthKey]) 1);
  1.1369 +qed "K3_imp_K2";
  1.1370 +
  1.1371 +Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
  1.1372 +\          : parts (spies evs);                    \
  1.1373 +\        Says Kas A (Crypt (shrK A) \
  1.1374 +\                    {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
  1.1375 +\        : set evs;    \
  1.1376 +\        Key AuthKey ~: analz (spies evs);       \
  1.1377 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1378 +\  ==> Says Tgs A (Crypt AuthKey        \ 
  1.1379 +\                    {|Key ServKey, Agent B, Number Tt, ServTicket|})  \
  1.1380 +\        : set evs";      
  1.1381 +by (etac rev_mp 1);
  1.1382 +by (etac rev_mp 1);
  1.1383 +by (etac rev_mp 1);
  1.1384 +by (parts_induct_tac 1);
  1.1385 +by (Fake_parts_insert_tac 1);
  1.1386 +by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1.1387 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1.1388 +                               A_trusts_AuthTicket, unique_AuthKeys]) 1);
  1.1389 +qed "K4_trustworthy'";
  1.1390 +
  1.1391 +Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
  1.1392 +\          : set evs;       \
  1.1393 +\        Key ServKey ~: analz (spies evs);       \
  1.1394 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1395 +\  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1.1396 +by (simp_tac (simpset() addsimps [Issues_def]) 1);
  1.1397 +by (rtac exI 1);
  1.1398 +by (rtac conjI 1);
  1.1399 +by (assume_tac 1);
  1.1400 +by (Simp_tac 1);
  1.1401 +by (etac rev_mp 1);
  1.1402 +by (etac rev_mp 1);
  1.1403 +by (etac kerberos.induct 1);
  1.1404 +by (forward_tac [Says_ticket_in_parts_spies] 5);
  1.1405 +by (forward_tac [Says_ticket_in_parts_spies] 7);
  1.1406 +by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1.1407 +by (ALLGOALS Asm_simp_tac);
  1.1408 +by (Clarify_tac 1);
  1.1409 +(*K6*)
  1.1410 +by Auto_tac;
  1.1411 +by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1.1412 +(*Level 15: case study necessary because the assumption doesn't state
  1.1413 +  the form of ServTicket. The guarantee becomes stronger.*)
  1.1414 +by (case_tac "Key AuthKey : analz (spies evs5)" 1);
  1.1415 +by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
  1.1416 +			       analz.Decrypt RS analz.Fst],
  1.1417 +	       simpset()) 1);
  1.1418 +by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy',
  1.1419 +                               impOfSubs parts_spies_takeWhile_mono,
  1.1420 +                               impOfSubs parts_spies_evs_revD2]
  1.1421 +                        addIs [Says_Auth] 
  1.1422 +                        addEs spies_partsEs) 1);
  1.1423 +by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1.1424 +qed "A_Knows_A_Knows_ServKey_lemma";
  1.1425 +
  1.1426 +Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
  1.1427 +\          : set evs;       \
  1.1428 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1.1429 +\          : parts (spies evs);\
  1.1430 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}\
  1.1431 +\          : parts (spies evs);                                        \
  1.1432 +\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;\
  1.1433 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1434 +\  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1.1435 +by (blast_tac (claset() addSDs [Confidentiality_Serv_A,
  1.1436 +	                       A_Knows_A_Knows_ServKey_lemma]) 1);
  1.1437 +qed "A_Knows_A_Knows_ServKey";
  1.1438 +
  1.1439 +Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);     \
  1.1440 +\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1.1441 +\          : parts (spies evs);                                         \
  1.1442 +\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}  \ 
  1.1443 +\          : parts (spies evs);                                          \
  1.1444 +\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
  1.1445 +\          : parts (spies evs);                                            \
  1.1446 +\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
  1.1447 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1448 +\  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1.1449 +by (blast_tac (claset() addDs [A_Authenticity, Confidentiality_B,
  1.1450 +	                       A_Knows_A_Knows_ServKey_lemma]) 1);
  1.1451 +qed "B_Knows_A_Knows_ServKey";
  1.1452 +
  1.1453 +
  1.1454 +Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);     \
  1.1455 +\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1.1456 +\          : parts (spies evs);                                         \
  1.1457 +\        ~ ExpirServ Tt evs;                                        \
  1.1458 +\        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1.1459 +\  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1.1460 +by (blast_tac (claset() addDs [A_Authenticity_refined, 
  1.1461 +                               Confidentiality_B_refined,
  1.1462 +	                       A_Knows_A_Knows_ServKey_lemma]) 1);
  1.1463 +qed "B_Knows_A_Knows_ServKey_refined";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/KerberosIV.thy	Tue Apr 20 14:33:48 1999 +0200
     2.3 @@ -0,0 +1,236 @@
     2.4 +(*  Title:      HOL/Auth/KerberosIV
     2.5 +    ID:         $Id$
     2.6 +    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +The Kerberos protocol, version IV.
    2.10 +*)
    2.11 +
    2.12 +KerberosIV = Shared +
    2.13 +
    2.14 +syntax
    2.15 +  Kas, Tgs :: agent    (*the two servers are translations...*)
    2.16 +
    2.17 +
    2.18 +translations
    2.19 +  "Kas"       == "Server"
    2.20 +  "Tgs"       == "Friend 0"   
    2.21 +
    2.22 +
    2.23 +rules
    2.24 +  (*Tgs is secure --- we already know that Kas is secure*)
    2.25 +  Tgs_not_bad "Tgs ~: bad"
    2.26 +  
    2.27 +(*The current time is just the length of the trace!*)
    2.28 +syntax
    2.29 +    CT :: event list=>nat
    2.30 +
    2.31 +    ExpirAuth :: [nat, event list] => bool
    2.32 +
    2.33 +    ExpirServ :: [nat, event list] => bool 
    2.34 +
    2.35 +    ExpirAutc :: [nat, event list] => bool 
    2.36 +
    2.37 +    RecentResp :: [nat, nat] => bool
    2.38 +
    2.39 +
    2.40 +constdefs
    2.41 + (* AuthKeys are those contained in an AuthTicket *)
    2.42 +    AuthKeys :: event list => key set
    2.43 +    "AuthKeys evs == {AuthKey. EX A Peer Tk. Says Kas A
    2.44 +                        (Crypt (shrK A) {|Key AuthKey, Agent Peer, Tk, 
    2.45 +                   (Crypt (shrK Peer) {|Agent A, Agent Peer, Key AuthKey, Tk|})
    2.46 +                  |}) : set evs}"
    2.47 +                      
    2.48 + (* A is the true creator of X if she has sent X and X never appeared on
    2.49 +    the trace before this event. Recall that traces grow from head. *)
    2.50 +  Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
    2.51 +   "A Issues B with X on evs == 
    2.52 +      EX Y. Says A B Y : set evs & X : parts {Y} &
    2.53 +      X ~: parts (spies (takeWhile (% z. z  ~= Says A B Y) (rev evs)))"
    2.54 +
    2.55 +
    2.56 +consts
    2.57 +
    2.58 +    (*Duration of the authentication key*)
    2.59 +    AuthLife   :: nat
    2.60 +
    2.61 +    (*Duration of the service key*)
    2.62 +    ServLife   :: nat
    2.63 +
    2.64 +    (*Duration of an authenticator*)
    2.65 +    AutcLife   :: nat
    2.66 +
    2.67 +    (*Upper bound on the time of reaction of a server*)
    2.68 +    RespLife   :: nat 
    2.69 +
    2.70 +rules
    2.71 +     AuthLife_LB    "2 <= AuthLife"
    2.72 +     ServLife_LB    "2 <= ServLife"
    2.73 +     AutcLife_LB    "1 <= AutcLife" 
    2.74 +     RespLife_LB    "1 <= RespLife"
    2.75 +
    2.76 +translations
    2.77 +   "CT" == "length"
    2.78 +
    2.79 +   "ExpirAuth T evs" == "AuthLife + T < CT evs"
    2.80 +
    2.81 +   "ExpirServ T evs" == "ServLife + T < CT evs"
    2.82 +
    2.83 +   "ExpirAutc T evs" == "AutcLife + T < CT evs"
    2.84 +
    2.85 +   "RecentResp T1 T2" == "T1 <= RespLife + T2"
    2.86 +
    2.87 +(*---------------------------------------------------------------------*)
    2.88 +
    2.89 +
    2.90 +(* Predicate formalising the association between AuthKeys and ServKeys *)
    2.91 +constdefs 
    2.92 +  KeyCryptKey :: [key, key, event list] => bool
    2.93 +  "KeyCryptKey AuthKey ServKey evs ==
    2.94 +     EX A B tt. 
    2.95 +       Says Tgs A (Crypt AuthKey
    2.96 +                     {|Key ServKey, Agent B, tt,
    2.97 +                       Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
    2.98 +         : set evs"
    2.99 +
   2.100 +consts
   2.101 +
   2.102 +kerberos   :: event list set
   2.103 +inductive "kerberos"
   2.104 +  intrs 
   2.105 +        
   2.106 +    Nil  "[]: kerberos"
   2.107 +
   2.108 +    Fake "[| evs: kerberos;  B ~= Spy;  
   2.109 +             X: synth (analz (spies evs)) |]
   2.110 +          ==> Says Spy B X  # evs : kerberos"
   2.111 +
   2.112 +(* FROM the initiator *)
   2.113 +    K1   "[| evs1: kerberos |]
   2.114 +          ==> Says A Kas {|Agent A, Agent Tgs, Number (CT evs1)|} # evs1 
   2.115 +          : kerberos"
   2.116 +
   2.117 +(* Adding the timestamp serves to A in K3 to check that
   2.118 +   she doesn't get a reply too late. This kind of timeouts are ordinary. 
   2.119 +   If a server's reply is late, then it is likely to be fake. *)
   2.120 +
   2.121 +(*---------------------------------------------------------------------*)
   2.122 +
   2.123 +(*FROM Kas *)
   2.124 +    K2  "[| evs2: kerberos; Key AuthKey ~: used evs2;
   2.125 +            Says A' Kas {|Agent A, Agent Tgs, Number Ta|} : set evs2 |]
   2.126 +          ==> Says Kas A
   2.127 +                (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2), 
   2.128 +                      (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, 
   2.129 +                          Number (CT evs2)|})|}) # evs2 : kerberos"
   2.130 +(* 
   2.131 +  The internal encryption builds the AuthTicket.
   2.132 +  The timestamp doesn't change inside the two encryptions: the external copy
   2.133 +  will be used by the initiator in K3; the one inside the 
   2.134 +  AuthTicket by Tgs in K4.
   2.135 +*)
   2.136 +
   2.137 +(*---------------------------------------------------------------------*)
   2.138 +
   2.139 +(* FROM the initiator *)
   2.140 +    K3  "[| evs3: kerberos; 
   2.141 +            Says A Kas {|Agent A, Agent Tgs, Number Ta|} : set evs3;
   2.142 +            Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, 
   2.143 +              AuthTicket|}) : set evs3; 
   2.144 +            RecentResp Tk Ta
   2.145 +         |]
   2.146 +          ==> Says A Tgs {|AuthTicket, 
   2.147 +                           (Crypt AuthKey {|Agent A, Number (CT evs3)|}), 
   2.148 +                           Agent B|} # evs3 : kerberos"
   2.149 +(*The two events amongst the premises allow A to accept only those AuthKeys 
   2.150 +  that are not issued late. *)
   2.151 +
   2.152 +(*---------------------------------------------------------------------*)
   2.153 +
   2.154 +(* FROM Tgs *)
   2.155 +(* Note that the last temporal check is not mentioned in the original MIT
   2.156 +   specification. Adding it strengthens the guarantees assessed by the 
   2.157 +   protocol. Theorems that exploit it have the suffix `_refined'
   2.158 +*) 
   2.159 +    K4  "[| evs4: kerberos; Key ServKey ~: used evs4; B ~= Tgs; 
   2.160 +            Says A' Tgs {|
   2.161 +             (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
   2.162 +				 Number Tk|}),
   2.163 +             (Crypt AuthKey {|Agent A, Number Ta1|}), Agent B|}
   2.164 +	        : set evs4;
   2.165 +            ~ ExpirAuth Tk evs4;
   2.166 +            ~ ExpirAutc Ta1 evs4; 
   2.167 +            ServLife + (CT evs4) <= AuthLife + Tk
   2.168 +         |]
   2.169 +          ==> Says Tgs A 
   2.170 +                (Crypt AuthKey {|Key ServKey, Agent B, Number (CT evs4),  
   2.171 +			       Crypt (shrK B) {|Agent A, Agent B, Key ServKey,
   2.172 +		 			        Number (CT evs4)|} |})
   2.173 +	        # evs4 : kerberos"
   2.174 +(* Tgs creates a new session key per each request for a service, without 
   2.175 +   checking if there is still a fresh one for that service.
   2.176 +   The cipher under Tgs' key is the AuthTicket, the cipher under B's key
   2.177 +   is the ServTicket, which is built now.
   2.178 +   NOTE that the last temporal check is not present in the MIT specification.
   2.179 +  
   2.180 +*)
   2.181 +
   2.182 +(*---------------------------------------------------------------------*)
   2.183 +
   2.184 +(* FROM the initiator *)
   2.185 +    K5  "[| evs5: kerberos;  
   2.186 +            Says A Tgs 
   2.187 +                {|AuthTicket, (Crypt AuthKey {|Agent A, Number Ta1|} ),
   2.188 +		  Agent B|}
   2.189 +              : set evs5;
   2.190 +            Says Tgs' A 
   2.191 +             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} ) 
   2.192 +                : set evs5;
   2.193 +            RecentResp Tt Ta1 |]
   2.194 +          ==> Says A B {|ServTicket,
   2.195 +			 Crypt ServKey {|Agent A, Number (CT evs5)|} |}
   2.196 +               # evs5 : kerberos"
   2.197 +(* Checks similar to those in K3. *)
   2.198 +
   2.199 +(*---------------------------------------------------------------------*)
   2.200 +
   2.201 +(* FROM the responder*)
   2.202 +     K6  "[| evs6: kerberos;
   2.203 +            Says A' B {|           
   2.204 +              (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} ),
   2.205 +              (Crypt ServKey {|Agent A, Number Ta2|} )|}
   2.206 +            : set evs6;
   2.207 +            ~ ExpirServ Tt evs6;
   2.208 +            ~ ExpirAutc Ta2 evs6
   2.209 +         |]
   2.210 +          ==> Says B A (Crypt ServKey (Number Ta2) )
   2.211 +               # evs6 : kerberos"
   2.212 +(* Checks similar to those in K4. *)
   2.213 +
   2.214 +(*---------------------------------------------------------------------*)
   2.215 +
   2.216 +(* Leaking an AuthKey... *)
   2.217 +    Oops1 "[| evsO1: kerberos;  A ~= Spy;
   2.218 +              Says Kas A
   2.219 +                (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, 
   2.220 +                                  AuthTicket|})  : set evsO1;
   2.221 +              ExpirAuth Tk evsO1 |]
   2.222 +          ==> Says A Spy {|Agent A, Agent Tgs, Number Tk, Key AuthKey|} 
   2.223 +               # evsO1 : kerberos"
   2.224 +
   2.225 +(*---------------------------------------------------------------------*)
   2.226 +
   2.227 +(*Leaking a ServKey... *)
   2.228 +    Oops2 "[| evsO2: kerberos;  A ~= Spy;
   2.229 +              Says Tgs A 
   2.230 +                (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
   2.231 +                   : set evsO2;
   2.232 +              ExpirServ Tt evsO2 |]
   2.233 +          ==> Says A Spy {|Agent A, Agent B, Number Tt, Key ServKey|} 
   2.234 +               # evsO2 : kerberos"
   2.235 +
   2.236 +(*---------------------------------------------------------------------*)
   2.237 +
   2.238 +
   2.239 +end
     3.1 --- a/src/HOL/Auth/README.html	Tue Apr 20 14:32:48 1999 +0200
     3.2 +++ b/src/HOL/Auth/README.html	Tue Apr 20 14:33:48 1999 +0200
     3.3 @@ -14,7 +14,8 @@
     3.4  
     3.5  <LI>the Needham-Schroeder protocol (public-key and shared-key versions)
     3.6  
     3.7 -<LI>the Kerberos protocol (the simplified form published in the BAN paper)
     3.8 +<LI>two versions of Kerberos: the simplified form published in the BAN paper
     3.9 +	and also the full protocol (Kerberos IV)
    3.10  
    3.11  <LI>three versions of the Yahalom protocol, including a bad one that 
    3.12  	illustrates the purpose of the Oops rule
     4.1 --- a/src/HOL/Auth/ROOT.ML	Tue Apr 20 14:32:48 1999 +0200
     4.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Apr 20 14:33:48 1999 +0200
     4.3 @@ -15,6 +15,7 @@
     4.4  (*Shared-key protocols*)
     4.5  time_use_thy "NS_Shared";
     4.6  time_use_thy "Kerberos_BAN";
     4.7 +time_use_thy "KerberosIV";
     4.8  time_use_thy "OtwayRees";
     4.9  time_use_thy "OtwayRees_AN";
    4.10  time_use_thy "OtwayRees_Bad";