isabelle: comparison src/HOL/Auth/KerberosIV.thy

equal deleted inserted replaced

-:ee8b5c36ba2b
+:9f27383426db
 header{*The Kerberos Protocol, Version IV*}
 theory KerberosIV imports Public begin
+text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
 syntax
 Kas :: agent
 Tgs :: agent  --{*the two servers are translations...*}
 axioms
 Tgs_not_bad [iff]: "Tgs \<notin> bad"
 --{*Tgs is secure --- we already know that Kas is secure*}
-(*The current time is just the length of the trace!*)
+(*The current time is the length of the trace*)
 syntax
 CT :: "event list=>nat"
-ExpirAuth :: "[nat, event list] => bool"
+expiredAK :: "[nat, event list] => bool"
-ExpirServ :: "[nat, event list] => bool"
+expiredSK :: "[nat, event list] => bool"
-ExpirAutc :: "[nat, event list] => bool"
+expiredA :: "[nat, event list] => bool"
-RecentResp :: "[nat, nat] => bool"
+valid :: "[nat, nat] => bool" ("valid _ wrt _")
 constdefs
-(* AuthKeys are those contained in an AuthTicket *)
+(* authKeys are those contained in an authTicket *)
-AuthKeys :: "event list => key set"
+authKeys :: "event list => key set"
-"AuthKeys evs == {AuthKey. \<exists>A Peer Tk. Says Kas A
+"authKeys evs == {authK. \<exists>A Peer Ta. Says Kas A
-(Crypt (shrK A) {|Key AuthKey, Agent Peer, Tk,
+(Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
-(Crypt (shrK Peer) {|Agent A, Agent Peer, Key AuthKey, Tk|})
+(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
-|}) \<in> set evs}"
+\<rbrace>) \<in> set evs}"
 (* 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 _")
 "A Issues B with X on evs ==
 \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
 X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
+(* Yields the subtrace of a given trace from its beginning to a given event *)
+before :: "[event, event list] => event list" ("before _ on _")
+"before ev on evs ==  takeWhile (% z. z ~= ev) (rev evs)"
+(* States than an event really appears only once on a trace *)
+Unique :: "[event, event list] => bool" ("Unique _ on _")
+"Unique ev on evs ==
+ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
 consts
 (*Duration of the authentication key*)
-AuthLife   :: nat
+authKlife   :: nat
 (*Duration of the service key*)
-ServLife   :: nat
+servKlife   :: nat
 (*Duration of an authenticator*)
-AutcLife   :: nat
+authlife   :: nat
 (*Upper bound on the time of reaction of a server*)
-RespLife   :: nat
+replylife   :: nat
-specification (AuthLife)
+specification (authKlife)
-AuthLife_LB [iff]: "2 \<le> AuthLife"
+authKlife_LB [iff]: "2 \<le> authKlife"
 by blast
-specification (ServLife)
+specification (servKlife)
-ServLife_LB [iff]: "2 \<le> ServLife"
+servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
 by blast
-specification (AutcLife)
+specification (authlife)
-AutcLife_LB [iff]: "Suc 0 \<le> AutcLife"
+authlife_LB [iff]: "Suc 0 \<le> authlife"
 by blast
-specification (RespLife)
+specification (replylife)
-RespLife_LB [iff]: "Suc 0 \<le> RespLife"
+replylife_LB [iff]: "Suc 0 \<le> replylife"
 by blast
 translations
 "CT" == "length "
-"ExpirAuth T evs" == "AuthLife + T < CT evs"
+"expiredAK Ta evs" == "authKlife + Ta < CT evs"
-"ExpirServ T evs" == "ServLife + T < CT evs"
+"expiredSK Ts evs" == "servKlife + Ts < CT evs"
-"ExpirAutc T evs" == "AutcLife + T < CT evs"
+"expiredA T evs" == "authlife + T < CT evs"
-"RecentResp T1 T2" == "T1 <= RespLife + T2"
+"valid T1 wrt T2" == "T1 <= replylife + T2"
 (*---------------------------------------------------------------------*)
-(* Predicate formalising the association between AuthKeys and ServKeys *)
+(* Predicate formalising the association between authKeys and servKeys *)
 constdefs
-KeyCryptKey :: "[key, key, event list] => bool"
+AKcryptSK :: "[key, key, event list] => bool"
-"KeyCryptKey AuthKey ServKey evs ==
+"AKcryptSK authK servK evs ==
-\<exists>A B tt.
+\<exists>A B Ts.
-Says Tgs A (Crypt AuthKey
+Says Tgs A (Crypt authK
-{|Key ServKey, Agent B, tt,
+\<lbrace>Key servK, Agent B, Number Ts,
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
 \<in> set evs"
 consts
-kerberos   :: "event list set"
+kerbIV   :: "event list set"
-inductive "kerberos"
+inductive "kerbIV"
 intros
-Nil:  "[] \<in> kerberos"
+Nil:  "[] \<in> kerbIV"
-Fake: "[| evsf \<in> kerberos;  X \<in> synth (analz (spies evsf)) |]
+Fake: "\<lbrakk> evsf \<in> kerbIV;  X \<in> synth (analz (spies evsf)) \<rbrakk>
-==> Says Spy B X  # evsf \<in> kerberos"
+\<Longrightarrow> Says Spy B X  # evsf \<in> kerbIV"
 (* FROM the initiator *)
-K1:   "[| evs1 \<in> kerberos |]
+K1:   "\<lbrakk> evs1 \<in> kerbIV \<rbrakk>
-==> Says A Kas {|Agent A, Agent Tgs, Number (CT evs1)|} # evs1
+\<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
-\<in> kerberos"
+\<in> kerbIV"
 (* 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 \<in> kerberos; Key AuthKey \<notin> used evs2; AuthKey \<in> symKeys;
+K2:  "\<lbrakk> evs2 \<in> kerbIV; Key authK \<notin> used evs2; authK \<in> symKeys;
-Says A' Kas {|Agent A, Agent Tgs, Number Ta|} \<in> set evs2 |]
+Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
-==> Says Kas A
+\<Longrightarrow> Says Kas A
-(Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2),
+(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2),
-(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
+(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
-Number (CT evs2)|})|}) # evs2 \<in> kerberos"
+Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV"
 (*
-The internal encryption builds the AuthTicket.
+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.
+authTicket by Tgs in K4.
 *)
 (*---------------------------------------------------------------------*)
 (* FROM the initiator *)
-K3:  "[| evs3 \<in> kerberos;
+K3:  "\<lbrakk> evs3 \<in> kerbIV;
-Says A Kas {|Agent A, Agent Tgs, Number Ta|} \<in> set evs3;
+Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
-Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
+Says Kas' A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
-AuthTicket|}) \<in> set evs3;
+authTicket\<rbrace>) \<in> set evs3;
-RecentResp Tk Ta
+valid Ta wrt T1
-|]
+\<rbrakk>
-==> Says A Tgs {|AuthTicket,
+\<Longrightarrow> Says A Tgs \<lbrace>authTicket,
-(Crypt AuthKey {|Agent A, Number (CT evs3)|}),
+(Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
-Agent B|} # evs3 \<in> kerberos"
+Agent B\<rbrace> # evs3 \<in> kerbIV"
-(*The two events amongst the premises allow A to accept only those AuthKeys
+(*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 strengthens the guarantees assessed by the
+specification. Adding it makes many goals "available" to the peers.
-protocol. Theorems that exploit it have the suffix `_refined'
+Theorems that exploit it have the suffix `_u', which stands for updated
+protocol.
 *)
-K4:  "[| evs4 \<in> kerberos; Key ServKey \<notin> used evs4; ServKey \<in> symKeys;
+K4:  "\<lbrakk> evs4 \<in> kerbIV; Key servK \<notin> used evs4; servK \<in> symKeys;
-B \<noteq> Tgs;  AuthKey \<in> symKeys;
+B \<noteq> Tgs;  authK \<in> symKeys;
-Says A' Tgs {|
+Says A' Tgs \<lbrace>
-(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
+(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
-				 Number Tk|}),
+				 Number Ta\<rbrace>),
-(Crypt AuthKey {|Agent A, Number Ta1|}), Agent B|}
+(Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
 	        \<in> set evs4;
-~ ExpirAuth Tk evs4;
+\<not> expiredAK Ta evs4;
-~ ExpirAutc Ta1 evs4;
+\<not> expiredA T2 evs4;
-ServLife + (CT evs4) <= AuthLife + Tk
+servKlife + (CT evs4) <= authKlife + Ta
-|]
+\<rbrakk>
-==> Says Tgs A
+\<Longrightarrow> Says Tgs A
-(Crypt AuthKey {|Key ServKey, Agent B, Number (CT evs4),
+(Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4),
-			       Crypt (shrK B) {|Agent A, Agent B, Key ServKey,
+			       Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK,
-		 			        Number (CT evs4)|} |})
+		 			        Number (CT evs4)\<rbrace> \<rbrace>)
-	        # evs4 \<in> kerberos"
+	        # evs4 \<in> kerbIV"
 (* 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
+The cipher under Tgs' key is the authTicket, the cipher under B's key
-is the ServTicket, which is built now.
+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 \<in> kerberos; AuthKey \<in> symKeys; ServKey \<in> symKeys;
+K5:  "\<lbrakk> evs5 \<in> kerbIV; authK \<in> symKeys; servK \<in> symKeys;
 Says A Tgs
-{|AuthTicket, Crypt AuthKey {|Agent A, Number Ta1|},
+\<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
-		  Agent B|}
+		  Agent B\<rbrace>
 \<in> set evs5;
 Says Tgs' A
-(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evs5;
-RecentResp Tt Ta1 |]
+valid Ts wrt T2 \<rbrakk>
-==> Says A B {|ServTicket,
+\<Longrightarrow> Says A B \<lbrace>servTicket,
-			 Crypt ServKey {|Agent A, Number (CT evs5)|} |}
+			 Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
-# evs5 \<in> kerberos"
+# evs5 \<in> kerbIV"
 (* Checks similar to those in K3. *)
 (*---------------------------------------------------------------------*)
 (* FROM the responder*)
-K6:  "[| evs6 \<in> kerberos;
+K6:  "\<lbrakk> evs6 \<in> kerbIV;
-Says A' B {|
+Says A' B \<lbrace>
-(Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}),
+(Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
-(Crypt ServKey {|Agent A, Number Ta2|})|}
+(Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
 \<in> set evs6;
-~ ExpirServ Tt evs6;
+\<not> expiredSK Ts evs6;
-~ ExpirAutc Ta2 evs6
+\<not> expiredA T3 evs6
-|]
+\<rbrakk>
-==> Says B A (Crypt ServKey (Number Ta2))
+\<Longrightarrow> Says B A (Crypt servK (Number T3))
-# evs6 \<in> kerberos"
+# evs6 \<in> kerbIV"
 (* Checks similar to those in K4. *)
 (*---------------------------------------------------------------------*)
-(* Leaking an AuthKey... *)
+(* Leaking an authK... *)
-Oops1: "[| evsO1 \<in> kerberos;  A \<noteq> Spy;
+Oops1: "\<lbrakk> evsO1 \<in> kerbIV;  A \<noteq> Spy;
 Says Kas A
-(Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
+(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
-AuthTicket|})  \<in> set evsO1;
+authTicket\<rbrace>)  \<in> set evsO1;
-ExpirAuth Tk evsO1 |]
+expiredAK Ta evsO1 \<rbrakk>
-==> Says A Spy {|Agent A, Agent Tgs, Number Tk, Key AuthKey|}
+\<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
-# evsO1 \<in> kerberos"
+# evsO1 \<in> kerbIV"
 (*---------------------------------------------------------------------*)
-(*Leaking a ServKey... *)
+(*Leaking a servK... *)
-Oops2: "[| evsO2 \<in> kerberos;  A \<noteq> Spy;
+Oops2: "\<lbrakk> evsO2 \<in> kerbIV;  A \<noteq> Spy;
 Says Tgs A
-(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evsO2;
-ExpirServ Tt evsO2 |]
+expiredSK Ts evsO2 \<rbrakk>
-==> Says A Spy {|Agent A, Agent B, Number Tt, Key ServKey|}
+\<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
-# evsO2 \<in> kerberos"
+# evsO2 \<in> kerbIV"
 (*---------------------------------------------------------------------*)
 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]
-subsection{*Lemmas about Lists*}
+subsection{*Lemmas 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 (induct_tac [2] "a", auto)
 done
 done
 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
-subsection{*Lemmas about @{term AuthKeys}*}
+subsection{*Lemmas about @{term authKeys}*}
-lemma AuthKeys_empty: "AuthKeys [] = {}"
+lemma authKeys_empty: "authKeys [] = {}"
-apply (unfold AuthKeys_def)
+apply (unfold authKeys_def)
 apply (simp (no_asm))
 done
-lemma AuthKeys_not_insert:
+lemma authKeys_not_insert:
-"(\<forall>A Tk akey Peer.
+"(\<forall>A Ta akey Peer.
-ev \<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,
+ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
-(Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))
+(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
-==> AuthKeys (ev # evs) = AuthKeys evs"
+\<Longrightarrow> authKeys (ev # evs) = authKeys evs"
-by (unfold AuthKeys_def, auto)
+by (unfold authKeys_def, auto)
-lemma AuthKeys_insert:
+lemma authKeys_insert:
-"AuthKeys
+"authKeys
-(Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk,
+(Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
-(Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs)
+(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
-= insert K (AuthKeys evs)"
+= insert K (authKeys evs)"
-by (unfold AuthKeys_def, auto)
+by (unfold authKeys_def, auto)
-lemma AuthKeys_simp:
+lemma authKeys_simp:
-"K \<in> AuthKeys
+"K \<in> authKeys
-(Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk,
+(Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
-(Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs)
+(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
-==> K = K' | K \<in> AuthKeys evs"
+\<Longrightarrow> K = K' | K \<in> authKeys evs"
-by (unfold AuthKeys_def, auto)
+by (unfold authKeys_def, auto)
-lemma AuthKeysI:
+lemma authKeysI:
-"Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk,
+"Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
-(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \<in> set evs
+(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
-==> K \<in> AuthKeys evs"
+\<Longrightarrow> K \<in> authKeys evs"
-by (unfold AuthKeys_def, auto)
+by (unfold authKeys_def, auto)
-lemma AuthKeys_used: "K \<in> AuthKeys evs ==> Key K \<in> used evs"
+lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
-by (simp add: AuthKeys_def, blast)
+by (simp add: authKeys_def, blast)
 subsection{*Forwarding Lemmas*}
 text{*--For reasoning about the encrypted portion of message K3--*}
 lemma K3_msg_in_parts_spies:
-"Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|})
+"Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>)
-\<in> set evs ==> AuthTicket \<in> parts (spies evs)"
+\<in> set evs \<Longrightarrow> authTicket \<in> parts (spies evs)"
-by blast
+apply blast
+done
 lemma Oops_range_spies1:
-"[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|})
+"\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
 \<in> set evs ;
-evs \<in> kerberos |] ==> AuthKey \<notin> range shrK & AuthKey \<in> symKeys"
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
 apply (erule rev_mp)
-apply (erule kerberos.induct, auto)
+apply (erule kerbIV.induct, auto)
 done
 text{*--For reasoning about the encrypted portion of message K5--*}
 lemma K5_msg_in_parts_spies:
-"Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})
+"Says Tgs' A (Crypt authK \<lbrace>servK, Agent B, Ts, servTicket\<rbrace>)
-\<in> set evs ==> ServTicket \<in> parts (spies evs)"
+\<in> set evs \<Longrightarrow> servTicket \<in> parts (spies evs)"
-by blast
+apply blast
+done
 lemma Oops_range_spies2:
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
 \<in> set evs ;
-evs \<in> kerberos |] ==> ServKey \<notin> range shrK & ServKey \<in> symKeys"
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys"
 apply (erule rev_mp)
-apply (erule kerberos.induct, auto)
+apply (erule kerbIV.induct, auto)
 done
-lemma Says_ticket_in_parts_spies:
+lemma Says_ticket_parts:
-"Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \<in> set evs
+"Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
-==> Ticket \<in> parts (spies evs)"
+\<Longrightarrow> Ticket \<in> parts (spies evs)"
-by blast
+apply blast
+done
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 lemma Spy_see_shrK [simp]:
-"evs \<in> kerberos ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
+"evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 apply (blast+)
 done
 lemma Spy_analz_shrK [simp]:
-"evs \<in> kerberos ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
+"evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
 by auto
 lemma Spy_see_shrK_D [dest!]:
-"[| Key (shrK A) \<in> parts (spies evs);  evs \<in> kerberos |] ==> A:bad"
+"\<lbrakk> Key (shrK A) \<in> parts (spies evs);  evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A:bad"
 by (blast dest: Spy_see_shrK)
 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
 text{*Nobody can have used non-existent keys!*}
 lemma new_keys_not_used [simp]:
-"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerberos|]
+"\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV\<rbrakk>
-==> K \<notin> keysFor (parts (spies evs))"
+\<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake*}
 apply (force dest!: keysFor_parts_insert)
 txt{*Others*}
 done
 (*Earlier, all protocol proofs declared this theorem.
 But few of them actually need it! (Another is Yahalom) *)
 lemma new_keys_not_analzd:
-"[|evs \<in> kerberos; K \<in> symKeys; Key K \<notin> used evs|]
+"\<lbrakk>evs \<in> kerbIV; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
-==> K \<notin> keysFor (analz (spies evs))"
+\<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
+subsection{*Lemmas for reasoning about predicate "before"*}
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+apply (induct_tac "evs")
+apply simp
+apply (induct_tac "a")
+apply auto
+done
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+apply (induct_tac "evs")
+apply simp
+apply (induct_tac "a")
+apply auto
+done
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+apply (induct_tac "evs")
+apply simp
+apply (induct_tac "a")
+apply auto
+done
+lemma used_evs_rev: "used evs = used (rev evs)"
+apply (induct_tac "evs")
+apply simp
+apply (induct_tac "a")
+apply (simp add: used_Says_rev)
+apply (simp add: used_Gets_rev)
+apply (simp add: used_Notes_rev)
+done
+lemma used_takeWhile_used [rule_format]:
+"x : used (takeWhile P X) --> x : used X"
+apply (induct_tac "X")
+apply simp
+apply (induct_tac "a")
+apply (simp_all add: used_Nil)
+apply (blast dest!: initState_into_used)+
+done
+lemma set_evs_rev: "set evs = set (rev evs)"
+apply auto
+done
+lemma takeWhile_void [rule_format]:
+"x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs"
+apply auto
+done
 subsection{*Regularity Lemmas*}
 text{*These concern the form of items passed in messages*}
-text{*Describes the form of AuthKey, AuthTicket, and K sent by Kas*}
+text{*Describes the form of all components sent by Kas*}
 lemma Says_Kas_message_form:
-"[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|})
+"\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
 \<in> set evs;
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow>
-==> AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs & AuthKey \<in> symKeys &
+K = shrK A  & Peer = Tgs &
-AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}) &
+authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
-K = shrK A  & Peer = Tgs"
+authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>) &
-apply (erule rev_mp)
+Key authK \<notin> used(before
-apply (erule kerberos.induct)
+Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
-apply (simp_all (no_asm) add: AuthKeys_def AuthKeys_insert)
+on evs) &
-apply (blast+)
+Ta = CT (before
-done
+Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
+on evs)"
+apply (unfold before_def)
+apply (erule rev_mp)
+apply (erule kerbIV.induct)
+apply (simp_all (no_asm) add: authKeys_def authKeys_insert, blast, blast)
+txt{*K2*}
+apply (simp (no_asm) add: takeWhile_tail)
+apply (rule conjI)
+apply clarify
+apply (rule conjI)
+apply clarify
+apply (rule conjI)
+apply blast
+apply (rule conjI)
+apply clarify
+apply (rule conjI)
+txt{*subcase: used before*}
+apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD]
+used_takeWhile_used)
+txt{*subcase: CT before*}
+apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
+apply blast
+txt{*rest*}
+apply blast+
+done
 (*This lemma is essential for proving Says_Tgs_message_form:
-the session key AuthKey
+the session key authK
 supplied by Kas in the authentication ticket
 cannot be a long-term key!
-Generalised to any session keys (both AuthKey and ServKey).
+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|}
+"\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
 \<in> parts (spies evs); Tgs_B \<notin> bad;
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> SesKey \<notin> range shrK"
+\<Longrightarrow> SesKey \<notin> range shrK"
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
 done
-lemma A_trusts_AuthTicket:
+lemma authTicket_authentic:
-"[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
+"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
 \<in> parts (spies evs);
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk,
+\<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
 \<in> set evs"
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake, K4*}
 apply (blast+)
 done
-lemma AuthTicket_crypt_AuthKey:
+lemma authTicket_crypt_authK:
-"[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}
+"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
 \<in> parts (spies evs);
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> AuthKey \<in> AuthKeys evs"
+\<Longrightarrow> authK \<in> authKeys evs"
-apply (frule A_trusts_AuthTicket, assumption)
+apply (frule authTicket_authentic, assumption)
-apply (simp (no_asm) add: AuthKeys_def)
+apply (simp (no_asm) add: authKeys_def)
 apply blast
 done
-text{*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*}
+text{*Describes the form of servK, servTicket and authK sent by Tgs*}
 lemma Says_Tgs_message_form:
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evs;
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> B \<noteq> Tgs &
+\<Longrightarrow> B \<noteq> Tgs &
-ServKey \<notin> range shrK & ServKey \<notin> AuthKeys evs & ServKey \<in> symKeys &
+authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
-ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) &
+servK \<notin> range shrK & servK \<notin> authKeys evs & servK \<in> symKeys &
-AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs & AuthKey \<in> symKeys"
+servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>) &
-apply (erule rev_mp)
+Key servK \<notin> used (before
-apply (erule kerberos.induct)
+Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
-apply (simp_all add: AuthKeys_insert AuthKeys_not_insert AuthKeys_empty AuthKeys_simp, blast, auto)
+on evs) &
-txt{*Three subcases of Message 4*}
+Ts = CT(before
-apply (blast dest!: AuthKeys_used Says_Kas_message_form)
+Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
+on evs) "
+apply (unfold before_def)
+apply (erule rev_mp)
+apply (erule kerbIV.induct)
+apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast)
+txt{*We need this simplification only for Message 4*}
+apply (simp (no_asm) add: takeWhile_tail)
+apply auto
+txt{*Five subcases of Message 4*}
 apply (blast dest!: SesKey_is_session_key)
-apply (blast dest: AuthTicket_crypt_AuthKey)
+apply (blast dest: authTicket_crypt_authK)
-done
+apply (blast dest!: authKeys_used Says_Kas_message_form)
+txt{*subcase: used before*}
-text{*Authenticity of AuthKey for A:
+apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD]
-If a certain encrypted message appears then it originated with Kas*}
+used_takeWhile_used)
-lemma A_trusts_AuthKey:
+txt{*subcase: CT before*}
-"[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}
+apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
-\<in> parts (spies evs);
+done
-A \<notin> bad;  evs \<in> kerberos |]
-==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})
+lemma authTicket_form:
+"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+A \<notin> bad;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys &
+authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>"
+apply (erule rev_mp)
+apply (erule kerbIV.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (blast+)
+done
+text{* This form holds also over an authTicket, but is not needed below.*}
+lemma servTicket_form:
+"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+Key authK \<notin> analz (spies evs);
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys &
+(\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerbIV.induct, analz_mono_contra)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
+done
+text{* Essentially the same as @{text authTicket_form} *}
+lemma Says_kas_message_form:
+"\<lbrakk> Says Kas' A (Crypt (shrK A)
+\<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys &
+authTicket =
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
+| authTicket \<in> analz (spies evs)"
+by (blast dest: analz_shrK_Decrypt authTicket_form
+Says_imp_spies [THEN analz.Inj])
+lemma Says_tgs_message_form:
+"\<lbrakk> Says Tgs' A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
+\<in> set evs;  authK \<in> symKeys;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> servK \<notin> range shrK &
+(\<exists>A. servTicket =
+	      Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)
+| servTicket \<in> analz (spies evs)"
+apply (frule Says_imp_spies [THEN analz.Inj], auto)
+apply (force dest!: servTicket_form)
+apply (frule analz_into_parts)
+apply (frule servTicket_form, auto)
+done
+subsection{*Authenticity theorems: confirm origin of sensitive messages*}
+lemma authK_authentic:
+"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
 \<in> set evs"
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake*}
 apply blast
 txt{*K4*}
-apply (blast dest!: A_trusts_AuthTicket [THEN Says_Kas_message_form])
+apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
 done
 text{*If a certain encrypted message appears then it originated with Tgs*}
-lemma A_trusts_K4:
+lemma servK_authentic:
-"[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
+"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
 \<in> parts (spies evs);
-Key AuthKey \<notin> analz (spies evs);
+Key authK \<notin> analz (spies evs);
-AuthKey \<notin> range shrK;
+authK \<notin> range shrK;
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> \<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+\<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake*}
 apply blast
 txt{*K2*}
 apply blast
 txt{*K4*}
 apply auto
 done
-lemma AuthTicket_form:
+lemma servK_authentic_bis:
-"[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}
+"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
 \<in> parts (spies evs);
-A \<notin> bad;
+Key authK \<notin> analz (spies evs);
-evs \<in> kerberos |]
+B \<noteq> Tgs;
-==> AuthKey \<notin> range shrK & AuthKey \<in> symKeys &
+evs \<in> kerbIV \<rbrakk>
-AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}"
+\<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
-apply (erule rev_mp)
+\<in> set evs"
-apply (erule kerberos.induct)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
-apply (blast+)
+txt{*Fake*}
-done
+apply blast
+txt{*K4*}
-text{* This form holds also over an AuthTicket, but is not needed below.*}
+apply blast
-lemma ServTicket_form:
+done
-"[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
-\<in> parts (spies evs);
+text{*Authenticity of servK for B*}
-Key AuthKey \<notin> analz (spies evs);
+lemma servTicket_authentic_Tgs:
-evs \<in> kerberos |]
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
-==> ServKey \<notin> range shrK & ServKey \<in> symKeys &
+\<in> parts (spies evs); B \<noteq> Tgs;  B \<notin> bad;
-(\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})"
+evs \<in> kerbIV \<rbrakk>
-apply (erule rev_mp)
+\<Longrightarrow> \<exists>authK.
-apply (erule rev_mp)
+Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
-apply (erule kerberos.induct, analz_mono_contra)
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+\<in> set evs"
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
+apply (erule rev_mp)
-done
+apply (erule rev_mp)
+apply (erule kerbIV.induct)
-text{* Essentially the same as @{text AuthTicket_form} *}
+apply (frule_tac [7] K5_msg_in_parts_spies)
-lemma Says_kas_message_form:
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
-"[| Says Kas' A (Crypt (shrK A)
+apply blast+
-{|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \<in> set evs;
+done
-evs \<in> kerberos |]
-==> AuthKey \<notin> range shrK & AuthKey \<in> symKeys &
+text{*Anticipated here from next subsection*}
-AuthTicket =
+lemma K4_imp_K2:
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
-| AuthTicket \<in> analz (spies evs)"
+\<in> set evs;  evs \<in> kerbIV\<rbrakk>
-by (blast dest: analz_shrK_Decrypt AuthTicket_form
+\<Longrightarrow> \<exists>Ta. Says Kas A
-Says_imp_spies [THEN analz.Inj])
+(Crypt (shrK A)
+\<lbrace>Key authK, Agent Tgs, Number Ta,
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
-lemma Says_tgs_message_form:
+\<in> set evs"
-"[| Says Tgs' A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+apply (erule rev_mp)
-\<in> set evs;  AuthKey \<in> symKeys;
+apply (erule kerbIV.induct)
-evs \<in> kerberos |]
+apply (frule_tac [7] K5_msg_in_parts_spies)
-==> ServKey \<notin> range shrK &
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
-(\<exists>A. ServTicket =
+apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
-	      Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})
+done
-| ServTicket \<in> analz (spies evs)"
-apply (frule Says_imp_spies [THEN analz.Inj], auto)
+text{*Anticipated here from next subsection*}
-apply (force dest!: ServTicket_form)
+lemma u_K4_imp_K2:
-apply (frule analz_into_parts)
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
-apply (frule ServTicket_form, auto)
+\<in> set evs; evs \<in> kerbIV\<rbrakk>
-done
+\<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
-subsection{*Unicity Theorems*}
+\<in> set evs
+& servKlife + Ts <= authKlife + Ta)"
-text{* The session key, if secure, uniquely identifies the Ticket
+apply (erule rev_mp)
-whether AuthTicket or ServTicket. As a matter of fact, one can read
+apply (erule kerbIV.induct)
-also Tgs in the place of B.                                     *}
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
-lemma unique_CryptKey:
+apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
-"[| Crypt (shrK B)  {|Agent A,  Agent B,  Key SesKey, T|}
+done
-\<in> parts (spies evs);
-Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}
+lemma servTicket_authentic_Kas:
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<exists>authK Ta.
+Says Kas A
+(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
+\<in> set evs"
+apply (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
+done
+lemma u_servTicket_authentic_Kas:
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
+\<in> set evs
+& servKlife + Ts <= authKlife + Ta"
+apply (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
+done
+lemma servTicket_authentic:
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<exists>Ta authK.
+Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
+\<in> set evs
+& Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
+\<in> set evs"
+apply (blast dest: servTicket_authentic_Tgs K4_imp_K2)
+done
+lemma u_servTicket_authentic:
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<exists>Ta authK.
+(Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
+\<in> set evs
+& Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
+\<in> set evs
+& servKlife + Ts <= authKlife + Ta)"
+apply (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
+done
+lemma u_NotexpiredSK_NotexpiredAK:
+"\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
+\<Longrightarrow> \<not> expiredAK Ta evs"
+apply (blast dest: leI le_trans dest: leD)
+done
+subsection{* Reliability: friendly agents send something if something else happened*}
+lemma K3_imp_K2:
+"\<lbrakk> Says A Tgs
+\<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
+\<in> set evs;
+A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A)
+\<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
+\<in> set evs"
+apply (erule rev_mp)
+apply (erule kerbIV.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast)
+apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN authK_authentic])
+done
+text{*Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.*}
+lemma Key_unique_SesKey:
+"\<lbrakk> Crypt K  \<lbrace>Key SesKey,  Agent B, T, Ticket\<rbrace>
+\<in> parts (spies evs);
+Crypt K' \<lbrace>Key SesKey,  Agent B', T', Ticket'\<rbrace>
 \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> A=A' & B=B' & T=T'"
+\<Longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket'"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake, K2, K4*}
 apply (blast+)
 done
-text{*An AuthKey is encrypted by one and only one Shared key.
+lemma Tgs_authenticates_A:
-A ServKey is encrypted by one and only one AuthKey.
+"\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs);
-*}
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
-lemma Key_unique_SesKey:
+\<in> parts (spies evs);
-"[| Crypt K  {|Key SesKey,  Agent B, T, Ticket|}
+Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV \<rbrakk>
-\<in> parts (spies evs);
+\<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
-Crypt K' {|Key SesKey,  Agent B', T', Ticket'|}
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
+Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs"
+apply (drule authTicket_authentic, assumption, rotate_tac 4)
+apply (erule rev_mp, erule rev_mp, erule rev_mp)
+apply (erule kerbIV.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)
+txt{*Fake*}
+apply blast
+txt{*K2*}
+apply (force dest!: Crypt_imp_keysFor)
+txt{*K3*}
+apply (blast dest: Key_unique_SesKey)
+txt{*K5*}
+txt{*If authKa were compromised, so would be authK*}
+apply (case_tac "Key authKa \<in> analz (spies evs5)")
+apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
+txt{*Besides, 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 @{text servK_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:
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
+Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
+servTicket\<rbrace>) \<in> set evs;
+Key servK \<notin> analz (spies evs);
+A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerbIV.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
+txt{*K3*}
+apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
+txt{*K4*}
+apply (force dest!: Crypt_imp_keysFor)
+txt{*K5*}
+apply (blast dest: Key_unique_SesKey)
+done
+text{*Anticipated here from next subsection*}
+lemma unique_CryptKey:
+"\<lbrakk> Crypt (shrK B)  \<lbrace>Agent A,  Agent B,  Key SesKey, T\<rbrace>
+\<in> parts (spies evs);
+Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
 \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> K=K' & B=B' & T=T' & Ticket=Ticket'"
+\<Longrightarrow> A=A' & B=B' & T=T'"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake, K2, K4*}
 apply (blast+)
 done
+lemma Says_K6:
+"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
+Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
+servTicket\<rbrace>) \<in> set evs;
+Key servK \<notin> analz (spies evs);
+A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerbIV.induct, analz_mono_contra)
+apply (frule_tac [5] Says_ticket_parts)
+apply (frule_tac [7] Says_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
+text{*Needs a unicity theorem, hence moved here*}
+lemma servK_authentic_ter:
+"\<lbrakk> Says Kas A
+(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+Key authK \<notin> analz (spies evs);
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
+\<in> set evs"
+apply (frule Says_Kas_message_form, assumption)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerbIV.induct, analz_mono_contra)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
+txt{*K2 and K4 remain*}
+prefer 2 apply (blast dest!: unique_CryptKey)
+apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
+done
+subsection{*Unicity Theorems*}
+text{* The 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.                                     *}
 (*
 At reception of any message mentioning A, Kas associates shrK A with
-a new AuthKey. Realistic, as the user gets a new AuthKey at each login.
+a new authK. Realistic, as the user gets a new authK at each login.
-Similarly, at reception of any message mentioning an AuthKey
+Similarly, at reception of any message mentioning an authK
 (a legitimate user could make several requests to Tgs - by K3), Tgs
-associates it with a new ServKey.
+associates it with a new servK.
 Therefore, a goal like
-"evs \<in> kerberos
+"evs \<in> kerbIV
-==> Key Kc \<notin> analz (spies evs) -->
+\<Longrightarrow> Key Kc \<notin> analz (spies evs) \<longrightarrow>
 (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket.
-Crypt Kc {|Key K, Agent B, T, Ticket|}
+Crypt Kc \<lbrace>Key K, Agent B, T, Ticket\<rbrace>
-\<in> parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')"
+\<in> parts (spies evs) \<longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket')"
 would fail on the K2 and K4 cases.
 *)
-lemma unique_AuthKeys:
+lemma unique_authKeys:
-"[| Says Kas A
+"\<lbrakk> Says Kas A
-(Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \<in> set evs;
+(Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs;
 Says Kas A'
-(Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) \<in> set evs;
+(Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs;
-evs \<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' & Ka=Ka' & Ta=Ta' & X=X'"
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*K2*}
 apply blast
 done
-text{* ServKey uniquely identifies the message from Tgs *}
+text{* servK uniquely identifies the message from Tgs *}
-lemma unique_ServKeys:
+lemma unique_servKeys:
-"[| Says Tgs A
+"\<lbrakk> Says Tgs A
-(Crypt K {|Key ServKey, Agent B, Tt, X|}) \<in> set evs;
+(Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs;
 Says Tgs A'
-(Crypt K' {|Key ServKey, Agent B', Tt', X'|}) \<in> set evs;
+(Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs;
-evs \<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'"
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' & B=B' & K=K' & Ts=Ts' & X=X'"
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*K4*}
 apply blast
 done
+text{* Revised unicity theorems *}
-subsection{*Lemmas About the Predicate @{term KeyCryptKey}*}
+lemma Kas_Unique:
-lemma not_KeyCryptKey_Nil [iff]: "~ KeyCryptKey AuthKey ServKey []"
+"\<lbrakk> Says Kas A
-by (simp add: KeyCryptKey_def)
+(Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow>
-lemma KeyCryptKeyI:
+Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>))
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \<in> set evs;
+on evs"
-evs \<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs"
+apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
-apply (unfold KeyCryptKey_def)
+apply blast
+done
+lemma Tgs_Unique:
+"\<lbrakk> Says Tgs A
+(Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs;
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow>
+Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>))
+on evs"
+apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
+apply blast
+done
+subsection{*Lemmas About the Predicate @{term AKcryptSK}*}
+lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
+by (simp add: AKcryptSK_def)
+lemma AKcryptSKI:
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
+evs \<in> kerbIV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
+apply (unfold AKcryptSK_def)
 apply (blast dest: Says_Tgs_message_form)
 done
-lemma KeyCryptKey_Says [simp]:
+lemma AKcryptSK_Says [simp]:
-"KeyCryptKey AuthKey ServKey (Says S A X # evs) =
+"AKcryptSK authK servK (Says S A X # evs) =
 (Tgs = S &
-(\<exists>B tt. X = Crypt AuthKey
+(\<exists>B Ts. X = Crypt authK
-{|Key ServKey, Agent B, tt,
+\<lbrace>Key servK, Agent B, Number Ts,
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
-| KeyCryptKey AuthKey ServKey evs)"
+| AKcryptSK authK servK evs)"
-apply (unfold KeyCryptKey_def)
+apply (unfold AKcryptSK_def)
 apply (simp (no_asm))
 apply blast
 done
-(*A fresh AuthKey cannot be associated with any other
+(*A fresh authK cannot be associated with any other
 (with respect to a given trace). *)
-lemma Auth_fresh_not_KeyCryptKey:
+lemma Auth_fresh_not_AKcryptSK:
-"[| Key AuthKey \<notin> used evs; evs \<in> kerberos |]
+"\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV \<rbrakk>
-==> ~ KeyCryptKey AuthKey ServKey evs"
+\<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold KeyCryptKey_def)
+apply (unfold AKcryptSK_def)
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
 done
-(*A fresh ServKey cannot be associated with any other
+(*A fresh servK cannot be associated with any other
 (with respect to a given trace). *)
-lemma Serv_fresh_not_KeyCryptKey:
+lemma Serv_fresh_not_AKcryptSK:
-"Key ServKey \<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs"
+"Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold KeyCryptKey_def, blast)
+apply (unfold AKcryptSK_def, blast)
 done
-lemma AuthKey_not_KeyCryptKey:
+lemma authK_not_AKcryptSK:
-"[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}
+"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
-\<in> parts (spies evs);  evs \<in> kerberos |]
+\<in> parts (spies evs);  evs \<in> kerbIV \<rbrakk>
-==> ~ KeyCryptKey K AuthKey evs"
+\<Longrightarrow> \<not> AKcryptSK K authK evs"
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 txt{*Fake*}
 apply blast
 txt{*K2: by freshness*}
-apply (simp add: KeyCryptKey_def)
+apply (simp add: AKcryptSK_def)
 txt{*K4*}
 apply (blast+)
 done
 text{*A secure serverkey cannot have been used to encrypt others*}
-lemma ServKey_not_KeyCryptKey:
+lemma servK_not_AKcryptSK:
-"[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \<in> parts (spies evs);
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs);
 Key SK \<notin> analz (spies evs);  SK \<in> symKeys;
-B \<noteq> Tgs;  evs \<in> kerberos |]
+B \<noteq> Tgs;  evs \<in> kerbIV \<rbrakk>
-==> ~ KeyCryptKey SK K evs"
+\<Longrightarrow> \<not> AKcryptSK SK K evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
 txt{*K4 splits into distinct subcases*}
 apply auto
-txt{*ServKey can't have been enclosed in two certificates*}
+txt{*servK can't have been enclosed in two certificates*}
 prefer 2 apply (blast dest: unique_CryptKey)
-txt{*ServKey is fresh and so could not have been used, by
+txt{*servK is fresh and so could not have been used, by
 @{text new_keys_not_used}*}
-apply (force dest!: Crypt_imp_invKey_keysFor simp add: KeyCryptKey_def)
+apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
 done
-text{*Long term keys are not issued as ServKeys*}
+text{*Long term keys are not issued as servKeys*}
-lemma shrK_not_KeyCryptKey:
+lemma shrK_not_AKcryptSK:
-"evs \<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs"
+"evs \<in> kerbIV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
-apply (unfold KeyCryptKey_def)
+apply (unfold AKcryptSK_def)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, auto)
 done
-text{*The Tgs message associates ServKey with AuthKey and therefore not with any
+text{*The Tgs message associates servK with authK and therefore not with any
-other key AuthKey.*}
+other key authK.*}
-lemma Says_Tgs_KeyCryptKey:
+lemma Says_Tgs_AKcryptSK:
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |})
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>)
 \<in> set evs;
-AuthKey' \<noteq> AuthKey;  evs \<in> kerberos |]
+authK' \<noteq> authK;  evs \<in> kerbIV \<rbrakk>
-==> ~ KeyCryptKey AuthKey' ServKey evs"
+\<Longrightarrow> \<not> AKcryptSK authK' servK evs"
-apply (unfold KeyCryptKey_def)
+apply (unfold AKcryptSK_def)
-apply (blast dest: unique_ServKeys)
+apply (blast dest: unique_servKeys)
 done
-lemma KeyCryptKey_not_KeyCryptKey:
+text{*Equivalently*}
-"[| KeyCryptKey AuthKey ServKey evs;  evs \<in> kerberos |]
+lemma not_different_AKcryptSK:
-==> ~ KeyCryptKey ServKey K evs"
+"\<lbrakk> AKcryptSK authK servK evs;
-apply (erule rev_mp)
+authK' \<noteq> authK;  evs \<in> kerbIV \<rbrakk>
-apply (erule kerberos.induct)
+\<Longrightarrow> \<not> AKcryptSK authK' servK evs  \<and> servK \<in> symKeys"
+apply (simp add: AKcryptSK_def)
+apply (blast dest: unique_servKeys Says_Tgs_message_form)
+done
+lemma AKcryptSK_not_AKcryptSK:
+"\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<not> AKcryptSK servK K evs"
+apply (erule rev_mp)
+apply (erule kerbIV.induct)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, safe)
 txt{*K4 splits into subcases*}
 apply simp_all
-prefer 4 apply (blast dest!: AuthKey_not_KeyCryptKey)
+prefer 4 apply (blast dest!: authK_not_AKcryptSK)
-txt{*ServKey is fresh and so could not have been used, by
+txt{*servK is fresh and so could not have been used, by
 @{text new_keys_not_used}*}
 prefer 2
-apply (force dest!: Crypt_imp_invKey_keysFor simp add: KeyCryptKey_def)
+apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
 txt{*Others by freshness*}
 apply (blast+)
 done
 text{*The only session keys that can be found with the help of session keys are
 those sent by Tgs in step K4.  *}
 text{*We 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 \<in> analz (Key`KK Un H)) --> (K:KK | Key K \<in> analz H)
+"P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
-==>
+\<Longrightarrow>
-P --> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
+P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
 by (blast intro: analz_mono [THEN subsetD])
-lemma KeyCryptKey_analz_insert:
+lemma AKcryptSK_analz_insert:
-"[| KeyCryptKey K K' evs; K \<in> symKeys; evs \<in> kerberos |]
+"\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV \<rbrakk>
-==> Key K' \<in> analz (insert (Key K) (spies evs))"
+\<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
-apply (simp add: KeyCryptKey_def, clarify)
+apply (simp add: AKcryptSK_def, clarify)
 apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
 done
-lemma AuthKeys_are_not_KeyCryptKey:
+lemma authKeys_are_not_AKcryptSK:
-"[| K \<in> AuthKeys evs Un range shrK;  evs \<in> kerberos |]
+"\<lbrakk> K \<in> authKeys evs Un range shrK;  evs \<in> kerbIV \<rbrakk>
-==> \<forall>SK. ~ KeyCryptKey SK K evs"
+\<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
-apply (simp add: KeyCryptKey_def)
+apply (simp add: authKeys_def AKcryptSK_def)
+apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
+done
+lemma not_authKeys_not_AKcryptSK:
+"\<lbrakk> K \<notin> authKeys evs;
+K \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
+apply (simp add: AKcryptSK_def)
 apply (blast dest: Says_Tgs_message_form)
 done
-lemma not_AuthKeys_not_KeyCryptKey:
-"[| K \<notin> AuthKeys evs;
-K \<notin> range shrK; evs \<in> kerberos |]
-==> \<forall>SK. ~ KeyCryptKey K SK evs"
-apply (simp add: KeyCryptKey_def)
-apply (blast dest: Says_Tgs_message_form)
-done
 subsection{*Secrecy Theorems*}
 text{*For the Oops2 case of the next theorem*}
-lemma Oops2_not_KeyCryptKey:
+lemma Oops2_not_AKcryptSK:
-"[| evs \<in> kerberos;
+"\<lbrakk> evs \<in> kerbIV;
-Says Tgs A (Crypt AuthKey
+Says Tgs A (Crypt authK
-{|Key ServKey, Agent B, Number Tt, ServTicket|})
+\<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
-\<in> set evs |]
+\<in> set evs \<rbrakk>
-==> ~ KeyCryptKey ServKey SK evs"
+\<Longrightarrow> \<not> AKcryptSK servK SK evs"
-apply (blast dest: KeyCryptKeyI KeyCryptKey_not_KeyCryptKey)
+apply (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
 done
 text{* Big 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.
 [simplified by LCP] *}
 lemma Key_analz_image_Key [rule_format (no_asm)]:
-"evs \<in> kerberos ==>
+"evs \<in> kerbIV \<Longrightarrow>
-(\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) -->
+(\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
-(\<forall>K \<in> KK. ~ KeyCryptKey K SK evs)   -->
+(\<forall>K \<in> KK. \<not> AKcryptSK K SK evs)   \<longrightarrow>
 (Key SK \<in> analz (Key`KK Un (spies evs))) =
 (SK \<in> KK | Key SK \<in> analz (spies evs)))"
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [10] Oops_range_spies2)
 apply (frule_tac [9] Oops_range_spies1)
 apply (frule_tac [7] Says_tgs_message_form)
 apply (frule_tac [5] Says_kas_message_form)
 apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
 txt{*Case-splits for Oops1 and message 5: the negated case simplifies using
 the induction hypothesis*}
-apply (case_tac [11] "KeyCryptKey AuthKey SK evsO1")
+apply (case_tac [11] "AKcryptSK authK SK evsO1")
-apply (case_tac [8] "KeyCryptKey ServKey SK evs5")
+apply (case_tac [8] "AKcryptSK servK SK evs5")
 apply (simp_all del: image_insert
-add: analz_image_freshK_simps KeyCryptKey_Says)
+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)
 txt{*Fake*}
 apply spy_analz
-apply (simp_all del: image_insert
-add: shrK_not_KeyCryptKey
-Oops2_not_KeyCryptKey Auth_fresh_not_KeyCryptKey
-Serv_fresh_not_KeyCryptKey Says_Tgs_KeyCryptKey Spy_analz_shrK)
---{*Splitting the @{text simp_all} into two parts makes it faster.*}
 txt{*K2*}
 apply blast
 txt{*K3*}
 apply blast
 txt{*K4*}
-apply (blast dest!: AuthKey_not_KeyCryptKey)
+apply (blast dest!: authK_not_AKcryptSK)
 txt{*K5*}
-apply (case_tac "Key ServKey \<in> analz (spies evs5) ")
+apply (case_tac "Key servK \<in> analz (spies evs5) ")
-txt{*If ServKey is compromised then the result follows directly...*}
+txt{*If 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 ServKey is uncompromised.*}
+txt{*...therefore servK is uncompromised.*}
-txt{*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*}
+txt{*The AKcryptSK servK SK evs5 case leads to a contradiction.*}
-apply (blast elim!: ServKey_not_KeyCryptKey [THEN [2] rev_notE] del: allE ballE)
+apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
 txt{*Another K5 case*}
 apply blast
 txt{*Oops1*}
 apply simp
-apply (blast dest!: KeyCryptKey_analz_insert)
+apply (blast dest!: AKcryptSK_analz_insert)
 done
 text{* First simplification law for analz: no session keys encrypt
 authentication keys or shared keys. *}
 lemma analz_insert_freshK1:
-"[| evs \<in> kerberos;  K \<in> (AuthKeys evs) Un range shrK;
+"\<lbrakk> evs \<in> kerbIV;  K \<in> authKeys evs Un range shrK;
-K \<in> symKeys;
+SesKey \<notin> range shrK \<rbrakk>
-SesKey \<notin> range shrK |]
+\<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
-==> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
 (K = SesKey | Key K \<in> analz (spies evs))"
-apply (frule AuthKeys_are_not_KeyCryptKey, assumption)
+apply (frule authKeys_are_not_AKcryptSK, assumption)
 apply (simp del: image_insert
 add: analz_image_freshK_simps add: Key_analz_image_Key)
 done
 text{* Second simplification law for analz: no service keys encrypt any other keys.*}
 lemma analz_insert_freshK2:
-"[| evs \<in> kerberos;  ServKey \<notin> (AuthKeys evs); ServKey \<notin> range shrK;
+"\<lbrakk> evs \<in> kerbIV;  servK \<notin> (authKeys evs); servK \<notin> range shrK;
-K \<in> symKeys|]
+K \<in> symKeys \<rbrakk>
-==> (Key K \<in> analz (insert (Key ServKey) (spies evs))) =
+\<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
-(K = ServKey | Key K \<in> analz (spies evs))"
+(K = servK | Key K \<in> analz (spies evs))"
-apply (frule not_AuthKeys_not_KeyCryptKey, assumption, assumption)
+apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
 apply (simp del: image_insert
 add: analz_image_freshK_simps add: Key_analz_image_Key)
 done
-text{* Third simplification law for analz: only one authentication key encrypts a
+text{* Third simplification law for analz: only one authentication key encrypts a certain service key.*}
-certain service key.*}
 lemma analz_insert_freshK3:
-"[| Says Tgs A
+"\<lbrakk> AKcryptSK authK servK evs;
-(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
-\<in> set evs;  ServKey \<in> symKeys;
+\<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
-AuthKey \<noteq> AuthKey'; AuthKey' \<notin> range shrK; evs \<in> kerberos |]
+(servK = authK' | Key servK \<in> analz (spies evs))"
-==> (Key ServKey \<in> analz (insert (Key AuthKey') (spies evs))) =
+apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
-(ServKey = AuthKey' | Key ServKey \<in> analz (spies evs))"
-apply (drule_tac AuthKey' = AuthKey' in Says_Tgs_KeyCryptKey, blast, assumption)
 apply (simp del: image_insert
 add: analz_image_freshK_simps add: Key_analz_image_Key)
 done
+lemma analz_insert_freshK3_bis:
+"\<lbrakk> Says Tgs A
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
+\<in> set evs;
+authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
+(servK = authK' | Key servK \<in> analz (spies evs))"
+apply (frule AKcryptSKI, assumption)
+apply (simp add: analz_insert_freshK3)
+done
 text{*a weakness of the protocol*}
-lemma AuthKey_compromises_ServKey:
+lemma authK_compromises_servK:
-"[| Says Tgs A
+"\<lbrakk> Says Tgs A
-(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
-\<in> set evs;  AuthKey \<in> symKeys;
+\<in> set evs;  authK \<in> symKeys;
-Key AuthKey \<in> analz (spies evs); evs \<in> kerberos |]
+Key authK \<in> analz (spies evs); evs \<in> kerbIV \<rbrakk>
-==> Key ServKey \<in> analz (spies evs)"
+\<Longrightarrow> Key servK \<in> analz (spies evs)"
 by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
+lemma servK_notin_authKeysD:
-subsection{* Guarantees for Kas *}
+"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts,
-lemma ServKey_notin_AuthKeysD:
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
-"[| Crypt AuthKey {|Key ServKey, Agent B, Tt,
+\<in> parts (spies evs);
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}
+Key servK \<notin> analz (spies evs);
-\<in> parts (spies evs);
+B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
-Key ServKey \<notin> analz (spies evs);
+\<Longrightarrow> servK \<notin> authKeys evs"
-B \<noteq> Tgs; evs \<in> kerberos |]
+apply (erule rev_mp)
-==> ServKey \<notin> AuthKeys evs"
+apply (erule rev_mp)
-apply (erule rev_mp)
+apply (simp add: authKeys_def)
-apply (erule rev_mp)
+apply (erule kerbIV.induct, analz_mono_contra)
-apply (simp add: AuthKeys_def)
-apply (erule kerberos.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
 apply (blast+)
 done
 text{*If Spy sees the Authentication Key sent in msg K2, then
 the Key has expired.*}
 lemma Confidentiality_Kas_lemma [rule_format]:
-"[| AuthKey \<in> symKeys; A \<notin> bad;  evs \<in> kerberos |]
+"\<lbrakk> authK \<in> symKeys; A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-==> Says Kas A
+\<Longrightarrow> Says Kas A
 (Crypt (shrK A)
-{|Key AuthKey, Agent Tgs, Number Tk,
+\<lbrace>Key authK, Agent Tgs, Number Ta,
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
-\<in> set evs -->
+\<in> set evs \<longrightarrow>
-Key AuthKey \<in> analz (spies evs) -->
+Key authK \<in> analz (spies evs) \<longrightarrow>
-ExpirAuth Tk evs"
+expiredAK Ta evs"
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (frule_tac [10] Oops_range_spies2)
 apply (frule_tac [9] Oops_range_spies1)
 apply (frule_tac [7] Says_tgs_message_form)
 apply (frule_tac [5] Says_kas_message_form)
 apply (safe del: impI conjI impCE)
 txt{*K2*}
 apply blast
 txt{*K4*}
 apply blast
 txt{*Level 8: K5*}
-apply (blast dest: ServKey_notin_AuthKeysD Says_Kas_message_form intro: less_SucI)
+apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
 txt{*Oops1*}
-apply (blast dest!: unique_AuthKeys intro: less_SucI)
+apply (blast dest!: unique_authKeys intro: less_SucI)
 txt{*Oops2*}
 apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
 done
 lemma Confidentiality_Kas:
-"[| Says Kas A
+"\<lbrakk> Says Kas A
-(Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})
+(Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
 \<in> set evs;
-~ ExpirAuth Tk evs;
+\<not> expiredAK Ta evs;
-A \<notin> bad;  evs \<in> kerberos |]
+A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-==> Key AuthKey \<notin> analz (spies evs)"
+\<Longrightarrow> Key authK \<notin> analz (spies evs)"
 by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
-subsection{* Guarantees for Tgs *}
 text{*If Spy sees the Service Key sent in msg K4, then
 the Key has expired.*}
 lemma Confidentiality_lemma [rule_format]:
-"[| Says Tgs A
+"\<lbrakk> Says Tgs A
-	    (Crypt AuthKey
+	    (Crypt authK
-	       {|Key ServKey, Agent B, Number Tt,
+	       \<lbrace>Key servK, Agent B, Number Ts,
-		 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})
+		 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
 	   \<in> set evs;
-	Key AuthKey \<notin> analz (spies evs);
+	Key authK \<notin> analz (spies evs);
-ServKey \<in> symKeys;
+servK \<in> symKeys;
-	A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+	A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
-==> Key ServKey \<in> analz (spies evs) -->
+\<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
-	  ExpirServ Tt evs"
+	  expiredSK Ts evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct)
+apply (erule kerbIV.induct)
 apply (rule_tac [9] impI)+;
 --{*The Oops1 case is unusual: must simplify
 @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
 @{text analz_mono_contra} weaken it to
 @{term "Authkey \<notin> analz (spies evs)"},
-for we then conclude @{term "AuthKey \<noteq> AuthKeya"}.*}
+for we then conclude @{term "authK \<noteq> authKa"}.*}
 apply analz_mono_contra
 apply (frule_tac [10] Oops_range_spies2)
 apply (frule_tac [9] Oops_range_spies1)
 apply (frule_tac [7] Says_tgs_message_form)
 apply (frule_tac [5] 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 pushes)
+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)
 txt{*Fake*}
 apply spy_analz
 txt{*K2*}
 apply (blast intro: parts_insertI less_SucI)
 txt{*K4*}
-apply (blast dest: A_trusts_AuthTicket Confidentiality_Kas)
+apply (blast dest: authTicket_authentic Confidentiality_Kas)
 txt{*Oops2*}
 prefer 3
 apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
 txt{*Oops1*}
 prefer 2
 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
-txt{*K5.  Not clear how this step could be integrated with the main
+txt{*K5. Not obvious how this step could be integrated with the main
-simplification step.*}
+simplification step. Done in KerberosV.thy *}
 apply clarify
 apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl)
-apply (frule Says_imp_spies [THEN parts.Inj, THEN ServKey_notin_AuthKeysD])
+apply (frule Says_imp_spies [THEN parts.Inj, THEN servK_notin_authKeysD])
 apply (assumption, blast, assumption)
 apply (simp add: analz_insert_freshK2)
 apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
 done
-text{* In the real world Tgs can't check wheter AuthKey is secure! *}
+text{* In the real world Tgs can't check wheter authK is secure! *}
-lemma Confidentiality_Tgs1:
+lemma Confidentiality_Tgs:
-"[| Says Tgs A
+"\<lbrakk> Says Tgs A
-(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evs;
-Key AuthKey \<notin> analz (spies evs);
+Key authK \<notin> analz (spies evs);
-~ ExpirServ Tt evs;
+\<not> expiredSK Ts evs;
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
-==> Key ServKey \<notin> analz (spies evs)"
+\<Longrightarrow> Key servK \<notin> analz (spies evs)"
 apply (blast dest: Says_Tgs_message_form Confidentiality_lemma)
 done
 text{* In the real world Tgs CAN check what Kas sends! *}
-lemma Confidentiality_Tgs2:
+lemma Confidentiality_Tgs_bis:
-"[| Says Kas A
+"\<lbrakk> Says Kas A
-(Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})
+(Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
 \<in> set evs;
 Says Tgs A
-(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evs;
-~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
+\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
-==> Key ServKey \<notin> analz (spies evs)"
+\<Longrightarrow> Key servK \<notin> analz (spies evs)"
-apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs1)
+apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
 done
 text{*Most general form*}
-lemmas Confidentiality_Tgs3 = A_trusts_AuthTicket [THEN Confidentiality_Tgs2]
+lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
+lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]
-subsection{* Guarantees for Alice *}
+text{*Needs a confidentiality guarantee, hence moved here.
-lemmas Confidentiality_Auth_A = A_trusts_AuthKey [THEN Confidentiality_Kas]
+Authenticity of servK for A*}
+lemma servK_authentic_bis_r:
-lemma A_trusts_K4_bis:
+"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
-"[| Says Kas A
+\<in> parts (spies evs);
-(Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \<in> set evs;
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
-Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
+\<in> parts (spies evs);
+\<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
+\<in> set evs"
+apply (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
+done
+lemma Confidentiality_Serv_A:
+"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
+A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Key servK \<notin> 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:
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
+A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Key servK \<notin> analz (spies evs)"
+apply (frule authK_authentic)
+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
+(*
+The proof above is fast.  It can be done in one command in 17 secs:
+apply (blast dest: authK_authentic servK_authentic
+Says_Kas_message_form servTicket_authentic
+unique_servKeys unique_authKeys
+Confidentiality_Kas
+Confidentiality_Tgs_bis)
+It is very brittle: we can't use this command partway
+through the script above.
+*)
+lemma u_Confidentiality_B:
+"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredSK Ts evs;
+A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Key servK \<notin> analz (spies evs)"
+apply (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
+done
+subsection{*Parties authentication: each party verifies "the identity of
+another party who generated some data" (quoted from Neuman and Ts'o).*}
+text{*These 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.*}
+text{*@{text Tgs_authenticates_A} can be found above*}
+lemma A_authenticates_Tgs:
+"\<lbrakk> Says Kas A
+(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
 \<in> parts (spies evs);
-Key AuthKey \<notin> analz (spies evs);
+Key authK \<notin> analz (spies evs);
-evs \<in> kerberos |]
+evs \<in> kerbIV \<rbrakk>
-==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+\<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
 \<in> set evs"
 apply (frule Says_Kas_message_form, assumption)
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
 txt{*K2 and K4 remain*}
 prefer 2 apply (blast dest!: unique_CryptKey)
-apply (blast dest!: A_trusts_K4 Says_Tgs_message_form AuthKeys_used)
+apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
 done
-lemma Confidentiality_Serv_A:
+lemma B_authenticates_A:
-"[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
-\<in> parts (spies evs);
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
+\<in> parts (spies evs);
-\<in> parts (spies evs);
+Key servK \<notin> analz (spies evs);
-~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
+A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
-==> Key ServKey \<notin> analz (spies evs)"
+Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
-apply (drule A_trusts_AuthKey, assumption, assumption)
+apply (blast dest: servTicket_authentic_Tgs intro: Says_K5)
-apply (blast dest: Confidentiality_Kas Says_Kas_message_form A_trusts_K4_bis Confidentiality_Tgs2)
+done
-done
+text{*The second assumption tells B what kind of key servK is.*}
+lemma B_authenticates_A_r:
-subsection{* Guarantees for Bob *}
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
-text{* Theorems for the refined model have suffix "refined"                *}
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);
-lemma K4_imp_K2:
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+\<in> parts (spies evs);
-\<in> set evs;  evs \<in> kerberos|]
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
-==> \<exists>Tk. Says Kas A
+\<in> parts (spies evs);
-(Crypt (shrK A)
+\<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
-{|Key AuthKey, Agent Tgs, Number Tk,
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
+\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
-\<in> set evs"
+Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
-apply (erule rev_mp)
+apply (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
-apply (erule kerberos.induct)
+done
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
+text{* @{text u_B_authenticates_A} would be the same as @{text B_authenticates_A} because the servK confidentiality assumption is yet unrelaxed*}
-apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN A_trusts_AuthTicket])
-done
+lemma u_B_authenticates_A_r:
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
-lemma K4_imp_K2_refined:
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+\<in> parts (spies evs);
-\<in> set evs; evs \<in> kerberos|]
+\<not> expiredSK Ts evs;
-==> \<exists>Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
+\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
-\<in> set evs
+Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
-& ServLife + Tt <= AuthLife + Tk)"
+apply (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
-apply (erule rev_mp)
+done
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+lemma A_authenticates_B:
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
+"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
-apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN A_trusts_AuthTicket])
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
-done
+\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
-text{*Authenticity of ServKey for B*}
+\<in> parts (spies evs);
-lemma B_trusts_ServKey:
+Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}
+A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
-\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
+\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
-evs \<in> kerberos |]
+apply (frule authK_authentic)
-==> \<exists>AuthKey.
+apply assumption+
-Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,
+apply (frule servK_authentic)
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|})
+prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form)
-\<in> set evs"
+apply assumption+
-apply (erule rev_mp)
+apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6)
-apply (erule kerberos.induct)
+(*Single command proof: slower!
-apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
-apply (blast+)
-done
-lemma B_trusts_ServTicket_Kas:
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
-evs \<in> kerberos |]
-==> \<exists>AuthKey Tk.
-Says Kas A
-(Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
-\<in> set evs"
-by (blast dest!: B_trusts_ServKey K4_imp_K2)
-lemma B_trusts_ServTicket_Kas_refined:
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
-evs \<in> kerberos |]
-==> \<exists>AuthKey Tk. Says Kas A (Crypt(shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
-\<in> set evs
-& ServLife + Tt <= AuthLife + Tk"
-by (blast dest!: B_trusts_ServKey K4_imp_K2_refined)
-lemma B_trusts_ServTicket:
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
-evs \<in> kerberos |]
-==> \<exists>Tk AuthKey.
-Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
-\<in> set evs
-& Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})
-\<in> set evs"
-by (blast dest: B_trusts_ServKey K4_imp_K2)
-lemma B_trusts_ServTicket_refined:
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
-evs \<in> kerberos |]
-==> \<exists>Tk AuthKey.
-(Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
-Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})
-\<in> set evs
-& Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})
-\<in> set evs
-& ServLife + Tt <= AuthLife + Tk)"
-by (blast dest: B_trusts_ServKey K4_imp_K2_refined)
-lemma NotExpirServ_NotExpirAuth_refined:
-"[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]
-==> ~ ExpirAuth Tk evs"
-by (blast dest: leI le_trans dest: leD)
-lemma Confidentiality_B:
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
-\<in> parts (spies evs);
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
-\<in> parts (spies evs);
-~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
-==> Key ServKey \<notin> analz (spies evs)"
-apply (frule A_trusts_AuthKey)
-apply (frule_tac [3] Confidentiality_Kas)
-apply (frule_tac [6] B_trusts_ServTicket, auto)
-apply (blast dest!: Confidentiality_Tgs2 dest: Says_Kas_message_form A_trusts_K4 unique_ServKeys unique_AuthKeys)
-done
-(*
-The proof above is fast.  It can be done in one command in 17 secs:
-apply (blast dest: A_trusts_AuthKey A_trusts_K4
-Says_Kas_message_form B_trusts_ServTicket
-unique_ServKeys unique_AuthKeys
-Confidentiality_Kas
-Confidentiality_Tgs2)
-It is very brittle: we can't use this command partway
-through the script above.
 *)
+done
+lemma A_authenticates_B_r:
-text{*Most general form -- only for refined model! *}
+"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
-lemma Confidentiality_B_refined:
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
-"[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+\<in> parts (spies evs);
-\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
-~ ExpirServ Tt evs;
+\<in> parts (spies evs);
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
-==> Key ServKey \<notin> analz (spies evs)"
+A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
-apply (blast dest: B_trusts_ServTicket_refined NotExpirServ_NotExpirAuth_refined Confidentiality_Tgs2)
+\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
-done
+apply (frule authK_authentic)
-subsection{* Authenticity theorems *}
-text{*1. Session Keys authenticity: they originated with servers.*}
-text{*Authenticity of ServKey for A*}
-lemma A_trusts_ServKey:
-"[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
-\<in> parts (spies evs);
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
-\<in> parts (spies evs);
-~ ExpirAuth Tk evs; A \<notin> bad; evs \<in> kerberos |]
-==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
-\<in> set evs"
-by (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis)
-text{*Note: requires a temporal check*}
-(***2. Parties authenticity: each party verifies "the identity of
-another party who generated some data" (quoted from Neuman & Ts'o).***)
-(*These 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.***)
-text{*B checks authenticity of A by theorems @{text A_Authenticity} and
-@{text A_authenticity_refined} *}
-lemma Says_Auth:
-"[| Crypt ServKey {|Agent A, Number Ta|} \<in> parts (spies evs);
-Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,
-ServTicket|}) \<in> set evs;
-Key ServKey \<notin> analz (spies evs);
-A \<notin> bad; B \<notin> bad; evs \<in> kerberos |]
-==> Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \<in> set evs"
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [5] Says_ticket_in_parts_spies)
-apply (frule_tac [7] Says_ticket_in_parts_spies)
-apply (simp_all (no_asm_simp) add: all_conj_distrib)
-apply blast
-txt{*K3*}
-apply (blast dest: A_trusts_AuthKey Says_Kas_message_form Says_Tgs_message_form)
-txt{*K4*}
-apply (force dest!: Crypt_imp_keysFor)
-txt{*K5*}
-apply (blast dest: Key_unique_SesKey)
-done
-text{*The second assumption tells B what kind of key ServKey is.*}
-lemma A_Authenticity:
-"[| Crypt ServKey {|Agent A, Number Ta|} \<in> parts (spies evs);
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
-\<in> parts (spies evs);
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
-\<in> parts (spies evs);
-~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
-==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},
-Crypt ServKey {|Agent A, Number Ta|} |} \<in> set evs"
-by (blast intro: Says_Auth dest: Confidentiality_B Key_unique_SesKey B_trusts_ServKey)
-text{*Stronger form in the refined model*}
-lemma A_Authenticity_refined:
-"[| Crypt ServKey {|Agent A, Number Ta2|} \<in> parts (spies evs);
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
-\<in> parts (spies evs);
-~ ExpirServ Tt evs;
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
-==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},
-Crypt ServKey {|Agent A, Number Ta2|} |} \<in> set evs"
-by (blast dest: Confidentiality_B_refined B_trusts_ServKey Key_unique_SesKey intro: Says_Auth)
-text{*A checks authenticity of B by theorem @{text B_authenticity}*}
-lemma Says_K6:
-"[| Crypt ServKey (Number Ta) \<in> parts (spies evs);
-Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,
-ServTicket|}) \<in> set evs;
-Key ServKey \<notin> analz (spies evs);
-A \<notin> bad; B \<notin> bad; evs \<in> kerberos |]
-==> Says B A (Crypt ServKey (Number Ta)) \<in> set evs"
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [5] Says_ticket_in_parts_spies)
-apply (frule_tac [7] Says_ticket_in_parts_spies)
-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
-lemma K4_trustworthy:
-"[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|}
-\<in> parts (spies evs);
-Key AuthKey \<notin> analz (spies evs);  AuthKey \<notin> range shrK;
-evs \<in> kerberos |]
-==> \<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})
-\<in> set evs"
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
-apply (blast+)
-done
-lemma B_Authenticity:
-"[| Crypt ServKey (Number Ta) \<in> parts (spies evs);
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
-\<in> parts (spies evs);
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
-\<in> parts (spies evs);
-~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
-==> Says B A (Crypt ServKey (Number Ta)) \<in> set evs"
-apply (frule A_trusts_AuthKey)
 apply (frule_tac [3] Says_Kas_message_form)
 apply (frule_tac [4] Confidentiality_Kas)
-apply (frule_tac [7] K4_trustworthy)
+apply (frule_tac [7] servK_authentic)
 prefer 8 apply blast
 apply (erule_tac [9] exE)
 apply (frule_tac [9] K4_imp_K2)
-txt{*Yes the proof's a mess, but I don't know how to improve it.*}
 apply assumption+
-apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs1
+apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs
 )
 done
-(***3. Parties' knowledge of session keys. A knows a session key if she
+subsection{* Key distribution guarantees
-used it to build a cipher.***)
+An agent knows a session key if he used it to issue a cipher.
+These guarantees also convey a stronger form of
-lemma B_Knows_B_Knows_ServKey_lemma:
+authentication - non-injective agreement on the session key*}
-"[| Says B A (Crypt ServKey (Number Ta)) \<in> set evs;
-Key ServKey \<notin> analz (spies evs);
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+lemma Kas_Issues_A:
-==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+"\<lbrakk> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs;
+evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
+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 kerbIV.induct)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (frule_tac [5] Says_ticket_parts)
-apply (frule_tac [5] Says_ticket_in_parts_spies)
+apply (frule_tac [7] Says_ticket_parts)
-apply (frule_tac [7] Says_ticket_in_parts_spies)
 apply (simp_all (no_asm_simp) add: all_conj_distrib)
-apply blast
+txt{*K2*}
-txt{*K6 requires numerous lemmas*}
 apply (simp add: takeWhile_tail)
-apply (blast dest: B_trusts_ServTicket parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: Says_K6)
+apply (blast dest: authK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD])
 done
-(*Key ServKey \<notin> analz (spies evs) could be relaxed by Confidentiality_B
-but this is irrelevant because B knows what he knows!                  *)
+lemma A_authenticates_and_keydist_to_Kas:
+"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace> \<in> parts (spies evs);
-lemma B_Knows_B_Knows_ServKey:
+A \<notin> bad; evs \<in> kerbIV \<rbrakk>
-"[| Says B A (Crypt ServKey (Number Ta)) \<in> set evs;
+\<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+on evs"
-\<in> parts (spies evs);
+apply (blast dest: authK_authentic Kas_Issues_A)
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
+done
-\<in> parts (spies evs);
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
+lemma honest_never_says_newer_timestamp_in_auth:
-\<in> parts (spies evs);
+"\<lbrakk> (CT evs) \<le> T; A \<notin> bad; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk>
-~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
+\<Longrightarrow> \<forall> B Y.  Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+apply (erule rev_mp)
-==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+apply (erule kerbIV.induct)
-by (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma)
+apply (simp_all)
+apply force+
-lemma B_Knows_B_Knows_ServKey_refined:
+done
-"[| Says B A (Crypt ServKey (Number Ta)) \<in> set evs;
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+lemma honest_never_says_current_timestamp_in_auth:
-\<in> parts (spies evs);
+"\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk>
-~ ExpirServ Tt evs;
+\<Longrightarrow> \<forall> A B Y. A \<notin> bad \<longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+apply (frule eq_imp_le)
-==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+apply (blast dest: honest_never_says_newer_timestamp_in_auth)
-by (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma)
+done
-lemma A_Knows_B_Knows_ServKey:
+lemma A_trusts_secure_authenticator:
-"[| Crypt ServKey (Number Ta) \<in> parts (spies evs);
+"\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs);
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
+Key K \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk>
-\<in> parts (spies evs);
+\<Longrightarrow> \<exists> B X. Says A Tgs \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>, Agent B\<rbrace> \<in> set evs \<or>
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
+Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs";
-\<in> parts (spies evs);
+apply (erule rev_mp)
-~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
+apply (erule rev_mp)
-A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+apply (erule kerbIV.induct, analz_mono_contra)
-==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+apply (frule_tac [5] Says_ticket_parts)
-by (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma)
+apply (frule_tac [7] Says_ticket_parts)
+apply (simp_all add: all_conj_distrib)
-lemma K3_imp_K2:
+apply blast+
-"[| Says A Tgs
+done
-{|AuthTicket, Crypt AuthKey {|Agent A, Number Ta|}, Agent B|}
-\<in> set evs;
+lemma A_Issues_Tgs:
-A \<notin> bad;  evs \<in> kerberos |]
+"\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
-==> \<exists>Tk. Says Kas A (Crypt (shrK A)
+\<in> set evs;
-{|Key AuthKey, Agent Tgs, Tk, AuthTicket|})
+Key authK \<notin> analz (spies evs);
-\<in> set evs"
+A \<notin> bad; evs \<in> kerbIV \<rbrakk>
-apply (erule rev_mp)
+\<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast)
-apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN A_trusts_AuthKey])
-done
-lemma K4_trustworthy':
-"[| Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
-\<in> parts (spies evs);
-Says Kas A (Crypt (shrK A)
-{|Key AuthKey, Agent Tgs, Tk, AuthTicket|})
-\<in> set evs;
-Key AuthKey \<notin> analz (spies evs);
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
-==> Says Tgs A (Crypt AuthKey
-{|Key ServKey, Agent B, Number Tt, ServTicket|})
-\<in> set evs"
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
-apply (force dest!: Crypt_imp_keysFor)
-apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN A_trusts_AuthTicket] unique_AuthKeys)
-done
-lemma A_Knows_A_Knows_ServKey_lemma:
-"[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|}
-\<in> set evs;
-Key ServKey \<notin> analz (spies evs);
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
-==> A Issues B with (Crypt ServKey {|Agent A, Number 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 rev_mp)
-apply (erule kerberos.induct, analz_mono_contra)
+apply (erule kerbIV.induct, analz_mono_contra)
-apply (frule_tac [5] Says_ticket_in_parts_spies)
+apply (frule_tac [5] Says_ticket_parts)
-apply (frule_tac [7] Says_ticket_in_parts_spies)
+apply (frule_tac [7] Says_ticket_parts)
+apply (simp_all (no_asm_simp) add: all_conj_distrib)
+txt{*fake*}
+apply blast
+txt{*K3*}
+(*
+apply clarify
+apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption, assumption, assumption)
+*)
+apply (simp add: takeWhile_tail)
+apply auto
+apply (force dest!: authK_authentic Says_Kas_message_form)
+apply (drule parts_spies_takeWhile_mono [THEN subsetD, THEN parts_spies_evs_revD2 [THEN subsetD]])
+apply (drule A_trusts_secure_authenticator, assumption, assumption)
+apply (simp add: honest_never_says_current_timestamp_in_auth)
+done
+lemma Tgs_authenticates_and_keydist_to_A:
+"\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs);
+Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
+\<in> parts (spies evs);
+Key authK \<notin> analz (spies evs);
+A \<notin> bad; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
+apply (blast dest: A_Issues_Tgs Tgs_authenticates_A)
+done
+lemma Tgs_Issues_A:
+"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>)
+\<in> set evs;
+Key authK \<notin> analz (spies evs);  evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> Tgs Issues A with
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) 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 kerbIV.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)
+txt{*K4*}
+apply (simp add: takeWhile_tail)
+(*Last two thms installed only to derive authK \<notin> 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:
+"\<lbrakk>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> \<in> parts (spies evs);
+Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> \<exists>A. Tgs Issues A with
+(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
+apply (blast dest: Tgs_Issues_A servK_authentic_bis)
+done
+lemma B_Issues_A:
+"\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
+Key servK \<notin> analz (spies evs);
+A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> 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 kerbIV.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
+txt{*K6 requires numerous lemmas*}
+apply (simp add: takeWhile_tail)
+apply (blast dest: servTicket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: Says_K6)
+done
+lemma B_Issues_A_r:
+"\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
+A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
+apply (blast dest!: Confidentiality_B B_Issues_A)
+done
+lemma u_B_Issues_A_r:
+"\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredSK Ts evs;
+A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
+apply (blast dest!: u_Confidentiality_B B_Issues_A)
+done
+lemma A_authenticates_and_keydist_to_B:
+"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
+A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
+apply (blast dest!: A_authenticates_B B_Issues_A)
+done
+lemma A_authenticates_and_keydist_to_B_r:
+"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
+\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
+A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
+apply (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A)
+done
+lemma A_Issues_B:
+"\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace>
+\<in> set evs;
+Key servK \<notin> analz (spies evs);
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) 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 kerbIV.induct, analz_mono_contra)
+apply (frule_tac [5] Says_ticket_parts)
+apply (frule_tac [7] Says_ticket_parts)
 apply (simp_all (no_asm_simp))
 apply clarify
 txt{*K5*}
 apply auto
 apply (simp add: takeWhile_tail)
 txt{*Level 15: case study necessary because the assumption doesn't state
-the form of ServTicket. The guarantee becomes stronger.*}
+the form of servTicket. The guarantee becomes stronger.*}
 apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
-K3_imp_K2 K4_trustworthy'
+K3_imp_K2 servK_authentic_ter
 parts_spies_takeWhile_mono [THEN subsetD]
 parts_spies_evs_revD2 [THEN subsetD]
-intro: Says_Auth)
+intro: Says_K5)
 apply (simp add: takeWhile_tail)
 done
-lemma A_Knows_A_Knows_ServKey:
+lemma A_Issues_B_r:
-"[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|}
+"\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace>
 \<in> set evs;
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
 \<in> parts (spies evs);
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
 \<in> parts (spies evs);
-~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
+\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
+\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-by (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma)
+apply (blast dest!: Confidentiality_Serv_A A_Issues_B)
+done
-lemma B_Knows_A_Knows_ServKey:
-"[| Crypt ServKey {|Agent A, Number Ta|} \<in> parts (spies evs);
+lemma B_authenticates_and_keydist_to_A:
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
-\<in> parts (spies evs);
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
-Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}
+\<in> parts (spies evs);
-\<in> parts (spies evs);
+Key servK \<notin> analz (spies evs);
-Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-\<in> parts (spies evs);
+\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
+apply (blast dest: B_authenticates_A A_Issues_B)
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
+done
-==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
-by (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma)
+lemma B_authenticates_and_keydist_to_A_r:
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
-lemma B_Knows_A_Knows_ServKey_refined:
+\<in> parts (spies evs);
-"[| Crypt ServKey {|Agent A, Number Ta|} \<in> parts (spies evs);
+Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
-Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+\<in> parts (spies evs);
-\<in> parts (spies evs);
+Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
-~ ExpirServ Tt evs;
+\<in> parts (spies evs);
-B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
+\<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
-==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
-by (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma)
+\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
+apply (blast dest: B_authenticates_A Confidentiality_B A_Issues_B)
+done
+text{* @{text u_B_authenticates_and_keydist_to_A} would be the same as @{text B_authenticates_and_keydist_to_A} because the
+servK confidentiality assumption is yet unrelaxed*}
+lemma u_B_authenticates_and_keydist_to_A_r:
+"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
+Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
+\<in> parts (spies evs);
+\<not> expiredSK Ts evs;
+B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
+\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
+apply (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B)
+done
 end

changeset 18886	9f27383426db
parent 16796	140f1e0ea846
child 20768	1d478c2d621f