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