src/HOL/Auth/KerberosIV.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 8741 61bc5ed22b62
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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     ftac K3_msg_in_parts_spies (i+4)  THEN
   152     ftac K5_msg_in_parts_spies (i+6)  THEN
   153     ftac Oops_parts_spies1 (i+8)  THEN
   154     ftac 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 non-existent 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 long-term 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 (ftac 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 split-up 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 split-up 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 (ftac 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     ftac Oops_range_spies2 10, 
   647     ftac Oops_range_spies1 9, 
   648     ftac Says_tgs_message_form 7,
   649     ftac 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 (ftac analz_mono_KK 2
   704     THEN assume_tac 2
   705     THEN assume_tac 2);
   706 by (ftac 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 (ftac 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 			delrules [le_maxI1, le_maxI2]
   717                         addDs [impOfSubs analz_mono]) 2);
   718 (*Level 27: Oops 1*)
   719 by (dres_inst_tac [("x","SK")] spec 1);
   720 by (dres_inst_tac [("x","insert AuthKey KK")] spec 1);
   721 by (case_tac "KeyCryptKey AuthKey SK evsO1" 1);
   722 by (ALLGOALS Asm_full_simp_tac);
   723 by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
   724 by (blast_tac (claset() delrules [le_maxI1, le_maxI2] 
   725 			addDs [impOfSubs analz_mono]) 1);
   726 qed_spec_mp "Key_analz_image_Key";
   727 
   728 
   729 (* First simplification law for analz: no session keys encrypt  *)
   730 (* authentication keys or shared keys.                          *)
   731 Goal "[| evs : kerberos;  K : (AuthKeys evs) Un range shrK;      \
   732 \        SesKey ~: range shrK |]                                 \
   733 \     ==> Key K : analz (insert (Key SesKey) (spies evs)) = \
   734 \         (K = SesKey | Key K : analz (spies evs))";
   735 by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1);
   736 by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
   737 qed "analz_insert_freshK1";
   738 
   739 
   740 (* Second simplification law for analz: no service keys encrypt *)
   741 (* any other keys.					        *)
   742 Goal "[| evs : kerberos;  ServKey ~: (AuthKeys evs); ServKey ~: range shrK|]\
   743 \     ==> Key K : analz (insert (Key ServKey) (spies evs)) = \
   744 \         (K = ServKey | Key K : analz (spies evs))";
   745 by (ftac not_AuthKeys_not_KeyCryptKey 1 
   746     THEN assume_tac 1
   747     THEN assume_tac 1);
   748 by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
   749 qed "analz_insert_freshK2";
   750 
   751 
   752 (* Third simplification law for analz: only one authentication key *)
   753 (* encrypts a certain service key.                                 *)
   754 Goal  
   755  "[| Says Tgs A    \
   756 \           (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   757 \             : set evs;          \ 
   758 \           AuthKey ~= AuthKey'; AuthKey' ~: range shrK; evs : kerberos |]    \
   759 \       ==> Key ServKey : analz (insert (Key AuthKey') (spies evs)) =  \
   760 \               (ServKey = AuthKey' | Key ServKey : analz (spies evs))";
   761 by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);
   762 by (Blast_tac 1);
   763 by (assume_tac 1);
   764 by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
   765 qed "analz_insert_freshK3";
   766 
   767 
   768 (*a weakness of the protocol*)
   769 Goal "[| Says Tgs A    \
   770 \             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   771 \          : set evs;          \ 
   772 \        Key AuthKey : analz (spies evs); evs : kerberos |]    \
   773 \     ==> Key ServKey : analz (spies evs)";
   774 by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
   775 			       analz.Decrypt RS analz.Fst],
   776 	       simpset()) 1);
   777 qed "AuthKey_compromises_ServKey";
   778 
   779 
   780 (********************** Guarantees for Kas *****************************)
   781 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, \
   782 \                     Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}\
   783 \          : parts (spies evs); \
   784 \        Key ServKey ~: analz (spies evs);                          \
   785 \        B ~= Tgs; evs : kerberos |]                            \
   786 \     ==> ServKey ~: AuthKeys evs";
   787 by (etac rev_mp 1);
   788 by (etac rev_mp 1);
   789 by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);
   790 by (parts_induct_tac 1);
   791 by (Fake_parts_insert_tac 1);
   792 by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
   793 bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE));
   794 bind_thm ("ServKey_notin_AuthKeysD", result());
   795 
   796 
   797 (** If Spy sees the Authentication Key sent in msg K2, then 
   798     the Key has expired  **)
   799 Goal "[| A ~: bad;  evs : kerberos |]           \
   800 \     ==> Says Kas A                             \
   801 \              (Crypt (shrK A)                      \
   802 \                 {|Key AuthKey, Agent Tgs, Number Tk,     \
   803 \         Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
   804 \           : set evs -->                 \
   805 \         Key AuthKey : analz (spies evs) -->                       \
   806 \         ExpirAuth Tk evs";
   807 by (etac kerberos.induct 1);
   808 by analz_sees_tac;
   809 by (ALLGOALS 
   810     (asm_simp_tac 
   811      (simpset() addsimps ([Says_Kas_message_form, 
   812 			   analz_insert_eq, not_parts_not_analz, 
   813 			   analz_insert_freshK1] @ pushes))));
   814 (*Fake*) 
   815 by (spy_analz_tac 1);
   816 (*K2*)
   817 by (blast_tac (claset() addSEs spies_partsEs
   818             addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);
   819 (*K4*)
   820 by (blast_tac (claset() addSEs spies_partsEs) 1);
   821 (*Level 8: K5*)
   822 by (blast_tac (claset() addEs [ServKey_notin_AuthKeys]
   823                         addDs [Says_Kas_message_form, 
   824 	       		       Says_imp_spies RS parts.Inj]
   825                         addIs [less_SucI]) 1);
   826 (*Oops1*)
   827 by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1);
   828 (*Oops2*)
   829 by (blast_tac (claset() addDs [Says_Tgs_message_form,
   830                                Says_Kas_message_form]) 1);
   831 val lemma = result() RS mp RS mp RSN(1,rev_notE);
   832 
   833 
   834 Goal "[| Says Kas A                                             \
   835 \             (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
   836 \          : set evs;                                \
   837 \        ~ ExpirAuth Tk evs;                         \
   838 \        A ~: bad;  evs : kerberos |]            \
   839 \     ==> Key AuthKey ~: analz (spies evs)";
   840 by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
   841 by (blast_tac (claset() addSDs [lemma]) 1);
   842 qed "Confidentiality_Kas";
   843 
   844 
   845 
   846 
   847 
   848 
   849 (********************** Guarantees for Tgs *****************************)
   850 
   851 (** If Spy sees the Service Key sent in msg K4, then 
   852     the Key has expired  **)
   853 Goal "[| A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]           \
   854 \  ==> Key AuthKey ~: analz (spies evs) --> \
   855 \      Says Tgs A            \
   856 \        (Crypt AuthKey                      \
   857 \           {|Key ServKey, Agent B, Number Tt,     \
   858 \             Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})\
   859 \        : set evs -->                 \
   860 \      Key ServKey : analz (spies evs) -->                       \
   861 \      ExpirServ Tt evs";
   862 by (etac kerberos.induct 1);
   863 (*The Oops1 case is unusual: must simplify Authkey ~: analz (spies (ev#evs))
   864   rather than weakening it to Authkey ~: analz (spies evs), for we then
   865   conclude AuthKey ~= AuthKeya.*)
   866 by (Clarify_tac 9);
   867 by analz_sees_tac;
   868 by (rotate_tac ~1 11);
   869 by (ALLGOALS 
   870     (asm_full_simp_tac 
   871      (simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form,
   872 			   analz_insert_eq, not_parts_not_analz, 
   873 			   analz_insert_freshK1, analz_insert_freshK2] @ pushes))));
   874 (*Fake*) 
   875 by (spy_analz_tac 1);
   876 (*K2*)
   877 by (blast_tac (claset() addSEs spies_partsEs
   878             addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);
   879 (*K4*)
   880 by (case_tac "A ~= Aa" 1);
   881 by (blast_tac (claset() addSEs spies_partsEs
   882                         addIs [less_SucI]) 1);
   883 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst, 
   884                                A_trusts_AuthTicket, 
   885                                Confidentiality_Kas,
   886                                impOfSubs analz_subset_parts]) 1);
   887 by (ALLGOALS Clarify_tac);
   888 (*Oops2*)
   889 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   890                                Key_unique_SesKey] addIs [less_SucI]) 3);
   891 (** Level 12 **)
   892 (*Oops1*)
   893 by (ftac Says_Kas_message_form 2);
   894 by (assume_tac 2);
   895 by (blast_tac (claset() addDs [analz_insert_freshK3,
   896 			       Says_Kas_message_form, Says_Tgs_message_form] 
   897                         addIs  [less_SucI]) 2);
   898 (** Level 16 **)
   899 by (thin_tac "Says Aa Tgs ?X : set ?evs" 1);
   900 by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
   901 by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
   902 by (rotate_tac ~1 1);
   903 by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
   904 by (etac disjE 1);
   905 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   906                                Key_unique_SesKey]) 1);
   907 by (blast_tac (claset() addIs [less_SucI]) 1);
   908 val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE);
   909 
   910 
   911 (* In the real world Tgs can't check wheter AuthKey is secure! *)
   912 Goal 
   913  "[| Says Tgs A      \
   914 \             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   915 \             : set evs;              \
   916 \           Key AuthKey ~: analz (spies evs);        \
   917 \           ~ ExpirServ Tt evs;                         \
   918 \           A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   919 \        ==> Key ServKey ~: analz (spies evs)";
   920 by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
   921 by (blast_tac (claset() addDs [lemma]) 1);
   922 qed "Confidentiality_Tgs1";
   923 
   924 (* In the real world Tgs CAN check what Kas sends! *)
   925 Goal 
   926  "[| Says Kas A                                             \
   927 \              (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
   928 \             : set evs;                                \
   929 \           Says Tgs A      \
   930 \             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
   931 \             : set evs;              \
   932 \           ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
   933 \           A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   934 \        ==> Key ServKey ~: analz (spies evs)";
   935 by (blast_tac (claset() addSDs [Confidentiality_Kas,
   936                                 Confidentiality_Tgs1]) 1);
   937 qed "Confidentiality_Tgs2";
   938 
   939 (*Most general form*)
   940 val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2;
   941 
   942 
   943 (********************** Guarantees for Alice *****************************)
   944 
   945 val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas;
   946 
   947 Goal
   948  "[| Says Kas A \
   949 \      (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) : set evs;\
   950 \    Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}     \
   951 \      : parts (spies evs);                                       \
   952 \    Key AuthKey ~: analz (spies evs);            \
   953 \    evs : kerberos |]         \
   954 \==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
   955 \      : set evs";
   956 by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
   957 by (etac rev_mp 1);
   958 by (etac rev_mp 1);
   959 by (etac rev_mp 1);
   960 by (parts_induct_tac 1);
   961 by (Fake_parts_insert_tac 1);
   962 (*K2 and K4 remain*)
   963 by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts] 
   964                         addSDs [unique_CryptKey]) 2);
   965 by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 
   966 				AuthKeys_used]) 1);
   967 qed "A_trusts_K4_bis";
   968 
   969 
   970 Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
   971 \          : parts (spies evs);                              \
   972 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}     \
   973 \          : parts (spies evs);                                       \
   974 \        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
   975 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
   976 \     ==> Key ServKey ~: analz (spies evs)";
   977 by (dtac A_trusts_AuthKey 1);
   978 by (assume_tac 1);
   979 by (assume_tac 1);
   980 by (blast_tac (claset() addDs [Confidentiality_Kas, 
   981                                Says_Kas_message_form,
   982                                A_trusts_K4_bis, Confidentiality_Tgs2]) 1);
   983 qed "Confidentiality_Serv_A";
   984 
   985 
   986 (********************** Guarantees for Bob *****************************)
   987 (* Theorems for the refined model have suffix "refined"                *)
   988 
   989 Goal
   990 "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
   991 \            : set evs; evs : kerberos|]  \
   992 \  ==> EX Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
   993 \          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
   994 \            : set evs";
   995 by (etac rev_mp 1);
   996 by (parts_induct_tac 1);
   997 by Auto_tac;
   998 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
   999                                A_trusts_AuthTicket]) 1);
  1000 qed "K4_imp_K2";
  1001 
  1002 Goal
  1003 "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
  1004 \     : set evs; evs : kerberos|]  \
  1005 \  ==> EX Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
  1006 \          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1007 \            : set evs   \
  1008 \         & ServLife + Tt <= AuthLife + Tk)";
  1009 by (etac rev_mp 1);
  1010 by (parts_induct_tac 1);
  1011 by Auto_tac;
  1012 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1013                                A_trusts_AuthTicket]) 1);
  1014 qed "K4_imp_K2_refined";
  1015 
  1016 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}  \
  1017 \          : parts (spies evs);  B ~= Tgs;  B ~: bad;       \
  1018 \        evs : kerberos |]                        \
  1019 \==> EX AuthKey. \
  1020 \      Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,  \
  1021 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}) \
  1022 \      : set evs";
  1023 by (etac rev_mp 1);
  1024 by (parts_induct_tac 1);
  1025 by (Fake_parts_insert_tac 1);
  1026 by (Blast_tac 1);
  1027 qed "B_trusts_ServKey";
  1028 
  1029 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1030 \          : parts (spies evs);  B ~= Tgs;  B ~: bad;       \
  1031 \        evs : kerberos |]                        \
  1032 \  ==> EX AuthKey Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
  1033 \          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1034 \            : set evs";
  1035 by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1);
  1036 qed "B_trusts_ServTicket_Kas";
  1037 
  1038 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1039 \          : parts (spies evs); B ~= Tgs; B ~: bad;       \
  1040 \        evs : kerberos |]                        \
  1041 \  ==> EX AuthKey Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
  1042 \          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1043 \            : set evs            \
  1044 \          & ServLife + Tt <= AuthLife + Tk)";
  1045 by (blast_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1);
  1046 qed "B_trusts_ServTicket_Kas_refined";
  1047 
  1048 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1049 \          : parts (spies evs); B ~= Tgs; B ~: bad;        \
  1050 \        evs : kerberos |]                        \
  1051 \==> EX Tk AuthKey.        \
  1052 \    Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \
  1053 \                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1054 \      : set evs         \ 
  1055 \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
  1056 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
  1057 \      : set evs";
  1058 by (ftac B_trusts_ServKey 1);
  1059 by (etac exE 4);
  1060 by (ftac K4_imp_K2 4);
  1061 by (Blast_tac 5);
  1062 by (ALLGOALS assume_tac);
  1063 qed "B_trusts_ServTicket";
  1064 
  1065 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1066 \          : parts (spies evs); B ~= Tgs; B ~: bad;        \
  1067 \        evs : kerberos |]                        \
  1068 \==> EX Tk AuthKey.        \
  1069 \    (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \
  1070 \                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
  1071 \      : set evs         \ 
  1072 \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
  1073 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
  1074 \      : set evs         \
  1075 \    & ServLife + Tt <= AuthLife + Tk)";
  1076 by (ftac B_trusts_ServKey 1);
  1077 by (etac exE 4);
  1078 by (ftac K4_imp_K2_refined 4);
  1079 by (Blast_tac 5);
  1080 by (ALLGOALS assume_tac);
  1081 qed "B_trusts_ServTicket_refined";
  1082 
  1083 
  1084 Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]        \
  1085 \  ==> ~ ExpirAuth Tk evs";
  1086 by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1);
  1087 qed "NotExpirServ_NotExpirAuth_refined";
  1088 
  1089 
  1090 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \
  1091 \          : parts (spies evs);                                        \
  1092 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
  1093 \          : parts (spies evs);                                         \
  1094 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1095 \          : parts (spies evs);                     \
  1096 \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;     \
  1097 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1098 \     ==> Key ServKey ~: analz (spies evs)";
  1099 by (ftac A_trusts_AuthKey 1);
  1100 by (ftac Confidentiality_Kas 3);
  1101 by (ftac B_trusts_ServTicket 6);
  1102 by (etac exE 9);
  1103 by (etac exE 9);
  1104 by (ftac Says_Kas_message_form 9);
  1105 by (blast_tac (claset() addDs [A_trusts_K4, 
  1106                                unique_ServKeys, unique_AuthKeys,
  1107                                Confidentiality_Tgs2]) 10);
  1108 by (ALLGOALS assume_tac);
  1109 (*
  1110 The proof above executes in 8 secs. It can be done in one command in 50 secs:
  1111 by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,
  1112                                Says_Kas_message_form, B_trusts_ServTicket,
  1113                                unique_ServKeys, unique_AuthKeys,
  1114                                Confidentiality_Kas, 
  1115                                Confidentiality_Tgs2]) 1);
  1116 *)
  1117 qed "Confidentiality_B";
  1118 
  1119 
  1120 (*Most general form -- only for refined model! *)
  1121 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1122 \          : parts (spies evs);                      \
  1123 \        ~ ExpirServ Tt evs;                         \
  1124 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1125 \     ==> Key ServKey ~: analz (spies evs)";
  1126 by (blast_tac (claset() addDs [B_trusts_ServTicket_refined,
  1127 			       NotExpirServ_NotExpirAuth_refined, 
  1128                                Confidentiality_Tgs2]) 1);
  1129 qed "Confidentiality_B_refined";
  1130 
  1131 
  1132 (********************** Authenticity theorems *****************************)
  1133 
  1134 (***1. Session Keys authenticity: they originated with servers.***)
  1135 
  1136 (*Authenticity of AuthKey for A: "A_trusts_AuthKey"*)
  1137 
  1138 (*Authenticity of ServKey for A: "A_trusts_ServKey"*)
  1139 Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|} \
  1140 \          : parts (spies evs);                                     \
  1141 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
  1142 \          : parts (spies evs);                                        \
  1143 \        ~ ExpirAuth Tk evs; A ~: bad; evs : kerberos |]         \
  1144 \==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
  1145 \      : set evs";
  1146 by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1);
  1147 by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1);
  1148 qed "A_trusts_ServKey"; 
  1149 (*Note: requires a temporal check*)
  1150 
  1151 
  1152 (*Authenticity of ServKey for B: "B_trusts_ServKey"*)
  1153 
  1154 (***2. Parties authenticity: each party verifies "the identity of
  1155        another party who generated some data" (quoted from Neuman & Ts'o).***)
  1156        
  1157        (*These guarantees don't assess whether two parties agree on 
  1158          the same session key: sending a message containing a key
  1159          doesn't a priori state knowledge of the key.***)
  1160 
  1161 (*B checks authenticity of A: theorems "A_Authenticity", 
  1162                                        "A_authenticity_refined" *)
  1163 Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);  \
  1164 \        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \
  1165 \                                    ServTicket|}) : set evs;       \
  1166 \        Key ServKey ~: analz (spies evs);                \
  1167 \        A ~: bad; B ~: bad; evs : kerberos |]   \
  1168 \==> Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} : set evs";
  1169 by (etac rev_mp 1);
  1170 by (etac rev_mp 1);
  1171 by (etac rev_mp 1);
  1172 by (etac kerberos.induct 1);
  1173 by (ftac Says_ticket_in_parts_spies 5);
  1174 by (ftac Says_ticket_in_parts_spies 7);
  1175 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1176 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1177 by (Fake_parts_insert_tac 1);
  1178 (*K3*)
  1179 by (blast_tac (claset() addEs spies_partsEs
  1180                         addDs [A_trusts_AuthKey,
  1181                                Says_Kas_message_form, 
  1182                                Says_Tgs_message_form]) 1);
  1183 (*K4*)
  1184 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1185 (*K5*)
  1186 by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1);
  1187 qed "Says_Auth";
  1188 
  1189 (*The second assumption tells B what kind of key ServKey is.*)
  1190 Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);     \
  1191 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1192 \          : parts (spies evs);                                         \
  1193 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}  \ 
  1194 \          : parts (spies evs);                                          \
  1195 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
  1196 \          : parts (spies evs);                                            \
  1197 \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
  1198 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1199 \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1200 \                 Crypt ServKey {|Agent A, Number Ta|} |} : set evs";
  1201 by (ftac Confidentiality_B 1);
  1202 by (ftac B_trusts_ServKey 9);
  1203 by (etac exE 12);
  1204 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1205                         addSIs [Says_Auth]) 12);
  1206 by (ALLGOALS assume_tac);
  1207 qed "A_Authenticity";
  1208 
  1209 (*Stronger form in the refined model*)
  1210 Goal "[| Crypt ServKey {|Agent A, Number Ta2|} : parts (spies evs);     \
  1211 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1212 \          : parts (spies evs);                                         \
  1213 \        ~ ExpirServ Tt evs;                                        \
  1214 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1215 \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1216 \                 Crypt ServKey {|Agent A, Number Ta2|} |} : set evs";
  1217 by (ftac Confidentiality_B_refined 1);
  1218 by (ftac B_trusts_ServKey 6);
  1219 by (etac exE 9);
  1220 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1221                         addSIs [Says_Auth]) 9);
  1222 by (ALLGOALS assume_tac);
  1223 qed "A_Authenticity_refined";
  1224 
  1225 
  1226 (*A checks authenticity of B: theorem "B_authenticity"*)
  1227 
  1228 Goal "[| Crypt ServKey (Number Ta) : parts (spies evs);  \
  1229 \        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \
  1230 \                                    ServTicket|}) : set evs;       \
  1231 \        Key ServKey ~: analz (spies evs);                \
  1232 \        A ~: bad; B ~: bad; evs : kerberos |]   \
  1233 \     ==> Says B A (Crypt ServKey (Number Ta)) : set evs";
  1234 by (etac rev_mp 1);
  1235 by (etac rev_mp 1);
  1236 by (etac rev_mp 1);
  1237 by (etac kerberos.induct 1);
  1238 by (ftac Says_ticket_in_parts_spies 5);
  1239 by (ftac Says_ticket_in_parts_spies 7);
  1240 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1241 by (ALLGOALS Asm_simp_tac);
  1242 by (Fake_parts_insert_tac 1);
  1243 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1244 by (Clarify_tac 1);
  1245 by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
  1246 by (Clarify_tac 1);  (*PROOF FAILED if omitted*)
  1247 by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1);
  1248 qed "Says_K6";
  1249 
  1250 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|}   \
  1251 \          : parts (spies evs);    \
  1252 \        Key AuthKey ~: analz (spies evs); AuthKey ~: range shrK;  \
  1253 \        evs : kerberos |]              \
  1254 \ ==> EX A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})\
  1255 \             : set evs";
  1256 by (etac rev_mp 1);
  1257 by (etac rev_mp 1);
  1258 by (parts_induct_tac 1);
  1259 by (Fake_parts_insert_tac 1);
  1260 by (Blast_tac 1);
  1261 by (Blast_tac 1);
  1262 qed "K4_trustworthy";
  1263 
  1264 Goal "[| Crypt ServKey (Number Ta) : parts (spies evs);           \
  1265 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
  1266 \          : parts (spies evs);                                        \ 
  1267 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1268 \          : parts (spies evs);                                          \
  1269 \        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
  1270 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1271 \     ==> Says B A (Crypt ServKey (Number Ta)) : set evs";
  1272 by (ftac A_trusts_AuthKey 1);
  1273 by (ftac Says_Kas_message_form 3);
  1274 by (ftac Confidentiality_Kas 4);
  1275 by (ftac K4_trustworthy 7);
  1276 by (Blast_tac 8);
  1277 by (etac exE 9);
  1278 by (ftac K4_imp_K2 9);
  1279 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1280                         addSIs [Says_K6]
  1281                         addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10);
  1282 by (ALLGOALS assume_tac);
  1283 qed "B_Authenticity";
  1284 
  1285 
  1286 (***3. Parties' knowledge of session keys. A knows a session key if she
  1287        used it to build a cipher.***)
  1288 
  1289 Goal "[| Says B A (Crypt ServKey (Number Ta)) : set evs;           \
  1290 \        Key ServKey ~: analz (spies evs);                          \
  1291 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1292 \     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1293 by (simp_tac (simpset() addsimps [Issues_def]) 1);
  1294 by (rtac exI 1);
  1295 by (rtac conjI 1);
  1296 by (assume_tac 1);
  1297 by (Simp_tac 1);
  1298 by (etac rev_mp 1);
  1299 by (etac rev_mp 1);
  1300 by (etac kerberos.induct 1);
  1301 by (ftac Says_ticket_in_parts_spies 5);
  1302 by (ftac Says_ticket_in_parts_spies 7);
  1303 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1304 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1305 by (Fake_parts_insert_tac 1);
  1306 (*K6 requires numerous lemmas*)
  1307 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1308 by (blast_tac (claset() addDs [B_trusts_ServTicket,
  1309                                impOfSubs parts_spies_takeWhile_mono,
  1310                                impOfSubs parts_spies_evs_revD2]
  1311                         addIs [Says_K6]
  1312                         addEs spies_partsEs) 1);
  1313 qed "B_Knows_B_Knows_ServKey_lemma";
  1314 (*Key ServKey ~: analz (spies evs) could be relaxed by Confidentiality_B
  1315   but this is irrelevant because B knows what he knows!                  *)
  1316 
  1317 Goal "[| Says B A (Crypt ServKey (Number Ta)) : set evs;           \
  1318 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
  1319 \           : parts (spies evs);\
  1320 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}\
  1321 \           : parts (spies evs);\
  1322 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1323 \          : parts (spies evs);     \
  1324 \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;              \
  1325 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1326 \     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1327 by (blast_tac (claset() addSDs [Confidentiality_B,
  1328 	                       B_Knows_B_Knows_ServKey_lemma]) 1);
  1329 qed "B_Knows_B_Knows_ServKey";
  1330 
  1331 Goal "[| Says B A (Crypt ServKey (Number Ta)) : set evs;           \
  1332 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
  1333 \           : parts (spies evs);\
  1334 \        ~ ExpirServ Tt evs;            \
  1335 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1336 \     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1337 by (blast_tac (claset() addSDs [Confidentiality_B_refined,
  1338 	                       B_Knows_B_Knows_ServKey_lemma]) 1);
  1339 qed "B_Knows_B_Knows_ServKey_refined";
  1340 
  1341 
  1342 Goal "[| Crypt ServKey (Number Ta) : parts (spies evs);           \
  1343 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
  1344 \          : parts (spies evs);                                        \ 
  1345 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1346 \          : parts (spies evs);                                          \
  1347 \        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
  1348 \        A ~: bad;  B ~: bad; B ~= Tgs; evs : kerberos |]            \
  1349 \     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
  1350 by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A,
  1351                                 B_Knows_B_Knows_ServKey_lemma]) 1);
  1352 qed "A_Knows_B_Knows_ServKey";
  1353 
  1354 Goal "[| Says A Tgs     \
  1355 \            {|AuthTicket, Crypt AuthKey {|Agent A, Number Ta|}, Agent B|}\
  1356 \          : set evs;      \
  1357 \        A ~: bad;  evs : kerberos |]         \
  1358 \     ==> EX Tk. Says Kas A (Crypt (shrK A) \
  1359 \                     {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
  1360 \                  : set evs";
  1361 by (etac rev_mp 1);
  1362 by (parts_induct_tac 1);
  1363 by (Fake_parts_insert_tac 1);
  1364 by (Blast_tac 1);
  1365 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 
  1366 			       A_trusts_AuthKey]) 1);
  1367 qed "K3_imp_K2";
  1368 
  1369 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
  1370 \          : parts (spies evs);                    \
  1371 \        Says Kas A (Crypt (shrK A) \
  1372 \                    {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
  1373 \        : set evs;    \
  1374 \        Key AuthKey ~: analz (spies evs);       \
  1375 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1376 \  ==> Says Tgs A (Crypt AuthKey        \ 
  1377 \                    {|Key ServKey, Agent B, Number Tt, ServTicket|})  \
  1378 \        : set evs";      
  1379 by (etac rev_mp 1);
  1380 by (etac rev_mp 1);
  1381 by (etac rev_mp 1);
  1382 by (parts_induct_tac 1);
  1383 by (Fake_parts_insert_tac 1);
  1384 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1385 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1386                                A_trusts_AuthTicket, unique_AuthKeys]) 1);
  1387 qed "K4_trustworthy'";
  1388 
  1389 Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
  1390 \          : set evs;       \
  1391 \        Key ServKey ~: analz (spies evs);       \
  1392 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1393 \  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1394 by (simp_tac (simpset() addsimps [Issues_def]) 1);
  1395 by (rtac exI 1);
  1396 by (rtac conjI 1);
  1397 by (assume_tac 1);
  1398 by (Simp_tac 1);
  1399 by (etac rev_mp 1);
  1400 by (etac rev_mp 1);
  1401 by (etac kerberos.induct 1);
  1402 by (ftac Says_ticket_in_parts_spies 5);
  1403 by (ftac Says_ticket_in_parts_spies 7);
  1404 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1405 by (ALLGOALS Asm_simp_tac);
  1406 by (Clarify_tac 1);
  1407 (*K6*)
  1408 by Auto_tac;
  1409 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1410 (*Level 15: case study necessary because the assumption doesn't state
  1411   the form of ServTicket. The guarantee becomes stronger.*)
  1412 by (case_tac "Key AuthKey : analz (spies evs5)" 1);
  1413 by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
  1414 			       analz.Decrypt RS analz.Fst],
  1415 	       simpset()) 1);
  1416 by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy',
  1417                                impOfSubs parts_spies_takeWhile_mono,
  1418                                impOfSubs parts_spies_evs_revD2]
  1419                         addIs [Says_Auth] 
  1420                         addEs spies_partsEs) 1);
  1421 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1422 qed "A_Knows_A_Knows_ServKey_lemma";
  1423 
  1424 Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
  1425 \          : set evs;       \
  1426 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
  1427 \          : parts (spies evs);\
  1428 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}\
  1429 \          : parts (spies evs);                                        \
  1430 \        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;\
  1431 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1432 \  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1433 by (blast_tac (claset() addSDs [Confidentiality_Serv_A,
  1434 	                       A_Knows_A_Knows_ServKey_lemma]) 1);
  1435 qed "A_Knows_A_Knows_ServKey";
  1436 
  1437 Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);     \
  1438 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1439 \          : parts (spies evs);                                         \
  1440 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}  \ 
  1441 \          : parts (spies evs);                                          \
  1442 \        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
  1443 \          : parts (spies evs);                                            \
  1444 \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
  1445 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1446 \  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1447 by (blast_tac (claset() addDs [A_Authenticity, Confidentiality_B,
  1448 	                       A_Knows_A_Knows_ServKey_lemma]) 1);
  1449 qed "B_Knows_A_Knows_ServKey";
  1450 
  1451 
  1452 Goal "[| Crypt ServKey {|Agent A, Number Ta|} : parts (spies evs);     \
  1453 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1454 \          : parts (spies evs);                                         \
  1455 \        ~ ExpirServ Tt evs;                                        \
  1456 \        B ~= Tgs; A ~: bad;  B ~: bad;  evs : kerberos |]         \
  1457 \  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
  1458 by (blast_tac (claset() addDs [A_Authenticity_refined, 
  1459                                Confidentiality_B_refined,
  1460 	                       A_Knows_A_Knows_ServKey_lemma]) 1);
  1461 qed "B_Knows_A_Knows_ServKey_refined";