Theory KerberosV

(*  Title:      HOL/Auth/KerberosV.thy
    Author:     Giampaolo Bella, Catania University
*)

sectionThe Kerberos Protocol, Version V

theory KerberosV 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, Ta,
                     Crypt (shrK Peer) Agent A, Agent Peer, Key authK, Ta
                     set evs}"

definition
 (* A is the true creator of X if she has sent X and X never appeared on
    the trace before this event. Recall that traces grow from head. *)
  Issues :: "[agent, agent, msg, event list]  bool"
             ("_ Issues _ with _ on _") where
   "A Issues B with X on evs =
      (Y. Says A B Y  set evs  X  parts {Y} 
        X  parts (spies (takeWhile (λz. z   Says A B Y) (rev 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 T evs == authKlife + T < CT evs"

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

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

abbreviation
  valid :: "[nat, nat]  bool"  ("valid _ wrt _") 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 tt.
       Says Tgs A Crypt authK Key servK, Agent B, tt,
                    Crypt (shrK B) Agent A, Agent B, Key servK, tt 
          set evs"

inductive_set kerbV :: "event list set"
  where

   Nil:  "[]  kerbV"

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


(*Authentication phase*)
 | KV1:   " evs1  kerbV 
           Says A Kas Agent A, Agent Tgs, Number (CT evs1) # evs1
           kerbV"
   (*Unlike version IV, authTicket is not re-encrypted*)
 | KV2:  " evs2  kerbV; Key authK  used evs2; authK  symKeys;
            Says A' 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  kerbV"


(* Authorisation phase *)
 | KV3:  " evs3  kerbV; A  Kas; A  Tgs;
            Says A Kas Agent A, Agent Tgs, Number T1  set evs3;
            Says Kas' 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  kerbV"
   (*Unlike version IV, servTicket is not re-encrypted*)
 | KV4:  " evs4  kerbV; Key servK  used evs4; servK  symKeys;
            B  Tgs;  authK  symKeys;
            Says A' 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  kerbV"


(*Service phase*)
 | KV5:  " evs5  kerbV; authK  symKeys; servK  symKeys;
            A  Kas; A  Tgs;
            Says A Tgs
                authTicket, Crypt authK Agent A, Number T2,
                  Agent B
               set evs5;
            Says Tgs' 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  kerbV"

  | KV6:  " evs6  kerbV; B  Kas; B  Tgs;
            Says A' 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 Ta2))
               # evs6  kerbV"



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

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



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 lists, for reasoning about  Issues

lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done

lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done

lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
          (if Abad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done

lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a")
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done

lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]

lemma spies_takeWhile: "spies (takeWhile P evs)  spies evs"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txtResembles used_subset_append› in theory Event.
done

lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]


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 (auto simp add: authKeys_def)

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 (auto simp add: authKeys_def)

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 (auto simp add: authKeys_def)

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 (auto simp add: authKeys_def)

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


subsectionForwarding Lemmas

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

lemma Says_ticket_analz:
     "Says S A Crypt K SesKey, B, TimeStamp, Ticket
                set evs  Ticket  analz (spies evs)"
by (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])

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

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


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

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

lemma Spy_see_shrK_D [dest!]:
     " Key (shrK A)  parts (spies evs);  evs  kerbV   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  kerbV
      K  keysFor (parts (spies evs))"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_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  kerbV; 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, Ta, authTicket
            set evs;
         evs  kerbV 
       authK  range shrK  authK  authKeys evs  authK  symKeys  
  authTicket = (Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Ta) 
             K = shrK A   Peer = Tgs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (simp_all (no_asm) add: authKeys_def authKeys_insert)
apply blast+
done



(*This lemma is essential for proving Says_Tgs_message_form:

  the session key authK
  supplied by Kas in the authentication ticket
  cannot be a long-term key!

  Generalised to any session keys (both authK and servK).
*)
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  kerbV 
       SesKey  range shrK"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
done

lemma authTicket_authentic:
     " Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Ta
            parts (spies evs);
         evs  kerbV 
       Says Kas A Crypt (shrK A) Key authK, Agent Tgs, Ta,
                 Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, Ta
             set evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_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  kerbV 
       authK  authKeys evs"
by (metis authKeysI authTicket_authentic)

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



(*
lemma authTicket_form:
lemma servTicket_form:
lemma Says_kas_message_form:
lemma Says_tgs_message_form:

cannot be proved for version V, but a new proof strategy can be used in their
place. The new strategy merely says that both the authTicket and the servTicket
are in parts and in analz as soon as they appear, using lemmas Says_ticket_parts and Says_ticket_analz. 
The new strategy always lets the simplifier solve cases K3 and K5, saving on
long dedicated analyses, which seemed unavoidable. For this reason, lemma 
servK_notin_authKeysD is no longer needed.
*)

subsectionAuthenticity theorems: confirm origin of sensitive messages

lemma authK_authentic:
     " Crypt (shrK A) Key authK, Peer, Ta
            parts (spies evs);
         A  bad;  evs  kerbV 
        AT. Says Kas A Crypt (shrK A) Key authK, Peer, Ta, AT
             set evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all)
apply blast+
done

textIf a certain encrypted message appears then it originated with Tgs
lemma servK_authentic:
     " Crypt authK Key servK, Agent B, Ts
            parts (spies evs);
         Key authK  analz (spies evs);
         authK  range shrK;
         evs  kerbV 
  A ST. Says Tgs A Crypt authK Key servK, Agent B, Ts, ST
        set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all)
apply blast+
done

lemma servK_authentic_bis:
     " Crypt authK Key servK, Agent B, Ts
            parts (spies evs);
         Key authK  analz (spies evs);
         B  Tgs;
         evs  kerbV 
  A ST. Says Tgs A Crypt authK Key servK, Agent B, Ts, ST
        set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, blast+)
done

textAuthenticity of servK for B
lemma servTicket_authentic_Tgs:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbV 
  authK.
       Says Tgs A Crypt authK Key servK, Agent B, Ts,
                    Crypt (shrK B) Agent A, Agent B, Key servK, Ts
        set evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, 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  kerbV
    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 kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, auto)
apply (metis MPair_analz Says_imp_analz_Spy analz_conj_parts 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  kerbV
    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 kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, auto)
apply (blast dest!: Says_imp_spies [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  kerbV 
   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 (metis K4_imp_K2 servTicket_authentic_Tgs)

lemma u_servTicket_authentic_Kas:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbV 
   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 (metis 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  kerbV 
  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 (metis K4_imp_K2 servTicket_authentic_Tgs)

lemma u_servTicket_authentic:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);  B  Tgs;  B  bad;
         evs  kerbV 
  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 (metis servTicket_authentic_Tgs u_K4_imp_K2)

lemma u_NotexpiredSK_NotexpiredAK:
     " ¬ expiredSK Ts evs; servKlife + Ts  authKlife + Ta 
       ¬ expiredAK Ta evs"
by (metis order_le_less_trans)

subsectionReliability: friendly agents send somthing 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  kerbV 
       Ta AT. Says Kas A Crypt (shrK A) Key authK, Agent Tgs, Ta, 
                               AT  set evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, blast, blast)
apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, 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
            parts (spies evs);
         Crypt K' Key SesKey,  Agent B', T'
            parts (spies evs);  Key SesKey  analz (spies evs);
         evs  kerbV 
       K=K'  B=B'  T=T'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all)
txtFake, K2, K4
apply (blast+)
done

textThis inevitably has an existential form in version V
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  kerbV 
   ST. Says A B ST, Crypt servK Agent A, Number T3  set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_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  kerbV 
       A=A'  B=B'  T=T'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_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  kerbV 
       Says B A (Crypt servK (Number T3))  set evs"
apply (frule Says_Tgs_message_form, assumption, clarify)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts)
apply simp_all

txtfake
apply blast
txtK4
apply (force dest!: Crypt_imp_keysFor)
txtK6
apply (metis MPair_parts Says_imp_parts_knows_Spy unique_CryptKey)
done

textNeeds a unicity theorem, hence moved here
lemma servK_authentic_ter:
 " Says Kas A
       Crypt (shrK A) Key authK, Agent Tgs, Ta, authTicket  set evs;
     Crypt authK Key servK, Agent B, Ts
        parts (spies evs);
     Key authK  analz (spies evs);
     evs  kerbV 
  Says Tgs A Crypt authK Key servK, Agent B, Ts, 
                 Crypt (shrK B) Agent A, Agent B, Key servK, Ts 
        set evs"
apply (frule Says_Kas_message_form, assumption)
apply clarify
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
txtK2 and K4 remain
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
apply (blast dest!: unique_CryptKey)
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  kerbV   A=A'  Ka=Ka'  Ta=Ta'  X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all)
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  kerbV   A=A'  B=B'  K=K'  Ts=Ts'  X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all)
apply blast+
done

subsectionLemmas About the Predicate termAKcryptSK

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

lemma AKcryptSKI:
 " Says Tgs A Crypt authK Key servK, Agent B, tt, X   set evs;
     evs  kerbV   AKcryptSK authK servK evs"
by (metis AKcryptSK_def Says_Tgs_message_form)

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

lemma AKcryptSK_Notes [simp]:
   "AKcryptSK authK servK (Notes A X # evs) =
      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  kerbV 
       ¬ AKcryptSK authK servK evs"
apply (unfold AKcryptSK_def)
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_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 (auto simp add: AKcryptSK_def) 

lemma authK_not_AKcryptSK:
     " Crypt (shrK Tgs) Agent A, Agent Tgs, Key authK, tk
            parts (spies evs);  evs  kerbV 
       ¬ AKcryptSK K authK evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all)
txtFake,K2,K4
apply (auto simp add: AKcryptSK_def)
done

textA secure serverkey cannot have been used to encrypt others
lemma servK_not_AKcryptSK:
 " Crypt (shrK B) Agent A, Agent B, Key SK, tt  parts (spies evs);
     Key SK  analz (spies evs);  SK  symKeys;
     B  Tgs;  evs  kerbV 
   ¬ AKcryptSK SK K evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
txtK4
apply (metis Auth_fresh_not_AKcryptSK MPair_parts Says_imp_parts_knows_Spy authKeys_used authTicket_crypt_authK unique_CryptKey)
done

textLong term keys are not issued as servKeys
lemma shrK_not_AKcryptSK:
     "evs  kerbV  ¬ AKcryptSK K (shrK A) evs"
apply (unfold AKcryptSK_def)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, auto)
done

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, tt, X 
            set evs;
         authK'  authK;  evs  kerbV 
       ¬ AKcryptSK authK' servK evs"
by (metis AKcryptSK_def unique_servKeys)

lemma AKcryptSK_not_AKcryptSK:
     " AKcryptSK authK servK evs;  evs  kerbV 
       ¬ AKcryptSK servK K evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts)
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
apply (blast+)
done

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

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))  (KKK  Key K  analz H)
      
      P  (Key K  analz (Key`KK  H)) = (KKK  Key K  analz H)"
by (blast intro: analz_mono [THEN subsetD])


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

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

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


subsectionSecrecy Theorems

textFor the Oops2 case of the next theorem
lemma Oops2_not_AKcryptSK:
     " evs  kerbV;
         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  kerbV 
      (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 kerbV.induct)
apply (frule_tac [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
(*Used to apply Says_tgs_message form, which is no longer available. 
  Instead…*)
apply (drule_tac [7] Says_ticket_analz)
(*Used to apply Says_kas_message form, which is no longer available. 
  Instead…*)
apply (drule_tac [5] Says_ticket_analz)
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 [9] "AKcryptSK authK SK evsO1")
apply (case_tac [7] "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)
txtFake 
apply spy_analz
txtK2
apply blast 
txtCases K3 and K5 solved by the simplifier thanks to the ticket being in 
analz - this strategy is new wrt version IV 
txtK4
apply (blast dest!: authK_not_AKcryptSK)
txtOops1
apply (metis AKcryptSK_analz_insert insert_Key_singleton)
done

textFirst simplification law for analz: no session keys encrypt
authentication keys or shared keys.
lemma analz_insert_freshK1:
     " evs  kerbV;  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  kerbV;  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  kerbV 
         (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  kerbV 
         (Key servK  analz (insert (Key authK') (spies evs))) =
                (servK = authK' | Key servK  analz (spies evs))"
apply (frule AKcryptSKI, assumption)
apply (simp add: analz_insert_freshK3)
done

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  kerbV 
       Key servK  analz (spies evs)"
  by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')


textlemma servK_notin_authKeysD› not needed in version V

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  kerbV 
       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 kerbV.induct)
apply (frule_tac [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
apply (frule_tac [7] Says_ticket_analz)
apply (frule_tac [5] Says_ticket_analz)
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
txtOops1
apply (blast dest!: unique_authKeys intro: less_SucI)
txtOops2
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
done

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

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  kerbV 
       Key servK  analz (spies evs) 
          expiredSK Ts evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (rule_tac [9] 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 [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
apply (frule_tac [7] Says_ticket_analz)
apply (frule_tac [5] Says_ticket_analz)
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)
 txtOops1
 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
txtOops2
apply (metis Suc_le_eq linorder_linear linorder_not_le msg.simps(2) unique_servKeys)
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  kerbV 
       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  kerbV 
       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 exE, 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
            parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         ¬ expiredAK Ta evs; A  bad; evs  kerbV 
  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 (metis Confidentiality_Kas authK_authentic servK_authentic_ter)

lemma Confidentiality_Serv_A:
     " Crypt (shrK A) Key authK, Agent Tgs, Number Ta
            parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         ¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
         A  bad;  B  bad; B  Tgs; evs  kerbV 
       Key servK  analz (spies evs)"
apply (drule authK_authentic, assumption, assumption)
apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
done

lemma Confidentiality_B:
     " Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         Crypt (shrK A) Key authK, Agent Tgs, Number Ta
            parts (spies evs);
         ¬ expiredSK Ts evs; ¬ expiredAK Ta evs;
         A  bad;  B  bad; B  Tgs; evs  kerbV 
       Key servK  analz (spies evs)"
apply (frule authK_authentic)
apply (erule_tac [3] exE)
apply (frule_tac [3] Confidentiality_Kas)
apply (frule_tac [6] servTicket_authentic, auto)
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
done

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  kerbV 
       Key servK  analz (spies evs)"
by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)



subsectionParties authentication: each party verifies "the identity of
       another party who generated some data" (quoted from Neuman and Ts'o).

textThese guarantees don't assess whether two parties agree on
      the same session key: sending a message containing a key
      doesn't a priori state knowledge of the key.


textThese didn't have existential form in version IV
lemma B_authenticates_A:
     " Crypt servK Agent A, Number T3  parts (spies evs);
        Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);
        Key servK  analz (spies evs);
        A  bad; B  bad; B  Tgs; evs  kerbV 
    ST. Says A B ST, Crypt servK Agent A, Number T3   set evs"
by (blast dest: servTicket_authentic_Tgs intro: Says_K5)

textThe second assumption tells B what kind of key servK is.
lemma B_authenticates_A_r:
     " Crypt servK Agent A, Number T3  parts (spies evs);
         Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         Crypt (shrK A) Key authK, Agent Tgs, Number Ta
            parts (spies evs);
         ¬ expiredSK Ts evs; ¬ expiredAK Ta evs;
         B  Tgs; A  bad;  B  bad;  evs  kerbV 
    ST. Says A B ST, Crypt servK Agent A, Number T3   set evs"
by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)

textu_B_authenticates_A› would be the same as B_authenticates_A› because the
 servK confidentiality assumption is yet unrelaxed

lemma u_B_authenticates_A_r:
     " Crypt servK Agent A, Number T3  parts (spies evs);
         Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);
         ¬ expiredSK Ts evs;
         B  Tgs; A  bad;  B  bad;  evs  kerbV 
    ST. Says A B ST, Crypt servK Agent A, Number T3   set evs"
by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)

lemma A_authenticates_B:
     " Crypt servK (Number T3)  parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         Crypt (shrK A) Key authK, Agent Tgs, Number Ta
            parts (spies evs);
         Key authK  analz (spies evs); Key servK  analz (spies evs);
         A  bad;  B  bad; evs  kerbV 
       Says B A (Crypt servK (Number T3))  set evs"
  by (metis authK_authentic Oops_range_spies1 Says_K6 servK_authentic u_K4_imp_K2 unique_authKeys)

lemma A_authenticates_B_r:
     " Crypt servK (Number T3)  parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         Crypt (shrK A) Key authK, Agent Tgs, Number Ta
            parts (spies evs);
         ¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
         A  bad;  B  bad; evs  kerbV 
       Says B A (Crypt servK (Number T3))  set evs"
apply (frule authK_authentic)
apply (erule_tac [3] exE)
apply (frule_tac [3] Says_Kas_message_form)
apply (frule_tac [4] Confidentiality_Kas)
apply (frule_tac [7] servK_authentic)
apply auto
apply (metis Confidentiality_Tgs K4_imp_K2 Says_K6 unique_authKeys) 
done



subsectionParties' knowledge of session keys. 
       An agent knows a session key if he used it to issue a cipher. These
       guarantees can be interpreted both in terms of key distribution
       and of non-injective agreement on the session key.

lemma Kas_Issues_A:
   " Says Kas A Crypt (shrK A) Key authK, Peer, Ta, authTicket  set evs;
      evs  kerbV 
   Kas Issues A with (Crypt (shrK A) Key authK, Peer, Ta)
          on evs"
apply (simp (no_asm) add: Issues_def)
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txtK2
apply (simp add: takeWhile_tail)
apply (metis MPair_parts parts.Body parts_idem parts_spies_takeWhile_mono parts_trans spies_evs_rev usedI)
done

lemma A_authenticates_and_keydist_to_Kas:
  " Crypt (shrK A) Key authK, Peer, Ta  parts (spies evs);
     A  bad; evs  kerbV 
  Kas Issues A with (Crypt (shrK A) Key authK, Peer, Ta) 
          on evs"
by (blast dest!: authK_authentic Kas_Issues_A)

lemma Tgs_Issues_A:
    " Says Tgs A Crypt authK Key servK, Agent B, Number Ts, servTicket
          set evs; 
       Key authK  analz (spies evs);  evs  kerbV 
   Tgs Issues A with 
          (Crypt authK Key servK, Agent B, Number Ts) on evs"
apply (simp (no_asm) add: Issues_def)
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
apply (simp add: takeWhile_tail)
(*Last two thms installed only to derive authK ∉ range shrK*)
apply (blast dest: servK_authentic parts_spies_takeWhile_mono [THEN subsetD]
      parts_spies_evs_revD2 [THEN subsetD] authTicket_authentic 
      Says_Kas_message_form)
done

lemma A_authenticates_and_keydist_to_Tgs:
     " Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
       Key authK  analz (spies evs); B  Tgs; evs  kerbV 
   A. Tgs Issues A with 
          (Crypt authK Key servK, Agent B, Number Ts) on evs"
by (blast dest: Tgs_Issues_A servK_authentic_bis)

lemma B_Issues_A:
     " Says B A (Crypt servK (Number T3))  set evs;
         Key servK  analz (spies evs);
         A  bad;  B  bad; B  Tgs; evs  kerbV 
       B Issues A with (Crypt servK (Number T3)) on evs"
apply (simp (no_asm) add: Issues_def)
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
apply blast
txtK6 requires numerous lemmas
apply (simp add: takeWhile_tail)
apply (blast intro: Says_K6 dest: servTicket_authentic 
        parts_spies_takeWhile_mono [THEN subsetD] 
        parts_spies_evs_revD2 [THEN subsetD])
done

lemma A_authenticates_and_keydist_to_B:
     " Crypt servK (Number T3)  parts (spies evs);
         Crypt authK Key servK, Agent B, Number Ts
            parts (spies evs);
         Crypt (shrK A) Key authK, Agent Tgs, Number Ta
            parts (spies evs);
         Key authK  analz (spies evs); Key servK  analz (spies evs);
         A  bad;  B  bad; B  Tgs; evs  kerbV 
       B Issues A with (Crypt servK (Number T3)) on evs"
by (blast dest!: A_authenticates_B B_Issues_A)


(*Must use ≤ rather than =, otherwise it cannot be proved inductively!*)
(*This is too strong for version V but would hold for version IV if only B 
  in K6 said a fresh timestamp.
lemma honest_never_says_newer_timestamp:
     "⟦ (CT evs) ≤ T ; Number T ∈ parts {X}; evs ∈ kerbV ⟧ 
     ⟹ ∀ A B. A ≠ Spy ⟶ Says A B X ∉ set evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (simp_all)
apply force
apply force
txt{*clarifying case K3*}
apply (rule impI)
apply (rule impI)
apply (frule Suc_leD)
apply (clarify)
txt{*cannot solve K3 or K5 because the spy might send CT evs as authTicket
or servTicket, which the honest agent would forward*}
prefer 2 apply force
prefer 4 apply force
prefer 4 apply force
txt{*cannot solve K6 unless B updates the timestamp - rather than bouncing T3*}
oops
*)


textBut can prove a less general fact conerning only authenticators!
lemma honest_never_says_newer_timestamp_in_auth:
     " (CT evs)  T; Number T  parts {X}; A  bad; evs  kerbV  
      Says A B Y, X  set evs"
apply (erule rev_mp)
apply (erule kerbV.induct)
apply auto
done

lemma honest_never_says_current_timestamp_in_auth:
     " (CT evs) = T; Number T  parts {X}; A  bad; evs  kerbV  
      Says A B Y, X  set evs"
by (metis honest_never_says_newer_timestamp_in_auth le_refl)


lemma A_Issues_B:
     " Says A B ST, Crypt servK Agent A, Number T3  set evs;
         Key servK  analz (spies evs);
         B  Tgs; A  bad;  B  bad;  evs  kerbV 
    A Issues B with (Crypt servK Agent A, Number T3) on evs"
apply (simp (no_asm) add: Issues_def)
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts)
apply (simp_all (no_asm_simp))
txtK5
apply auto
apply (simp add: takeWhile_tail)
txtLevel 15: case study necessary because the assumption doesn't state
  the form of servTicket. The guarantee becomes stronger.
prefer 2 apply (simp add: takeWhile_tail)
(**This single command of version IV...
apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
                   K3_imp_K2 K4_trustworthy'
                   parts_spies_takeWhile_mono [THEN subsetD]
                   parts_spies_evs_revD2 [THEN subsetD]
             intro: Says_Auth)
...expands as follows - including extra exE because of new form of lemmas*)
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
apply (case_tac "Key authK  analz (spies evs5)")
 apply (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst])
apply (frule servK_authentic_ter, blast, assumption+)
apply (drule parts_spies_takeWhile_mono [THEN subsetD])
apply (drule parts_spies_evs_revD2 [THEN subsetD])
txttermSays_K5 closes the proof in version IV because it is clear which 
servTicket an authenticator appears with in msg 5. In version V an authenticator can appear with any item that the spy could replace the servTicket with
apply (frule Says_K5, blast)
txtWe need to state that an honest agent wouldn't send the wrong timestamp
within an authenticator, wathever it is paired with
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
done

lemma B_authenticates_and_keydist_to_A:
     " Crypt servK Agent A, Number T3  parts (spies evs);
         Crypt (shrK B) Agent A, Agent B, Key servK, Number Ts
            parts (spies evs);
         Key servK  analz (spies evs);
         B  Tgs; A  bad;  B  bad;  evs  kerbV 
    A Issues B with (Crypt servK Agent A, Number T3) on evs"
by (blast dest: B_authenticates_A A_Issues_B)



subsection
Novel guarantees, never studied before. Because honest agents always say
the right timestamp in authenticators, we can prove unicity guarantees based 
exactly on timestamps. Classical unicity guarantees are based on nonces.
Of course assuming the agent to be different from the Spy, rather than not in 
bad, would suffice below. Similar guarantees must also hold of
Kerberos IV.

textNotice that an honest agent can send the same timestamp on two
different traces of the same length, but not on the same trace!

lemma unique_timestamp_authenticator1:
     " Says A Kas Agent A, Agent Tgs, Number T1  set evs;
         Says A Kas' Agent A, Agent Tgs', Number T1  set evs;
         A bad; evs  kerbV 
   Kas=Kas'  Tgs=Tgs'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
done

lemma unique_timestamp_authenticator2:
     " Says A Tgs AT, Crypt AK Agent A, Number T2, Agent B  set evs;
     Says A Tgs' AT', Crypt AK' Agent A, Number T2, Agent B'  set evs;
         A bad; evs  kerbV 
   Tgs=Tgs'  AT=AT'  AK=AK'  B=B'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
done

lemma unique_timestamp_authenticator3:
     " Says A B ST, Crypt SK Agent A, Number T  set evs;
         Says A B' ST', Crypt SK' Agent A, Number T  set evs;
         A bad; evs  kerbV 
   B=B'  ST=ST'  SK=SK'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
done

textThe second part of the message is treated as an authenticator by the last
simplification step, even if it is not an authenticator!
lemma unique_timestamp_authticket:
     " Says Kas A X, Crypt (shrK Tgs) Agent A, Agent Tgs, Key AK, T  set evs;
       Says Kas A' X', Crypt (shrK Tgs') Agent A', Agent Tgs', Key AK', T  set evs;
         evs  kerbV 
   A=A'  X=X'  Tgs=Tgs'  AK=AK'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
done

textThe second part of the message is treated as an authenticator by the last
simplification step, even if it is not an authenticator!
lemma unique_timestamp_servticket:
     " Says Tgs A X, Crypt (shrK B) Agent A, Agent B, Key SK, T  set evs;
       Says Tgs A' X', Crypt (shrK B') Agent A', Agent B', Key SK', T  set evs;
         evs  kerbV 
   A=A'  X=X'  B=B'  SK=SK'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
done

(*Uses assumption K6's assumption that B ≠ Kas, otherwise B should say
fresh timestamp*)
lemma Kas_never_says_newer_timestamp:
     " (CT evs)  T; Number T  parts {X}; evs  kerbV  
       A. Says Kas A X  set evs"
apply (erule rev_mp)
apply (erule kerbV.induct, auto)
done

lemma Kas_never_says_current_timestamp:
     " (CT evs) = T; Number T  parts {X}; evs  kerbV  
       A. Says Kas A X  set evs"
by (metis Kas_never_says_newer_timestamp eq_imp_le)

lemma unique_timestamp_msg2:
     " Says Kas A Crypt (shrK A) Key AK, Agent Tgs, T, AT  set evs;
     Says Kas A' Crypt (shrK A') Key AK', Agent Tgs', T, AT'  set evs;
         evs  kerbV 
   A=A'  AK=AK'  Tgs=Tgs'  AT=AT'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: Kas_never_says_current_timestamp)
done

(*Uses assumption K6's assumption that B ≠ Tgs, otherwise B should say
fresh timestamp*)
lemma Tgs_never_says_newer_timestamp:
     " (CT evs)  T; Number T  parts {X}; evs  kerbV  
       A. Says Tgs A X  set evs"
apply (erule rev_mp)
apply (erule kerbV.induct, auto)
done

lemma Tgs_never_says_current_timestamp:
     " (CT evs) = T; Number T  parts {X}; evs  kerbV  
       A. Says Tgs A X  set evs"
by (metis Tgs_never_says_newer_timestamp eq_imp_le)

lemma unique_timestamp_msg4:
     " Says Tgs A Crypt (shrK A) Key SK, Agent B, T, ST  set evs;
       Says Tgs A' Crypt (shrK A') Key SK', Agent B', T, ST'  set evs;
         evs  kerbV  
   A=A'  SK=SK'  B=B'  ST=ST'"
apply (erule rev_mp, erule rev_mp)
apply (erule kerbV.induct)
apply (auto simp add: Tgs_never_says_current_timestamp)
done
 
end