src/HOL/Auth/KerberosIV_Gets.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61830 4f5ab843cf5b
child 67443 3abf6a722518
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/Auth/KerberosIV_Gets.thy
     2     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     3     Copyright   1998  University of Cambridge
     4 *)
     5 
     6 section\<open>The Kerberos Protocol, Version IV\<close>
     7 
     8 theory KerberosIV_Gets imports Public begin
     9 
    10 text\<open>The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.\<close>
    11 
    12 abbreviation
    13   Kas :: agent where "Kas == Server"
    14 
    15 abbreviation
    16   Tgs :: agent where "Tgs == Friend 0"
    17 
    18 
    19 axiomatization where
    20   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    21    \<comment>\<open>Tgs is secure --- we already know that Kas is secure\<close>
    22 
    23 definition
    24  (* authKeys are those contained in an authTicket *)
    25     authKeys :: "event list => key set" where
    26     "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A
    27                         (Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
    28                (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
    29                   \<rbrace>) \<in> set evs}"
    30 
    31 definition
    32  (* States than an event really appears only once on a trace *)
    33   Unique :: "[event, event list] => bool" ("Unique _ on _" [0, 50] 50)
    34   where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
    35 
    36 
    37 consts
    38     (*Duration of the authentication key*)
    39     authKlife   :: nat
    40 
    41     (*Duration of the service key*)
    42     servKlife   :: nat
    43 
    44     (*Duration of an authenticator*)
    45     authlife   :: nat
    46 
    47     (*Upper bound on the time of reaction of a server*)
    48     replylife   :: nat
    49 
    50 specification (authKlife)
    51   authKlife_LB [iff]: "2 \<le> authKlife"
    52     by blast
    53 
    54 specification (servKlife)
    55   servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
    56     by blast
    57 
    58 specification (authlife)
    59   authlife_LB [iff]: "Suc 0 \<le> authlife"
    60     by blast
    61 
    62 specification (replylife)
    63   replylife_LB [iff]: "Suc 0 \<le> replylife"
    64     by blast
    65 
    66 abbreviation
    67   (*The current time is just the length of the trace!*)
    68   CT :: "event list=>nat" where
    69   "CT == length"
    70 
    71 abbreviation
    72   expiredAK :: "[nat, event list] => bool" where
    73   "expiredAK Ta evs == authKlife + Ta < CT evs"
    74 
    75 abbreviation
    76   expiredSK :: "[nat, event list] => bool" where
    77   "expiredSK Ts evs == servKlife + Ts < CT evs"
    78 
    79 abbreviation
    80   expiredA :: "[nat, event list] => bool" where
    81   "expiredA T evs == authlife + T < CT evs"
    82 
    83 abbreviation
    84   valid :: "[nat, nat] => bool" ("valid _ wrt _" [0, 50] 50) where
    85   "valid T1 wrt T2 == T1 <= replylife + T2"
    86 
    87 (*---------------------------------------------------------------------*)
    88 
    89 
    90 (* Predicate formalising the association between authKeys and servKeys *)
    91 definition AKcryptSK :: "[key, key, event list] => bool" where
    92   "AKcryptSK authK servK evs ==
    93      \<exists>A B Ts.
    94        Says Tgs A (Crypt authK
    95                      \<lbrace>Key servK, Agent B, Number Ts,
    96                        Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
    97          \<in> set evs"
    98 
    99 inductive_set "kerbIV_gets" :: "event list set"
   100   where
   101 
   102    Nil:  "[] \<in> kerbIV_gets"
   103 
   104  | Fake: "\<lbrakk> evsf \<in> kerbIV_gets;  X \<in> synth (analz (spies evsf)) \<rbrakk>
   105           \<Longrightarrow> Says Spy B X  # evsf \<in> kerbIV_gets"
   106 
   107  | Reception: "\<lbrakk> evsr \<in> kerbIV_gets;  Says A B X \<in> set evsr \<rbrakk>
   108                 \<Longrightarrow> Gets B X # evsr \<in> kerbIV_gets"
   109 
   110 (* FROM the initiator *)
   111  | K1:   "\<lbrakk> evs1 \<in> kerbIV_gets \<rbrakk>
   112           \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
   113           \<in> kerbIV_gets"
   114 
   115 (* Adding the timestamp serves to A in K3 to check that
   116    she doesn't get a reply too late. This kind of timeouts are ordinary.
   117    If a server's reply is late, then it is likely to be fake. *)
   118 
   119 (*---------------------------------------------------------------------*)
   120 
   121 (*FROM Kas *)
   122  | K2:  "\<lbrakk> evs2 \<in> kerbIV_gets; Key authK \<notin> used evs2; authK \<in> symKeys;
   123             Gets Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
   124           \<Longrightarrow> Says Kas A
   125                 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2),
   126                       (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
   127                           Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV_gets"
   128 (*
   129   The internal encryption builds the authTicket.
   130   The timestamp doesn't change inside the two encryptions: the external copy
   131   will be used by the initiator in K3; the one inside the
   132   authTicket by Tgs in K4.
   133 *)
   134 
   135 (*---------------------------------------------------------------------*)
   136 
   137 (* FROM the initiator *)
   138  | K3:  "\<lbrakk> evs3 \<in> kerbIV_gets;
   139             Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
   140             Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   141               authTicket\<rbrace>) \<in> set evs3;
   142             valid Ta wrt T1
   143          \<rbrakk>
   144           \<Longrightarrow> Says A Tgs \<lbrace>authTicket,
   145                            (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
   146                            Agent B\<rbrace> # evs3 \<in> kerbIV_gets"
   147 (*The two events amongst the premises allow A to accept only those authKeys
   148   that are not issued late. *)
   149 
   150 (*---------------------------------------------------------------------*)
   151 
   152 (* FROM Tgs *)
   153 (* Note that the last temporal check is not mentioned in the original MIT
   154    specification. Adding it makes many goals "available" to the peers. 
   155    Theorems that exploit it have the suffix `_u', which stands for updated 
   156    protocol.
   157 *)
   158  | K4:  "\<lbrakk> evs4 \<in> kerbIV_gets; Key servK \<notin> used evs4; servK \<in> symKeys;
   159             B \<noteq> Tgs;  authK \<in> symKeys;
   160             Gets Tgs \<lbrace>
   161              (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
   162                                  Number Ta\<rbrace>),
   163              (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
   164                 \<in> set evs4;
   165             \<not> expiredAK Ta evs4;
   166             \<not> expiredA T2 evs4;
   167             servKlife + (CT evs4) <= authKlife + Ta
   168          \<rbrakk>
   169           \<Longrightarrow> Says Tgs A
   170                 (Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4),
   171                                Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK,
   172                                                 Number (CT evs4)\<rbrace> \<rbrace>)
   173                 # evs4 \<in> kerbIV_gets"
   174 (* Tgs creates a new session key per each request for a service, without
   175    checking if there is still a fresh one for that service.
   176    The cipher under Tgs' key is the authTicket, the cipher under B's key
   177    is the servTicket, which is built now.
   178    NOTE that the last temporal check is not present in the MIT specification.
   179 
   180 *)
   181 
   182 (*---------------------------------------------------------------------*)
   183 
   184 (* FROM the initiator *)
   185  | K5:  "\<lbrakk> evs5 \<in> kerbIV_gets; authK \<in> symKeys; servK \<in> symKeys;
   186             Says A Tgs
   187                 \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
   188                   Agent B\<rbrace>
   189               \<in> set evs5;
   190             Gets A
   191              (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   192                 \<in> set evs5;
   193             valid Ts wrt T2 \<rbrakk>
   194           \<Longrightarrow> Says A B \<lbrace>servTicket,
   195                          Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
   196                # evs5 \<in> kerbIV_gets"
   197 (* Checks similar to those in K3. *)
   198 
   199 (*---------------------------------------------------------------------*)
   200 
   201 (* FROM the responder*)
   202   | K6:  "\<lbrakk> evs6 \<in> kerbIV_gets;
   203             Gets B \<lbrace>
   204               (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
   205               (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
   206             \<in> set evs6;
   207             \<not> expiredSK Ts evs6;
   208             \<not> expiredA T3 evs6
   209          \<rbrakk>
   210           \<Longrightarrow> Says B A (Crypt servK (Number T3))
   211                # evs6 \<in> kerbIV_gets"
   212 (* Checks similar to those in K4. *)
   213 
   214 (*---------------------------------------------------------------------*)
   215 
   216 (* Leaking an authK... *)
   217  | Oops1: "\<lbrakk> evsO1 \<in> kerbIV_gets;  A \<noteq> Spy;
   218               Says Kas A
   219                 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   220                                   authTicket\<rbrace>)  \<in> set evsO1;
   221               expiredAK Ta evsO1 \<rbrakk>
   222           \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
   223                # evsO1 \<in> kerbIV_gets"
   224 
   225 (*---------------------------------------------------------------------*)
   226 
   227 (*Leaking a servK... *)
   228  | Oops2: "\<lbrakk> evsO2 \<in> kerbIV_gets;  A \<noteq> Spy;
   229               Says Tgs A
   230                 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   231                    \<in> set evsO2;
   232               expiredSK Ts evsO2 \<rbrakk>
   233           \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
   234                # evsO2 \<in> kerbIV_gets"
   235 
   236 (*---------------------------------------------------------------------*)
   237 
   238 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   239 declare parts.Body [dest]
   240 declare analz_into_parts [dest]
   241 declare Fake_parts_insert_in_Un [dest]
   242 
   243 subsection\<open>Lemmas about reception event\<close>
   244 
   245 lemma Gets_imp_Says :
   246      "\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
   247 apply (erule rev_mp)
   248 apply (erule kerbIV_gets.induct)
   249 apply auto
   250 done
   251 
   252 lemma Gets_imp_knows_Spy: 
   253      "\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
   254 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   255 
   256 (*Needed for force to work for example in new_keys_not_used*)
   257 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   258 
   259 lemma Gets_imp_knows:
   260      "\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
   261 by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
   262 
   263 subsection\<open>Lemmas about @{term authKeys}\<close>
   264 
   265 lemma authKeys_empty: "authKeys [] = {}"
   266 by (simp add: authKeys_def)
   267 
   268 lemma authKeys_not_insert:
   269  "(\<forall>A Ta akey Peer.
   270    ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
   271               (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
   272        \<Longrightarrow> authKeys (ev # evs) = authKeys evs"
   273 by (unfold authKeys_def, auto)
   274 
   275 lemma authKeys_insert:
   276   "authKeys
   277      (Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
   278       (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
   279        = insert K (authKeys evs)"
   280 by (unfold authKeys_def, auto)
   281 
   282 lemma authKeys_simp:
   283    "K \<in> authKeys
   284     (Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
   285      (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
   286         \<Longrightarrow> K = K' | K \<in> authKeys evs"
   287 by (unfold authKeys_def, auto)
   288 
   289 lemma authKeysI:
   290    "Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
   291      (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
   292         \<Longrightarrow> K \<in> authKeys evs"
   293 by (unfold authKeys_def, auto)
   294 
   295 lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
   296 by (simp add: authKeys_def, blast)
   297 
   298 
   299 subsection\<open>Forwarding Lemmas\<close>
   300 
   301 lemma Says_ticket_parts:
   302      "Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
   303       \<Longrightarrow> Ticket \<in> parts (spies evs)"
   304 by blast
   305 
   306 lemma Gets_ticket_parts:
   307      "\<lbrakk>Gets A (Crypt K \<lbrace>SesKey, Peer, Ta, Ticket\<rbrace>) \<in> set evs; evs \<in> kerbIV_gets \<rbrakk>
   308       \<Longrightarrow> Ticket \<in> parts (spies evs)"
   309 by (blast dest: Gets_imp_knows_Spy [THEN parts.Inj])
   310 
   311 lemma Oops_range_spies1:
   312      "\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
   313            \<in> set evs ;
   314          evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
   315 apply (erule rev_mp)
   316 apply (erule kerbIV_gets.induct, auto)
   317 done
   318 
   319 lemma Oops_range_spies2:
   320      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
   321            \<in> set evs ;
   322          evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys"
   323 apply (erule rev_mp)
   324 apply (erule kerbIV_gets.induct, auto)
   325 done
   326 
   327 
   328 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
   329 lemma Spy_see_shrK [simp]:
   330      "evs \<in> kerbIV_gets \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   331 apply (erule kerbIV_gets.induct)
   332 apply (frule_tac [8] Gets_ticket_parts)
   333 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   334 apply (blast+)
   335 done
   336 
   337 lemma Spy_analz_shrK [simp]:
   338      "evs \<in> kerbIV_gets \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   339 by auto
   340 
   341 lemma Spy_see_shrK_D [dest!]:
   342      "\<lbrakk> Key (shrK A) \<in> parts (spies evs);  evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A:bad"
   343 by (blast dest: Spy_see_shrK)
   344 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
   345 
   346 text\<open>Nobody can have used non-existent keys!\<close>
   347 lemma new_keys_not_used [simp]:
   348     "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV_gets\<rbrakk>
   349      \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
   350 apply (erule rev_mp)
   351 apply (erule kerbIV_gets.induct)
   352 apply (frule_tac [8] Gets_ticket_parts)
   353 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   354 txt\<open>Fake\<close>
   355 apply (force dest!: keysFor_parts_insert)
   356 txt\<open>Others\<close>
   357 apply (force dest!: analz_shrK_Decrypt)+
   358 done
   359 
   360 (*Earlier, all protocol proofs declared this theorem.
   361   But few of them actually need it! (Another is Yahalom) *)
   362 lemma new_keys_not_analzd:
   363  "\<lbrakk>evs \<in> kerbIV_gets; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
   364   \<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
   365 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
   366 
   367 
   368 subsection\<open>Regularity Lemmas\<close>
   369 text\<open>These concern the form of items passed in messages\<close>
   370 
   371 text\<open>Describes the form of all components sent by Kas\<close>
   372 
   373 lemma Says_Kas_message_form:
   374      "\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
   375            \<in> set evs;
   376          evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow>  
   377   K = shrK A  & Peer = Tgs &
   378   authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys & 
   379   authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>)"
   380 apply (erule rev_mp)
   381 apply (erule kerbIV_gets.induct)
   382 apply (simp_all (no_asm) add: authKeys_def authKeys_insert)
   383 apply blast+
   384 done
   385 
   386 
   387 lemma SesKey_is_session_key:
   388      "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
   389             \<in> parts (spies evs); Tgs_B \<notin> bad;
   390          evs \<in> kerbIV_gets \<rbrakk>
   391       \<Longrightarrow> SesKey \<notin> range shrK"
   392 apply (erule rev_mp)
   393 apply (erule kerbIV_gets.induct)
   394 apply (frule_tac [8] Gets_ticket_parts)
   395 apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
   396 done
   397 
   398 lemma authTicket_authentic:
   399      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
   400            \<in> parts (spies evs);
   401          evs \<in> kerbIV_gets \<rbrakk>
   402       \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   403                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   404             \<in> set evs"
   405 apply (erule rev_mp)
   406 apply (erule kerbIV_gets.induct)
   407 apply (frule_tac [8] Gets_ticket_parts)
   408 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   409 txt\<open>Fake, K4\<close>
   410 apply (blast+)
   411 done
   412 
   413 lemma authTicket_crypt_authK:
   414      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
   415            \<in> parts (spies evs);
   416          evs \<in> kerbIV_gets \<rbrakk>
   417       \<Longrightarrow> authK \<in> authKeys evs"
   418 apply (frule authTicket_authentic, assumption)
   419 apply (simp (no_asm) add: authKeys_def)
   420 apply blast
   421 done
   422 
   423 lemma Says_Tgs_message_form:
   424      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   425            \<in> set evs;
   426          evs \<in> kerbIV_gets \<rbrakk>
   427   \<Longrightarrow> B \<noteq> Tgs & 
   428       authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
   429       servK \<notin> range shrK & servK \<notin> authKeys evs & servK \<in> symKeys &
   430       servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>)"
   431 apply (erule rev_mp)
   432 apply (erule kerbIV_gets.induct)
   433 apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast, auto)
   434 txt\<open>Three subcases of Message 4\<close>
   435 apply (blast dest!: SesKey_is_session_key)
   436 apply (blast dest: authTicket_crypt_authK)
   437 apply (blast dest!: authKeys_used Says_Kas_message_form)
   438 done
   439 
   440 
   441 lemma authTicket_form:
   442      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>
   443            \<in> parts (spies evs);
   444          A \<notin> bad;
   445          evs \<in> kerbIV_gets \<rbrakk>
   446     \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys & 
   447         authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>"
   448 apply (erule rev_mp)
   449 apply (erule kerbIV_gets.induct)
   450 apply (frule_tac [8] Gets_ticket_parts)
   451 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   452 apply blast+
   453 done
   454 
   455 text\<open>This form holds also over an authTicket, but is not needed below.\<close>
   456 lemma servTicket_form:
   457      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>
   458               \<in> parts (spies evs);
   459             Key authK \<notin> analz (spies evs);
   460             evs \<in> kerbIV_gets \<rbrakk>
   461          \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys & 
   462     (\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)"
   463 apply (erule rev_mp)
   464 apply (erule rev_mp)
   465 apply (erule kerbIV_gets.induct, analz_mono_contra)
   466 apply (frule_tac [8] Gets_ticket_parts)
   467 apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
   468 done
   469 
   470 text\<open>Essentially the same as \<open>authTicket_form\<close>\<close>
   471 lemma Says_kas_message_form:
   472      "\<lbrakk> Gets A (Crypt (shrK A)
   473               \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
   474          evs \<in> kerbIV_gets \<rbrakk>
   475       \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys & 
   476           authTicket =
   477                   Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
   478           | authTicket \<in> analz (spies evs)"
   479 by (blast dest: analz_shrK_Decrypt authTicket_form
   480                 Gets_imp_knows_Spy [THEN analz.Inj])
   481 
   482 lemma Says_tgs_message_form:
   483  "\<lbrakk> Gets A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
   484        \<in> set evs;  authK \<in> symKeys;
   485      evs \<in> kerbIV_gets \<rbrakk>
   486   \<Longrightarrow> servK \<notin> range shrK &
   487       (\<exists>A. servTicket =
   488               Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)
   489        | servTicket \<in> analz (spies evs)"
   490 apply (frule Gets_imp_knows_Spy [THEN analz.Inj], auto)
   491  apply (force dest!: servTicket_form)
   492 apply (frule analz_into_parts)
   493 apply (frule servTicket_form, auto)
   494 done
   495 
   496 
   497 subsection\<open>Authenticity theorems: confirm origin of sensitive messages\<close>
   498 
   499 lemma authK_authentic:
   500      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>
   501            \<in> parts (spies evs);
   502          A \<notin> bad;  evs \<in> kerbIV_gets \<rbrakk>
   503       \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
   504             \<in> set evs"
   505 apply (erule rev_mp)
   506 apply (erule kerbIV_gets.induct)
   507 apply (frule_tac [8] Gets_ticket_parts)
   508 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   509 txt\<open>Fake\<close>
   510 apply blast
   511 txt\<open>K4\<close>
   512 apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
   513 done
   514 
   515 text\<open>If a certain encrypted message appears then it originated with Tgs\<close>
   516 lemma servK_authentic:
   517      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
   518            \<in> parts (spies evs);
   519          Key authK \<notin> analz (spies evs);
   520          authK \<notin> range shrK;
   521          evs \<in> kerbIV_gets \<rbrakk>
   522  \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   523        \<in> set evs"
   524 apply (erule rev_mp)
   525 apply (erule rev_mp)
   526 apply (erule kerbIV_gets.induct, analz_mono_contra)
   527 apply (frule_tac [8] Gets_ticket_parts)
   528 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   529 txt\<open>Fake\<close>
   530 apply blast
   531 txt\<open>K2\<close>
   532 apply blast
   533 txt\<open>K4\<close>
   534 apply auto
   535 done
   536 
   537 lemma servK_authentic_bis:
   538      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
   539            \<in> parts (spies evs);
   540          Key authK \<notin> analz (spies evs);
   541          B \<noteq> Tgs;
   542          evs \<in> kerbIV_gets \<rbrakk>
   543  \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   544        \<in> set evs"
   545 apply (erule rev_mp)
   546 apply (erule rev_mp)
   547 apply (erule kerbIV_gets.induct, analz_mono_contra)
   548 apply (frule_tac [8] Gets_ticket_parts)
   549 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   550 txt\<open>Fake\<close>
   551 apply blast
   552 txt\<open>K4\<close>
   553 apply blast
   554 done
   555 
   556 text\<open>Authenticity of servK for B\<close>
   557 lemma servTicket_authentic_Tgs:
   558      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   559            \<in> parts (spies evs); B \<noteq> Tgs;  B \<notin> bad;
   560          evs \<in> kerbIV_gets \<rbrakk>
   561  \<Longrightarrow> \<exists>authK.
   562        Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   563                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
   564        \<in> set evs"
   565 apply (erule rev_mp)
   566 apply (erule rev_mp)
   567 apply (erule kerbIV_gets.induct)
   568 apply (frule_tac [8] Gets_ticket_parts)
   569 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   570 apply blast+
   571 done
   572 
   573 text\<open>Anticipated here from next subsection\<close>
   574 lemma K4_imp_K2:
   575 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   576       \<in> set evs;  evs \<in> kerbIV_gets\<rbrakk>
   577    \<Longrightarrow> \<exists>Ta. Says Kas A
   578         (Crypt (shrK A)
   579          \<lbrace>Key authK, Agent Tgs, Number Ta,
   580            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   581         \<in> set evs"
   582 apply (erule rev_mp)
   583 apply (erule kerbIV_gets.induct)
   584 apply (frule_tac [8] Gets_ticket_parts)
   585 apply (frule_tac [6] Gets_ticket_parts, simp_all, auto)
   586 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
   587 done
   588 
   589 text\<open>Anticipated here from next subsection\<close>
   590 lemma u_K4_imp_K2:
   591 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   592       \<in> set evs; evs \<in> kerbIV_gets\<rbrakk>
   593    \<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   594            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   595              \<in> set evs
   596           & servKlife + Ts <= authKlife + Ta)"
   597 apply (erule rev_mp)
   598 apply (erule kerbIV_gets.induct)
   599 apply (frule_tac [8] Gets_ticket_parts)
   600 apply (frule_tac [6] Gets_ticket_parts, simp_all, auto)
   601 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
   602 done
   603 
   604 lemma servTicket_authentic_Kas:
   605      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   606            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   607          evs \<in> kerbIV_gets \<rbrakk>
   608   \<Longrightarrow> \<exists>authK Ta.
   609        Says Kas A
   610          (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   611             Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   612         \<in> set evs"
   613 by (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
   614 
   615 lemma u_servTicket_authentic_Kas:
   616      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   617            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   618          evs \<in> kerbIV_gets \<rbrakk>
   619   \<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   620            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   621              \<in> set evs
   622            & servKlife + Ts <= authKlife + Ta"
   623 by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
   624 
   625 lemma servTicket_authentic:
   626      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   627            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   628          evs \<in> kerbIV_gets \<rbrakk>
   629  \<Longrightarrow> \<exists>Ta authK.
   630      Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   631                    Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   632        \<in> set evs
   633      & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   634                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
   635        \<in> set evs"
   636 by (blast dest: servTicket_authentic_Tgs K4_imp_K2)
   637 
   638 lemma u_servTicket_authentic:
   639      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   640            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   641          evs \<in> kerbIV_gets \<rbrakk>
   642  \<Longrightarrow> \<exists>Ta authK.
   643      (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   644                    Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   645        \<in> set evs
   646      & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   647                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
   648        \<in> set evs
   649      & servKlife + Ts <= authKlife + Ta)"
   650 by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
   651 
   652 lemma u_NotexpiredSK_NotexpiredAK:
   653      "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
   654       \<Longrightarrow> \<not> expiredAK Ta evs"
   655 by (blast dest: leI le_trans dest: leD)
   656 
   657 
   658 subsection\<open>Reliability: friendly agents send something if something else happened\<close>
   659 
   660 lemma K3_imp_K2:
   661      "\<lbrakk> Says A Tgs
   662              \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
   663            \<in> set evs;
   664          A \<notin> bad;  evs \<in> kerbIV_gets \<rbrakk>
   665       \<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A)
   666                       \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
   667                    \<in> set evs"
   668 apply (erule rev_mp)
   669 apply (erule kerbIV_gets.induct)
   670 apply (frule_tac [8] Gets_ticket_parts)
   671 apply (frule_tac [6] Gets_ticket_parts, simp_all, blast, blast)
   672 apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic])
   673 done
   674 
   675 text\<open>Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.\<close>
   676 lemma Key_unique_SesKey:
   677      "\<lbrakk> Crypt K  \<lbrace>Key SesKey,  Agent B, T, Ticket\<rbrace>
   678            \<in> parts (spies evs);
   679          Crypt K' \<lbrace>Key SesKey,  Agent B', T', Ticket'\<rbrace>
   680            \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
   681          evs \<in> kerbIV_gets \<rbrakk>
   682       \<Longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket'"
   683 apply (erule rev_mp)
   684 apply (erule rev_mp)
   685 apply (erule rev_mp)
   686 apply (erule kerbIV_gets.induct, analz_mono_contra)
   687 apply (frule_tac [8] Gets_ticket_parts)
   688 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   689 txt\<open>Fake, K2, K4\<close>
   690 apply (blast+)
   691 done
   692 
   693 lemma Tgs_authenticates_A:
   694   "\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 
   695       Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
   696            \<in> parts (spies evs);
   697       Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
   698  \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
   699           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
   700           Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs"  
   701 apply (drule authTicket_authentic, assumption, rotate_tac 4)
   702 apply (erule rev_mp, erule rev_mp, erule rev_mp)
   703 apply (erule kerbIV_gets.induct, analz_mono_contra)
   704 apply (frule_tac [6] Gets_ticket_parts)
   705 apply (frule_tac [9] Gets_ticket_parts)
   706 apply (simp_all (no_asm_simp) add: all_conj_distrib)
   707 txt\<open>Fake\<close>
   708 apply blast
   709 txt\<open>K2\<close>
   710 apply (force dest!: Crypt_imp_keysFor)
   711 txt\<open>K3\<close>
   712 apply (blast dest: Key_unique_SesKey)
   713 txt\<open>K5\<close>
   714 txt\<open>If authKa were compromised, so would be authK\<close>
   715 apply (case_tac "Key authKa \<in> analz (spies evs5)")
   716 apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
   717 txt\<open>Besides, since authKa originated with Kas anyway...\<close>
   718 apply (clarify, drule K3_imp_K2, assumption, assumption)
   719 apply (clarify, drule Says_Kas_message_form, assumption)
   720 txt\<open>...it cannot be a shared key*. Therefore @{term servK_authentic} applies. 
   721      Contradition: Tgs used authK as a servkey, 
   722      while Kas used it as an authkey\<close>
   723 apply (blast dest: servK_authentic Says_Tgs_message_form)
   724 done
   725 
   726 lemma Says_K5:
   727      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
   728          Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   729                                      servTicket\<rbrace>) \<in> set evs;
   730          Key servK \<notin> analz (spies evs);
   731          A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
   732  \<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
   733 apply (erule rev_mp)
   734 apply (erule rev_mp)
   735 apply (erule rev_mp)
   736 apply (erule kerbIV_gets.induct, analz_mono_contra)
   737 apply (frule_tac [6] Gets_ticket_parts)
   738 apply (frule_tac [9] Gets_ticket_parts)
   739 apply (simp_all (no_asm_simp) add: all_conj_distrib)
   740 apply blast
   741 txt\<open>K3\<close>
   742 apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
   743 txt\<open>K4\<close>
   744 apply (force dest!: Crypt_imp_keysFor)
   745 txt\<open>K5\<close>
   746 apply (blast dest: Key_unique_SesKey)
   747 done
   748 
   749 text\<open>Anticipated here from next subsection\<close>
   750 lemma unique_CryptKey:
   751      "\<lbrakk> Crypt (shrK B)  \<lbrace>Agent A,  Agent B,  Key SesKey, T\<rbrace>
   752            \<in> parts (spies evs);
   753          Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
   754            \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
   755          evs \<in> kerbIV_gets \<rbrakk>
   756       \<Longrightarrow> A=A' & B=B' & T=T'"
   757 apply (erule rev_mp)
   758 apply (erule rev_mp)
   759 apply (erule rev_mp)
   760 apply (erule kerbIV_gets.induct, analz_mono_contra)
   761 apply (frule_tac [8] Gets_ticket_parts)
   762 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   763 txt\<open>Fake, K2, K4\<close>
   764 apply (blast+)
   765 done
   766 
   767 lemma Says_K6:
   768      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
   769          Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   770                                      servTicket\<rbrace>) \<in> set evs;
   771          Key servK \<notin> analz (spies evs);
   772          A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
   773       \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
   774 apply (erule rev_mp)
   775 apply (erule rev_mp)
   776 apply (erule rev_mp)
   777 apply (erule kerbIV_gets.induct, analz_mono_contra)
   778 apply (frule_tac [8] Gets_ticket_parts)
   779 apply (frule_tac [6] Gets_ticket_parts)
   780 apply (simp_all (no_asm_simp))
   781 apply blast
   782 apply (force dest!: Crypt_imp_keysFor, clarify)
   783 apply (frule Says_Tgs_message_form, assumption, clarify) (*PROOF FAILED if omitted*)
   784 apply (blast dest: unique_CryptKey)
   785 done
   786 
   787 text\<open>Needs a unicity theorem, hence moved here\<close>
   788 lemma servK_authentic_ter:
   789  "\<lbrakk> Says Kas A
   790     (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
   791      Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
   792        \<in> parts (spies evs);
   793      Key authK \<notin> analz (spies evs);
   794      evs \<in> kerbIV_gets \<rbrakk>
   795  \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   796        \<in> set evs"
   797 apply (frule Says_Kas_message_form, assumption)
   798 apply (erule rev_mp)
   799 apply (erule rev_mp)
   800 apply (erule rev_mp)
   801 apply (erule kerbIV_gets.induct, analz_mono_contra)
   802 apply (frule_tac [8] Gets_ticket_parts)
   803 apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
   804 txt\<open>K2 and K4 remain\<close>
   805 prefer 2 apply (blast dest!: unique_CryptKey)
   806 apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
   807 done
   808 
   809 
   810 subsection\<open>Unicity Theorems\<close>
   811 
   812 text\<open>The session key, if secure, uniquely identifies the Ticket
   813    whether authTicket or servTicket. As a matter of fact, one can read
   814    also Tgs in the place of B.\<close>
   815 
   816 
   817 lemma unique_authKeys:
   818      "\<lbrakk> Says Kas A
   819               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs;
   820          Says Kas A'
   821               (Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs;
   822          evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A=A' & Ka=Ka' & Ta=Ta' & X=X'"
   823 apply (erule rev_mp)
   824 apply (erule rev_mp)
   825 apply (erule kerbIV_gets.induct)
   826 apply (frule_tac [8] Gets_ticket_parts)
   827 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   828 txt\<open>K2\<close>
   829 apply blast
   830 done
   831 
   832 text\<open>servK uniquely identifies the message from Tgs\<close>
   833 lemma unique_servKeys:
   834      "\<lbrakk> Says Tgs A
   835               (Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs;
   836          Says Tgs A'
   837               (Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs;
   838          evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A=A' & B=B' & K=K' & Ts=Ts' & X=X'"
   839 apply (erule rev_mp)
   840 apply (erule rev_mp)
   841 apply (erule kerbIV_gets.induct)
   842 apply (frule_tac [8] Gets_ticket_parts)
   843 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   844 txt\<open>K4\<close>
   845 apply blast
   846 done
   847 
   848 text\<open>Revised unicity theorems\<close>
   849 
   850 lemma Kas_Unique:
   851      "\<lbrakk> Says Kas A
   852               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
   853         evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> 
   854    Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>)) 
   855    on evs"
   856 apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def)
   857 apply blast
   858 done
   859 
   860 lemma Tgs_Unique:
   861      "\<lbrakk> Says Tgs A
   862               (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs;
   863         evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> 
   864   Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)) 
   865   on evs"
   866 apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def)
   867 apply blast
   868 done
   869 
   870 
   871 subsection\<open>Lemmas About the Predicate @{term AKcryptSK}\<close>
   872 
   873 lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
   874 by (simp add: AKcryptSK_def)
   875 
   876 lemma AKcryptSKI:
   877  "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
   878      evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
   879 apply (unfold AKcryptSK_def)
   880 apply (blast dest: Says_Tgs_message_form)
   881 done
   882 
   883 lemma AKcryptSK_Says [simp]:
   884    "AKcryptSK authK servK (Says S A X # evs) =
   885      (Tgs = S &
   886       (\<exists>B Ts. X = Crypt authK
   887                 \<lbrace>Key servK, Agent B, Number Ts,
   888                   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
   889      | AKcryptSK authK servK evs)"
   890 by (auto simp add: AKcryptSK_def)
   891 
   892 (*A fresh authK cannot be associated with any other
   893   (with respect to a given trace). *)
   894 lemma Auth_fresh_not_AKcryptSK:
   895      "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV_gets \<rbrakk>
   896       \<Longrightarrow> \<not> AKcryptSK authK servK evs"
   897 apply (unfold AKcryptSK_def)
   898 apply (erule rev_mp)
   899 apply (erule kerbIV_gets.induct)
   900 apply (frule_tac [8] Gets_ticket_parts)
   901 apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
   902 done
   903 
   904 (*A fresh servK cannot be associated with any other
   905   (with respect to a given trace). *)
   906 lemma Serv_fresh_not_AKcryptSK:
   907  "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
   908 by (unfold AKcryptSK_def, blast)
   909 
   910 lemma authK_not_AKcryptSK:
   911      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
   912            \<in> parts (spies evs);  evs \<in> kerbIV_gets \<rbrakk>
   913       \<Longrightarrow> \<not> AKcryptSK K authK evs"
   914 apply (erule rev_mp)
   915 apply (erule kerbIV_gets.induct)
   916 apply (frule_tac [8] Gets_ticket_parts)
   917 apply (frule_tac [6] Gets_ticket_parts, simp_all)
   918 txt\<open>Fake\<close>
   919 apply blast
   920 txt\<open>Reception\<close>
   921 apply (simp add: AKcryptSK_def)
   922 txt\<open>K2: by freshness\<close>
   923 apply (simp add: AKcryptSK_def)
   924 txt\<open>K4\<close>
   925 by (blast+)
   926 
   927 text\<open>A secure serverkey cannot have been used to encrypt others\<close>
   928 lemma servK_not_AKcryptSK:
   929  "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs);
   930      Key SK \<notin> analz (spies evs);  SK \<in> symKeys;
   931      B \<noteq> Tgs;  evs \<in> kerbIV_gets \<rbrakk>
   932   \<Longrightarrow> \<not> AKcryptSK SK K evs"
   933 apply (erule rev_mp)
   934 apply (erule rev_mp)
   935 apply (erule kerbIV_gets.induct, analz_mono_contra)
   936 apply (frule_tac [8] Gets_ticket_parts)
   937 apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
   938 txt\<open>Reception\<close>
   939 apply (simp add: AKcryptSK_def)
   940 txt\<open>K4 splits into distinct subcases\<close>
   941 apply auto
   942 txt\<open>servK can't have been enclosed in two certificates\<close>
   943  prefer 2 apply (blast dest: unique_CryptKey)
   944 txt\<open>servK is fresh and so could not have been used, by
   945    \<open>new_keys_not_used\<close>\<close>
   946 by (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
   947 
   948 text\<open>Long term keys are not issued as servKeys\<close>
   949 lemma shrK_not_AKcryptSK:
   950      "evs \<in> kerbIV_gets \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
   951 apply (unfold AKcryptSK_def)
   952 apply (erule kerbIV_gets.induct)
   953 apply (frule_tac [8] Gets_ticket_parts)
   954 by (frule_tac [6] Gets_ticket_parts, auto)
   955 
   956 text\<open>The Tgs message associates servK with authK and therefore not with any
   957   other key authK.\<close>
   958 lemma Says_Tgs_AKcryptSK:
   959      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>)
   960            \<in> set evs;
   961          authK' \<noteq> authK;  evs \<in> kerbIV_gets \<rbrakk>
   962       \<Longrightarrow> \<not> AKcryptSK authK' servK evs"
   963 apply (unfold AKcryptSK_def)
   964 by (blast dest: unique_servKeys)
   965 
   966 text\<open>Equivalently\<close>
   967 lemma not_different_AKcryptSK:
   968      "\<lbrakk> AKcryptSK authK servK evs;
   969         authK' \<noteq> authK;  evs \<in> kerbIV_gets \<rbrakk>
   970       \<Longrightarrow> \<not> AKcryptSK authK' servK evs  \<and> servK \<in> symKeys"
   971 apply (simp add: AKcryptSK_def)
   972 by (blast dest: unique_servKeys Says_Tgs_message_form)
   973 
   974 lemma AKcryptSK_not_AKcryptSK:
   975      "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbIV_gets \<rbrakk>
   976       \<Longrightarrow> \<not> AKcryptSK servK K evs"
   977 apply (erule rev_mp)
   978 apply (erule kerbIV_gets.induct)
   979 apply (frule_tac [8] Gets_ticket_parts)
   980 apply (frule_tac [6] Gets_ticket_parts)
   981 txt\<open>Reception\<close>
   982 prefer 3 apply (simp add: AKcryptSK_def)
   983 apply (simp_all, safe)
   984 txt\<open>K4 splits into subcases\<close>
   985 prefer 4 apply (blast dest!: authK_not_AKcryptSK)
   986 txt\<open>servK is fresh and so could not have been used, by
   987    \<open>new_keys_not_used\<close>\<close>
   988  prefer 2 
   989  apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
   990 txt\<open>Others by freshness\<close>
   991 by (blast+)
   992 
   993 text\<open>The only session keys that can be found with the help of session keys are
   994   those sent by Tgs in step K4.\<close>
   995 
   996 text\<open>We take some pains to express the property
   997   as a logical equivalence so that the simplifier can apply it.\<close>
   998 lemma Key_analz_image_Key_lemma:
   999      "P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
  1000       \<Longrightarrow>
  1001       P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
  1002 by (blast intro: analz_mono [THEN subsetD])
  1003 
  1004 
  1005 lemma AKcryptSK_analz_insert:
  1006      "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV_gets \<rbrakk>
  1007       \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
  1008 apply (simp add: AKcryptSK_def, clarify)
  1009 by (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
  1010 
  1011 lemma authKeys_are_not_AKcryptSK:
  1012      "\<lbrakk> K \<in> authKeys evs Un range shrK;  evs \<in> kerbIV_gets \<rbrakk>
  1013       \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
  1014 apply (simp add: authKeys_def AKcryptSK_def)
  1015 by (blast dest: Says_Kas_message_form Says_Tgs_message_form)
  1016 
  1017 lemma not_authKeys_not_AKcryptSK:
  1018      "\<lbrakk> K \<notin> authKeys evs;
  1019          K \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
  1020       \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
  1021 apply (simp add: AKcryptSK_def)
  1022 by (blast dest: Says_Tgs_message_form)
  1023 
  1024 
  1025 subsection\<open>Secrecy Theorems\<close>
  1026 
  1027 text\<open>For the Oops2 case of the next theorem\<close>
  1028 lemma Oops2_not_AKcryptSK:
  1029      "\<lbrakk> evs \<in> kerbIV_gets;
  1030          Says Tgs A (Crypt authK
  1031                      \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1032            \<in> set evs \<rbrakk>
  1033       \<Longrightarrow> \<not> AKcryptSK servK SK evs"
  1034 by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
  1035    
  1036 text\<open>Big simplification law for keys SK that are not crypted by keys in KK
  1037  It helps prove three, otherwise hard, facts about keys. These facts are
  1038  exploited as simplification laws for analz, and also "limit the damage"
  1039  in case of loss of a key to the spy. See ESORICS98.\<close>
  1040 lemma Key_analz_image_Key [rule_format (no_asm)]:
  1041      "evs \<in> kerbIV_gets \<Longrightarrow>
  1042       (\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
  1043        (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs)   \<longrightarrow>
  1044        (Key SK \<in> analz (Key`KK Un (spies evs))) =
  1045        (SK \<in> KK | Key SK \<in> analz (spies evs)))"
  1046 apply (erule kerbIV_gets.induct)
  1047 apply (frule_tac [11] Oops_range_spies2)
  1048 apply (frule_tac [10] Oops_range_spies1)
  1049 apply (frule_tac [8] Says_tgs_message_form)
  1050 apply (frule_tac [6] Says_kas_message_form)
  1051 apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
  1052 txt\<open>Case-splits for Oops1 and message 5: the negated case simplifies using
  1053  the induction hypothesis\<close>
  1054 apply (case_tac [12] "AKcryptSK authK SK evsO1")
  1055 apply (case_tac [9] "AKcryptSK servK SK evs5")
  1056 apply (simp_all del: image_insert
  1057         add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
  1058              Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
  1059        Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
  1060   \<comment>\<open>18 seconds on a 1.8GHz machine??\<close>
  1061 txt\<open>Fake\<close> 
  1062 apply spy_analz
  1063 txt\<open>Reception\<close>
  1064 apply (simp add: AKcryptSK_def)
  1065 txt\<open>K2\<close>
  1066 apply blast 
  1067 txt\<open>K3\<close>
  1068 apply blast 
  1069 txt\<open>K4\<close>
  1070 apply (blast dest!: authK_not_AKcryptSK)
  1071 txt\<open>K5\<close>
  1072 apply (case_tac "Key servK \<in> analz (spies evs5) ")
  1073 txt\<open>If servK is compromised then the result follows directly...\<close>
  1074 apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
  1075 txt\<open>...therefore servK is uncompromised.\<close>
  1076 txt\<open>The AKcryptSK servK SK evs5 case leads to a contradiction.\<close>
  1077 apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
  1078 txt\<open>Another K5 case\<close>
  1079 apply blast 
  1080 txt\<open>Oops1\<close>
  1081 apply simp 
  1082 by (blast dest!: AKcryptSK_analz_insert)
  1083 
  1084 text\<open>First simplification law for analz: no session keys encrypt
  1085 authentication keys or shared keys.\<close>
  1086 lemma analz_insert_freshK1:
  1087      "\<lbrakk> evs \<in> kerbIV_gets;  K \<in> authKeys evs Un range shrK;
  1088         SesKey \<notin> range shrK \<rbrakk>
  1089       \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
  1090           (K = SesKey | Key K \<in> analz (spies evs))"
  1091 apply (frule authKeys_are_not_AKcryptSK, assumption)
  1092 apply (simp del: image_insert
  1093             add: analz_image_freshK_simps add: Key_analz_image_Key)
  1094 done
  1095 
  1096 
  1097 text\<open>Second simplification law for analz: no service keys encrypt any other keys.\<close>
  1098 lemma analz_insert_freshK2:
  1099      "\<lbrakk> evs \<in> kerbIV_gets;  servK \<notin> (authKeys evs); servK \<notin> range shrK;
  1100         K \<in> symKeys \<rbrakk>
  1101       \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
  1102           (K = servK | Key K \<in> analz (spies evs))"
  1103 apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
  1104 apply (simp del: image_insert
  1105             add: analz_image_freshK_simps add: Key_analz_image_Key)
  1106 done
  1107 
  1108 
  1109 text\<open>Third simplification law for analz: only one authentication key encrypts a certain service key.\<close>
  1110 
  1111 lemma analz_insert_freshK3:
  1112  "\<lbrakk> AKcryptSK authK servK evs;
  1113     authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
  1114         \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
  1115                 (servK = authK' | Key servK \<in> analz (spies evs))"
  1116 apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
  1117 apply (simp del: image_insert
  1118             add: analz_image_freshK_simps add: Key_analz_image_Key)
  1119 done
  1120 
  1121 lemma analz_insert_freshK3_bis:
  1122  "\<lbrakk> Says Tgs A
  1123             (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1124         \<in> set evs; 
  1125      authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
  1126         \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
  1127                 (servK = authK' | Key servK \<in> analz (spies evs))"
  1128 apply (frule AKcryptSKI, assumption)
  1129 by (simp add: analz_insert_freshK3)
  1130 
  1131 text\<open>a weakness of the protocol\<close>
  1132 lemma authK_compromises_servK:
  1133      "\<lbrakk> Says Tgs A
  1134               (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1135            \<in> set evs;  authK \<in> symKeys;
  1136          Key authK \<in> analz (spies evs); evs \<in> kerbIV_gets \<rbrakk>
  1137       \<Longrightarrow> Key servK \<in> analz (spies evs)"
  1138 by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
  1139 
  1140 lemma servK_notin_authKeysD:
  1141      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts,
  1142                       Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
  1143            \<in> parts (spies evs);
  1144          Key servK \<notin> analz (spies evs);
  1145          B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
  1146       \<Longrightarrow> servK \<notin> authKeys evs"
  1147 apply (erule rev_mp)
  1148 apply (erule rev_mp)
  1149 apply (simp add: authKeys_def)
  1150 apply (erule kerbIV_gets.induct, analz_mono_contra)
  1151 apply (frule_tac [8] Gets_ticket_parts)
  1152 apply (frule_tac [6] Gets_ticket_parts, simp_all)
  1153 by (blast+)
  1154 
  1155 
  1156 text\<open>If Spy sees the Authentication Key sent in msg K2, then
  1157     the Key has expired.\<close>
  1158 lemma Confidentiality_Kas_lemma [rule_format]:
  1159      "\<lbrakk> authK \<in> symKeys; A \<notin> bad;  evs \<in> kerbIV_gets \<rbrakk>
  1160       \<Longrightarrow> Says Kas A
  1161                (Crypt (shrK A)
  1162                   \<lbrace>Key authK, Agent Tgs, Number Ta,
  1163           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
  1164             \<in> set evs \<longrightarrow>
  1165           Key authK \<in> analz (spies evs) \<longrightarrow>
  1166           expiredAK Ta evs"
  1167 apply (erule kerbIV_gets.induct)
  1168 apply (frule_tac [11] Oops_range_spies2)
  1169 apply (frule_tac [10] Oops_range_spies1)
  1170 apply (frule_tac [8] Says_tgs_message_form)
  1171 apply (frule_tac [6] Says_kas_message_form)
  1172 apply (safe del: impI conjI impCE)
  1173 apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
  1174 txt\<open>Fake\<close>
  1175 apply spy_analz
  1176 txt\<open>K2\<close>
  1177 apply blast
  1178 txt\<open>K4\<close>
  1179 apply blast
  1180 txt\<open>Level 8: K5\<close>
  1181 apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
  1182 txt\<open>Oops1\<close>
  1183 apply (blast dest!: unique_authKeys intro: less_SucI)
  1184 txt\<open>Oops2\<close>
  1185 by (blast dest: Says_Tgs_message_form Says_Kas_message_form)
  1186 
  1187 lemma Confidentiality_Kas:
  1188      "\<lbrakk> Says Kas A
  1189               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
  1190            \<in> set evs;
  1191          \<not> expiredAK Ta evs;
  1192          A \<notin> bad;  evs \<in> kerbIV_gets \<rbrakk>
  1193       \<Longrightarrow> Key authK \<notin> analz (spies evs)"
  1194 by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
  1195 
  1196 text\<open>If Spy sees the Service Key sent in msg K4, then
  1197     the Key has expired.\<close>
  1198 
  1199 lemma Confidentiality_lemma [rule_format]:
  1200      "\<lbrakk> Says Tgs A
  1201             (Crypt authK
  1202                \<lbrace>Key servK, Agent B, Number Ts,
  1203                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
  1204            \<in> set evs;
  1205         Key authK \<notin> analz (spies evs);
  1206         servK \<in> symKeys;
  1207         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1208       \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
  1209           expiredSK Ts evs"
  1210 apply (erule rev_mp)
  1211 apply (erule rev_mp)
  1212 apply (erule kerbIV_gets.induct)
  1213 apply (rule_tac [10] impI)+
  1214   \<comment>\<open>The Oops1 case is unusual: must simplify
  1215     @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
  1216    \<open>analz_mono_contra\<close> weaken it to
  1217    @{term "Authkey \<notin> analz (spies evs)"},
  1218   for we then conclude @{term "authK \<noteq> authKa"}.\<close>
  1219 apply analz_mono_contra
  1220 apply (frule_tac [11] Oops_range_spies2)
  1221 apply (frule_tac [10] Oops_range_spies1)
  1222 apply (frule_tac [8] Says_tgs_message_form)
  1223 apply (frule_tac [6] Says_kas_message_form)
  1224 apply (safe del: impI conjI impCE)
  1225 apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
  1226 txt\<open>Fake\<close>
  1227 apply spy_analz
  1228 txt\<open>K2\<close>
  1229 apply (blast intro: parts_insertI less_SucI)
  1230 txt\<open>K4\<close>
  1231 apply (blast dest: authTicket_authentic Confidentiality_Kas)
  1232 txt\<open>Oops2\<close>
  1233   prefer 3
  1234   apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
  1235 txt\<open>Oops1\<close>
  1236  prefer 2
  1237 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
  1238 txt\<open>K5. Not clear how this step could be integrated with the main
  1239        simplification step. Done in KerberosV.thy\<close>
  1240 apply clarify
  1241 apply (erule_tac V = "Says Aa Tgs X \<in> set evs" for X evs in thin_rl)
  1242 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD])
  1243 apply (assumption, assumption, blast, assumption)
  1244 apply (simp add: analz_insert_freshK2)
  1245 apply (blast dest: Key_unique_SesKey intro: less_SucI)
  1246 done
  1247 
  1248 
  1249 text\<open>In the real world Tgs can't check wheter authK is secure!\<close>
  1250 lemma Confidentiality_Tgs:
  1251      "\<lbrakk> Says Tgs A
  1252               (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1253            \<in> set evs;
  1254          Key authK \<notin> analz (spies evs);
  1255          \<not> expiredSK Ts evs;
  1256          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1257       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1258 by (blast dest: Says_Tgs_message_form Confidentiality_lemma)
  1259 
  1260 text\<open>In the real world Tgs CAN check what Kas sends!\<close>
  1261 lemma Confidentiality_Tgs_bis:
  1262      "\<lbrakk> Says Kas A
  1263                (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
  1264            \<in> set evs;
  1265          Says Tgs A
  1266               (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1267            \<in> set evs;
  1268          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1269          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1270       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1271 by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
  1272 
  1273 text\<open>Most general form\<close>
  1274 lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
  1275 
  1276 lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]
  1277 
  1278 text\<open>Needs a confidentiality guarantee, hence moved here.
  1279       Authenticity of servK for A\<close>
  1280 lemma servK_authentic_bis_r:
  1281      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1282            \<in> parts (spies evs);
  1283          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1284            \<in> parts (spies evs);
  1285          \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1286  \<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1287        \<in> set evs"
  1288 by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
  1289 
  1290 lemma Confidentiality_Serv_A:
  1291      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1292            \<in> parts (spies evs);
  1293          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1294            \<in> parts (spies evs);
  1295          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1296          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1297       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1298 by (metis Confidentiality_Auth_A Confidentiality_Tgs K4_imp_K2 authK_authentic authTicket_form servK_authentic unique_authKeys)
  1299 
  1300 (*deleted Confidentiality_B, which was identical to Confidentiality_Serv_A*)
  1301 
  1302 lemma u_Confidentiality_B:
  1303      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1304            \<in> parts (spies evs);
  1305          \<not> expiredSK Ts evs;
  1306          A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
  1307       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1308 by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
  1309 
  1310 
  1311 
  1312 subsection\<open>2. Parties' strong authentication: 
  1313        non-injective agreement on the session key. The same guarantees also
  1314        express key distribution, hence their names\<close>
  1315 
  1316 text\<open>Authentication here still is weak agreement - of B with A\<close>
  1317 lemma A_authenticates_B:
  1318      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
  1319          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1320            \<in> parts (spies evs);
  1321          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1322            \<in> parts (spies evs);
  1323          Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
  1324          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1325       \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
  1326 by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6)
  1327 
  1328 (*These two have never been proved, because never were they needed before!*)
  1329 lemma shrK_in_initState_Server[iff]:  "Key (shrK A) \<in> initState Kas"
  1330 by (induct_tac "A", auto)
  1331 
  1332 lemma shrK_in_knows_Server [iff]: "Key (shrK A) \<in> knows Kas evs"
  1333 by (simp add: initState_subset_knows [THEN subsetD])
  1334 (*Because of our simple model of Tgs, the equivalent for it required an axiom*)
  1335 
  1336 
  1337 lemma A_authenticates_and_keydist_to_Kas:
  1338    "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs;
  1339       A \<notin> bad;  evs \<in> kerbIV_gets \<rbrakk>
  1340   \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs
  1341   \<and> Key authK \<in> analz(knows Kas evs)"
  1342 by (force dest!: authK_authentic Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
  1343 
  1344 
  1345 lemma K3_imp_Gets_evs:
  1346   "\<lbrakk> Says A Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
  1347                  Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> 
  1348       \<in> set evs;  A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1349  \<Longrightarrow>  Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, 
  1350                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
  1351        \<in> set evs"
  1352 apply (erule rev_mp)
  1353 apply (erule kerbIV_gets.induct)
  1354 apply auto
  1355 apply (blast dest: authTicket_form)
  1356 done
  1357 
  1358 lemma Tgs_authenticates_and_keydist_to_A:
  1359   "\<lbrakk>  Gets Tgs \<lbrace>
  1360           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
  1361           Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs;
  1362       Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1363  \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
  1364           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
  1365           Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs
  1366  \<and>  Key authK \<in> analz (knows A evs)"  
  1367 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
  1368 apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN parts.Fst], assumption)
  1369 apply (drule Tgs_authenticates_A, assumption+, simp)
  1370 apply (force dest!: K3_imp_Gets_evs Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
  1371 done
  1372 
  1373 lemma K4_imp_Gets:
  1374   "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1375        \<in> set evs; evs \<in> kerbIV_gets \<rbrakk>
  1376  \<Longrightarrow> \<exists> Ta X. 
  1377      Gets Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, X\<rbrace>
  1378        \<in> set evs"
  1379 apply (erule rev_mp)
  1380 apply (erule kerbIV_gets.induct)
  1381 apply auto
  1382 done
  1383 
  1384 lemma A_authenticates_and_keydist_to_Tgs:
  1385  "\<lbrakk>  Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
  1386        \<in> set evs;
  1387      Gets A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1388        \<in> set evs;
  1389      Key authK \<notin> analz (spies evs); A \<notin> bad;
  1390      evs \<in> kerbIV_gets \<rbrakk>
  1391  \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1392        \<in> set evs
  1393   \<and> Key authK \<in> analz (knows Tgs evs)
  1394   \<and> Key servK \<in> analz (knows Tgs evs)"
  1395 apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
  1396 apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
  1397 apply (frule authK_authentic, assumption+)
  1398 apply (drule servK_authentic_ter, assumption+)
  1399 apply (frule K4_imp_Gets, assumption, erule exE, erule exE)
  1400 apply (drule Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst], assumption, force)
  1401 apply (metis Says_imp_knows analz.Fst analz.Inj analz_symKeys_Decrypt authTicket_form)
  1402 done
  1403 
  1404 lemma K5_imp_Gets:
  1405   "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs;
  1406     A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1407  \<Longrightarrow> \<exists> authK Ts authTicket T2.
  1408     Gets A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) \<in> set evs
  1409  \<and> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>  \<in> set evs"
  1410 apply (erule rev_mp)
  1411 apply (erule kerbIV_gets.induct)
  1412 apply auto
  1413 done 
  1414 
  1415 lemma K3_imp_Gets:
  1416   "\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
  1417        \<in> set evs;
  1418     A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1419  \<Longrightarrow> \<exists> Ta. Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs"
  1420 apply (erule rev_mp)
  1421 apply (erule kerbIV_gets.induct)
  1422 apply auto
  1423 done 
  1424 
  1425 lemma B_authenticates_and_keydist_to_A:
  1426      "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
  1427                 Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs;
  1428         Key servK \<notin> analz (spies evs);
  1429         A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
  1430  \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
  1431                Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs
  1432   \<and> Key servK \<in> analz (knows A evs)"
  1433 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN servTicket_authentic_Tgs], assumption+)  
  1434 apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption)
  1435 apply (erule exE, drule Says_K5, assumption+)
  1436 apply (frule K5_imp_Gets, assumption+)
  1437 apply clarify
  1438 apply (drule K3_imp_Gets, assumption+)
  1439 apply (erule exE)
  1440 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption+, clarify)
  1441 apply (force dest!: Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
  1442 done
  1443 
  1444 
  1445 lemma K6_imp_Gets:
  1446   "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
  1447      B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1448 \<Longrightarrow> \<exists> Ts X. Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,X\<rbrace>
  1449        \<in> set evs"
  1450 apply (erule rev_mp)
  1451 apply (erule kerbIV_gets.induct)
  1452 apply auto
  1453 done
  1454 
  1455 
  1456 lemma A_authenticates_and_keydist_to_B:
  1457   "\<lbrakk> Gets A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>,
  1458              Crypt servK (Number T3)\<rbrace> \<in> set evs;
  1459      Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
  1460            \<in> set evs;
  1461      Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
  1462      A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
  1463  \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs 
  1464    \<and> Key servK \<in> analz (knows B evs)"
  1465 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
  1466 apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption)
  1467 apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
  1468 apply (drule A_authenticates_B, assumption+)
  1469 apply (force dest!: K6_imp_Gets Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
  1470 done
  1471 
  1472 end
  1473