Theory KerberosIV_Gets

(*  Title:      HOL/Auth/KerberosIV_Gets.thy
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

sectionThe Kerberos Protocol, Version IV

theory KerberosIV_Gets imports Public begin

textThe "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.

abbreviation
  Kas :: agent where "Kas == Server"

abbreviation
  Tgs :: agent where "Tgs == Friend 0"


axiomatization where
  Tgs_not_bad [iff]: "Tgs  bad"
   ― ‹Tgs is secure --- we already know that Kas is secure

definition
 (* authKeys are those contained in an authTicket *)
    authKeys :: "event list  key set" where
    "authKeys evs = {authK. A Peer Ta. Says Kas A
                        (Crypt (shrK A) Key authK, Agent Peer, Number Ta,
               (Crypt (shrK Peer) Agent A, Agent Peer, Key authK, Number Ta)
                  )  set evs}"

definition
 (* States than an event really appears only once on a trace *)
  Unique :: "[event, event list]  bool" ("Unique _ on _" [0, 50] 50)
  where "(Unique ev on evs) = (ev  set (tl (dropWhile (λz. z  ev) evs)))"


consts
    (*Duration of the authentication key*)
    authKlife   :: nat

    (*Duration of the service key*)
    servKlife   :: nat

    (*Duration of an authenticator*)
    authlife   :: nat

    (*Upper bound on the time of reaction of a server*)
    replylife   :: nat

specification (authKlife)
  authKlife_LB [iff]: "2  authKlife"
    by blast

specification (servKlife)
  servKlife_LB [iff]: "2 + authKlife  servKlife"
    by blast

specification (authlife)
  authlife_LB [iff]: "Suc 0  authlife"
    by blast

specification (replylife)
  replylife_LB [iff]: "Suc 0  replylife"
    by blast

abbreviation
  (*The current time is just the length of the trace!*)
  CT :: "event list  nat" where
  "CT == length"

abbreviation
  expiredAK :: "[nat, event list]  bool" where
  "expiredAK Ta evs == authKlife + Ta < CT evs"

abbreviation
  expiredSK :: "[nat, event list]  bool" where
  "expiredSK Ts evs == servKlife + Ts < CT evs"

abbreviation
  expiredA :: "[nat, event list]  bool" where
  "expiredA T evs == authlife + T < CT evs"

abbreviation
  valid :: "[nat, nat]  bool" ("valid _ wrt _" [0, 50] 50) where
  "valid T1 wrt T2 == T1  replylife + T2"

(*---------------------------------------------------------------------*)


(* Predicate formalising the association between authKeys and servKeys *)
definition AKcryptSK :: "[key, key, event list]  bool" where
  "AKcryptSK authK servK evs ==
     A B Ts.
       Says Tgs A (Crypt authK
                     Key servK, Agent B, Number Ts,
                       Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts )
          set evs"

inductive_set "kerbIV_gets" :: "event list set"
  where

   Nil:  "[]  kerbIV_gets"

 | Fake: " evsf  kerbIV_gets;  X  synth (analz (spies evsf)) 
           Says Spy B X  # evsf  kerbIV_gets"

 | Reception: " evsr  kerbIV_gets;  Says A B X  set evsr 
                 Gets B X # evsr  kerbIV_gets"

(* FROM the initiator *)
 | K1:   " evs1  kerbIV_gets 
           Says A Kas Agent A, Agent Tgs, Number (CT evs1) # evs1
           kerbIV_gets"

(* Adding the timestamp serves to A in K3 to check that
   she doesn't get a reply too late. This kind of timeouts are ordinary.
   If a server's reply is late, then it is likely to be fake. *)

(*---------------------------------------------------------------------*)

(*FROM Kas *)
 | K2:  " evs2  kerbIV_gets; Key authK  used evs2; authK  symKeys;
            Gets Kas Agent A, Agent Tgs, Number T1  set evs2 
           Says Kas A
                (Crypt (shrK A) Key authK, Agent Tgs, Number (CT evs2),
                      (Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK,
                          Number (CT evs2))) # evs2  kerbIV_gets"
(*
  The internal encryption builds the authTicket.
  The timestamp doesn't change inside the two encryptions: the external copy
  will be used by the initiator in K3; the one inside the
  authTicket by Tgs in K4.
*)

(*---------------------------------------------------------------------*)

(* FROM the initiator *)
 | K3:  " evs3  kerbIV_gets;
            Says A Kas Agent A, Agent Tgs, Number T1  set evs3;
            Gets A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
              authTicket)  set evs3;
            valid Ta wrt T1
         
           Says A Tgs authTicket,
                           (Crypt authK Agent A, Number (CT evs3)),
                           Agent B # evs3  kerbIV_gets"
(*The two events amongst the premises allow A to accept only those authKeys
  that are not issued late. *)

(*---------------------------------------------------------------------*)

(* FROM Tgs *)
(* Note that the last temporal check is not mentioned in the original MIT
   specification. Adding it makes many goals "available" to the peers. 
   Theorems that exploit it have the suffix `_u', which stands for updated 
   protocol.
*)
 | K4:  " evs4  kerbIV_gets; Key servK  used evs4; servK  symKeys;
            B  Tgs;  authK  symKeys;
            Gets Tgs 
             (Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK,
                                 Number Ta),
             (Crypt authK Agent A, Number T2), Agent B
                 set evs4;
            ¬ expiredAK Ta evs4;
            ¬ expiredA T2 evs4;
            servKlife + (CT evs4)  authKlife + Ta
         
           Says Tgs A
                (Crypt authK Key servK, Agent B, Number (CT evs4),
                               Crypt (shrK B) Agent A, Agent B, Key servK,
                                                Number (CT evs4) )
                # evs4  kerbIV_gets"
(* Tgs creates a new session key per each request for a service, without
   checking if there is still a fresh one for that service.
   The cipher under Tgs' key is the authTicket, the cipher under B's key
   is the servTicket, which is built now.
   NOTE that the last temporal check is not present in the MIT specification.

*)

(*---------------------------------------------------------------------*)

(* FROM the initiator *)
 | K5:  " evs5  kerbIV_gets; authK  symKeys; servK  symKeys;
            Says A Tgs
                authTicket, Crypt authK Agent A, Number T2,
                  Agent B
               set evs5;
            Gets A
             (Crypt authK Key servK, Agent B, Number Ts, servTicket)
                 set evs5;
            valid Ts wrt T2 
           Says A B servTicket,
                         Crypt servK Agent A, Number (CT evs5) 
               # evs5  kerbIV_gets"
(* Checks similar to those in K3. *)

(*---------------------------------------------------------------------*)

(* FROM the responder*)
  | K6:  " evs6  kerbIV_gets;
            Gets B 
              (Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts),
              (Crypt servK Agent A, Number T3)
             set evs6;
            ¬ expiredSK Ts evs6;
            ¬ expiredA T3 evs6
         
           Says B A (Crypt servK (Number T3))
               # evs6  kerbIV_gets"
(* Checks similar to those in K4. *)

(*---------------------------------------------------------------------*)

(* Leaking an authK... *)
 | Oops1: " evsO1  kerbIV_gets;  A  Spy;
              Says Kas A
                (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
                                  authTicket)   set evsO1;
              expiredAK Ta evsO1 
           Says A Spy Agent A, Agent Tgs, Number Ta, Key authK
               # evsO1  kerbIV_gets"

(*---------------------------------------------------------------------*)

(*Leaking a servK... *)
 | Oops2: " evsO2  kerbIV_gets;  A  Spy;
              Says Tgs A
                (Crypt authK Key servK, Agent B, Number Ts, servTicket)
                    set evsO2;
              expiredSK Ts evsO2 
           Says A Spy Agent A, Agent B, Number Ts, Key servK
               # evsO2  kerbIV_gets"

(*---------------------------------------------------------------------*)

declare Says_imp_knows_Spy [THEN parts.Inj, dest]
declare parts.Body [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]

subsectionLemmas about reception event

lemma Gets_imp_Says :
     " Gets B X  set evs; evs  kerbIV_gets   A. Says A B X  set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply auto
done

lemma Gets_imp_knows_Spy: 
     " Gets B X  set evs; evs  kerbIV_gets    X  knows Spy evs"
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)

(*Needed for force to work for example in new_keys_not_used*)
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]

lemma Gets_imp_knows:
     " Gets B X  set evs; evs  kerbIV_gets    X  knows B evs"
by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)

subsectionLemmas about termauthKeys

lemma authKeys_empty: "authKeys [] = {}"
by (simp add: authKeys_def)

lemma authKeys_not_insert:
 "(A Ta akey Peer.
   ev  Says Kas A (Crypt (shrK A) akey, Agent Peer, Ta,
              (Crypt (shrK Peer) Agent A, Agent Peer, akey, Ta)))
        authKeys (ev # evs) = authKeys evs"
by (unfold authKeys_def, auto)

lemma authKeys_insert:
  "authKeys
     (Says Kas A (Crypt (shrK A) Key K, Agent Peer, Number Ta,
      (Crypt (shrK Peer) Agent A, Agent Peer, Key K, Number Ta)) # evs)
       = insert K (authKeys evs)"
by (unfold authKeys_def, auto)

lemma authKeys_simp:
   "K  authKeys
    (Says Kas A (Crypt (shrK A) Key K', Agent Peer, Number Ta,
     (Crypt (shrK Peer) Agent A, Agent Peer, Key K', Number Ta)) # evs)
         K = K' | K  authKeys evs"
by (unfold authKeys_def, auto)

lemma authKeysI:
   "Says Kas A (Crypt (shrK A) Key K, Agent Tgs, Number Ta,
     (Crypt (shrK Tgs) Agent A, Agent Tgs, Key K, Number Ta))  set evs
         K  authKeys evs"
by (unfold authKeys_def, auto)

lemma authKeys_used: "K  authKeys evs  Key K  used evs"
by (simp add: authKeys_def, blast)


subsectionForwarding Lemmas

lemma Says_ticket_parts:
     "Says S A (Crypt K SesKey, B, TimeStamp, Ticket)  set evs
       Ticket  parts (spies evs)"
by blast

lemma Gets_ticket_parts:
     "Gets A (Crypt K SesKey, Peer, Ta, Ticket)  set evs; evs  kerbIV_gets 
       Ticket  parts (spies evs)"
by (blast dest: Gets_imp_knows_Spy [THEN parts.Inj])

lemma Oops_range_spies1:
     " Says Kas A (Crypt KeyA Key authK, Peer, Ta, authTicket)
            set evs ;
         evs  kerbIV_gets   authK  range shrK  authK  symKeys"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, auto)
done

lemma Oops_range_spies2:
     " Says Tgs A (Crypt authK Key servK, Agent B, Ts, servTicket)
            set evs ;
         evs  kerbIV_gets   servK  range shrK  servK  symKeys"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, auto)
done


(*Spy never sees another agent's shared key! (unless it's lost at start)*)
lemma Spy_see_shrK [simp]:
     "evs  kerbIV_gets  (Key (shrK A)  parts (spies evs)) = (A  bad)"
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
apply (blast+)
done

lemma Spy_analz_shrK [simp]:
     "evs  kerbIV_gets  (Key (shrK A)  analz (spies evs)) = (A  bad)"
by auto

lemma Spy_see_shrK_D [dest!]:
     " Key (shrK A)  parts (spies evs);  evs  kerbIV_gets   Abad"
by (blast dest: Spy_see_shrK)
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]

textNobody can have used non-existent keys!
lemma new_keys_not_used [simp]:
    "Key K  used evs; K  symKeys; evs  kerbIV_gets
      K  keysFor (parts (spies evs))"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake
apply (force dest!: keysFor_parts_insert)
txtOthers
apply (force dest!: analz_shrK_Decrypt)+
done

(*Earlier, all protocol proofs declared this theorem.
  But few of them actually need it! (Another is Yahalom) *)
lemma new_keys_not_analzd:
 "evs  kerbIV_gets; K  symKeys; Key K  used evs
   K  keysFor (analz (spies evs))"
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])


subsectionRegularity Lemmas
textThese concern the form of items passed in messages

textDescribes the form of all components sent by Kas

lemma Says_Kas_message_form:
     " Says Kas A (Crypt K Key authK, Agent Peer, Number Ta, authTicket)
            set evs;
         evs  kerbIV_gets    
  K = shrK A   Peer = Tgs 
  authK  range shrK  authK  authKeys evs  authK  symKeys  
  authTicket = (Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (simp_all (no_asm) add: authKeys_def authKeys_insert)
apply blast+
done


lemma SesKey_is_session_key:
     " Crypt (shrK Tgs_B) Agent A, Agent Tgs_B, Key SesKey, Number T
             parts (spies evs); Tgs_B  bad;
         evs  kerbIV_gets 
       SesKey  range shrK"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
done

lemma authTicket_authentic:
     " Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta
            parts (spies evs);
         evs  kerbIV_gets 
       Says Kas A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
                 Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
             set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake, K4
apply (blast+)
done

lemma authTicket_crypt_authK:
     " Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta
            parts (spies evs);
         evs  kerbIV_gets 
       authK  authKeys evs"
apply (frule authTicket_authentic, assumption)
apply (simp (no_asm) add: authKeys_def)
apply blast
done

lemma Says_Tgs_message_form:
     " Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
            set evs;
         evs  kerbIV_gets 
   B  Tgs  
      authK  range shrK  authK  authKeys evs  authK  symKeys 
      servK  range shrK  servK  authKeys evs  servK  symKeys 
      servTicket = (Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts)"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast, auto)
txtThree subcases of Message 4
apply (blast dest!: SesKey_is_session_key)
apply (blast dest: authTicket_crypt_authK)
apply (blast dest!: authKeys_used Says_Kas_message_form)
done


lemma authTicket_form:
     " Crypt (shrK A) Key authK, Agent Tgs, Ta, authTicket
            parts (spies evs);
         A  bad;
         evs  kerbIV_gets 
     authK  range shrK  authK  symKeys 
        authTicket = Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Ta"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
apply blast+
done

textThis form holds also over an authTicket, but is not needed below.
lemma servTicket_form:
     " Crypt authK Key servK, Agent B, Ts, servTicket
               parts (spies evs);
            Key authK  analz (spies evs);
            evs  kerbIV_gets 
          servK  range shrK  servK  symKeys  
    (A. servTicket = Crypt (shrK B) Agent A, Agent B, Key servK, Ts)"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
done

textEssentially the same as authTicket_form›
lemma Says_kas_message_form:
     " Gets A (Crypt (shrK A)
              Key authK, Agent Tgs, Ta, authTicket)  set evs;
         evs  kerbIV_gets 
       authK  range shrK  authK  symKeys  
          authTicket =
                  Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Ta
          | authTicket  analz (spies evs)"
by (blast dest: analz_shrK_Decrypt authTicket_form
                Gets_imp_knows_Spy [THEN analz.Inj])

lemma Says_tgs_message_form:
 " Gets A (Crypt authK Key servK, Agent B, Ts, servTicket)
        set evs;  authK  symKeys;
     evs  kerbIV_gets 
   servK  range shrK 
      (A. servTicket =
              Crypt (shrK B) Agent A, Agent B, Key servK, Ts)
       | servTicket  analz (spies evs)"
apply (frule Gets_imp_knows_Spy [THEN analz.Inj], auto)
 apply (force dest!: servTicket_form)
apply (frule analz_into_parts)
apply (frule servTicket_form, auto)
done


subsectionAuthenticity theorems: confirm origin of sensitive messages

lemma authK_authentic:
     " Crypt (shrK A) Key authK, Peer, Ta, authTicket
            parts (spies evs);
         A  bad;  evs  kerbIV_gets 
       Says Kas A (Crypt (shrK A) Key authK, Peer, Ta, authTicket)
             set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake
apply blast
txtK4
apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
done

textIf a certain encrypted message appears then it originated with Tgs
lemma servK_authentic:
     " Crypt authK Key servK, Agent B, Number Ts, servTicket
            parts (spies evs);
         Key authK  analz (spies evs);
         authK  range shrK;
         evs  kerbIV_gets 
  A. Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake
apply blast
txtK2
apply blast
txtK4
apply auto
done

lemma servK_authentic_bis:
     " Crypt authK Key servK, Agent B, Number Ts, servTicket
            parts (spies evs);
         Key authK  analz (spies evs);
         B  Tgs;
         evs  kerbIV_gets 
  A. Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake
apply blast
txtK4
apply blast
done

textAuthenticity of servK for B
lemma servTicket_authentic_Tgs:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs); B  Tgs;  B  bad;
         evs  kerbIV_gets 
  authK.
       Says Tgs A (Crypt authK Key servK, Agent B, Number Ts,
                   Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts)
        set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
apply blast+
done

textAnticipated here from next subsection
lemma K4_imp_K2:
" Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
       set evs;  evs  kerbIV_gets
    Ta. Says Kas A
        (Crypt (shrK A)
         Key authK, Agent Tgs, Number Ta,
           Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
         set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, auto)
apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
done

textAnticipated here from next subsection
lemma u_K4_imp_K2:
" Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
       set evs; evs  kerbIV_gets
    Ta. (Says Kas A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
           Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
              set evs
           servKlife + Ts  authKlife + Ta)"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, auto)
apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
done

lemma servTicket_authentic_Kas:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbIV_gets 
   authK Ta.
       Says Kas A
         (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
            Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
         set evs"
by (blast dest!: servTicket_authentic_Tgs K4_imp_K2)

lemma u_servTicket_authentic_Kas:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbIV_gets 
   authK Ta. Says Kas A (Crypt(shrK A) Key authK, Agent Tgs, Number Ta,
           Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
              set evs
            servKlife + Ts  authKlife + Ta"
by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)

lemma servTicket_authentic:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbIV_gets 
  Ta authK.
     Says Kas A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
                   Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
        set evs
      Says Tgs A (Crypt authK Key servK, Agent B, Number Ts,
                   Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts)
        set evs"
by (blast dest: servTicket_authentic_Tgs K4_imp_K2)

lemma u_servTicket_authentic:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbIV_gets 
  Ta authK.
     (Says Kas A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta,
                   Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
        set evs
      Says Tgs A (Crypt authK Key servK, Agent B, Number Ts,
                   Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts)
        set evs
      servKlife + Ts  authKlife + Ta)"
by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)

lemma u_NotexpiredSK_NotexpiredAK:
     " ¬ expiredSK Ts evs; servKlife + Ts  authKlife + Ta 
       ¬ expiredAK Ta evs"
by (blast dest: leI le_trans dest: leD)


subsectionReliability: friendly agents send something if something else happened

lemma K3_imp_K2:
     " Says A Tgs
             authTicket, Crypt authK Agent A, Number T2, Agent B
            set evs;
         A  bad;  evs  kerbIV_gets 
       Ta. Says Kas A (Crypt (shrK A)
                      Key authK, Agent Tgs, Number Ta, authTicket)
                    set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast, blast)
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic])
done

textAnticipated 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.
lemma Key_unique_SesKey:
     " Crypt K  Key SesKey,  Agent B, T, Ticket
            parts (spies evs);
         Crypt K' Key SesKey,  Agent B', T', Ticket'
            parts (spies evs);  Key SesKey  analz (spies evs);
         evs  kerbIV_gets 
       K=K'  B=B'  T=T'  Ticket=Ticket'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake, K2, K4
apply (blast+)
done

lemma Tgs_authenticates_A:
  "  Crypt authK Agent A, Number T2  parts (spies evs); 
      Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta
            parts (spies evs);
      Key authK  analz (spies evs); A  bad; evs  kerbIV_gets 
   B. Says A Tgs 
          Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta,
          Crypt authK Agent A, Number T2, Agent B   set evs"  
apply (drule authTicket_authentic, assumption, rotate_tac 4)
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [6] Gets_ticket_parts)
apply (frule_tac [9] Gets_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txtFake
apply blast
txtK2
apply (force dest!: Crypt_imp_keysFor)
txtK3
apply (blast dest: Key_unique_SesKey)
txtK5
txtIf authKa were compromised, so would be authK
apply (case_tac "Key authKa  analz (spies evs5)")
apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
txtBesides, since authKa originated with Kas anyway...
apply (clarify, drule K3_imp_K2, assumption, assumption)
apply (clarify, drule Says_Kas_message_form, assumption)
txt...it cannot be a shared key*. Therefore termservK_authentic applies. 
     Contradition: Tgs used authK as a servkey, 
     while Kas used it as an authkey
apply (blast dest: servK_authentic Says_Tgs_message_form)
done

lemma Says_K5:
     " Crypt servK Agent A, Number T3  parts (spies evs);
         Says Tgs A (Crypt authK Key servK, Agent B, Number Ts,
                                     servTicket)  set evs;
         Key servK  analz (spies evs);
         A  bad; B  bad; evs  kerbIV_gets 
  Says A B servTicket, Crypt servK Agent A, Number T3  set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [6] Gets_ticket_parts)
apply (frule_tac [9] Gets_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
apply blast
txtK3
apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
txtK4
apply (force dest!: Crypt_imp_keysFor)
txtK5
apply (blast dest: Key_unique_SesKey)
done

textAnticipated here from next subsection
lemma unique_CryptKey:
     " Crypt (shrK B)  Agent A,  Agent B,  Key SesKey, T
            parts (spies evs);
         Crypt (shrK B') Agent A', Agent B', Key SesKey, T'
            parts (spies evs);  Key SesKey  analz (spies evs);
         evs  kerbIV_gets 
       A=A'  B=B'  T=T'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake, K2, K4
apply (blast+)
done

lemma Says_K6:
     " Crypt servK (Number T3)  parts (spies evs);
         Says Tgs A (Crypt authK Key servK, Agent B, Number Ts,
                                     servTicket)  set evs;
         Key servK  analz (spies evs);
         A  bad; B  bad; evs  kerbIV_gets 
       Says B A (Crypt servK (Number T3))  set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts)
apply (simp_all (no_asm_simp))
apply blast
apply (force dest!: Crypt_imp_keysFor, clarify)
apply (frule Says_Tgs_message_form, assumption, clarify) (*PROOF FAILED if omitted*)
apply (blast dest: unique_CryptKey)
done

textNeeds a unicity theorem, hence moved here
lemma servK_authentic_ter:
 " Says Kas A
    (Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket)  set evs;
     Crypt authK Key servK, Agent B, Number Ts, servTicket
        parts (spies evs);
     Key authK  analz (spies evs);
     evs  kerbIV_gets 
  Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs"
apply (frule Says_Kas_message_form, assumption)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
txtK2 and K4 remain
prefer 2 apply (blast dest!: unique_CryptKey)
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
done


subsectionUnicity Theorems

textThe session key, if secure, uniquely identifies the Ticket
   whether authTicket or servTicket. As a matter of fact, one can read
   also Tgs in the place of B.


lemma unique_authKeys:
     " Says Kas A
              (Crypt Ka Key authK, Agent Tgs, Ta, X)  set evs;
         Says Kas A'
              (Crypt Ka' Key authK, Agent Tgs, Ta', X')  set evs;
         evs  kerbIV_gets   A=A'  Ka=Ka'  Ta=Ta'  X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtK2
apply blast
done

textservK uniquely identifies the message from Tgs
lemma unique_servKeys:
     " Says Tgs A
              (Crypt K Key servK, Agent B, Ts, X)  set evs;
         Says Tgs A'
              (Crypt K' Key servK, Agent B', Ts', X')  set evs;
         evs  kerbIV_gets   A=A'  B=B'  K=K'  Ts=Ts'  X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtK4
apply blast
done

textRevised unicity theorems

lemma Kas_Unique:
     " Says Kas A
              (Crypt Ka Key authK, Agent Tgs, Ta, authTicket)  set evs;
        evs  kerbIV_gets   
   Unique (Says Kas A (Crypt Ka Key authK, Agent Tgs, Ta, authTicket)) 
   on evs"
apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def)
apply blast
done

lemma Tgs_Unique:
     " Says Tgs A
              (Crypt authK Key servK, Agent B, Ts, servTicket)  set evs;
        evs  kerbIV_gets   
  Unique (Says Tgs A (Crypt authK Key servK, Agent B, Ts, servTicket)) 
  on evs"
apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def)
apply blast
done


subsectionLemmas About the Predicate termAKcryptSK

lemma not_AKcryptSK_Nil [iff]: "¬ AKcryptSK authK servK []"
by (simp add: AKcryptSK_def)

lemma AKcryptSKI:
 " Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, X )  set evs;
     evs  kerbIV_gets   AKcryptSK authK servK evs"
apply (unfold AKcryptSK_def)
apply (blast dest: Says_Tgs_message_form)
done

lemma AKcryptSK_Says [simp]:
   "AKcryptSK authK servK (Says S A X # evs) =
     (Tgs = S 
      (B Ts. X = Crypt authK
                Key servK, Agent B, Number Ts,
                  Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts )
     | AKcryptSK authK servK evs)"
by (auto simp add: AKcryptSK_def)

(*A fresh authK cannot be associated with any other
  (with respect to a given trace). *)
lemma Auth_fresh_not_AKcryptSK:
     " Key authK  used evs; evs  kerbIV_gets 
       ¬ AKcryptSK authK servK evs"
apply (unfold AKcryptSK_def)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
done

(*A fresh servK cannot be associated with any other
  (with respect to a given trace). *)
lemma Serv_fresh_not_AKcryptSK:
 "Key servK  used evs  ¬ AKcryptSK authK servK evs"
by (unfold AKcryptSK_def, blast)

lemma authK_not_AKcryptSK:
     " Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, tk
            parts (spies evs);  evs  kerbIV_gets 
       ¬ AKcryptSK K authK evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
txtFake
apply blast
txtReception
apply (simp add: AKcryptSK_def)
txtK2: by freshness
apply (simp add: AKcryptSK_def)
txtK4
by (blast+)

textA secure serverkey cannot have been used to encrypt others
lemma servK_not_AKcryptSK:
 " Crypt (shrK B) Agent A, Agent B, Key SK, Number Ts  parts (spies evs);
     Key SK  analz (spies evs);  SK  symKeys;
     B  Tgs;  evs  kerbIV_gets 
   ¬ AKcryptSK SK K evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
txtReception
apply (simp add: AKcryptSK_def)
txtK4 splits into distinct subcases
apply auto
txtservK can't have been enclosed in two certificates
 prefer 2 apply (blast dest: unique_CryptKey)
txtservK is fresh and so could not have been used, by
   new_keys_not_used›
by (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)

textLong term keys are not issued as servKeys
lemma shrK_not_AKcryptSK:
     "evs  kerbIV_gets  ¬ AKcryptSK K (shrK A) evs"
apply (unfold AKcryptSK_def)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
by (frule_tac [6] Gets_ticket_parts, auto)

textThe Tgs message associates servK with authK and therefore not with any
  other key authK.
lemma Says_Tgs_AKcryptSK:
     " Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, X )
            set evs;
         authK'  authK;  evs  kerbIV_gets 
       ¬ AKcryptSK authK' servK evs"
apply (unfold AKcryptSK_def)
by (blast dest: unique_servKeys)

textEquivalently
lemma not_different_AKcryptSK:
     " AKcryptSK authK servK evs;
        authK'  authK;  evs  kerbIV_gets 
       ¬ AKcryptSK authK' servK evs   servK  symKeys"
apply (simp add: AKcryptSK_def)
by (blast dest: unique_servKeys Says_Tgs_message_form)

lemma AKcryptSK_not_AKcryptSK:
     " AKcryptSK authK servK evs;  evs  kerbIV_gets 
       ¬ AKcryptSK servK K evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts)
txtReception
prefer 3 apply (simp add: AKcryptSK_def)
apply (simp_all, safe)
txtK4 splits into subcases
prefer 4 apply (blast dest!: authK_not_AKcryptSK)
txtservK is fresh and so could not have been used, by
   new_keys_not_used›
 prefer 2 
 apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
txtOthers by freshness
by (blast+)

textThe only session keys that can be found with the help of session keys are
  those sent by Tgs in step K4.

textWe take some pains to express the property
  as a logical equivalence so that the simplifier can apply it.
lemma Key_analz_image_Key_lemma:
     "P  (Key K  analz (Key`KK  H))  (K  KK | Key K  analz H)
      
      P  (Key K  analz (Key`KK  H)) = (K  KK | Key K  analz H)"
by (blast intro: analz_mono [THEN subsetD])


lemma AKcryptSK_analz_insert:
     " AKcryptSK K K' evs; K  symKeys; evs  kerbIV_gets 
       Key K'  analz (insert (Key K) (spies evs))"
apply (simp add: AKcryptSK_def, clarify)
by (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)

lemma authKeys_are_not_AKcryptSK:
     " K  authKeys evs  range shrK;  evs  kerbIV_gets 
       SK. ¬ AKcryptSK SK K evs  K  symKeys"
apply (simp add: authKeys_def AKcryptSK_def)
by (blast dest: Says_Kas_message_form Says_Tgs_message_form)

lemma not_authKeys_not_AKcryptSK:
     " K  authKeys evs;
         K  range shrK; evs  kerbIV_gets 
       SK. ¬ AKcryptSK K SK evs"
apply (simp add: AKcryptSK_def)
by (blast dest: Says_Tgs_message_form)


subsectionSecrecy Theorems

textFor the Oops2 case of the next theorem
lemma Oops2_not_AKcryptSK:
     " evs  kerbIV_gets;
         Says Tgs A (Crypt authK
                     Key servK, Agent B, Number Ts, servTicket)
            set evs 
       ¬ AKcryptSK servK SK evs"
by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
   
textBig simplification law for keys SK that are not crypted by keys in KK
 It helps prove three, otherwise hard, facts about keys. These facts are
 exploited as simplification laws for analz, and also "limit the damage"
 in case of loss of a key to the spy. See ESORICS98.
lemma Key_analz_image_Key [rule_format (no_asm)]:
     "evs  kerbIV_gets 
      (SK KK. SK  symKeys  KK  -(range shrK) 
       (K  KK. ¬ AKcryptSK K SK evs)   
       (Key SK  analz (Key`KK  (spies evs))) =
       (SK  KK | Key SK  analz (spies evs)))"
apply (erule kerbIV_gets.induct)
apply (frule_tac [11] Oops_range_spies2)
apply (frule_tac [10] Oops_range_spies1)
apply (frule_tac [8] Says_tgs_message_form)
apply (frule_tac [6] Says_kas_message_form)
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
txtCase-splits for Oops1 and message 5: the negated case simplifies using
 the induction hypothesis
apply (case_tac [12] "AKcryptSK authK SK evsO1")
apply (case_tac [9] "AKcryptSK servK SK evs5")
apply (simp_all del: image_insert
        add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
             Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
       Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
  ― ‹18 seconds on a 1.8GHz machine??
txtFake 
apply spy_analz
txtReception
apply (simp add: AKcryptSK_def)
txtK2
apply blast 
txtK3
apply blast 
txtK4
apply (blast dest!: authK_not_AKcryptSK)
txtK5
apply (case_tac "Key servK  analz (spies evs5) ")
txtIf servK is compromised then the result follows directly...
apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
txt...therefore servK is uncompromised.
txtThe AKcryptSK servK SK evs5 case leads to a contradiction.
apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
txtAnother K5 case
apply blast 
txtOops1
apply simp 
by (blast dest!: AKcryptSK_analz_insert)

textFirst simplification law for analz: no session keys encrypt
authentication keys or shared keys.
lemma analz_insert_freshK1:
     " evs  kerbIV_gets;  K  authKeys evs  range shrK;
        SesKey  range shrK 
       (Key K  analz (insert (Key SesKey) (spies evs))) =
          (K = SesKey | Key K  analz (spies evs))"
apply (frule authKeys_are_not_AKcryptSK, assumption)
apply (simp del: image_insert
            add: analz_image_freshK_simps add: Key_analz_image_Key)
done


textSecond simplification law for analz: no service keys encrypt any other keys.
lemma analz_insert_freshK2:
     " evs  kerbIV_gets;  servK  (authKeys evs); servK  range shrK;
        K  symKeys 
       (Key K  analz (insert (Key servK) (spies evs))) =
          (K = servK | Key K  analz (spies evs))"
apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
apply (simp del: image_insert
            add: analz_image_freshK_simps add: Key_analz_image_Key)
done


textThird simplification law for analz: only one authentication key encrypts a certain service key.

lemma analz_insert_freshK3:
 " AKcryptSK authK servK evs;
    authK'  authK; authK'  range shrK; evs  kerbIV_gets 
         (Key servK  analz (insert (Key authK') (spies evs))) =
                (servK = authK' | Key servK  analz (spies evs))"
apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
apply (simp del: image_insert
            add: analz_image_freshK_simps add: Key_analz_image_Key)
done

lemma analz_insert_freshK3_bis:
 " Says Tgs A
            (Crypt authK Key servK, Agent B, Number Ts, servTicket)
         set evs; 
     authK  authK'; authK'  range shrK; evs  kerbIV_gets 
         (Key servK  analz (insert (Key authK') (spies evs))) =
                (servK = authK' | Key servK  analz (spies evs))"
apply (frule AKcryptSKI, assumption)
by (simp add: analz_insert_freshK3)

texta weakness of the protocol
lemma authK_compromises_servK:
     " Says Tgs A
              (Crypt authK Key servK, Agent B, Number Ts, servTicket)
            set evs;  authK  symKeys;
         Key authK  analz (spies evs); evs  kerbIV_gets 
       Key servK  analz (spies evs)"
by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])

lemma servK_notin_authKeysD:
     " Crypt authK Key servK, Agent B, Ts,
                      Crypt (shrK B) Agent A, Agent B, Key servK, Ts
            parts (spies evs);
         Key servK  analz (spies evs);
         B  Tgs; evs  kerbIV_gets 
       servK  authKeys evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (simp add: authKeys_def)
apply (erule kerbIV_gets.induct, analz_mono_contra)
apply (frule_tac [8] Gets_ticket_parts)
apply (frule_tac [6] Gets_ticket_parts, simp_all)
by (blast+)


textIf Spy sees the Authentication Key sent in msg K2, then
    the Key has expired.
lemma Confidentiality_Kas_lemma [rule_format]:
     " authK  symKeys; A  bad;  evs  kerbIV_gets 
       Says Kas A
               (Crypt (shrK A)
                  Key authK, Agent Tgs, Number Ta,
          Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
             set evs 
          Key authK  analz (spies evs) 
          expiredAK Ta evs"
apply (erule kerbIV_gets.induct)
apply (frule_tac [11] Oops_range_spies2)
apply (frule_tac [10] Oops_range_spies1)
apply (frule_tac [8] Says_tgs_message_form)
apply (frule_tac [6] Says_kas_message_form)
apply (safe del: impI conjI impCE)
apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
txtFake
apply spy_analz
txtK2
apply blast
txtK4
apply blast
txtLevel 8: K5
apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
txtOops1
apply (blast dest!: unique_authKeys intro: less_SucI)
txtOops2
by (blast dest: Says_Tgs_message_form Says_Kas_message_form)

lemma Confidentiality_Kas:
     " Says Kas A
              (Crypt Ka Key authK, Agent Tgs, Number Ta, authTicket)
            set evs;
         ¬ expiredAK Ta evs;
         A  bad;  evs  kerbIV_gets 
       Key authK  analz (spies evs)"
by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)

textIf Spy sees the Service Key sent in msg K4, then
    the Key has expired.

lemma Confidentiality_lemma [rule_format]:
     " Says Tgs A
            (Crypt authK
               Key servK, Agent B, Number Ts,
                 Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts)
            set evs;
        Key authK  analz (spies evs);
        servK  symKeys;
        A  bad;  B  bad; evs  kerbIV_gets 
       Key servK  analz (spies evs) 
          expiredSK Ts evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (rule_tac [10] impI)+
  ― ‹The Oops1 case is unusual: must simplify
    termAuthkey  analz (spies (ev#evs)), not letting
   analz_mono_contra› weaken it to
   termAuthkey  analz (spies evs),
  for we then conclude termauthK  authKa.
apply analz_mono_contra
apply (frule_tac [11] Oops_range_spies2)
apply (frule_tac [10] Oops_range_spies1)
apply (frule_tac [8] Says_tgs_message_form)
apply (frule_tac [6] Says_kas_message_form)
apply (safe del: impI conjI impCE)
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)
txtFake
apply spy_analz
txtK2
apply (blast intro: parts_insertI less_SucI)
txtK4
apply (blast dest: authTicket_authentic Confidentiality_Kas)
txtOops2
  prefer 3
  apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
txtOops1
 prefer 2
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
txtK5. Not clear how this step could be integrated with the main
       simplification step. Done in KerberosV.thy
apply clarify
apply (erule_tac V = "Says Aa Tgs X  set evs" for X evs in thin_rl)
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD])
apply (assumption, assumption, blast, assumption)
apply (simp add: analz_insert_freshK2)
apply (blast dest: Key_unique_SesKey intro: less_SucI)
done


textIn the real world Tgs can't check wheter authK is secure!
lemma Confidentiality_Tgs:
     " Says Tgs A
              (Crypt authK Key servK, Agent B, Number Ts, servTicket)
            set evs;
         Key authK  analz (spies evs);
         ¬ expiredSK Ts evs;
         A  bad;  B  bad; evs  kerbIV_gets 
       Key servK  analz (spies evs)"
by (blast dest: Says_Tgs_message_form Confidentiality_lemma)

textIn the real world Tgs CAN check what Kas sends!
lemma Confidentiality_Tgs_bis:
     " Says Kas A
               (Crypt Ka Key authK, Agent Tgs, Number Ta, authTicket)
            set evs;
         Says Tgs A
              (Crypt authK Key servK, Agent B, Number Ts, servTicket)
            set evs;
         ¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
         A  bad;  B  bad; evs  kerbIV_gets 
       Key servK  analz (spies evs)"
by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)

textMost general form
lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]

lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]

textNeeds a confidentiality guarantee, hence moved here.
      Authenticity of servK for A
lemma servK_authentic_bis_r:
     " Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket
            parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts, servTicket
            parts (spies evs);
         ¬ expiredAK Ta evs; A  bad; evs  kerbIV_gets 
 Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs"
by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)

lemma Confidentiality_Serv_A:
     " Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket
            parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts, servTicket
            parts (spies evs);
         ¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
         A  bad;  B  bad; evs  kerbIV_gets 
       Key servK  analz (spies evs)"
by (metis Confidentiality_Auth_A Confidentiality_Tgs K4_imp_K2 authK_authentic authTicket_form servK_authentic unique_authKeys)

(*deleted Confidentiality_B, which was identical to Confidentiality_Serv_A*)

lemma u_Confidentiality_B:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);
         ¬ expiredSK Ts evs;
         A  bad;  B  bad;  B  Tgs; evs  kerbIV_gets 
       Key servK  analz (spies evs)"
by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)



subsection2. Parties' strong authentication: 
       non-injective agreement on the session key. The same guarantees also
       express key distribution, hence their names

textAuthentication here still is weak agreement - of B with A
lemma A_authenticates_B:
     " Crypt servK (Number T3)  parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts, servTicket
            parts (spies evs);
         Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket
            parts (spies evs);
         Key authK  analz (spies evs); Key servK  analz (spies evs);
         A  bad;  B  bad; evs  kerbIV_gets 
       Says B A (Crypt servK (Number T3))  set evs"
by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6)

(*These two have never been proved, because never were they needed before!*)
lemma shrK_in_initState_Server[iff]:  "Key (shrK A)  initState Kas"
by (induct_tac "A", auto)

lemma shrK_in_knows_Server [iff]: "Key (shrK A)  knows Kas evs"
by (simp add: initState_subset_knows [THEN subsetD])
(*Because of our simple model of Tgs, the equivalent for it required an axiom*)


lemma A_authenticates_and_keydist_to_Kas:
   " Gets A (Crypt (shrK A) Key authK, Peer, Ta, authTicket)  set evs;
      A  bad;  evs  kerbIV_gets 
   Says Kas A (Crypt (shrK A) Key authK, Peer, Ta, authTicket)  set evs
   Key authK  analz(knows Kas evs)"
by (force dest!: authK_authentic Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])


lemma K3_imp_Gets_evs:
  " Says A Tgs Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta,
                 Crypt authK Agent A, Number T2, Agent B 
       set evs;  A  bad; evs  kerbIV_gets 
   Gets A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta, 
                 Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta)
        set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply auto
apply (blast dest: authTicket_form)
done

lemma Tgs_authenticates_and_keydist_to_A:
  "  Gets Tgs 
          Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta,
          Crypt authK Agent A, Number T2, Agent B   set evs;
      Key authK  analz (spies evs); A  bad; evs  kerbIV_gets 
   B. Says A Tgs 
          Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta,
          Crypt authK Agent A, Number T2, Agent B   set evs
   Key authK  analz (knows A evs)"  
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN parts.Fst], assumption)
apply (drule Tgs_authenticates_A, assumption+, simp)
apply (force dest!: K3_imp_Gets_evs Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
done

lemma K4_imp_Gets:
  " Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs; evs  kerbIV_gets 
   Ta X. 
     Gets Tgs Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Number Ta, X
        set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply auto
done

lemma A_authenticates_and_keydist_to_Tgs:
 "  Gets A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket)
        set evs;
     Gets A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs;
     Key authK  analz (spies evs); A  bad;
     evs  kerbIV_gets 
  Says Tgs A (Crypt authK Key servK, Agent B, Number Ts, servTicket)
        set evs
   Key authK  analz (knows Tgs evs)
   Key servK  analz (knows Tgs evs)"
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
apply (frule authK_authentic, assumption+)
apply (drule servK_authentic_ter, assumption+)
apply (frule K4_imp_Gets, assumption, erule exE, erule exE)
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)
apply (metis Says_imp_knows analz.Fst analz.Inj analz_symKeys_Decrypt authTicket_form)
done

lemma K5_imp_Gets:
  " Says A B servTicket, Crypt servK Agent A, Number T3  set evs;
    A  bad; evs  kerbIV_gets 
   authK Ts authTicket T2.
    Gets A (Crypt authK Key servK, Agent B, Number Ts, servTicket)  set evs
  Says A Tgs authTicket, Crypt authK Agent A, Number T2, Agent B   set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply auto
done 

lemma K3_imp_Gets:
  " Says A Tgs authTicket, Crypt authK Agent A, Number T2, Agent B
        set evs;
    A  bad; evs  kerbIV_gets 
   Ta. Gets A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket)  set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply auto
done 

lemma B_authenticates_and_keydist_to_A:
     " Gets B Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts,
                Crypt servK Agent A, Number T3  set evs;
        Key servK  analz (spies evs);
        A  bad; B  bad; B  Tgs; evs  kerbIV_gets 
  Says A B Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts,
               Crypt servK Agent A, Number T3  set evs
   Key servK  analz (knows A evs)"
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN servTicket_authentic_Tgs], assumption+)  
apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption)
apply (erule exE, drule Says_K5, assumption+)
apply (frule K5_imp_Gets, assumption+)
apply clarify
apply (drule K3_imp_Gets, assumption+)
apply (erule exE)
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption+, clarify)
apply (force dest!: Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
done


lemma K6_imp_Gets:
  " Says B A (Crypt servK (Number T3))  set evs;
     B  bad; evs  kerbIV_gets 
  Ts X. Gets B Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts,X
        set evs"
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply auto
done


lemma A_authenticates_and_keydist_to_B:
  " Gets A Crypt authK Key servK, Agent B, Number Ts, servTicket,
             Crypt servK (Number T3)  set evs;
     Gets A (Crypt (shrK A) Key authK, Agent Tgs, Number Ta, authTicket)
            set evs;
     Key authK  analz (spies evs); Key servK  analz (spies evs);
     A  bad;  B  bad; evs  kerbIV_gets 
  Says B A (Crypt servK (Number T3))  set evs 
    Key servK  analz (knows B evs)"
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption)
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
apply (drule A_authenticates_B, assumption+)
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])
done

end