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