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