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