src/HOL/Auth/KerberosIV.ML
changeset 11222 72c5997e1145
parent 11204 bb01189f0565
child 11288 7fe6593133d4
equal deleted inserted replaced
11221:60c6e91f6079 11222:72c5997e1145
     1 (*  Title:      HOL/Auth/KerberosIV
     1 (*  Title:      HOL/Auth/KerberosIV
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     3     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     4     Copyright   1998  University of Cambridge
     5 
     5 
     6 The Kerberos protocol, version IV.
     6 The Kerberos protocol, version IV.  Proofs streamlined by lcp.
     7 *)
     7 *)
       
     8 
       
     9 
       
    10 AddDs  [Says_imp_knows_Spy RS parts.Inj, parts.Body];
       
    11 AddDs  [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
     8 
    12 
     9 Pretty.setdepth 20;
    13 Pretty.setdepth 20;
    10 set timing;
    14 set timing;
    11 
    15 
    12 AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
    16 AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
    93 by Auto_tac;
    97 by Auto_tac;
    94 qed "AuthKeysI";
    98 qed "AuthKeysI";
    95 
    99 
    96 Goalw [AuthKeys_def] "K \\<in> AuthKeys evs ==> Key K \\<in> used evs";
   100 Goalw [AuthKeys_def] "K \\<in> AuthKeys evs ==> Key K \\<in> used evs";
    97 by (Simp_tac 1);
   101 by (Simp_tac 1);
    98 by (blast_tac (claset() addSEs spies_partsEs) 1);
   102 by (Blast_tac 1);
    99 qed "AuthKeys_used";
   103 qed "AuthKeys_used";
   100 
   104 
   101 
   105 
   102 (**** FORWARDING LEMMAS ****)
   106 (**** FORWARDING LEMMAS ****)
   103 
   107 
   104 (*--For reasoning about the encrypted portion of message K3--*)
   108 (*--For reasoning about the encrypted portion of message K3--*)
   105 Goal "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
   109 Goal "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
   106 \              \\<in> set evs ==> AuthTicket \\<in> parts (spies evs)";
   110 \              \\<in> set evs ==> AuthTicket \\<in> parts (spies evs)";
   107 by (blast_tac (claset() addSEs spies_partsEs) 1);
   111 by (Blast_tac 1);
   108 qed "K3_msg_in_parts_spies";
   112 qed "K3_msg_in_parts_spies";
   109 
   113 
   110 Goal "Says Kas A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
   114 Goal "Says Kas A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
   111 \              \\<in> set evs ==> AuthKey \\<in> parts (spies evs)";
   115 \              \\<in> set evs ==> AuthKey \\<in> parts (spies evs)";
   112 by (blast_tac (claset() addSEs spies_partsEs) 1);
   116 by (Blast_tac 1);
   113 qed "Oops_parts_spies1";
   117 qed "Oops_parts_spies1";
   114                               
   118                               
   115 Goal "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|}) \
   119 Goal "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|}) \
   116 \          \\<in> set evs ;\
   120 \          \\<in> set evs ;\
   117 \        evs \\<in> kerberos |] ==> AuthKey \\<notin> range shrK";
   121 \        evs \\<in> kerberos |] ==> AuthKey \\<notin> range shrK";
   121 qed "Oops_range_spies1";
   125 qed "Oops_range_spies1";
   122 
   126 
   123 (*--For reasoning about the encrypted portion of message K5--*)
   127 (*--For reasoning about the encrypted portion of message K5--*)
   124 Goal "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
   128 Goal "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
   125  \             \\<in> set evs ==> ServTicket \\<in> parts (spies evs)";
   129  \             \\<in> set evs ==> ServTicket \\<in> parts (spies evs)";
   126 by (blast_tac (claset() addSEs spies_partsEs) 1);
   130 by (Blast_tac 1);
   127 qed "K5_msg_in_parts_spies";
   131 qed "K5_msg_in_parts_spies";
   128 
   132 
   129 Goal "Says Tgs A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
   133 Goal "Says Tgs A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
   130 \                  \\<in> set evs ==> ServKey \\<in> parts (spies evs)";
   134 \                  \\<in> set evs ==> ServKey \\<in> parts (spies evs)";
   131 by (blast_tac (claset() addSEs spies_partsEs) 1);
   135 by (Blast_tac 1);
   132 qed "Oops_parts_spies2";
   136 qed "Oops_parts_spies2";
   133 
   137 
   134 Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) \
   138 Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) \
   135 \          \\<in> set evs ;\
   139 \          \\<in> set evs ;\
   136 \        evs \\<in> kerberos |] ==> ServKey \\<notin> range shrK";
   140 \        evs \\<in> kerberos |] ==> ServKey \\<notin> range shrK";
   139 by Auto_tac;
   143 by Auto_tac;
   140 qed "Oops_range_spies2";
   144 qed "Oops_range_spies2";
   141 
   145 
   142 Goal "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \\<in> set evs \
   146 Goal "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \\<in> set evs \
   143 \     ==> Ticket \\<in> parts (spies evs)";
   147 \     ==> Ticket \\<in> parts (spies evs)";
   144 by (blast_tac (claset() addSEs spies_partsEs) 1);
   148 by (Blast_tac 1);
   145 qed "Says_ticket_in_parts_spies";
   149 qed "Says_ticket_in_parts_spies";
   146 (*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*)
   150 (*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*)
   147 
   151 
   148 fun parts_induct_tac i = 
   152 fun parts_induct_tac i = 
   149     etac kerberos.induct i  THEN 
   153     etac kerberos.induct i  THEN 
   156 
   160 
   157 
   161 
   158 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
   162 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
   159 Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
   163 Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
   160 by (parts_induct_tac 1);
   164 by (parts_induct_tac 1);
   161 by (Fake_parts_insert_tac 1);
       
   162 by (ALLGOALS Blast_tac);
   165 by (ALLGOALS Blast_tac);
   163 qed "Spy_see_shrK";
   166 qed "Spy_see_shrK";
   164 Addsimps [Spy_see_shrK];
   167 Addsimps [Spy_see_shrK];
   165 
   168 
   166 Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
   169 Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
   167 by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset()));
   170 by Auto_tac;
   168 qed "Spy_analz_shrK";
   171 qed "Spy_analz_shrK";
   169 Addsimps [Spy_analz_shrK];
   172 Addsimps [Spy_analz_shrK];
   170 
   173 
   171 Goal "[| Key (shrK A) \\<in> parts (spies evs);  evs \\<in> kerberos |] ==> A:bad";
   174 Goal "[| Key (shrK A) \\<in> parts (spies evs);  evs \\<in> kerberos |] ==> A:bad";
   172 by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
   175 by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
   179 \     Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
   182 \     Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
   180 by (parts_induct_tac 1);
   183 by (parts_induct_tac 1);
   181 (*Fake*)
   184 (*Fake*)
   182 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   185 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   183 (*Others*)
   186 (*Others*)
   184 by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
   187 by (ALLGOALS Blast_tac);
   185 qed_spec_mp "new_keys_not_used";
   188 qed_spec_mp "new_keys_not_used";
   186 Addsimps [new_keys_not_used];
   189 Addsimps [new_keys_not_used];
   187 
   190 
   188 (*Earlier, all protocol proofs declared this theorem.  
   191 (*Earlier, all protocol proofs declared this theorem.  
   189   But few of them actually need it! (Another is Yahalom) *)
   192   But few of them actually need it! (Another is Yahalom) *)
   221 \           \\<in> parts (spies evs); Tgs_B \\<notin> bad;\
   224 \           \\<in> parts (spies evs); Tgs_B \\<notin> bad;\
   222 \        evs \\<in> kerberos |]    \
   225 \        evs \\<in> kerberos |]    \
   223 \     ==> SesKey \\<notin> range shrK";
   226 \     ==> SesKey \\<notin> range shrK";
   224 by (etac rev_mp 1);
   227 by (etac rev_mp 1);
   225 by (parts_induct_tac 1);
   228 by (parts_induct_tac 1);
   226 by (Fake_parts_insert_tac 1);
   229 by (Blast_tac 1);
   227 qed "SesKey_is_session_key";
   230 qed "SesKey_is_session_key";
   228 
   231 
   229 Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}  \
   232 Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}  \
   230 \          \\<in> parts (spies evs);                              \
   233 \          \\<in> parts (spies evs);                              \
   231 \        evs \\<in> kerberos |]                          \
   234 \        evs \\<in> kerberos |]                          \
   232 \     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, \
   235 \     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, \
   233 \                Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})  \
   236 \                Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})  \
   234 \           \\<in> set evs";
   237 \           \\<in> set evs";
   235 by (etac rev_mp 1);
   238 by (etac rev_mp 1);
   236 by (parts_induct_tac 1);
   239 by (parts_induct_tac 1);
   237 (*Fake*)
   240 (*Fake, K4*)
   238 by (Fake_parts_insert_tac 1);
   241 by (ALLGOALS Blast_tac);
   239 (*K4*)
       
   240 by (Blast_tac 1);
       
   241 qed "A_trusts_AuthTicket";
   242 qed "A_trusts_AuthTicket";
   242 
   243 
   243 Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}\
   244 Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}\
   244 \          \\<in> parts (spies evs);\
   245 \          \\<in> parts (spies evs);\
   245 \        evs \\<in> kerberos |]    \
   246 \        evs \\<in> kerberos |]    \
   261 by (etac kerberos.induct 1);
   262 by (etac kerberos.induct 1);
   262 by (ALLGOALS
   263 by (ALLGOALS
   263     (asm_full_simp_tac
   264     (asm_full_simp_tac
   264      (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert,
   265      (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert,
   265 			  AuthKeys_empty, AuthKeys_simp])));
   266 			  AuthKeys_empty, AuthKeys_simp])));
   266 by (blast_tac (claset() addEs  spies_partsEs) 1);
   267 by (blast_tac (claset()) 1);
   267 by Auto_tac;
   268 by Auto_tac;
   268 by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1);
   269 by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1);
   269 by (blast_tac (claset() addSDs [SesKey_is_session_key]
   270 by (blast_tac (claset() addSDs [SesKey_is_session_key]) 1);
   270                         addEs spies_partsEs) 1);
   271 by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey]) 1);
   271 by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey] 
       
   272                         addEs spies_partsEs) 1);
       
   273 qed "Says_Tgs_message_form";
   272 qed "Says_Tgs_message_form";
   274 
   273 
   275 (*If a certain encrypted message appears then it originated with Kas*)
   274 (*If a certain encrypted message appears then it originated with Kas*)
   276 Goal "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}  \
   275 Goal "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}  \
   277 \          \\<in> parts (spies evs);                              \
   276 \          \\<in> parts (spies evs);                              \
   279 \     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})  \
   278 \     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})  \
   280 \           \\<in> set evs";
   279 \           \\<in> set evs";
   281 by (etac rev_mp 1);
   280 by (etac rev_mp 1);
   282 by (parts_induct_tac 1);
   281 by (parts_induct_tac 1);
   283 (*Fake*)
   282 (*Fake*)
   284 by (Fake_parts_insert_tac 1);
   283 by (Blast_tac 1);
   285 (*K4*)
   284 (*K4*)
   286 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst,
   285 by (blast_tac (claset() addSDs [A_trusts_AuthTicket RS Says_Kas_message_form])
   287 			       A_trusts_AuthTicket RS Says_Kas_message_form])
       
   288     1);
   286     1);
   289 qed "A_trusts_AuthKey";
   287 qed "A_trusts_AuthKey";
   290 
   288 
   291 
   289 
   292 (*If a certain encrypted message appears then it originated with Tgs*)
   290 (*If a certain encrypted message appears then it originated with Tgs*)
   299 \      \\<in> set evs";
   297 \      \\<in> set evs";
   300 by (etac rev_mp 1);
   298 by (etac rev_mp 1);
   301 by (etac rev_mp 1);
   299 by (etac rev_mp 1);
   302 by (parts_induct_tac 1);
   300 by (parts_induct_tac 1);
   303 (*Fake*)
   301 (*Fake*)
   304 by (Fake_parts_insert_tac 1);
   302 by (Blast_tac 1);
   305 (*K2*)
   303 (*K2*)
   306 by (Blast_tac 1);
   304 by (Blast_tac 1);
   307 (*K4*)
   305 (*K4*)
   308 by Auto_tac;
   306 by Auto_tac;
   309 qed "A_trusts_K4";
   307 qed "A_trusts_K4";
   314 \        evs \\<in> kerberos |]                \
   312 \        evs \\<in> kerberos |]                \
   315 \   ==> AuthKey \\<notin> range shrK &               \
   313 \   ==> AuthKey \\<notin> range shrK &               \
   316 \       AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}";
   314 \       AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}";
   317 by (etac rev_mp 1);
   315 by (etac rev_mp 1);
   318 by (parts_induct_tac 1);
   316 by (parts_induct_tac 1);
   319 by (Fake_parts_insert_tac 1);
   317 by (ALLGOALS Blast_tac);
   320 by (Blast_tac 1);
       
   321 qed "AuthTicket_form";
   318 qed "AuthTicket_form";
   322 
   319 
   323 (* This form holds also over an AuthTicket, but is not needed below.     *)
   320 (* This form holds also over an AuthTicket, but is not needed below.     *)
   324 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|} \
   321 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|} \
   325 \             \\<in> parts (spies evs); \
   322 \             \\<in> parts (spies evs); \
   328 \        ==> ServKey \\<notin> range shrK &  \
   325 \        ==> ServKey \\<notin> range shrK &  \
   329 \   (\\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})";
   326 \   (\\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})";
   330 by (etac rev_mp 1);
   327 by (etac rev_mp 1);
   331 by (etac rev_mp 1);
   328 by (etac rev_mp 1);
   332 by (parts_induct_tac 1);
   329 by (parts_induct_tac 1);
   333 by (Fake_parts_insert_tac 1);
   330 by (Blast_tac 1);
   334 qed "ServTicket_form";
   331 qed "ServTicket_form";
   335 
   332 
   336 Goal "[| Says Kas' A (Crypt (shrK A) \
   333 Goal "[| Says Kas' A (Crypt (shrK A) \
   337 \             {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} ) \\<in> set evs; \
   334 \             {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} ) \\<in> set evs; \
   338 \        evs \\<in> kerberos |]    \
   335 \        evs \\<in> kerberos |]    \
   339 \     ==> AuthKey \\<notin> range shrK & \
   336 \     ==> AuthKey \\<notin> range shrK & \
   340 \         AuthTicket = \
   337 \         AuthTicket = \
   341 \                 Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}\
   338 \                 Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}\
   342 \         | AuthTicket \\<in> analz (spies evs)";
   339 \         | AuthTicket \\<in> analz (spies evs)";
   343 by (case_tac "A \\<in> bad" 1);
   340 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, 
   344 by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);
   341                                AuthTicket_form]) 1);
   345 by (forward_tac [Says_imp_spies RS parts.Inj] 1);
       
   346 by (blast_tac (claset() addSDs [AuthTicket_form]) 1);
       
   347 qed "Says_kas_message_form";
   342 qed "Says_kas_message_form";
   348 (* Essentially the same as AuthTicket_form *)
   343 (* Essentially the same as AuthTicket_form *)
   349 
   344 
   350 Goal "[| Says Tgs' A (Crypt AuthKey \
   345 Goal "[| Says Tgs' A (Crypt AuthKey \
   351 \             {|Key ServKey, Agent B, Tt, ServTicket|} ) \\<in> set evs; \
   346 \             {|Key ServKey, Agent B, Tt, ServTicket|} ) \\<in> set evs; \
   352 \        evs \\<in> kerberos |]    \
   347 \        evs \\<in> kerberos |]    \
   353 \     ==> ServKey \\<notin> range shrK & \
   348 \     ==> ServKey \\<notin> range shrK & \
   354 \         (\\<exists>A. ServTicket = \
   349 \         (\\<exists>A. ServTicket = \
   355 \                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})  \
   350 \                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})  \
   356 \          | ServTicket \\<in> analz (spies evs)";
   351 \          | ServTicket \\<in> analz (spies evs)";
   357 by (case_tac "Key AuthKey \\<in> analz (spies evs)" 1);
   352 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, 
   358 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1); 
   353                                ServTicket_form]) 1);
   359 by (forward_tac [Says_imp_spies RS parts.Inj] 1);
       
   360 by (blast_tac (claset() addSDs [ServTicket_form]) 1);
       
   361 qed "Says_tgs_message_form";
   354 qed "Says_tgs_message_form";
   362 (* This form MUST be used in analz_sees_tac below *)
   355 (* This form MUST be used in analz_sees_tac below *)
   363 
   356 
   364 
   357 
   365 (*****************UNICITY THEOREMS****************)
   358 (*****************UNICITY THEOREMS****************)
   377 by (etac rev_mp 1);
   370 by (etac rev_mp 1);
   378 by (etac rev_mp 1);
   371 by (etac rev_mp 1);
   379 by (etac rev_mp 1);
   372 by (etac rev_mp 1);
   380 by (parts_induct_tac 1);
   373 by (parts_induct_tac 1);
   381 (*Fake, K2, K4*)
   374 (*Fake, K2, K4*)
   382 by (Fake_parts_insert_tac 1);
   375 by (ALLGOALS Blast_tac); 
   383 by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
       
   384 qed "unique_CryptKey";
   376 qed "unique_CryptKey";
   385 
   377 
   386 (*An AuthKey is encrypted by one and only one Shared key.
   378 (*An AuthKey is encrypted by one and only one Shared key.
   387   A ServKey is encrypted by one and only one AuthKey.
   379   A ServKey is encrypted by one and only one AuthKey.
   388 *)
   380 *)
   395 by (etac rev_mp 1);
   387 by (etac rev_mp 1);
   396 by (etac rev_mp 1);
   388 by (etac rev_mp 1);
   397 by (etac rev_mp 1);
   389 by (etac rev_mp 1);
   398 by (parts_induct_tac 1);
   390 by (parts_induct_tac 1);
   399 (*Fake, K2, K4*)
   391 (*Fake, K2, K4*)
   400 by (Fake_parts_insert_tac 1);
   392 by (ALLGOALS Blast_tac); 
   401 by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
       
   402 qed "Key_unique_SesKey";
   393 qed "Key_unique_SesKey";
   403 
   394 
   404 
   395 
   405 (*
   396 (*
   406   At reception of any message mentioning A, Kas associates shrK A with
   397   At reception of any message mentioning A, Kas associates shrK A with
   427 \        evs \\<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
   418 \        evs \\<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
   428 by (etac rev_mp 1);
   419 by (etac rev_mp 1);
   429 by (etac rev_mp 1);
   420 by (etac rev_mp 1);
   430 by (parts_induct_tac 1);
   421 by (parts_induct_tac 1);
   431 (*K2*)
   422 (*K2*)
   432 by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
   423 by (Blast_tac 1); 
   433 qed "unique_AuthKeys";
   424 qed "unique_AuthKeys";
   434 
   425 
   435 (* ServKey uniquely identifies the message from Tgs *)
   426 (* ServKey uniquely identifies the message from Tgs *)
   436 Goal "[| Says Tgs A                                             \
   427 Goal "[| Says Tgs A                                             \
   437 \             (Crypt K {|Key ServKey, Agent B, Tt, X|}) \\<in> set evs; \ 
   428 \             (Crypt K {|Key ServKey, Agent B, Tt, X|}) \\<in> set evs; \ 
   440 \        evs \\<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
   431 \        evs \\<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
   441 by (etac rev_mp 1);
   432 by (etac rev_mp 1);
   442 by (etac rev_mp 1);
   433 by (etac rev_mp 1);
   443 by (parts_induct_tac 1);
   434 by (parts_induct_tac 1);
   444 (*K4*)
   435 (*K4*)
   445 by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
   436 by (Blast_tac 1); 
   446 qed "unique_ServKeys";
   437 qed "unique_ServKeys";
   447 
   438 
   448 
   439 
   449 (*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
   440 (*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
   450 
   441 
   455 
   446 
   456 Goalw [KeyCryptKey_def]
   447 Goalw [KeyCryptKey_def]
   457  "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
   448  "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
   458 \             \\<in> set evs;    \
   449 \             \\<in> set evs;    \
   459 \           evs \\<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs";
   450 \           evs \\<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs";
   460 by (ftac Says_Tgs_message_form 1);
   451 by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); 
   461 by (assume_tac 1);
       
   462 by (Blast_tac 1);
       
   463 qed "KeyCryptKeyI";
   452 qed "KeyCryptKeyI";
   464 
   453 
   465 Goalw [KeyCryptKey_def]
   454 Goalw [KeyCryptKey_def]
   466    "KeyCryptKey AuthKey ServKey (Says S A X # evs) =                       \
   455    "KeyCryptKey AuthKey ServKey (Says S A X # evs) =                       \
   467 \    (Tgs = S &                                                            \
   456 \    (Tgs = S &                                                            \
   480  "[| Key AuthKey \\<notin> used evs; evs \\<in> kerberos |] \
   469  "[| Key AuthKey \\<notin> used evs; evs \\<in> kerberos |] \
   481 \        ==> ~ KeyCryptKey AuthKey ServKey evs";
   470 \        ==> ~ KeyCryptKey AuthKey ServKey evs";
   482 by (etac rev_mp 1);
   471 by (etac rev_mp 1);
   483 by (parts_induct_tac 1);
   472 by (parts_induct_tac 1);
   484 by (Asm_full_simp_tac 1);
   473 by (Asm_full_simp_tac 1);
   485 by (blast_tac (claset() addSEs spies_partsEs) 1);
   474 by (Blast_tac 1);
   486 qed "Auth_fresh_not_KeyCryptKey";
   475 qed "Auth_fresh_not_KeyCryptKey";
   487 
   476 
   488 (*A fresh ServKey cannot be associated with any other
   477 (*A fresh ServKey cannot be associated with any other
   489   (with respect to a given trace). *)
   478   (with respect to a given trace). *)
   490 Goalw [KeyCryptKey_def]
   479 Goalw [KeyCryptKey_def]
   491  "Key ServKey \\<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs";
   480  "Key ServKey \\<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs";
   492 by (blast_tac (claset() addSEs spies_partsEs) 1);
   481 by (Blast_tac 1);
   493 qed "Serv_fresh_not_KeyCryptKey";
   482 qed "Serv_fresh_not_KeyCryptKey";
   494 
   483 
   495 Goal
   484 Goal
   496  "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
   485  "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
   497 \             \\<in> parts (spies evs);  evs \\<in> kerberos |] \
   486 \             \\<in> parts (spies evs);  evs \\<in> kerberos |] \
   498 \        ==> ~ KeyCryptKey K AuthKey evs";
   487 \        ==> ~ KeyCryptKey K AuthKey evs";
   499 by (etac rev_mp 1);
   488 by (etac rev_mp 1);
   500 by (parts_induct_tac 1);
   489 by (parts_induct_tac 1);
   501 (*K4*)
   490 (*K4*)
   502 by (blast_tac (claset() addEs spies_partsEs) 3);
   491 by (Blast_tac 3);
   503 (*K2: by freshness*)
   492 (*K2: by freshness*)
   504 by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); 
   493 by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); 
   505 by (blast_tac (claset() addEs spies_partsEs) 2);
   494 by (ALLGOALS Blast_tac); 
   506 by (Fake_parts_insert_tac 1);
       
   507 qed "AuthKey_not_KeyCryptKey";
   495 qed "AuthKey_not_KeyCryptKey";
   508 
   496 
   509 (*A secure serverkey cannot have been used to encrypt others*)
   497 (*A secure serverkey cannot have been used to encrypt others*)
   510 Goal
   498 Goal
   511  "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\<in> parts (spies evs); \
   499  "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\<in> parts (spies evs); \
   513 \    B \\<noteq> Tgs;  evs \\<in> kerberos |] \
   501 \    B \\<noteq> Tgs;  evs \\<in> kerberos |] \
   514 \ ==> ~ KeyCryptKey SK K evs";
   502 \ ==> ~ KeyCryptKey SK K evs";
   515 by (etac rev_mp 1);
   503 by (etac rev_mp 1);
   516 by (etac rev_mp 1);
   504 by (etac rev_mp 1);
   517 by (parts_induct_tac 1);
   505 by (parts_induct_tac 1);
   518 by (Fake_parts_insert_tac 1);
   506 by (Blast_tac 1);
   519 (*K4 splits into distinct subcases*)
   507 (*K4 splits into distinct subcases*)
   520 by Auto_tac;  
   508 by Auto_tac;  
   521 (*ServKey can't have been enclosed in two certificates*)
   509 (*ServKey can't have been enclosed in two certificates*)
   522 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   510 by (blast_tac (claset() addDs [unique_CryptKey]) 2);
   523                        addSEs [MPair_parts]
       
   524                        addDs  [unique_CryptKey]) 4);
       
   525 (*ServKey is fresh and so could not have been used, by new_keys_not_used*)
   511 (*ServKey is fresh and so could not have been used, by new_keys_not_used*)
   526 by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
   512 by (force_tac (claset() addSDs [Crypt_imp_invKey_keysFor],
   527 				Crypt_imp_invKey_keysFor],
   513 	       simpset() addsimps [KeyCryptKey_def]) 1); 
   528 	       simpset() addsimps [KeyCryptKey_def]) 2); 
       
   529 (*Others by freshness*)
       
   530 by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
       
   531 qed "ServKey_not_KeyCryptKey";
   514 qed "ServKey_not_KeyCryptKey";
   532 
   515 
   533 (*Long term keys are not issued as ServKeys*)
   516 (*Long term keys are not issued as ServKeys*)
   534 Goalw [KeyCryptKey_def]
   517 Goalw [KeyCryptKey_def]
   535  "evs \\<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs";
   518  "evs \\<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs";
   551 by (etac rev_mp 1);
   534 by (etac rev_mp 1);
   552 by (parts_induct_tac 1);
   535 by (parts_induct_tac 1);
   553 by (Step_tac 1);
   536 by (Step_tac 1);
   554 by (ALLGOALS Asm_full_simp_tac);
   537 by (ALLGOALS Asm_full_simp_tac);
   555 (*K4 splits into subcases*)
   538 (*K4 splits into subcases*)
   556 by (blast_tac (claset() addEs spies_partsEs 
   539 by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 4);
   557                        addSDs [AuthKey_not_KeyCryptKey]) 4);
       
   558 (*ServKey is fresh and so could not have been used, by new_keys_not_used*)
   540 (*ServKey is fresh and so could not have been used, by new_keys_not_used*)
   559 by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
   541 by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
   560 				Crypt_imp_invKey_keysFor],
   542 				Crypt_imp_invKey_keysFor],
   561                       simpset() addsimps [KeyCryptKey_def]) 2); 
   543                simpset() addsimps [KeyCryptKey_def]) 2); 
   562 (*Others by freshness*)
   544 (*Others by freshness*)
   563 by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
   545 by (ALLGOALS Blast_tac);
   564 qed "KeyCryptKey_not_KeyCryptKey";
   546 qed "KeyCryptKey_not_KeyCryptKey";
   565 
   547 
   566 (*The only session keys that can be found with the help of session keys are
   548 (*The only session keys that can be found with the help of session keys are
   567   those sent by Tgs in step K4.  *)
   549   those sent by Tgs in step K4.  *)
   568 
   550 
   646 by (spy_analz_tac 1);
   628 by (spy_analz_tac 1);
   647 (* Base + K2 done by the simplifier! *)
   629 (* Base + K2 done by the simplifier! *)
   648 (*K3*)
   630 (*K3*)
   649 by (Blast_tac 1);
   631 by (Blast_tac 1);
   650 (*K4*)
   632 (*K4*)
   651 by (blast_tac (claset() addEs spies_partsEs 
   633 by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 1);
   652                         addSDs [AuthKey_not_KeyCryptKey]) 1);
       
   653 (*K5*)
   634 (*K5*)
   654 by (case_tac "Key ServKey \\<in> analz (spies evs5)" 1);
   635 by (case_tac "Key ServKey \\<in> analz (spies evs5)" 1);
   655 (*If ServKey is compromised then the result follows directly...*)
   636 (*If ServKey is compromised then the result follows directly...*)
   656 by (asm_simp_tac 
   637 by (asm_simp_tac 
   657      (simpset() addsimps [analz_insert_eq, 
   638      (simpset() addsimps [analz_insert_eq, 
   658 			 impOfSubs (Un_upper2 RS analz_mono)]) 1);
   639 			 impOfSubs (Un_upper2 RS analz_mono)]) 1);
   659 (*...therefore ServKey is uncompromised.*)
   640 (*...therefore ServKey is uncompromised.*)
   660 (*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*)
   641 (*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*)
   661 by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)]
   642 by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)]
   662 		        addEs spies_partsEs delrules [allE, ballE]) 1);
   643 		        delrules [allE, ballE]) 1);
   663 (** Level 13: Oops1 **)
   644 (** Level 13: Oops1 **)
   664 by (Asm_full_simp_tac 1);
   645 by (Asm_full_simp_tac 1);
   665 by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
   646 by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
   666 qed_spec_mp "Key_analz_image_Key";
   647 qed_spec_mp "Key_analz_image_Key";
   667 
   648 
   726 \     ==> ServKey \\<notin> AuthKeys evs";
   707 \     ==> ServKey \\<notin> AuthKeys evs";
   727 by (etac rev_mp 1);
   708 by (etac rev_mp 1);
   728 by (etac rev_mp 1);
   709 by (etac rev_mp 1);
   729 by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);
   710 by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);
   730 by (parts_induct_tac 1);
   711 by (parts_induct_tac 1);
   731 by (Fake_parts_insert_tac 1);
   712 by (ALLGOALS Blast_tac);
   732 by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
       
   733 bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE));
   713 bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE));
   734 bind_thm ("ServKey_notin_AuthKeysD", result());
   714 bind_thm ("ServKey_notin_AuthKeysD", result());
   735 
   715 
   736 
   716 
   737 (** If Spy sees the Authentication Key sent in msg K2, then 
   717 (** If Spy sees the Authentication Key sent in msg K2, then 
   752 			   analz_insert_eq, not_parts_not_analz, 
   732 			   analz_insert_eq, not_parts_not_analz, 
   753 			   analz_insert_freshK1] @ pushes))));
   733 			   analz_insert_freshK1] @ pushes))));
   754 (*Fake*) 
   734 (*Fake*) 
   755 by (spy_analz_tac 1);
   735 by (spy_analz_tac 1);
   756 (*K2*)
   736 (*K2*)
   757 by (blast_tac (claset() addSEs spies_partsEs
   737 by (Blast_tac 1);
   758             addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);
       
   759 (*K4*)
   738 (*K4*)
   760 by (blast_tac (claset() addSEs spies_partsEs) 1);
   739 by (Blast_tac 1);
   761 (*Level 8: K5*)
   740 (*Level 8: K5*)
   762 by (blast_tac (claset() addEs [ServKey_notin_AuthKeys]
   741 by (blast_tac (claset() addEs [ServKey_notin_AuthKeys]
   763                         addDs [Says_Kas_message_form, 
   742                         addDs [Says_Kas_message_form]
   764 	       		       Says_imp_spies RS parts.Inj]
       
   765                         addIs [less_SucI]) 1);
   743                         addIs [less_SucI]) 1);
   766 (*Oops1*)
   744 (*Oops1*)
   767 by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1);
   745 by (blast_tac (claset() addSDs [unique_AuthKeys] addIs [less_SucI]) 1);
   768 (*Oops2*)
   746 (*Oops2*)
   769 by (blast_tac (claset() addDs [Says_Tgs_message_form,
   747 by (blast_tac (claset() addDs [Says_Tgs_message_form,
   770                                Says_Kas_message_form]) 1);
   748                                Says_Kas_message_form]) 1);
   771 val lemma = result() RS mp RS mp RSN(1,rev_notE);
   749 val lemma = result() RS mp RS mp RSN(1,rev_notE);
   772 
   750 
   775 \             (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
   753 \             (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
   776 \          \\<in> set evs;                                \
   754 \          \\<in> set evs;                                \
   777 \        ~ ExpirAuth Tk evs;                         \
   755 \        ~ ExpirAuth Tk evs;                         \
   778 \        A \\<notin> bad;  evs \\<in> kerberos |]            \
   756 \        A \\<notin> bad;  evs \\<in> kerberos |]            \
   779 \     ==> Key AuthKey \\<notin> analz (spies evs)";
   757 \     ==> Key AuthKey \\<notin> analz (spies evs)";
   780 by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
   758 by (blast_tac (claset() addDs [Says_Kas_message_form, lemma]) 1);
   781 by (blast_tac (claset() addSDs [lemma]) 1);
       
   782 qed "Confidentiality_Kas";
   759 qed "Confidentiality_Kas";
   783 
   760 
   784 
   761 
   785 (********************** Guarantees for Tgs *****************************)
   762 (********************** Guarantees for Tgs *****************************)
   786 
   763 
   810 			  analz_insert_freshK1, analz_insert_freshK2] 
   787 			  analz_insert_freshK1, analz_insert_freshK2] 
   811 			 @ pushes)));
   788 			 @ pushes)));
   812 (*Fake*) 
   789 (*Fake*) 
   813 by (spy_analz_tac 1);
   790 by (spy_analz_tac 1);
   814 (*K2*)
   791 (*K2*)
   815 by (blast_tac (claset() addSEs spies_partsEs
   792 by (blast_tac (claset()
   816             addIs [parts_insertI, less_SucI]) 1);
   793             addIs [parts_insertI, less_SucI]) 1);
   817 (*K4*)
   794 (*K4*)
   818 by (case_tac "A \\<noteq> Aa" 1);
   795 by (blast_tac (claset() addDs [A_trusts_AuthTicket, Confidentiality_Kas]) 1);
   819 by (blast_tac (claset() addSEs spies_partsEs
       
   820                         addIs [less_SucI]) 1);
       
   821 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst, 
       
   822                                A_trusts_AuthTicket, 
       
   823                                Confidentiality_Kas,
       
   824                                impOfSubs analz_subset_parts]) 1);
       
   825 by (ALLGOALS Clarify_tac);
   796 by (ALLGOALS Clarify_tac);
   826 (*Oops2*)
   797 (*Oops2*)
   827 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   798 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   828                                Key_unique_SesKey] addIs [less_SucI]) 3);
   799                                Key_unique_SesKey] addIs [less_SucI]) 3);
   829 (** Level 12 **)
   800 (** Level 10 **)
   830 (*Oops1*)
   801 (*Oops1*)
   831 by (ftac Says_Kas_message_form 2);
       
   832 by (assume_tac 2);
       
   833 by (blast_tac (claset() addDs [analz_insert_freshK3,
   802 by (blast_tac (claset() addDs [analz_insert_freshK3,
   834 			       Says_Kas_message_form, Says_Tgs_message_form] 
   803 			       Says_Kas_message_form, Says_Tgs_message_form] 
   835                         addIs  [less_SucI]) 2);
   804                         addIs  [less_SucI]) 2);
   836 (** Level 16 **)
   805 (*K5*)
   837 by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
   806 by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
   838 by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
   807 by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
   839 by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
   808 by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
   840 by (rotate_tac ~1 1);
   809 by (rotate_tac ~1 1);
   841 by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
   810 by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
   842 by (etac disjE 1);
   811 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
   843 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   812                         addIs  [less_SucI]) 1);
   844                                Key_unique_SesKey]) 1);
       
   845 by (blast_tac (claset() addIs [less_SucI]) 1);
       
   846 val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE);
   813 val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE);
   847 
   814 
   848 
   815 
   849 (* In the real world Tgs can't check wheter AuthKey is secure! *)
   816 (* In the real world Tgs can't check wheter AuthKey is secure! *)
   850 Goal 
   817 Goal 
   853 \             \\<in> set evs;              \
   820 \             \\<in> set evs;              \
   854 \           Key AuthKey \\<notin> analz (spies evs);        \
   821 \           Key AuthKey \\<notin> analz (spies evs);        \
   855 \           ~ ExpirServ Tt evs;                         \
   822 \           ~ ExpirServ Tt evs;                         \
   856 \           A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
   823 \           A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
   857 \        ==> Key ServKey \\<notin> analz (spies evs)";
   824 \        ==> Key ServKey \\<notin> analz (spies evs)";
   858 by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
   825 by (blast_tac (claset() addDs [Says_Tgs_message_form, lemma]) 1);
   859 by (blast_tac (claset() addDs [lemma]) 1);
       
   860 qed "Confidentiality_Tgs1";
   826 qed "Confidentiality_Tgs1";
   861 
   827 
   862 (* In the real world Tgs CAN check what Kas sends! *)
   828 (* In the real world Tgs CAN check what Kas sends! *)
   863 Goal 
   829 Goal 
   864  "[| Says Kas A                                             \
   830  "[| Says Kas A                                             \
   894 by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
   860 by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
   895 by (etac rev_mp 1);
   861 by (etac rev_mp 1);
   896 by (etac rev_mp 1);
   862 by (etac rev_mp 1);
   897 by (etac rev_mp 1);
   863 by (etac rev_mp 1);
   898 by (parts_induct_tac 1);
   864 by (parts_induct_tac 1);
   899 by (Fake_parts_insert_tac 1);
   865 by (Blast_tac 1);
   900 (*K2 and K4 remain*)
   866 (*K2 and K4 remain*)
   901 by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts] 
   867 by (blast_tac (claset() addSDs [unique_CryptKey]) 2);
   902                         addSDs [unique_CryptKey]) 2);
       
   903 by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 
   868 by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 
   904 				AuthKeys_used]) 1);
   869 				AuthKeys_used]) 1);
   905 qed "A_trusts_K4_bis";
   870 qed "A_trusts_K4_bis";
   906 
   871 
   907 
   872 
   958 \      Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,  \
   923 \      Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,  \
   959 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}) \
   924 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}) \
   960 \      \\<in> set evs";
   925 \      \\<in> set evs";
   961 by (etac rev_mp 1);
   926 by (etac rev_mp 1);
   962 by (parts_induct_tac 1);
   927 by (parts_induct_tac 1);
   963 by (Fake_parts_insert_tac 1);
   928 by (ALLGOALS Blast_tac);
   964 by (Blast_tac 1);
       
   965 qed "B_trusts_ServKey";
   929 qed "B_trusts_ServKey";
   966 
   930 
   967 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
   931 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
   968 \          \\<in> parts (spies evs);  B \\<noteq> Tgs;  B \\<notin> bad;       \
   932 \          \\<in> parts (spies evs);  B \\<noteq> Tgs;  B \\<notin> bad;       \
   969 \        evs \\<in> kerberos |]                        \
   933 \        evs \\<in> kerberos |]                        \
   991 \                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
   955 \                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
   992 \      \\<in> set evs         \ 
   956 \      \\<in> set evs         \ 
   993 \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
   957 \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
   994 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
   958 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
   995 \      \\<in> set evs";
   959 \      \\<in> set evs";
   996 by (ftac B_trusts_ServKey 1);
   960 by (blast_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2]) 1);
   997 by (etac exE 4);
       
   998 by (ftac K4_imp_K2 4);
       
   999 by (Blast_tac 5);
       
  1000 by (ALLGOALS assume_tac);
       
  1001 qed "B_trusts_ServTicket";
   961 qed "B_trusts_ServTicket";
  1002 
   962 
  1003 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
   963 Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
  1004 \          \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad;        \
   964 \          \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad;        \
  1005 \        evs \\<in> kerberos |]                        \
   965 \        evs \\<in> kerberos |]                        \
  1009 \      \\<in> set evs         \ 
   969 \      \\<in> set evs         \ 
  1010 \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
   970 \    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
  1011 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
   971 \                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
  1012 \      \\<in> set evs         \
   972 \      \\<in> set evs         \
  1013 \    & ServLife + Tt <= AuthLife + Tk)";
   973 \    & ServLife + Tt <= AuthLife + Tk)";
  1014 by (ftac B_trusts_ServKey 1);
   974 by (blast_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2_refined]) 1);
  1015 by (etac exE 4);
       
  1016 by (ftac K4_imp_K2_refined 4);
       
  1017 by (Blast_tac 5);
       
  1018 by (ALLGOALS assume_tac);
       
  1019 qed "B_trusts_ServTicket_refined";
   975 qed "B_trusts_ServTicket_refined";
  1020 
   976 
  1021 
   977 
  1022 Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]        \
   978 Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]        \
  1023 \  ==> ~ ExpirAuth Tk evs";
   979 \  ==> ~ ExpirAuth Tk evs";
  1035 \        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
   991 \        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
  1036 \     ==> Key ServKey \\<notin> analz (spies evs)";
   992 \     ==> Key ServKey \\<notin> analz (spies evs)";
  1037 by (ftac A_trusts_AuthKey 1);
   993 by (ftac A_trusts_AuthKey 1);
  1038 by (ftac Confidentiality_Kas 3);
   994 by (ftac Confidentiality_Kas 3);
  1039 by (ftac B_trusts_ServTicket 6);
   995 by (ftac B_trusts_ServTicket 6);
  1040 by (etac exE 9);
   996 by (blast_tac (claset() addSDs [Confidentiality_Tgs2]
  1041 by (etac exE 9);
   997 			addDs [Says_Kas_message_form, A_trusts_K4, 
  1042 by (ftac Says_Kas_message_form 9);
   998                                unique_ServKeys, unique_AuthKeys]) 9);
  1043 by (blast_tac (claset() addDs [A_trusts_K4, 
       
  1044                                unique_ServKeys, unique_AuthKeys,
       
  1045                                Confidentiality_Tgs2]) 10);
       
  1046 by (ALLGOALS assume_tac);
   999 by (ALLGOALS assume_tac);
  1047 (*
  1000 (*
  1048 The proof above executes in 8 secs. It can be done in one command in 50 secs:
  1001 The proof above is fast.  It can be done in one command in 50 secs:
  1049 by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,
  1002 by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,
  1050                                Says_Kas_message_form, B_trusts_ServTicket,
  1003                                Says_Kas_message_form, B_trusts_ServTicket,
  1051                                unique_ServKeys, unique_AuthKeys,
  1004                                unique_ServKeys, unique_AuthKeys,
  1052                                Confidentiality_Kas, 
  1005                                Confidentiality_Kas, 
  1053                                Confidentiality_Tgs2]) 1);
  1006                                Confidentiality_Tgs2]) 1);
  1079 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
  1032 \        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
  1080 \          \\<in> parts (spies evs);                                        \
  1033 \          \\<in> parts (spies evs);                                        \
  1081 \        ~ ExpirAuth Tk evs; A \\<notin> bad; evs \\<in> kerberos |]         \
  1034 \        ~ ExpirAuth Tk evs; A \\<notin> bad; evs \\<in> kerberos |]         \
  1082 \==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
  1035 \==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
  1083 \      \\<in> set evs";
  1036 \      \\<in> set evs";
  1084 by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1);
  1037 by (blast_tac (claset() addDs [A_trusts_AuthKey, Confidentiality_Auth_A, 
  1085 by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1);
  1038                                A_trusts_K4_bis]) 1);
  1086 qed "A_trusts_ServKey"; 
  1039 qed "A_trusts_ServKey"; 
  1087 (*Note: requires a temporal check*)
  1040 (*Note: requires a temporal check*)
  1088 
  1041 
  1089 
  1042 
  1090 (*Authenticity of ServKey for B: "B_trusts_ServKey"*)
  1043 (*Authenticity of ServKey for B: "B_trusts_ServKey"*)
  1110 by (etac kerberos.induct 1);
  1063 by (etac kerberos.induct 1);
  1111 by (ftac Says_ticket_in_parts_spies 5);
  1064 by (ftac Says_ticket_in_parts_spies 5);
  1112 by (ftac Says_ticket_in_parts_spies 7);
  1065 by (ftac Says_ticket_in_parts_spies 7);
  1113 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1066 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1114 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1067 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1115 by (Fake_parts_insert_tac 1);
  1068 by (Blast_tac 1);
  1116 (*K3*)
  1069 (*K3*)
  1117 by (blast_tac (claset() addEs spies_partsEs
  1070 by (blast_tac (claset() addDs [A_trusts_AuthKey,
  1118                         addDs [A_trusts_AuthKey,
       
  1119                                Says_Kas_message_form, 
  1071                                Says_Kas_message_form, 
  1120                                Says_Tgs_message_form]) 1);
  1072                                Says_Tgs_message_form]) 1);
  1121 (*K4*)
  1073 (*K4*)
  1122 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1074 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1123 (*K5*)
  1075 (*K5*)
  1124 by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1);
  1076 by (blast_tac (claset() addDs [Key_unique_SesKey]) 1);
  1125 qed "Says_Auth";
  1077 qed "Says_Auth";
  1126 
  1078 
  1127 (*The second assumption tells B what kind of key ServKey is.*)
  1079 (*The second assumption tells B what kind of key ServKey is.*)
  1128 Goal "[| Crypt ServKey {|Agent A, Number Ta|} \\<in> parts (spies evs);     \
  1080 Goal "[| Crypt ServKey {|Agent A, Number Ta|} \\<in> parts (spies evs);     \
  1129 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1081 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1134 \          \\<in> parts (spies evs);                                            \
  1086 \          \\<in> parts (spies evs);                                            \
  1135 \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
  1087 \        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
  1136 \        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
  1088 \        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
  1137 \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1089 \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1138 \                 Crypt ServKey {|Agent A, Number Ta|} |} \\<in> set evs";
  1090 \                 Crypt ServKey {|Agent A, Number Ta|} |} \\<in> set evs";
  1139 by (ftac Confidentiality_B 1);
  1091 by (blast_tac (claset() addIs [Says_Auth]
  1140 by (ftac B_trusts_ServKey 9);
  1092                         addDs [Confidentiality_B, Key_unique_SesKey,
  1141 by (etac exE 12);
  1093                                B_trusts_ServKey]) 1);
  1142 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
       
  1143                         addSIs [Says_Auth]) 12);
       
  1144 by (ALLGOALS assume_tac);
       
  1145 qed "A_Authenticity";
  1094 qed "A_Authenticity";
  1146 
  1095 
  1147 (*Stronger form in the refined model*)
  1096 (*Stronger form in the refined model*)
  1148 Goal "[| Crypt ServKey {|Agent A, Number Ta2|} \\<in> parts (spies evs);     \
  1097 Goal "[| Crypt ServKey {|Agent A, Number Ta2|} \\<in> parts (spies evs);     \
  1149 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1098 \        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
  1150 \          \\<in> parts (spies evs);                                         \
  1099 \          \\<in> parts (spies evs);                                         \
  1151 \        ~ ExpirServ Tt evs;                                        \
  1100 \        ~ ExpirServ Tt evs;                                        \
  1152 \        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
  1101 \        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
  1153 \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1102 \  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
  1154 \                 Crypt ServKey {|Agent A, Number Ta2|} |} \\<in> set evs";
  1103 \                 Crypt ServKey {|Agent A, Number Ta2|} |} \\<in> set evs";
  1155 by (ftac Confidentiality_B_refined 1);
  1104 by (blast_tac (claset() addDs [Confidentiality_B_refined, B_trusts_ServKey, 
  1156 by (ftac B_trusts_ServKey 6);
  1105                                Key_unique_SesKey]
  1157 by (etac exE 9);
  1106                         addIs [Says_Auth]) 1);
  1158 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
       
  1159                         addSIs [Says_Auth]) 9);
       
  1160 by (ALLGOALS assume_tac);
       
  1161 qed "A_Authenticity_refined";
  1107 qed "A_Authenticity_refined";
  1162 
  1108 
  1163 
  1109 
  1164 (*A checks authenticity of B: theorem "B_authenticity"*)
  1110 (*A checks authenticity of B: theorem "B_authenticity"*)
  1165 
  1111 
  1175 by (etac kerberos.induct 1);
  1121 by (etac kerberos.induct 1);
  1176 by (ftac Says_ticket_in_parts_spies 5);
  1122 by (ftac Says_ticket_in_parts_spies 5);
  1177 by (ftac Says_ticket_in_parts_spies 7);
  1123 by (ftac Says_ticket_in_parts_spies 7);
  1178 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1124 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1179 by (ALLGOALS Asm_simp_tac);
  1125 by (ALLGOALS Asm_simp_tac);
  1180 by (Fake_parts_insert_tac 1);
  1126 by (Blast_tac 1);
  1181 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1127 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1182 by (Clarify_tac 1);
  1128 by (Clarify_tac 1);
  1183 by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
  1129 by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
  1184 by (Clarify_tac 1);  (*PROOF FAILED if omitted*)
  1130 by (Clarify_tac 1);  (*PROOF FAILED if omitted*)
  1185 by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1);
  1131 by (blast_tac (claset() addDs [unique_CryptKey]) 1);
  1186 qed "Says_K6";
  1132 qed "Says_K6";
  1187 
  1133 
  1188 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|}   \
  1134 Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|}   \
  1189 \          \\<in> parts (spies evs);    \
  1135 \          \\<in> parts (spies evs);    \
  1190 \        Key AuthKey \\<notin> analz (spies evs); AuthKey \\<notin> range shrK;  \
  1136 \        Key AuthKey \\<notin> analz (spies evs); AuthKey \\<notin> range shrK;  \
  1192 \ ==> \\<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})\
  1138 \ ==> \\<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})\
  1193 \             \\<in> set evs";
  1139 \             \\<in> set evs";
  1194 by (etac rev_mp 1);
  1140 by (etac rev_mp 1);
  1195 by (etac rev_mp 1);
  1141 by (etac rev_mp 1);
  1196 by (parts_induct_tac 1);
  1142 by (parts_induct_tac 1);
  1197 by (Fake_parts_insert_tac 1);
  1143 by (Blast_tac 1);
  1198 by (Blast_tac 1);
  1144 by (Blast_tac 1);
  1199 by (Blast_tac 1);
  1145 by (Blast_tac 1);
  1200 qed "K4_trustworthy";
  1146 qed "K4_trustworthy";
  1201 
  1147 
  1202 Goal "[| Crypt ServKey (Number Ta) \\<in> parts (spies evs);           \
  1148 Goal "[| Crypt ServKey (Number Ta) \\<in> parts (spies evs);           \
  1212 by (ftac Confidentiality_Kas 4);
  1158 by (ftac Confidentiality_Kas 4);
  1213 by (ftac K4_trustworthy 7);
  1159 by (ftac K4_trustworthy 7);
  1214 by (Blast_tac 8);
  1160 by (Blast_tac 8);
  1215 by (etac exE 9);
  1161 by (etac exE 9);
  1216 by (ftac K4_imp_K2 9);
  1162 by (ftac K4_imp_K2 9);
  1217 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
  1163 (*Yes the proof's a mess, but I don't know how to improve it.*)
       
  1164 by (blast_tac (claset() addDs [Key_unique_SesKey]
  1218                         addSIs [Says_K6]
  1165                         addSIs [Says_K6]
  1219                         addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10);
  1166                         addDs [Confidentiality_Tgs1]) 10);
  1220 by (ALLGOALS assume_tac);
  1167 by (ALLGOALS assume_tac);
  1221 qed "B_Authenticity";
  1168 qed "B_Authenticity";
  1222 
  1169 
  1223 
  1170 
  1224 (***3. Parties' knowledge of session keys. A knows a session key if she
  1171 (***3. Parties' knowledge of session keys. A knows a session key if she
  1238 by (etac kerberos.induct 1);
  1185 by (etac kerberos.induct 1);
  1239 by (ftac Says_ticket_in_parts_spies 5);
  1186 by (ftac Says_ticket_in_parts_spies 5);
  1240 by (ftac Says_ticket_in_parts_spies 7);
  1187 by (ftac Says_ticket_in_parts_spies 7);
  1241 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1188 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
  1242 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1189 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
  1243 by (Fake_parts_insert_tac 1);
  1190 by (Blast_tac 1);
  1244 (*K6 requires numerous lemmas*)
  1191 (*K6 requires numerous lemmas*)
  1245 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1192 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1246 by (blast_tac (claset() addDs [B_trusts_ServTicket,
  1193 by (blast_tac (claset() addDs [B_trusts_ServTicket,
  1247                                impOfSubs parts_spies_takeWhile_mono,
  1194                                impOfSubs parts_spies_takeWhile_mono,
  1248                                impOfSubs parts_spies_evs_revD2]
  1195                                impOfSubs parts_spies_evs_revD2]
  1249                         addIs [Says_K6]
  1196                         addIs [Says_K6]) 1);
  1250                         addEs spies_partsEs) 1);
       
  1251 qed "B_Knows_B_Knows_ServKey_lemma";
  1197 qed "B_Knows_B_Knows_ServKey_lemma";
  1252 (*Key ServKey \\<notin> analz (spies evs) could be relaxed by Confidentiality_B
  1198 (*Key ServKey \\<notin> analz (spies evs) could be relaxed by Confidentiality_B
  1253   but this is irrelevant because B knows what he knows!                  *)
  1199   but this is irrelevant because B knows what he knows!                  *)
  1254 
  1200 
  1255 Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set evs;           \
  1201 Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set evs;           \
  1296 \     ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) \
  1242 \     ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) \
  1297 \                     {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
  1243 \                     {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
  1298 \                  \\<in> set evs";
  1244 \                  \\<in> set evs";
  1299 by (etac rev_mp 1);
  1245 by (etac rev_mp 1);
  1300 by (parts_induct_tac 1);
  1246 by (parts_induct_tac 1);
  1301 by (Fake_parts_insert_tac 1);
  1247 by (Blast_tac 1);
  1302 by (Blast_tac 1);
  1248 by (Blast_tac 1);
  1303 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 
  1249 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 
  1304 			       A_trusts_AuthKey]) 1);
  1250 			       A_trusts_AuthKey]) 1);
  1305 qed "K3_imp_K2";
  1251 qed "K3_imp_K2";
  1306 
  1252 
  1316 \        \\<in> set evs";      
  1262 \        \\<in> set evs";      
  1317 by (etac rev_mp 1);
  1263 by (etac rev_mp 1);
  1318 by (etac rev_mp 1);
  1264 by (etac rev_mp 1);
  1319 by (etac rev_mp 1);
  1265 by (etac rev_mp 1);
  1320 by (parts_induct_tac 1);
  1266 by (parts_induct_tac 1);
  1321 by (Fake_parts_insert_tac 1);
  1267 by (Blast_tac 1);
  1322 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1268 by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
  1323 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1269 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  1324                                A_trusts_AuthTicket, unique_AuthKeys]) 1);
  1270                                A_trusts_AuthTicket, unique_AuthKeys]) 1);
  1325 qed "K4_trustworthy'";
  1271 qed "K4_trustworthy'";
  1326 
  1272 
  1345 (*K6*)
  1291 (*K6*)
  1346 by Auto_tac;
  1292 by Auto_tac;
  1347 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1293 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1348 (*Level 15: case study necessary because the assumption doesn't state
  1294 (*Level 15: case study necessary because the assumption doesn't state
  1349   the form of ServTicket. The guarantee becomes stronger.*)
  1295   the form of ServTicket. The guarantee becomes stronger.*)
  1350 by (case_tac "Key AuthKey \\<in> analz (spies evs5)" 1);
  1296 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz_Decrypt',
  1351 by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
  1297                                K3_imp_K2, K4_trustworthy',
  1352 			       analz.Decrypt RS analz.Fst],
       
  1353 	       simpset()) 1);
       
  1354 by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy',
       
  1355                                impOfSubs parts_spies_takeWhile_mono,
  1298                                impOfSubs parts_spies_takeWhile_mono,
  1356                                impOfSubs parts_spies_evs_revD2]
  1299                                impOfSubs parts_spies_evs_revD2]
  1357                         addIs [Says_Auth] 
  1300                         addIs [Says_Auth]) 1);
  1358                         addEs spies_partsEs) 1);
       
  1359 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1301 by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
  1360 qed "A_Knows_A_Knows_ServKey_lemma";
  1302 qed "A_Knows_A_Knows_ServKey_lemma";
  1361 
  1303 
  1362 Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
  1304 Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
  1363 \          \\<in> set evs;       \
  1305 \          \\<in> set evs;       \