src/HOL/Auth/KerberosIV.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 61830 4f5ab843cf5b
child 67443 3abf6a722518
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Auth/KerberosIV.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 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  (* A is the true creator of X if she has sent X and X never appeared on
    33     the trace before this event. Recall that traces grow from head. *)
    34   Issues :: "[agent, agent, msg, event list] => bool"
    35              ("_ Issues _ with _ on _" [50, 0, 0, 50] 50) where
    36    "(A Issues B with X on evs) =
    37       (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
    38         X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
    39 
    40 definition
    41  (* Yields the subtrace of a given trace from its beginning to a given event *)
    42   before :: "[event, event list] => event list" ("before _ on _" [0, 50] 50)
    43   where "(before ev on evs) = takeWhile (% z. z ~= ev) (rev evs)"
    44 
    45 definition
    46  (* States than an event really appears only once on a trace *)
    47   Unique :: "[event, event list] => bool" ("Unique _ on _" [0, 50] 50)
    48   where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
    49 
    50 
    51 consts
    52     (*Duration of the authentication key*)
    53     authKlife   :: nat
    54 
    55     (*Duration of the service key*)
    56     servKlife   :: nat
    57 
    58     (*Duration of an authenticator*)
    59     authlife   :: nat
    60 
    61     (*Upper bound on the time of reaction of a server*)
    62     replylife   :: nat
    63 
    64 specification (authKlife)
    65   authKlife_LB [iff]: "2 \<le> authKlife"
    66     by blast
    67 
    68 specification (servKlife)
    69   servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
    70     by blast
    71 
    72 specification (authlife)
    73   authlife_LB [iff]: "Suc 0 \<le> authlife"
    74     by blast
    75 
    76 specification (replylife)
    77   replylife_LB [iff]: "Suc 0 \<le> replylife"
    78     by blast
    79 
    80 abbreviation
    81   (*The current time is the length of the trace*)
    82   CT :: "event list=>nat" where
    83   "CT == length"
    84 
    85 abbreviation
    86   expiredAK :: "[nat, event list] => bool" where
    87   "expiredAK Ta evs == authKlife + Ta < CT evs"
    88 
    89 abbreviation
    90   expiredSK :: "[nat, event list] => bool" where
    91   "expiredSK Ts evs == servKlife + Ts < CT evs"
    92 
    93 abbreviation
    94   expiredA :: "[nat, event list] => bool" where
    95   "expiredA T evs == authlife + T < CT evs"
    96 
    97 abbreviation
    98   valid :: "[nat, nat] => bool" ("valid _ wrt _" [0, 50] 50) where
    99   "valid T1 wrt T2 == T1 <= replylife + T2"
   100 
   101 (*---------------------------------------------------------------------*)
   102 
   103 
   104 (* Predicate formalising the association between authKeys and servKeys *)
   105 definition AKcryptSK :: "[key, key, event list] => bool" where
   106   "AKcryptSK authK servK evs ==
   107      \<exists>A B Ts.
   108        Says Tgs A (Crypt authK
   109                      \<lbrace>Key servK, Agent B, Number Ts,
   110                        Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
   111          \<in> set evs"
   112 
   113 inductive_set kerbIV :: "event list set"
   114   where
   115 
   116    Nil:  "[] \<in> kerbIV"
   117 
   118  | Fake: "\<lbrakk> evsf \<in> kerbIV;  X \<in> synth (analz (spies evsf)) \<rbrakk>
   119           \<Longrightarrow> Says Spy B X  # evsf \<in> kerbIV"
   120 
   121 (* FROM the initiator *)
   122  | K1:   "\<lbrakk> evs1 \<in> kerbIV \<rbrakk>
   123           \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
   124           \<in> kerbIV"
   125 
   126 (* Adding the timestamp serves to A in K3 to check that
   127    she doesn't get a reply too late. This kind of timeouts are ordinary.
   128    If a server's reply is late, then it is likely to be fake. *)
   129 
   130 (*---------------------------------------------------------------------*)
   131 
   132 (*FROM Kas *)
   133  | K2:  "\<lbrakk> evs2 \<in> kerbIV; Key authK \<notin> used evs2; authK \<in> symKeys;
   134             Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
   135           \<Longrightarrow> Says Kas A
   136                 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2),
   137                       (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
   138                           Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV"
   139 (*
   140   The internal encryption builds the authTicket.
   141   The timestamp doesn't change inside the two encryptions: the external copy
   142   will be used by the initiator in K3; the one inside the
   143   authTicket by Tgs in K4.
   144 *)
   145 
   146 (*---------------------------------------------------------------------*)
   147 
   148 (* FROM the initiator *)
   149  | K3:  "\<lbrakk> evs3 \<in> kerbIV;
   150             Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
   151             Says Kas' A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   152               authTicket\<rbrace>) \<in> set evs3;
   153             valid Ta wrt T1
   154          \<rbrakk>
   155           \<Longrightarrow> Says A Tgs \<lbrace>authTicket,
   156                            (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
   157                            Agent B\<rbrace> # evs3 \<in> kerbIV"
   158 (*The two events amongst the premises allow A to accept only those authKeys
   159   that are not issued late. *)
   160 
   161 (*---------------------------------------------------------------------*)
   162 
   163 (* FROM Tgs *)
   164 (* Note that the last temporal check is not mentioned in the original MIT
   165    specification. Adding it makes many goals "available" to the peers. 
   166    Theorems that exploit it have the suffix `_u', which stands for updated 
   167    protocol.
   168 *)
   169  | K4:  "\<lbrakk> evs4 \<in> kerbIV; Key servK \<notin> used evs4; servK \<in> symKeys;
   170             B \<noteq> Tgs;  authK \<in> symKeys;
   171             Says A' Tgs \<lbrace>
   172              (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
   173                                  Number Ta\<rbrace>),
   174              (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
   175                 \<in> set evs4;
   176             \<not> expiredAK Ta evs4;
   177             \<not> expiredA T2 evs4;
   178             servKlife + (CT evs4) <= authKlife + Ta
   179          \<rbrakk>
   180           \<Longrightarrow> Says Tgs A
   181                 (Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4),
   182                                Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK,
   183                                                 Number (CT evs4)\<rbrace> \<rbrace>)
   184                 # evs4 \<in> kerbIV"
   185 (* Tgs creates a new session key per each request for a service, without
   186    checking if there is still a fresh one for that service.
   187    The cipher under Tgs' key is the authTicket, the cipher under B's key
   188    is the servTicket, which is built now.
   189    NOTE that the last temporal check is not present in the MIT specification.
   190 
   191 *)
   192 
   193 (*---------------------------------------------------------------------*)
   194 
   195 (* FROM the initiator *)
   196  | K5:  "\<lbrakk> evs5 \<in> kerbIV; authK \<in> symKeys; servK \<in> symKeys;
   197             Says A Tgs
   198                 \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
   199                   Agent B\<rbrace>
   200               \<in> set evs5;
   201             Says Tgs' A
   202              (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   203                 \<in> set evs5;
   204             valid Ts wrt T2 \<rbrakk>
   205           \<Longrightarrow> Says A B \<lbrace>servTicket,
   206                          Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
   207                # evs5 \<in> kerbIV"
   208 (* Checks similar to those in K3. *)
   209 
   210 (*---------------------------------------------------------------------*)
   211 
   212 (* FROM the responder*)
   213   | K6:  "\<lbrakk> evs6 \<in> kerbIV;
   214             Says A' B \<lbrace>
   215               (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
   216               (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
   217             \<in> set evs6;
   218             \<not> expiredSK Ts evs6;
   219             \<not> expiredA T3 evs6
   220          \<rbrakk>
   221           \<Longrightarrow> Says B A (Crypt servK (Number T3))
   222                # evs6 \<in> kerbIV"
   223 (* Checks similar to those in K4. *)
   224 
   225 (*---------------------------------------------------------------------*)
   226 
   227 (* Leaking an authK... *)
   228  | Oops1: "\<lbrakk> evsO1 \<in> kerbIV;  A \<noteq> Spy;
   229               Says Kas A
   230                 (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   231                                   authTicket\<rbrace>)  \<in> set evsO1;
   232               expiredAK Ta evsO1 \<rbrakk>
   233           \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
   234                # evsO1 \<in> kerbIV"
   235 
   236 (*---------------------------------------------------------------------*)
   237 
   238 (*Leaking a servK... *)
   239  | Oops2: "\<lbrakk> evsO2 \<in> kerbIV;  A \<noteq> Spy;
   240               Says Tgs A
   241                 (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   242                    \<in> set evsO2;
   243               expiredSK Ts evsO2 \<rbrakk>
   244           \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
   245                # evsO2 \<in> kerbIV"
   246 
   247 (*---------------------------------------------------------------------*)
   248 
   249 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   250 declare parts.Body [dest]
   251 declare analz_into_parts [dest]
   252 declare Fake_parts_insert_in_Un [dest]
   253 
   254 
   255 subsection\<open>Lemmas about lists, for reasoning about  Issues\<close>
   256 
   257 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
   258 apply (induct_tac "evs")
   259 apply (rename_tac [2] a b)
   260 apply (induct_tac [2] a, auto)
   261 done
   262 
   263 lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
   264 apply (induct_tac "evs")
   265 apply (rename_tac [2] a b)
   266 apply (induct_tac [2] a, auto)
   267 done
   268 
   269 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
   270           (if A:bad then insert X (spies evs) else spies evs)"
   271 apply (induct_tac "evs")
   272 apply (rename_tac [2] a b)
   273 apply (induct_tac [2] a, auto)
   274 done
   275 
   276 lemma spies_evs_rev: "spies evs = spies (rev evs)"
   277 apply (induct_tac "evs")
   278 apply (rename_tac [2] a b)
   279 apply (induct_tac [2] a)
   280 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
   281 done
   282 
   283 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
   284 
   285 lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
   286 apply (induct_tac "evs")
   287 apply (rename_tac [2] a b)
   288 apply (induct_tac [2] "a", auto)
   289 txt\<open>Resembles \<open>used_subset_append\<close> in theory Event.\<close>
   290 done
   291 
   292 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
   293 
   294 
   295 subsection\<open>Lemmas about @{term authKeys}\<close>
   296 
   297 lemma authKeys_empty: "authKeys [] = {}"
   298 apply (unfold authKeys_def)
   299 apply (simp (no_asm))
   300 done
   301 
   302 lemma authKeys_not_insert:
   303  "(\<forall>A Ta akey Peer.
   304    ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
   305               (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
   306        \<Longrightarrow> authKeys (ev # evs) = authKeys evs"
   307 by (unfold authKeys_def, auto)
   308 
   309 lemma authKeys_insert:
   310   "authKeys
   311      (Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
   312       (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
   313        = insert K (authKeys evs)"
   314 by (unfold authKeys_def, auto)
   315 
   316 lemma authKeys_simp:
   317    "K \<in> authKeys
   318     (Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
   319      (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
   320         \<Longrightarrow> K = K' | K \<in> authKeys evs"
   321 by (unfold authKeys_def, auto)
   322 
   323 lemma authKeysI:
   324    "Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
   325      (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
   326         \<Longrightarrow> K \<in> authKeys evs"
   327 by (unfold authKeys_def, auto)
   328 
   329 lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
   330 by (simp add: authKeys_def, blast)
   331 
   332 
   333 subsection\<open>Forwarding Lemmas\<close>
   334 
   335 text\<open>--For reasoning about the encrypted portion of message K3--\<close>
   336 lemma K3_msg_in_parts_spies:
   337      "Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>)
   338                \<in> set evs \<Longrightarrow> authTicket \<in> parts (spies evs)"
   339 by blast
   340 
   341 lemma Oops_range_spies1:
   342      "\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
   343            \<in> set evs ;
   344          evs \<in> kerbIV \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
   345 apply (erule rev_mp)
   346 apply (erule kerbIV.induct, auto)
   347 done
   348 
   349 text\<open>--For reasoning about the encrypted portion of message K5--\<close>
   350 lemma K5_msg_in_parts_spies:
   351      "Says Tgs' A (Crypt authK \<lbrace>servK, Agent B, Ts, servTicket\<rbrace>)
   352                \<in> set evs \<Longrightarrow> servTicket \<in> parts (spies evs)"
   353 by blast
   354 
   355 lemma Oops_range_spies2:
   356      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
   357            \<in> set evs ;
   358          evs \<in> kerbIV \<rbrakk> \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys"
   359 apply (erule rev_mp)
   360 apply (erule kerbIV.induct, auto)
   361 done
   362 
   363 lemma Says_ticket_parts:
   364      "Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
   365       \<Longrightarrow> Ticket \<in> parts (spies evs)"
   366 by blast
   367 
   368 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
   369 lemma Spy_see_shrK [simp]:
   370      "evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   371 apply (erule kerbIV.induct)
   372 apply (frule_tac [7] K5_msg_in_parts_spies)
   373 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   374 apply (blast+)
   375 done
   376 
   377 lemma Spy_analz_shrK [simp]:
   378      "evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   379 by auto
   380 
   381 lemma Spy_see_shrK_D [dest!]:
   382      "\<lbrakk> Key (shrK A) \<in> parts (spies evs);  evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A:bad"
   383 by (blast dest: Spy_see_shrK)
   384 
   385 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
   386 
   387 text\<open>Nobody can have used non-existent keys!\<close>
   388 lemma new_keys_not_used [simp]:
   389     "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV\<rbrakk>
   390      \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
   391 apply (erule rev_mp)
   392 apply (erule kerbIV.induct)
   393 apply (frule_tac [7] K5_msg_in_parts_spies)
   394 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   395 txt\<open>Fake\<close>
   396 apply (force dest!: keysFor_parts_insert)
   397 txt\<open>Others\<close>
   398 apply (force dest!: analz_shrK_Decrypt)+
   399 done
   400 
   401 (*Earlier, all protocol proofs declared this theorem.
   402   But few of them actually need it! (Another is Yahalom) *)
   403 lemma new_keys_not_analzd:
   404  "\<lbrakk>evs \<in> kerbIV; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
   405   \<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
   406 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
   407 
   408 
   409 
   410 subsection\<open>Lemmas for reasoning about predicate "before"\<close>
   411 
   412 lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
   413 apply (induct_tac "evs")
   414 apply simp
   415 apply (rename_tac a b)
   416 apply (induct_tac "a")
   417 apply auto
   418 done
   419 
   420 lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
   421 apply (induct_tac "evs")
   422 apply simp
   423 apply (rename_tac a b)
   424 apply (induct_tac "a")
   425 apply auto
   426 done
   427 
   428 lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
   429 apply (induct_tac "evs")
   430 apply simp
   431 apply (rename_tac a b)
   432 apply (induct_tac "a")
   433 apply auto
   434 done
   435 
   436 lemma used_evs_rev: "used evs = used (rev evs)"
   437 apply (induct_tac "evs")
   438 apply simp
   439 apply (rename_tac a b)
   440 apply (induct_tac "a")
   441 apply (simp add: used_Says_rev)
   442 apply (simp add: used_Gets_rev)
   443 apply (simp add: used_Notes_rev)
   444 done
   445 
   446 lemma used_takeWhile_used [rule_format]: 
   447       "x : used (takeWhile P X) --> x : used X"
   448 apply (induct_tac "X")
   449 apply simp
   450 apply (rename_tac a b)
   451 apply (induct_tac "a")
   452 apply (simp_all add: used_Nil)
   453 apply (blast dest!: initState_into_used)+
   454 done
   455 
   456 lemma set_evs_rev: "set evs = set (rev evs)"
   457 by auto
   458 
   459 lemma takeWhile_void [rule_format]:
   460       "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs"
   461 by auto
   462 
   463 
   464 subsection\<open>Regularity Lemmas\<close>
   465 text\<open>These concern the form of items passed in messages\<close>
   466 
   467 text\<open>Describes the form of all components sent by Kas\<close>
   468 lemma Says_Kas_message_form:
   469      "\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
   470            \<in> set evs;
   471          evs \<in> kerbIV \<rbrakk> \<Longrightarrow>  
   472   K = shrK A  & Peer = Tgs &
   473   authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys & 
   474   authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>) &
   475   Key authK \<notin> used(before 
   476            Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
   477                    on evs) &
   478   Ta = CT (before 
   479            Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
   480            on evs)"
   481 apply (unfold before_def)
   482 apply (erule rev_mp)
   483 apply (erule kerbIV.induct)
   484 apply (simp_all (no_asm) add: authKeys_def authKeys_insert, blast, blast)
   485 txt\<open>K2\<close>
   486 apply (simp (no_asm) add: takeWhile_tail)
   487 apply (rule conjI)
   488 apply (metis Key_not_used authKeys_used length_rev set_rev takeWhile_void used_evs_rev)
   489 apply blast+
   490 done
   491 
   492 
   493 
   494 (*This lemma is essential for proving Says_Tgs_message_form:
   495 
   496   the session key authK
   497   supplied by Kas in the authentication ticket
   498   cannot be a long-term key!
   499 
   500   Generalised to any session keys (both authK and servK).
   501 *)
   502 lemma SesKey_is_session_key:
   503      "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
   504             \<in> parts (spies evs); Tgs_B \<notin> bad;
   505          evs \<in> kerbIV \<rbrakk>
   506       \<Longrightarrow> SesKey \<notin> range shrK"
   507 apply (erule rev_mp)
   508 apply (erule kerbIV.induct)
   509 apply (frule_tac [7] K5_msg_in_parts_spies)
   510 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
   511 done
   512 
   513 lemma authTicket_authentic:
   514      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
   515            \<in> parts (spies evs);
   516          evs \<in> kerbIV \<rbrakk>
   517       \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   518                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   519             \<in> set evs"
   520 apply (erule rev_mp)
   521 apply (erule kerbIV.induct)
   522 apply (frule_tac [7] K5_msg_in_parts_spies)
   523 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   524 txt\<open>Fake, K4\<close>
   525 apply (blast+)
   526 done
   527 
   528 lemma authTicket_crypt_authK:
   529      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
   530            \<in> parts (spies evs);
   531          evs \<in> kerbIV \<rbrakk>
   532       \<Longrightarrow> authK \<in> authKeys evs"
   533 apply (frule authTicket_authentic, assumption)
   534 apply (simp (no_asm) add: authKeys_def)
   535 apply blast
   536 done
   537 
   538 text\<open>Describes the form of servK, servTicket and authK sent by Tgs\<close>
   539 lemma Says_Tgs_message_form:
   540      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   541            \<in> set evs;
   542          evs \<in> kerbIV \<rbrakk>
   543   \<Longrightarrow> B \<noteq> Tgs & 
   544       authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
   545       servK \<notin> range shrK & servK \<notin> authKeys evs & servK \<in> symKeys &
   546       servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>) &
   547       Key servK \<notin> used (before
   548         Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   549                         on evs) &
   550       Ts = CT(before 
   551         Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   552               on evs) "
   553 apply (unfold before_def)
   554 apply (erule rev_mp)
   555 apply (erule kerbIV.induct)
   556 apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast)
   557 txt\<open>We need this simplification only for Message 4\<close>
   558 apply (simp (no_asm) add: takeWhile_tail)
   559 apply auto
   560 txt\<open>Five subcases of Message 4\<close>
   561 apply (blast dest!: SesKey_is_session_key)
   562 apply (blast dest: authTicket_crypt_authK)
   563 apply (blast dest!: authKeys_used Says_Kas_message_form)
   564 txt\<open>subcase: used before\<close>
   565 apply (metis used_evs_rev used_takeWhile_used)
   566 txt\<open>subcase: CT before\<close>
   567 apply (metis length_rev set_evs_rev takeWhile_void)
   568 done
   569 
   570 lemma authTicket_form:
   571      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>
   572            \<in> parts (spies evs);
   573          A \<notin> bad;
   574          evs \<in> kerbIV \<rbrakk>
   575     \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys & 
   576         authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>"
   577 apply (erule rev_mp)
   578 apply (erule kerbIV.induct)
   579 apply (frule_tac [7] K5_msg_in_parts_spies)
   580 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   581 apply (blast+)
   582 done
   583 
   584 text\<open>This form holds also over an authTicket, but is not needed below.\<close>
   585 lemma servTicket_form:
   586      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>
   587               \<in> parts (spies evs);
   588             Key authK \<notin> analz (spies evs);
   589             evs \<in> kerbIV \<rbrakk>
   590          \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys & 
   591     (\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)"
   592 apply (erule rev_mp)
   593 apply (erule rev_mp)
   594 apply (erule kerbIV.induct, analz_mono_contra)
   595 apply (frule_tac [7] K5_msg_in_parts_spies)
   596 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
   597 done
   598 
   599 text\<open>Essentially the same as \<open>authTicket_form\<close>\<close>
   600 lemma Says_kas_message_form:
   601      "\<lbrakk> Says Kas' A (Crypt (shrK A)
   602               \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
   603          evs \<in> kerbIV \<rbrakk>
   604       \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys & 
   605           authTicket =
   606                   Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
   607           | authTicket \<in> analz (spies evs)"
   608 by (blast dest: analz_shrK_Decrypt authTicket_form
   609                 Says_imp_spies [THEN analz.Inj])
   610 
   611 lemma Says_tgs_message_form:
   612  "\<lbrakk> Says Tgs' A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
   613        \<in> set evs;  authK \<in> symKeys;
   614      evs \<in> kerbIV \<rbrakk>
   615   \<Longrightarrow> servK \<notin> range shrK &
   616       (\<exists>A. servTicket =
   617               Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)
   618        | servTicket \<in> analz (spies evs)"
   619 by (metis Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Decrypt analz.Snd invKey_K servTicket_form)
   620 
   621 
   622 subsection\<open>Authenticity theorems: confirm origin of sensitive messages\<close>
   623 
   624 lemma authK_authentic:
   625      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>
   626            \<in> parts (spies evs);
   627          A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
   628       \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
   629             \<in> set evs"
   630 apply (erule rev_mp)
   631 apply (erule kerbIV.induct)
   632 apply (frule_tac [7] K5_msg_in_parts_spies)
   633 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   634 txt\<open>Fake\<close>
   635 apply blast
   636 txt\<open>K4\<close>
   637 apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
   638 done
   639 
   640 text\<open>If a certain encrypted message appears then it originated with Tgs\<close>
   641 lemma servK_authentic:
   642      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
   643            \<in> parts (spies evs);
   644          Key authK \<notin> analz (spies evs);
   645          authK \<notin> range shrK;
   646          evs \<in> kerbIV \<rbrakk>
   647  \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   648        \<in> set evs"
   649 apply (erule rev_mp)
   650 apply (erule rev_mp)
   651 apply (erule kerbIV.induct, analz_mono_contra)
   652 apply (frule_tac [7] K5_msg_in_parts_spies)
   653 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   654 txt\<open>Fake\<close>
   655 apply blast
   656 txt\<open>K2\<close>
   657 apply blast
   658 txt\<open>K4\<close>
   659 apply auto
   660 done
   661 
   662 lemma servK_authentic_bis:
   663      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
   664            \<in> parts (spies evs);
   665          Key authK \<notin> analz (spies evs);
   666          B \<noteq> Tgs;
   667          evs \<in> kerbIV \<rbrakk>
   668  \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   669        \<in> set evs"
   670 apply (erule rev_mp)
   671 apply (erule rev_mp)
   672 apply (erule kerbIV.induct, analz_mono_contra)
   673 apply (frule_tac [7] K5_msg_in_parts_spies)
   674 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   675 txt\<open>Fake\<close>
   676 apply blast
   677 txt\<open>K4\<close>
   678 apply blast
   679 done
   680 
   681 text\<open>Authenticity of servK for B\<close>
   682 lemma servTicket_authentic_Tgs:
   683      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   684            \<in> parts (spies evs); B \<noteq> Tgs;  B \<notin> bad;
   685          evs \<in> kerbIV \<rbrakk>
   686  \<Longrightarrow> \<exists>authK.
   687        Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   688                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
   689        \<in> set evs"
   690 apply (erule rev_mp)
   691 apply (erule rev_mp)
   692 apply (erule kerbIV.induct)
   693 apply (frule_tac [7] K5_msg_in_parts_spies)
   694 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   695 apply blast+
   696 done
   697 
   698 text\<open>Anticipated here from next subsection\<close>
   699 lemma K4_imp_K2:
   700 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   701       \<in> set evs;  evs \<in> kerbIV\<rbrakk>
   702    \<Longrightarrow> \<exists>Ta. Says Kas A
   703         (Crypt (shrK A)
   704          \<lbrace>Key authK, Agent Tgs, Number Ta,
   705            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   706         \<in> set evs"
   707 apply (erule rev_mp)
   708 apply (erule kerbIV.induct)
   709 apply (frule_tac [7] K5_msg_in_parts_spies)
   710 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
   711 apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
   712 done
   713 
   714 text\<open>Anticipated here from next subsection\<close>
   715 lemma u_K4_imp_K2:
   716 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   717       \<in> set evs; evs \<in> kerbIV\<rbrakk>
   718    \<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   719            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   720              \<in> set evs
   721           & servKlife + Ts <= authKlife + Ta)"
   722 apply (erule rev_mp)
   723 apply (erule kerbIV.induct)
   724 apply (frule_tac [7] K5_msg_in_parts_spies)
   725 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
   726 apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
   727 done
   728 
   729 lemma servTicket_authentic_Kas:
   730      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   731            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   732          evs \<in> kerbIV \<rbrakk>
   733   \<Longrightarrow> \<exists>authK Ta.
   734        Says Kas A
   735          (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   736             Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   737         \<in> set evs"
   738 by (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
   739 
   740 lemma u_servTicket_authentic_Kas:
   741      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   742            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   743          evs \<in> kerbIV \<rbrakk>
   744   \<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   745            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   746              \<in> set evs
   747            & servKlife + Ts <= authKlife + Ta"
   748 by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
   749 
   750 lemma servTicket_authentic:
   751      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   752            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   753          evs \<in> kerbIV \<rbrakk>
   754  \<Longrightarrow> \<exists>Ta authK.
   755      Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   756                    Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   757        \<in> set evs
   758      & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   759                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
   760        \<in> set evs"
   761 by (blast dest: servTicket_authentic_Tgs K4_imp_K2)
   762 
   763 lemma u_servTicket_authentic:
   764      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
   765            \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
   766          evs \<in> kerbIV \<rbrakk>
   767  \<Longrightarrow> \<exists>Ta authK.
   768      (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
   769                    Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
   770        \<in> set evs
   771      & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   772                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
   773        \<in> set evs
   774      & servKlife + Ts <= authKlife + Ta)"
   775 by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
   776 
   777 lemma u_NotexpiredSK_NotexpiredAK:
   778      "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
   779       \<Longrightarrow> \<not> expiredAK Ta evs"
   780   by (metis le_less_trans)
   781 
   782 
   783 subsection\<open>Reliability: friendly agents send something if something else happened\<close>
   784 
   785 lemma K3_imp_K2:
   786      "\<lbrakk> Says A Tgs
   787              \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
   788            \<in> set evs;
   789          A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
   790       \<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A)
   791                       \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
   792                    \<in> set evs"
   793 apply (erule rev_mp)
   794 apply (erule kerbIV.induct)
   795 apply (frule_tac [7] K5_msg_in_parts_spies)
   796 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast)
   797 apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN authK_authentic])
   798 done
   799 
   800 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>
   801 lemma Key_unique_SesKey:
   802      "\<lbrakk> Crypt K  \<lbrace>Key SesKey,  Agent B, T, Ticket\<rbrace>
   803            \<in> parts (spies evs);
   804          Crypt K' \<lbrace>Key SesKey,  Agent B', T', Ticket'\<rbrace>
   805            \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
   806          evs \<in> kerbIV \<rbrakk>
   807       \<Longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket'"
   808 apply (erule rev_mp)
   809 apply (erule rev_mp)
   810 apply (erule rev_mp)
   811 apply (erule kerbIV.induct, analz_mono_contra)
   812 apply (frule_tac [7] K5_msg_in_parts_spies)
   813 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   814 txt\<open>Fake, K2, K4\<close>
   815 apply (blast+)
   816 done
   817 
   818 lemma Tgs_authenticates_A:
   819   "\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 
   820       Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
   821            \<in> parts (spies evs);
   822       Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV \<rbrakk>
   823  \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
   824           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
   825           Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs"  
   826 apply (drule authTicket_authentic, assumption, rotate_tac 4)
   827 apply (erule rev_mp, erule rev_mp, erule rev_mp)
   828 apply (erule kerbIV.induct, analz_mono_contra)
   829 apply (frule_tac [5] Says_ticket_parts)
   830 apply (frule_tac [7] Says_ticket_parts)
   831 apply (simp_all (no_asm_simp) add: all_conj_distrib)
   832 txt\<open>Fake\<close>
   833 apply blast
   834 txt\<open>K2\<close>
   835 apply (force dest!: Crypt_imp_keysFor)
   836 txt\<open>K3\<close>
   837 apply (blast dest: Key_unique_SesKey)
   838 txt\<open>K5\<close>
   839 apply (metis K3_imp_K2 Key_unique_SesKey Spy_see_shrK parts.Body parts.Fst 
   840              Says_imp_knows_Spy [THEN parts.Inj])
   841 done
   842 
   843 lemma Says_K5:
   844      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
   845          Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   846                                      servTicket\<rbrace>) \<in> set evs;
   847          Key servK \<notin> analz (spies evs);
   848          A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
   849  \<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
   850 apply (erule rev_mp)
   851 apply (erule rev_mp)
   852 apply (erule rev_mp)
   853 apply (erule kerbIV.induct, analz_mono_contra)
   854 apply (frule_tac [5] Says_ticket_parts)
   855 apply (frule_tac [7] Says_ticket_parts)
   856 apply (simp_all (no_asm_simp) add: all_conj_distrib)
   857 apply blast
   858 txt\<open>K3\<close>
   859 apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
   860 txt\<open>K4\<close>
   861 apply (force dest!: Crypt_imp_keysFor)
   862 txt\<open>K5\<close>
   863 apply (blast dest: Key_unique_SesKey)
   864 done
   865 
   866 text\<open>Anticipated here from next subsection\<close>
   867 lemma unique_CryptKey:
   868      "\<lbrakk> Crypt (shrK B)  \<lbrace>Agent A,  Agent B,  Key SesKey, T\<rbrace>
   869            \<in> parts (spies evs);
   870          Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
   871            \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
   872          evs \<in> kerbIV \<rbrakk>
   873       \<Longrightarrow> A=A' & B=B' & T=T'"
   874 apply (erule rev_mp)
   875 apply (erule rev_mp)
   876 apply (erule rev_mp)
   877 apply (erule kerbIV.induct, analz_mono_contra)
   878 apply (frule_tac [7] K5_msg_in_parts_spies)
   879 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   880 txt\<open>Fake, K2, K4\<close>
   881 apply (blast+)
   882 done
   883 
   884 lemma Says_K6:
   885      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
   886          Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
   887                                      servTicket\<rbrace>) \<in> set evs;
   888          Key servK \<notin> analz (spies evs);
   889          A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
   890       \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
   891 apply (erule rev_mp)
   892 apply (erule rev_mp)
   893 apply (erule rev_mp)
   894 apply (erule kerbIV.induct, analz_mono_contra)
   895 apply (frule_tac [5] Says_ticket_parts)
   896 apply (frule_tac [7] Says_ticket_parts)
   897 apply (simp_all (no_asm_simp))
   898 apply blast
   899 apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used)
   900 apply (clarify)
   901 apply (frule Says_Tgs_message_form, assumption)
   902 apply (metis K3_msg_in_parts_spies parts.Fst Says_imp_knows_Spy [THEN parts.Inj] 
   903              unique_CryptKey) 
   904 done
   905 
   906 text\<open>Needs a unicity theorem, hence moved here\<close>
   907 lemma servK_authentic_ter:
   908  "\<lbrakk> Says Kas A
   909     (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
   910      Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
   911        \<in> parts (spies evs);
   912      Key authK \<notin> analz (spies evs);
   913      evs \<in> kerbIV \<rbrakk>
   914  \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
   915        \<in> set evs"
   916 apply (frule Says_Kas_message_form, assumption)
   917 apply (erule rev_mp)
   918 apply (erule rev_mp)
   919 apply (erule rev_mp)
   920 apply (erule kerbIV.induct, analz_mono_contra)
   921 apply (frule_tac [7] K5_msg_in_parts_spies)
   922 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
   923 txt\<open>K2\<close>
   924 apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
   925 txt\<open>K4 remain\<close>
   926 apply (blast dest!: unique_CryptKey)
   927 done
   928 
   929 
   930 subsection\<open>Unicity Theorems\<close>
   931 
   932 text\<open>The session key, if secure, uniquely identifies the Ticket
   933    whether authTicket or servTicket. As a matter of fact, one can read
   934    also Tgs in the place of B.\<close>
   935 
   936 
   937 (*
   938   At reception of any message mentioning A, Kas associates shrK A with
   939   a new authK. Realistic, as the user gets a new authK at each login.
   940   Similarly, at reception of any message mentioning an authK
   941   (a legitimate user could make several requests to Tgs - by K3), Tgs
   942   associates it with a new servK.
   943 
   944   Therefore, a goal like
   945 
   946    "evs \<in> kerbIV
   947      \<Longrightarrow> Key Kc \<notin> analz (spies evs) \<longrightarrow>
   948            (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket.
   949             Crypt Kc \<lbrace>Key K, Agent B, T, Ticket\<rbrace>
   950              \<in> parts (spies evs) \<longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket')"
   951 
   952   would fail on the K2 and K4 cases.
   953 *)
   954 
   955 lemma unique_authKeys:
   956      "\<lbrakk> Says Kas A
   957               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs;
   958          Says Kas A'
   959               (Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs;
   960          evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' & Ka=Ka' & Ta=Ta' & X=X'"
   961 apply (erule rev_mp)
   962 apply (erule rev_mp)
   963 apply (erule kerbIV.induct)
   964 apply (frule_tac [7] K5_msg_in_parts_spies)
   965 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   966 txt\<open>K2\<close>
   967 apply blast
   968 done
   969 
   970 text\<open>servK uniquely identifies the message from Tgs\<close>
   971 lemma unique_servKeys:
   972      "\<lbrakk> Says Tgs A
   973               (Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs;
   974          Says Tgs A'
   975               (Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs;
   976          evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' & B=B' & K=K' & Ts=Ts' & X=X'"
   977 apply (erule rev_mp)
   978 apply (erule rev_mp)
   979 apply (erule kerbIV.induct)
   980 apply (frule_tac [7] K5_msg_in_parts_spies)
   981 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
   982 txt\<open>K4\<close>
   983 apply blast
   984 done
   985 
   986 text\<open>Revised unicity theorems\<close>
   987 
   988 lemma Kas_Unique:
   989      "\<lbrakk> Says Kas A
   990               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
   991         evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 
   992    Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>)) 
   993    on evs"
   994 apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
   995 apply blast
   996 done
   997 
   998 lemma Tgs_Unique:
   999      "\<lbrakk> Says Tgs A
  1000               (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs;
  1001         evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 
  1002   Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)) 
  1003   on evs"
  1004 apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
  1005 apply blast
  1006 done
  1007 
  1008 
  1009 subsection\<open>Lemmas About the Predicate @{term AKcryptSK}\<close>
  1010 
  1011 lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
  1012 by (simp add: AKcryptSK_def)
  1013 
  1014 lemma AKcryptSKI:
  1015  "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
  1016      evs \<in> kerbIV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
  1017 apply (unfold AKcryptSK_def)
  1018 apply (blast dest: Says_Tgs_message_form)
  1019 done
  1020 
  1021 lemma AKcryptSK_Says [simp]:
  1022    "AKcryptSK authK servK (Says S A X # evs) =
  1023      (Tgs = S &
  1024       (\<exists>B Ts. X = Crypt authK
  1025                 \<lbrace>Key servK, Agent B, Number Ts,
  1026                   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
  1027      | AKcryptSK authK servK evs)"
  1028 by (auto simp add: AKcryptSK_def)
  1029 
  1030 
  1031 (*A fresh authK cannot be associated with any other
  1032   (with respect to a given trace). *)
  1033 lemma Auth_fresh_not_AKcryptSK:
  1034      "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV \<rbrakk>
  1035       \<Longrightarrow> \<not> AKcryptSK authK servK evs"
  1036 apply (unfold AKcryptSK_def)
  1037 apply (erule rev_mp)
  1038 apply (erule kerbIV.induct)
  1039 apply (frule_tac [7] K5_msg_in_parts_spies)
  1040 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
  1041 done
  1042 
  1043 (*A fresh servK cannot be associated with any other
  1044   (with respect to a given trace). *)
  1045 lemma Serv_fresh_not_AKcryptSK:
  1046  "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
  1047 by (unfold AKcryptSK_def, blast)
  1048 
  1049 lemma authK_not_AKcryptSK:
  1050      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
  1051            \<in> parts (spies evs);  evs \<in> kerbIV \<rbrakk>
  1052       \<Longrightarrow> \<not> AKcryptSK K authK evs"
  1053 apply (erule rev_mp)
  1054 apply (erule kerbIV.induct)
  1055 apply (frule_tac [7] K5_msg_in_parts_spies)
  1056 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
  1057 txt\<open>Fake\<close>
  1058 apply blast
  1059 txt\<open>K2: by freshness\<close>
  1060 apply (simp add: AKcryptSK_def)
  1061 txt\<open>K4\<close>
  1062 apply (blast+)
  1063 done
  1064 
  1065 text\<open>A secure serverkey cannot have been used to encrypt others\<close>
  1066 lemma servK_not_AKcryptSK:
  1067  "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs);
  1068      Key SK \<notin> analz (spies evs);  SK \<in> symKeys;
  1069      B \<noteq> Tgs;  evs \<in> kerbIV \<rbrakk>
  1070   \<Longrightarrow> \<not> AKcryptSK SK K evs"
  1071 apply (erule rev_mp)
  1072 apply (erule rev_mp)
  1073 apply (erule kerbIV.induct, analz_mono_contra)
  1074 apply (frule_tac [7] K5_msg_in_parts_spies)
  1075 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
  1076 txt\<open>K4\<close>
  1077 apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_keysFor new_keys_not_used parts.Fst parts.Snd Says_imp_knows_Spy [THEN parts.Inj] unique_CryptKey)
  1078 done
  1079 
  1080 text\<open>Long term keys are not issued as servKeys\<close>
  1081 lemma shrK_not_AKcryptSK:
  1082      "evs \<in> kerbIV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
  1083 apply (unfold AKcryptSK_def)
  1084 apply (erule kerbIV.induct)
  1085 apply (frule_tac [7] K5_msg_in_parts_spies)
  1086 apply (frule_tac [5] K3_msg_in_parts_spies, auto)
  1087 done
  1088 
  1089 text\<open>The Tgs message associates servK with authK and therefore not with any
  1090   other key authK.\<close>
  1091 lemma Says_Tgs_AKcryptSK:
  1092      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>)
  1093            \<in> set evs;
  1094          authK' \<noteq> authK;  evs \<in> kerbIV \<rbrakk>
  1095       \<Longrightarrow> \<not> AKcryptSK authK' servK evs"
  1096 apply (unfold AKcryptSK_def)
  1097 apply (blast dest: unique_servKeys)
  1098 done
  1099 
  1100 text\<open>Equivalently\<close>
  1101 lemma not_different_AKcryptSK:
  1102      "\<lbrakk> AKcryptSK authK servK evs;
  1103         authK' \<noteq> authK;  evs \<in> kerbIV \<rbrakk>
  1104       \<Longrightarrow> \<not> AKcryptSK authK' servK evs  \<and> servK \<in> symKeys"
  1105 apply (simp add: AKcryptSK_def)
  1106 apply (blast dest: unique_servKeys Says_Tgs_message_form)
  1107 done
  1108 
  1109 lemma AKcryptSK_not_AKcryptSK:
  1110      "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbIV \<rbrakk>
  1111       \<Longrightarrow> \<not> AKcryptSK servK K evs"
  1112 apply (erule rev_mp)
  1113 apply (erule kerbIV.induct)
  1114 apply (frule_tac [7] K5_msg_in_parts_spies)
  1115 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
  1116 apply (metis Auth_fresh_not_AKcryptSK Says_imp_spies authK_not_AKcryptSK 
  1117              authKeys_used authTicket_crypt_authK parts.Fst parts.Inj)
  1118 done
  1119 
  1120 text\<open>The only session keys that can be found with the help of session keys are
  1121   those sent by Tgs in step K4.\<close>
  1122 
  1123 text\<open>We take some pains to express the property
  1124   as a logical equivalence so that the simplifier can apply it.\<close>
  1125 lemma Key_analz_image_Key_lemma:
  1126      "P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
  1127       \<Longrightarrow>
  1128       P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
  1129 by (blast intro: analz_mono [THEN subsetD])
  1130 
  1131 
  1132 lemma AKcryptSK_analz_insert:
  1133      "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV \<rbrakk>
  1134       \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
  1135 apply (simp add: AKcryptSK_def, clarify)
  1136 apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
  1137 done
  1138 
  1139 lemma authKeys_are_not_AKcryptSK:
  1140      "\<lbrakk> K \<in> authKeys evs Un range shrK;  evs \<in> kerbIV \<rbrakk>
  1141       \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
  1142 apply (simp add: authKeys_def AKcryptSK_def)
  1143 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
  1144 done
  1145 
  1146 lemma not_authKeys_not_AKcryptSK:
  1147      "\<lbrakk> K \<notin> authKeys evs;
  1148          K \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
  1149       \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
  1150 apply (simp add: AKcryptSK_def)
  1151 apply (blast dest: Says_Tgs_message_form)
  1152 done
  1153 
  1154 
  1155 subsection\<open>Secrecy Theorems\<close>
  1156 
  1157 text\<open>For the Oops2 case of the next theorem\<close>
  1158 lemma Oops2_not_AKcryptSK:
  1159      "\<lbrakk> evs \<in> kerbIV;
  1160          Says Tgs A (Crypt authK
  1161                      \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1162            \<in> set evs \<rbrakk>
  1163       \<Longrightarrow> \<not> AKcryptSK servK SK evs"
  1164 by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
  1165    
  1166 text\<open>Big simplification law for keys SK that are not crypted by keys in KK
  1167  It helps prove three, otherwise hard, facts about keys. These facts are
  1168  exploited as simplification laws for analz, and also "limit the damage"
  1169  in case of loss of a key to the spy. See ESORICS98.
  1170  [simplified by LCP]\<close>
  1171 lemma Key_analz_image_Key [rule_format (no_asm)]:
  1172      "evs \<in> kerbIV \<Longrightarrow>
  1173       (\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
  1174        (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs)   \<longrightarrow>
  1175        (Key SK \<in> analz (Key`KK Un (spies evs))) =
  1176        (SK \<in> KK | Key SK \<in> analz (spies evs)))"
  1177 apply (erule kerbIV.induct)
  1178 apply (frule_tac [10] Oops_range_spies2)
  1179 apply (frule_tac [9] Oops_range_spies1)
  1180 apply (frule_tac [7] Says_tgs_message_form)
  1181 apply (frule_tac [5] Says_kas_message_form)
  1182 apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
  1183 txt\<open>Case-splits for Oops1 and message 5: the negated case simplifies using
  1184  the induction hypothesis\<close>
  1185 apply (case_tac [11] "AKcryptSK authK SK evsO1")
  1186 apply (case_tac [8] "AKcryptSK servK SK evs5")
  1187 apply (simp_all del: image_insert
  1188         add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
  1189              Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
  1190        Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
  1191 txt\<open>Fake\<close> 
  1192 apply spy_analz
  1193 txt\<open>K2\<close>
  1194 apply blast 
  1195 txt\<open>K3\<close>
  1196 apply blast 
  1197 txt\<open>K4\<close>
  1198 apply (blast dest!: authK_not_AKcryptSK)
  1199 txt\<open>K5\<close>
  1200 apply (case_tac "Key servK \<in> analz (spies evs5) ")
  1201 txt\<open>If servK is compromised then the result follows directly...\<close>
  1202 apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
  1203 txt\<open>...therefore servK is uncompromised.\<close>
  1204 txt\<open>The AKcryptSK servK SK evs5 case leads to a contradiction.\<close>
  1205 apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
  1206 txt\<open>Another K5 case\<close>
  1207 apply blast 
  1208 txt\<open>Oops1\<close>
  1209 apply simp 
  1210 apply (blast dest!: AKcryptSK_analz_insert)
  1211 done
  1212 
  1213 text\<open>First simplification law for analz: no session keys encrypt
  1214 authentication keys or shared keys.\<close>
  1215 lemma analz_insert_freshK1:
  1216      "\<lbrakk> evs \<in> kerbIV;  K \<in> authKeys evs Un range shrK;
  1217         SesKey \<notin> range shrK \<rbrakk>
  1218       \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
  1219           (K = SesKey | Key K \<in> analz (spies evs))"
  1220 apply (frule authKeys_are_not_AKcryptSK, assumption)
  1221 apply (simp del: image_insert
  1222             add: analz_image_freshK_simps add: Key_analz_image_Key)
  1223 done
  1224 
  1225 
  1226 text\<open>Second simplification law for analz: no service keys encrypt any other keys.\<close>
  1227 lemma analz_insert_freshK2:
  1228      "\<lbrakk> evs \<in> kerbIV;  servK \<notin> (authKeys evs); servK \<notin> range shrK;
  1229         K \<in> symKeys \<rbrakk>
  1230       \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
  1231           (K = servK | Key K \<in> analz (spies evs))"
  1232 apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
  1233 apply (simp del: image_insert
  1234             add: analz_image_freshK_simps add: Key_analz_image_Key)
  1235 done
  1236 
  1237 
  1238 text\<open>Third simplification law for analz: only one authentication key encrypts a certain service key.\<close>
  1239 
  1240 lemma analz_insert_freshK3:
  1241  "\<lbrakk> AKcryptSK authK servK evs;
  1242     authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
  1243         \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
  1244                 (servK = authK' | Key servK \<in> analz (spies evs))"
  1245 apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
  1246 apply (simp del: image_insert
  1247             add: analz_image_freshK_simps add: Key_analz_image_Key)
  1248 done
  1249 
  1250 lemma analz_insert_freshK3_bis:
  1251  "\<lbrakk> Says Tgs A
  1252             (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1253         \<in> set evs; 
  1254      authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
  1255         \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
  1256                 (servK = authK' | Key servK \<in> analz (spies evs))"
  1257 apply (frule AKcryptSKI, assumption)
  1258 apply (simp add: analz_insert_freshK3)
  1259 done
  1260 
  1261 text\<open>a weakness of the protocol\<close>
  1262 lemma authK_compromises_servK:
  1263      "\<lbrakk> Says Tgs A
  1264               (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1265            \<in> set evs;  authK \<in> symKeys;
  1266          Key authK \<in> analz (spies evs); evs \<in> kerbIV \<rbrakk>
  1267       \<Longrightarrow> Key servK \<in> analz (spies evs)"
  1268   by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
  1269 
  1270 lemma servK_notin_authKeysD:
  1271      "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts,
  1272                       Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
  1273            \<in> parts (spies evs);
  1274          Key servK \<notin> analz (spies evs);
  1275          B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1276       \<Longrightarrow> servK \<notin> authKeys evs"
  1277 apply (erule rev_mp)
  1278 apply (erule rev_mp)
  1279 apply (simp add: authKeys_def)
  1280 apply (erule kerbIV.induct, analz_mono_contra)
  1281 apply (frule_tac [7] K5_msg_in_parts_spies)
  1282 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
  1283 apply (blast+)
  1284 done
  1285 
  1286 
  1287 text\<open>If Spy sees the Authentication Key sent in msg K2, then
  1288     the Key has expired.\<close>
  1289 lemma Confidentiality_Kas_lemma [rule_format]:
  1290      "\<lbrakk> authK \<in> symKeys; A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1291       \<Longrightarrow> Says Kas A
  1292                (Crypt (shrK A)
  1293                   \<lbrace>Key authK, Agent Tgs, Number Ta,
  1294           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
  1295             \<in> set evs \<longrightarrow>
  1296           Key authK \<in> analz (spies evs) \<longrightarrow>
  1297           expiredAK Ta evs"
  1298 apply (erule kerbIV.induct)
  1299 apply (frule_tac [10] Oops_range_spies2)
  1300 apply (frule_tac [9] Oops_range_spies1)
  1301 apply (frule_tac [7] Says_tgs_message_form)
  1302 apply (frule_tac [5] Says_kas_message_form)
  1303 apply (safe del: impI conjI impCE)
  1304 apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
  1305 txt\<open>Fake\<close>
  1306 apply spy_analz
  1307 txt\<open>K2\<close>
  1308 apply blast
  1309 txt\<open>K4\<close>
  1310 apply blast
  1311 txt\<open>Level 8: K5\<close>
  1312 apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
  1313 txt\<open>Oops1\<close>
  1314 apply (blast dest!: unique_authKeys intro: less_SucI)
  1315 txt\<open>Oops2\<close>
  1316 apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
  1317 done
  1318 
  1319 lemma Confidentiality_Kas:
  1320      "\<lbrakk> Says Kas A
  1321               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
  1322            \<in> set evs;
  1323          \<not> expiredAK Ta evs;
  1324          A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1325       \<Longrightarrow> Key authK \<notin> analz (spies evs)"
  1326 by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
  1327 
  1328 text\<open>If Spy sees the Service Key sent in msg K4, then
  1329     the Key has expired.\<close>
  1330 
  1331 lemma Confidentiality_lemma [rule_format]:
  1332      "\<lbrakk> Says Tgs A
  1333             (Crypt authK
  1334                \<lbrace>Key servK, Agent B, Number Ts,
  1335                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
  1336            \<in> set evs;
  1337         Key authK \<notin> analz (spies evs);
  1338         servK \<in> symKeys;
  1339         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1340       \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
  1341           expiredSK Ts evs"
  1342 apply (erule rev_mp)
  1343 apply (erule rev_mp)
  1344 apply (erule kerbIV.induct)
  1345 apply (rule_tac [9] impI)+
  1346   \<comment>\<open>The Oops1 case is unusual: must simplify
  1347     @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
  1348    \<open>analz_mono_contra\<close> weaken it to
  1349    @{term "Authkey \<notin> analz (spies evs)"},
  1350   for we then conclude @{term "authK \<noteq> authKa"}.\<close>
  1351 apply analz_mono_contra
  1352 apply (frule_tac [10] Oops_range_spies2)
  1353 apply (frule_tac [9] Oops_range_spies1)
  1354 apply (frule_tac [7] Says_tgs_message_form)
  1355 apply (frule_tac [5] Says_kas_message_form)
  1356 apply (safe del: impI conjI impCE)
  1357 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)
  1358 txt\<open>Fake\<close>
  1359      apply spy_analz
  1360 txt\<open>K2\<close>
  1361     apply (blast intro: parts_insertI less_SucI)
  1362 txt\<open>K4\<close>
  1363    apply (blast dest: authTicket_authentic Confidentiality_Kas)
  1364 txt\<open>K5\<close>
  1365   apply (metis Says_imp_spies Says_ticket_parts Tgs_not_bad analz_insert_freshK2 
  1366              less_SucI parts.Inj servK_notin_authKeysD unique_CryptKey)
  1367 txt\<open>Oops1\<close> 
  1368  apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
  1369 txt\<open>Oops2\<close>
  1370 apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
  1371 done
  1372 
  1373 
  1374 text\<open>In the real world Tgs can't check wheter authK is secure!\<close>
  1375 lemma Confidentiality_Tgs:
  1376      "\<lbrakk> Says Tgs A
  1377               (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1378            \<in> set evs;
  1379          Key authK \<notin> analz (spies evs);
  1380          \<not> expiredSK Ts evs;
  1381          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1382       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1383 by (blast dest: Says_Tgs_message_form Confidentiality_lemma)
  1384 
  1385 text\<open>In the real world Tgs CAN check what Kas sends!\<close>
  1386 lemma Confidentiality_Tgs_bis:
  1387      "\<lbrakk> Says Kas A
  1388                (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
  1389            \<in> set evs;
  1390          Says Tgs A
  1391               (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1392            \<in> set evs;
  1393          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1394          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1395       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1396 by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
  1397 
  1398 text\<open>Most general form\<close>
  1399 lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
  1400 
  1401 lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]
  1402 
  1403 text\<open>Needs a confidentiality guarantee, hence moved here.
  1404       Authenticity of servK for A\<close>
  1405 lemma servK_authentic_bis_r:
  1406      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1407            \<in> parts (spies evs);
  1408          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1409            \<in> parts (spies evs);
  1410          \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1411  \<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1412        \<in> set evs"
  1413 by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
  1414 
  1415 lemma Confidentiality_Serv_A:
  1416      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1417            \<in> parts (spies evs);
  1418          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1419            \<in> parts (spies evs);
  1420          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1421          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1422       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1423 apply (drule authK_authentic, assumption, assumption)
  1424 apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
  1425 done
  1426 
  1427 lemma Confidentiality_B:
  1428      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1429            \<in> parts (spies evs);
  1430          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1431            \<in> parts (spies evs);
  1432          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1433            \<in> parts (spies evs);
  1434          \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
  1435          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1436       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1437 apply (frule authK_authentic)
  1438 apply (frule_tac [3] Confidentiality_Kas)
  1439 apply (frule_tac [6] servTicket_authentic, auto)
  1440 apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
  1441 done
  1442 (*
  1443 The proof above is fast.  It can be done in one command in 17 secs:
  1444 apply (blast dest: authK_authentic servK_authentic
  1445                                Says_Kas_message_form servTicket_authentic
  1446                                unique_servKeys unique_authKeys
  1447                                Confidentiality_Kas
  1448                                Confidentiality_Tgs_bis)
  1449 It is very brittle: we can't use this command partway
  1450 through the script above.
  1451 *)
  1452 
  1453 lemma u_Confidentiality_B:
  1454      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1455            \<in> parts (spies evs);
  1456          \<not> expiredSK Ts evs;
  1457          A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1458       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
  1459 by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
  1460 
  1461 
  1462 
  1463 subsection\<open>Parties authentication: each party verifies "the identity of
  1464        another party who generated some data" (quoted from Neuman and Ts'o).\<close>
  1465 
  1466 text\<open>These guarantees don't assess whether two parties agree on
  1467          the same session key: sending a message containing a key
  1468          doesn't a priori state knowledge of the key.\<close>
  1469 
  1470 
  1471 text\<open>\<open>Tgs_authenticates_A\<close> can be found above\<close>
  1472 
  1473 lemma A_authenticates_Tgs:
  1474  "\<lbrakk> Says Kas A
  1475     (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
  1476      Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1477        \<in> parts (spies evs);
  1478      Key authK \<notin> analz (spies evs);
  1479      evs \<in> kerbIV \<rbrakk>
  1480  \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
  1481        \<in> set evs"
  1482 apply (frule Says_Kas_message_form, assumption)
  1483 apply (erule rev_mp)
  1484 apply (erule rev_mp)
  1485 apply (erule rev_mp)
  1486 apply (erule kerbIV.induct, analz_mono_contra)
  1487 apply (frule_tac [7] K5_msg_in_parts_spies)
  1488 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
  1489 txt\<open>K2\<close>
  1490 apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
  1491 txt\<open>K4\<close>
  1492 apply (blast dest!: unique_CryptKey)
  1493 done
  1494 
  1495 
  1496 lemma B_authenticates_A:
  1497      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
  1498         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1499            \<in> parts (spies evs);
  1500         Key servK \<notin> analz (spies evs);
  1501         A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1502  \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
  1503                Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
  1504 by (blast dest: servTicket_authentic_Tgs intro: Says_K5)
  1505 
  1506 text\<open>The second assumption tells B what kind of key servK is.\<close>
  1507 lemma B_authenticates_A_r:
  1508      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
  1509          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1510            \<in> parts (spies evs);
  1511          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1512            \<in> parts (spies evs);
  1513          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1514            \<in> parts (spies evs);
  1515          \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
  1516          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1517    \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
  1518                   Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
  1519 by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
  1520 
  1521 text\<open>\<open>u_B_authenticates_A\<close> would be the same as \<open>B_authenticates_A\<close> because the servK confidentiality assumption is yet unrelaxed\<close>
  1522 
  1523 lemma u_B_authenticates_A_r:
  1524      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
  1525          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1526            \<in> parts (spies evs);
  1527          \<not> expiredSK Ts evs;
  1528          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1529    \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
  1530                   Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
  1531 by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
  1532 
  1533 lemma A_authenticates_B:
  1534      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
  1535          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1536            \<in> parts (spies evs);
  1537          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1538            \<in> parts (spies evs);
  1539          Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
  1540          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1541       \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
  1542 by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6)
  1543 
  1544 lemma A_authenticates_B_r:
  1545      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
  1546          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1547            \<in> parts (spies evs);
  1548          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1549            \<in> parts (spies evs);
  1550          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1551          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1552       \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
  1553 apply (frule authK_authentic)
  1554 apply (frule_tac [3] Says_Kas_message_form)
  1555 apply (frule_tac [4] Confidentiality_Kas)
  1556 apply (frule_tac [7] servK_authentic)
  1557 prefer 8 apply blast
  1558 apply (erule_tac [9] exE)
  1559 apply (frule_tac [9] K4_imp_K2)
  1560 apply assumption+
  1561 apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs
  1562 )
  1563 done
  1564 
  1565 
  1566 subsection\<open>Key distribution guarantees
  1567        An agent knows a session key if he used it to issue a cipher.
  1568        These guarantees also convey a stronger form of 
  1569        authentication - non-injective agreement on the session key\<close>
  1570 
  1571 
  1572 lemma Kas_Issues_A:
  1573    "\<lbrakk> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs;
  1574       evs \<in> kerbIV \<rbrakk>
  1575   \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 
  1576           on evs"
  1577 apply (simp (no_asm) add: Issues_def)
  1578 apply (rule exI)
  1579 apply (rule conjI, assumption)
  1580 apply (simp (no_asm))
  1581 apply (erule rev_mp)
  1582 apply (erule kerbIV.induct)
  1583 apply (frule_tac [5] Says_ticket_parts)
  1584 apply (frule_tac [7] Says_ticket_parts)
  1585 apply (simp_all (no_asm_simp) add: all_conj_distrib)
  1586 txt\<open>K2\<close>
  1587 apply (simp add: takeWhile_tail)
  1588 apply (blast dest: authK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD])
  1589 done
  1590 
  1591 lemma A_authenticates_and_keydist_to_Kas:
  1592   "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace> \<in> parts (spies evs);
  1593      A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1594  \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 
  1595           on evs"
  1596 by (blast dest: authK_authentic Kas_Issues_A)
  1597 
  1598 lemma honest_never_says_newer_timestamp_in_auth:
  1599      "\<lbrakk> (CT evs) \<le> T; A \<notin> bad; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 
  1600      \<Longrightarrow> \<forall> B Y.  Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
  1601 apply (erule rev_mp)
  1602 apply (erule kerbIV.induct)
  1603 apply force+
  1604 done
  1605 
  1606 lemma honest_never_says_current_timestamp_in_auth:
  1607      "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 
  1608      \<Longrightarrow> \<forall> A B Y. A \<notin> bad \<longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
  1609   by (metis eq_imp_le honest_never_says_newer_timestamp_in_auth)
  1610 
  1611 lemma A_trusts_secure_authenticator:
  1612     "\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs);
  1613        Key K \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk>
  1614 \<Longrightarrow> \<exists> B X. Says A Tgs \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>, Agent B\<rbrace> \<in> set evs \<or> 
  1615            Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs"
  1616 apply (erule rev_mp)
  1617 apply (erule rev_mp)
  1618 apply (erule kerbIV.induct, analz_mono_contra)
  1619 apply (frule_tac [5] Says_ticket_parts)
  1620 apply (frule_tac [7] Says_ticket_parts)
  1621 apply (simp_all add: all_conj_distrib)
  1622 apply blast+
  1623 done
  1624 
  1625 lemma A_Issues_Tgs:
  1626   "\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
  1627        \<in> set evs; 
  1628      Key authK \<notin> analz (spies evs);  
  1629      A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1630  \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
  1631 apply (simp (no_asm) add: Issues_def)
  1632 apply (rule exI)
  1633 apply (rule conjI, assumption)
  1634 apply (simp (no_asm))
  1635 apply (erule rev_mp)
  1636 apply (erule rev_mp)
  1637 apply (erule kerbIV.induct, analz_mono_contra)
  1638 apply (frule_tac [5] Says_ticket_parts)
  1639 apply (frule_tac [7] Says_ticket_parts)
  1640 apply (simp_all (no_asm_simp) add: all_conj_distrib)
  1641 txt\<open>fake\<close>
  1642 apply blast
  1643 txt\<open>K3\<close>
  1644 (*
  1645 apply clarify
  1646 apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption, assumption, assumption)
  1647 *)
  1648 apply (simp add: takeWhile_tail)
  1649 apply auto
  1650 apply (force dest!: authK_authentic Says_Kas_message_form)
  1651 apply (drule parts_spies_takeWhile_mono [THEN subsetD, THEN parts_spies_evs_revD2 [THEN subsetD]])
  1652 apply (drule A_trusts_secure_authenticator, assumption, assumption)
  1653 apply (simp add: honest_never_says_current_timestamp_in_auth)
  1654 done
  1655 
  1656 lemma Tgs_authenticates_and_keydist_to_A:
  1657   "\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 
  1658       Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
  1659            \<in> parts (spies evs);
  1660      Key authK \<notin> analz (spies evs);  
  1661      A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  1662  \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
  1663 by (blast dest: A_Issues_Tgs Tgs_authenticates_A)
  1664 
  1665 lemma Tgs_Issues_A:
  1666     "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>)
  1667          \<in> set evs; 
  1668        Key authK \<notin> analz (spies evs);  evs \<in> kerbIV \<rbrakk>
  1669   \<Longrightarrow> Tgs Issues A with 
  1670           (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
  1671 apply (simp (no_asm) add: Issues_def)
  1672 apply (rule exI)
  1673 apply (rule conjI, assumption)
  1674 apply (simp (no_asm))
  1675 apply (erule rev_mp)
  1676 apply (erule rev_mp)
  1677 apply (erule kerbIV.induct, analz_mono_contra)
  1678 apply (frule_tac [5] Says_ticket_parts)
  1679 apply (frule_tac [7] Says_ticket_parts)
  1680 apply (simp_all (no_asm_simp) add: all_conj_distrib)
  1681 txt\<open>K4\<close>
  1682 apply (simp add: takeWhile_tail)
  1683 (*Last two thms installed only to derive authK \<notin> range shrK*)
  1684 apply (metis knows_Spy_partsEs(2) parts.Fst usedI used_evs_rev used_takeWhile_used)
  1685 done
  1686 
  1687 lemma A_authenticates_and_keydist_to_Tgs:
  1688 "\<lbrakk>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> \<in> parts (spies evs);
  1689   Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1690  \<Longrightarrow> \<exists>A. Tgs Issues A with 
  1691           (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
  1692 by (blast dest: Tgs_Issues_A servK_authentic_bis)
  1693 
  1694 
  1695 
  1696 lemma B_Issues_A:
  1697      "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
  1698          Key servK \<notin> analz (spies evs);
  1699          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1700       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
  1701 apply (simp (no_asm) add: Issues_def)
  1702 apply (rule exI)
  1703 apply (rule conjI, assumption)
  1704 apply (simp (no_asm))
  1705 apply (erule rev_mp)
  1706 apply (erule rev_mp)
  1707 apply (erule kerbIV.induct, analz_mono_contra)
  1708 apply (frule_tac [5] Says_ticket_parts)
  1709 apply (frule_tac [7] Says_ticket_parts)
  1710 apply (simp_all (no_asm_simp) add: all_conj_distrib)
  1711 apply blast
  1712 txt\<open>K6 requires numerous lemmas\<close>
  1713 apply (simp add: takeWhile_tail)
  1714 apply (blast dest: servTicket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: Says_K6)
  1715 done
  1716 
  1717 lemma B_Issues_A_r:
  1718      "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
  1719          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1720             \<in> parts (spies evs);
  1721          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1722             \<in> parts (spies evs);
  1723          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1724            \<in> parts (spies evs);
  1725          \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
  1726          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1727       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
  1728 by (blast dest!: Confidentiality_B B_Issues_A)
  1729 
  1730 lemma u_B_Issues_A_r:
  1731      "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
  1732          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1733             \<in> parts (spies evs);
  1734          \<not> expiredSK Ts evs;
  1735          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1736       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
  1737 by (blast dest!: u_Confidentiality_B B_Issues_A)
  1738 
  1739 lemma A_authenticates_and_keydist_to_B:
  1740      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
  1741          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1742            \<in> parts (spies evs);
  1743          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1744            \<in> parts (spies evs);
  1745          Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
  1746          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1747       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
  1748 by (blast dest!: A_authenticates_B B_Issues_A)
  1749 
  1750 lemma A_authenticates_and_keydist_to_B_r:
  1751      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
  1752          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1753            \<in> parts (spies evs);
  1754          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1755            \<in> parts (spies evs);
  1756          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1757          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  1758       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
  1759 by (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A)
  1760 
  1761 
  1762 lemma A_Issues_B:
  1763      "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace>
  1764            \<in> set evs;
  1765          Key servK \<notin> analz (spies evs);
  1766          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1767    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
  1768 apply (simp (no_asm) add: Issues_def)
  1769 apply (rule exI)
  1770 apply (rule conjI, assumption)
  1771 apply (simp (no_asm))
  1772 apply (erule rev_mp)
  1773 apply (erule rev_mp)
  1774 apply (erule kerbIV.induct, analz_mono_contra)
  1775 apply (frule_tac [5] Says_ticket_parts)
  1776 apply (frule_tac [7] Says_ticket_parts)
  1777 apply (simp_all (no_asm_simp))
  1778 apply clarify
  1779 txt\<open>K5\<close>
  1780 apply auto
  1781 apply (simp add: takeWhile_tail)
  1782 txt\<open>Level 15: case analysis necessary because the assumption doesn't state
  1783   the form of servTicket. The guarantee becomes stronger.\<close>
  1784 apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
  1785                    K3_imp_K2 servK_authentic_ter
  1786                    parts_spies_takeWhile_mono [THEN subsetD]
  1787                    parts_spies_evs_revD2 [THEN subsetD]
  1788              intro: Says_K5)
  1789 apply (simp add: takeWhile_tail)
  1790 done
  1791 
  1792 lemma A_Issues_B_r:
  1793      "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace>
  1794            \<in> set evs;
  1795          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1796            \<in> parts (spies evs);
  1797          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1798            \<in> parts (spies evs);
  1799          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
  1800          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1801    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
  1802 by (blast dest!: Confidentiality_Serv_A A_Issues_B)
  1803 
  1804 lemma B_authenticates_and_keydist_to_A:
  1805      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
  1806          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1807            \<in> parts (spies evs);
  1808          Key servK \<notin> analz (spies evs);
  1809          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1810    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
  1811 by (blast dest: B_authenticates_A A_Issues_B)
  1812 
  1813 lemma B_authenticates_and_keydist_to_A_r:
  1814      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
  1815          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1816            \<in> parts (spies evs);
  1817          Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
  1818            \<in> parts (spies evs);
  1819          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
  1820            \<in> parts (spies evs);
  1821          \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
  1822          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1823    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
  1824 by (blast dest: B_authenticates_A Confidentiality_B A_Issues_B)
  1825 
  1826 text\<open>\<open>u_B_authenticates_and_keydist_to_A\<close> would be the same as \<open>B_authenticates_and_keydist_to_A\<close> because the
  1827  servK confidentiality assumption is yet unrelaxed\<close>
  1828 
  1829 lemma u_B_authenticates_and_keydist_to_A_r:
  1830      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
  1831          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
  1832            \<in> parts (spies evs);
  1833          \<not> expiredSK Ts evs;
  1834          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
  1835    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
  1836 by (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B)
  1837 
  1838 end