--- a/src/HOL/Auth/KerberosIV.ML Thu Sep 04 11:08:24 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1334 +0,0 @@
-(* Title: HOL/Auth/KerberosIV
- ID: $Id$
- Author: Giampaolo Bella, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-The Kerberos protocol, version IV. Proofs streamlined by lcp.
-*)
-
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-Pretty.setdepth 20;
-set timing;
-
-AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
-
-
-(** Reversed traces **)
-
-Goal "spies (evs @ [Says A B X]) = insert X (spies evs)";
-by (induct_tac "evs" 1);
-by (induct_tac "a" 2);
-by Auto_tac;
-qed "spies_Says_rev";
-
-Goal "spies (evs @ [Gets A X]) = spies evs";
-by (induct_tac "evs" 1);
-by (induct_tac "a" 2);
-by Auto_tac;
-qed "spies_Gets_rev";
-
-Goal "spies (evs @ [Notes A X]) = \
-\ (if A:bad then insert X (spies evs) else spies evs)";
-by (induct_tac "evs" 1);
-by (induct_tac "a" 2);
-by Auto_tac;
-qed "spies_Notes_rev";
-
-Goal "spies evs = spies (rev evs)";
-by (induct_tac "evs" 1);
-by (induct_tac "a" 2);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [spies_Says_rev, spies_Gets_rev,
- spies_Notes_rev])));
-qed "spies_evs_rev";
-bind_thm ("parts_spies_evs_revD2", spies_evs_rev RS equalityD2 RS parts_mono);
-
-Goal "spies (takeWhile P evs) <= spies evs";
-by (induct_tac "evs" 1);
-by (induct_tac "a" 2);
-by Auto_tac;
-(* Resembles "used_subset_append" in Event.ML*)
-qed "spies_takeWhile";
-bind_thm ("parts_spies_takeWhile_mono", spies_takeWhile RS parts_mono);
-
-
-(*****************LEMMAS ABOUT AuthKeys****************)
-
-Goalw [AuthKeys_def] "AuthKeys [] = {}";
-by (Simp_tac 1);
-qed "AuthKeys_empty";
-
-Goalw [AuthKeys_def]
- "(\\<forall>A Tk akey Peer. \
-\ ev \\<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk, \
-\ (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))\
-\ ==> AuthKeys (ev # evs) = AuthKeys evs";
-by Auto_tac;
-qed "AuthKeys_not_insert";
-
-Goalw [AuthKeys_def]
- "AuthKeys \
-\ (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk, \
-\ (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs) \
-\ = insert K (AuthKeys evs)";
-by Auto_tac;
-qed "AuthKeys_insert";
-
-Goalw [AuthKeys_def]
- "K \\<in> AuthKeys \
-\ (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk, \
-\ (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs) \
-\ ==> K = K' | K \\<in> AuthKeys evs";
-by Auto_tac;
-qed "AuthKeys_simp";
-
-Goalw [AuthKeys_def]
- "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk, \
-\ (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \\<in> set evs \
-\ ==> K \\<in> AuthKeys evs";
-by Auto_tac;
-qed "AuthKeysI";
-
-Goalw [AuthKeys_def] "K \\<in> AuthKeys evs ==> Key K \\<in> used evs";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "AuthKeys_used";
-
-
-(**** FORWARDING LEMMAS ****)
-
-(*--For reasoning about the encrypted portion of message K3--*)
-Goal "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
-\ \\<in> set evs ==> AuthTicket \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "K3_msg_in_parts_spies";
-
-Goal "Says Kas A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
-\ \\<in> set evs ==> AuthKey \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "Oops_parts_spies1";
-
-Goal "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|}) \
-\ \\<in> set evs ;\
-\ evs \\<in> kerberos |] ==> AuthKey \\<notin> range shrK";
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by Auto_tac;
-qed "Oops_range_spies1";
-
-(*--For reasoning about the encrypted portion of message K5--*)
-Goal "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
- \ \\<in> set evs ==> ServTicket \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "K5_msg_in_parts_spies";
-
-Goal "Says Tgs A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
-\ \\<in> set evs ==> ServKey \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "Oops_parts_spies2";
-
-Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) \
-\ \\<in> set evs ;\
-\ evs \\<in> kerberos |] ==> ServKey \\<notin> range shrK";
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by Auto_tac;
-qed "Oops_range_spies2";
-
-Goal "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \\<in> set evs \
-\ ==> Ticket \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "Says_ticket_in_parts_spies";
-(*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*)
-
-fun parts_induct_tac i =
- etac kerberos.induct i THEN
- REPEAT (FIRSTGOAL analz_mono_contra_tac) THEN
- ftac K3_msg_in_parts_spies (i+4) THEN
- ftac K5_msg_in_parts_spies (i+6) THEN
- ftac Oops_parts_spies1 (i+8) THEN
- ftac Oops_parts_spies2 (i+9) THEN
- prove_simple_subgoals_tac 1;
-
-
-(*Spy never sees another agent's shared key! (unless it's lost at start)*)
-Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
-by Auto_tac;
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-Goal "[| Key (shrK A) \\<in> parts (spies evs); evs \\<in> kerberos |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-
-(*Nobody can have used non-existent keys!*)
-Goal "evs \\<in> kerberos ==> \
-\ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
-by (parts_induct_tac 1);
-(*Fake*)
-by (force_tac (claset() addSDs [keysFor_parts_insert], simpset()) 1);
-(*Others*)
-by (ALLGOALS Blast_tac);
-qed_spec_mp "new_keys_not_used";
-Addsimps [new_keys_not_used];
-
-(*Earlier, all protocol proofs declared this theorem.
- But few of them actually need it! (Another is Yahalom) *)
-bind_thm ("new_keys_not_analzd",
- [analz_subset_parts RS keysFor_mono,
- new_keys_not_used] MRS contra_subsetD);
-
-
-(*********************** REGULARITY LEMMAS ***********************)
-(* concerning the form of items passed in messages *)
-(*****************************************************************)
-
-(*Describes the form of AuthKey, AuthTicket, and K sent by Kas*)
-Goal "[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|}) \
-\ \\<in> set evs; \
-\ evs \\<in> kerberos |] \
-\ ==> AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs & \
-\ AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|} ) &\
-\ K = shrK A & Peer = Tgs";
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [AuthKeys_def, AuthKeys_insert])));
-by (ALLGOALS Blast_tac);
-qed "Says_Kas_message_form";
-
-(*This lemma is essential for proving Says_Tgs_message_form:
-
- the session key AuthKey
- supplied by Kas in the authentication ticket
- cannot be a long-term key!
-
- Generalised to any session keys (both AuthKey and ServKey).
-*)
-Goal "[| Crypt (shrK Tgs_B) {|Agent A, Agent Tgs_B, Key SesKey, Number T|}\
-\ \\<in> parts (spies evs); Tgs_B \\<notin> bad;\
-\ evs \\<in> kerberos |] \
-\ ==> SesKey \\<notin> range shrK";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "SesKey_is_session_key";
-
-Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|} \
-\ \\<in> parts (spies evs); \
-\ evs \\<in> kerberos |] \
-\ ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, \
-\ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|}) \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake, K4*)
-by (ALLGOALS Blast_tac);
-qed "A_trusts_AuthTicket";
-
-Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}\
-\ \\<in> parts (spies evs);\
-\ evs \\<in> kerberos |] \
-\ ==> AuthKey \\<in> AuthKeys evs";
-by (ftac A_trusts_AuthTicket 1);
-by (assume_tac 1);
-by (simp_tac (simpset() addsimps [AuthKeys_def]) 1);
-by (Blast_tac 1);
-qed "AuthTicket_crypt_AuthKey";
-
-(*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*)
-Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
-\ \\<in> set evs; \
-\ evs \\<in> kerberos |] \
-\ ==> B \\<noteq> Tgs & ServKey \\<notin> range shrK & ServKey \\<notin> AuthKeys evs &\
-\ ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|} ) & \
-\ AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs";
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert,
- AuthKeys_empty, AuthKeys_simp])));
-by (Blast_tac 1);
-by Auto_tac;
-(*Three subcases of Message 4*)
-by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1);
-by (blast_tac (claset() addSDs [SesKey_is_session_key]) 1);
-by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey]) 1);
-qed "Says_Tgs_message_form";
-
-(*If a certain encrypted message appears then it originated with Kas*)
-Goal "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|} \
-\ \\<in> parts (spies evs); \
-\ A \\<notin> bad; evs \\<in> kerberos |] \
-\ ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}) \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake*)
-by (Blast_tac 1);
-(*K4*)
-by (blast_tac (claset() addSDs [A_trusts_AuthTicket RS Says_Kas_message_form])
- 1);
-qed "A_trusts_AuthKey";
-
-
-(*If a certain encrypted message appears then it originated with Tgs*)
-Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, 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, Tt, ServTicket|})\
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake*)
-by (Blast_tac 1);
-(*K2*)
-by (Blast_tac 1);
-(*K4*)
-by Auto_tac;
-qed "A_trusts_K4";
-
-Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} \
-\ \\<in> parts (spies evs); \
-\ A \\<notin> bad; \
-\ evs \\<in> kerberos |] \
-\ ==> AuthKey \\<notin> range shrK & \
-\ AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "AuthTicket_form";
-
-(* This form holds also over an AuthTicket, but is not needed below. *)
-Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|} \
-\ \\<in> parts (spies evs); \
-\ Key AuthKey \\<notin> analz (spies evs); \
-\ evs \\<in> kerberos |] \
-\ ==> ServKey \\<notin> range shrK & \
-\ (\\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "ServTicket_form";
-
-Goal "[| Says Kas' A (Crypt (shrK A) \
-\ {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} ) \\<in> set evs; \
-\ evs \\<in> kerberos |] \
-\ ==> AuthKey \\<notin> range shrK & \
-\ AuthTicket = \
-\ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}\
-\ | AuthTicket \\<in> analz (spies evs)";
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
- AuthTicket_form]) 1);
-qed "Says_kas_message_form";
-(* Essentially the same as AuthTicket_form *)
-
-Goal "[| Says Tgs' A (Crypt AuthKey \
-\ {|Key ServKey, Agent B, Tt, ServTicket|} ) \\<in> set evs; \
-\ evs \\<in> kerberos |] \
-\ ==> ServKey \\<notin> range shrK & \
-\ (\\<exists>A. ServTicket = \
-\ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) \
-\ | ServTicket \\<in> analz (spies evs)";
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
- ServTicket_form]) 1);
-qed "Says_tgs_message_form";
-(* This form MUST be used in analz_sees_tac below *)
-
-
-(*****************UNICITY THEOREMS****************)
-
-(* 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. *)
-
-Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key SesKey, T|} \
-\ \\<in> parts (spies evs); \
-\ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|} \
-\ \\<in> parts (spies evs); Key SesKey \\<notin> analz (spies evs); \
-\ evs \\<in> kerberos |] \
-\ ==> A=A' & B=B' & T=T'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake, K2, K4*)
-by (ALLGOALS Blast_tac);
-qed "unique_CryptKey";
-
-(*An AuthKey is encrypted by one and only one Shared key.
- A ServKey is encrypted by one and only one AuthKey.
-*)
-Goal "[| Crypt K {|Key SesKey, Agent B, T, Ticket|} \
-\ \\<in> parts (spies evs); \
-\ Crypt K' {|Key SesKey, Agent B', T', Ticket'|} \
-\ \\<in> parts (spies evs); Key SesKey \\<notin> analz (spies evs); \
-\ evs \\<in> kerberos |] \
-\ ==> K=K' & B=B' & T=T' & Ticket=Ticket'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake, K2, K4*)
-by (ALLGOALS Blast_tac);
-qed "Key_unique_SesKey";
-
-
-(*
- 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.
- Similarly, at reception of any message mentioning an AuthKey
- (a legitimate user could make several requests to Tgs - by K3), Tgs
- associates it with a new ServKey.
-
- Therefore, a goal like
-
- "evs \\<in> kerberos \
- \ ==> Key Kc \\<notin> analz (spies evs) --> \
- \ (\\<exists>K' B' T' Ticket'. \\<forall>K B T Ticket. \
- \ Crypt Kc {|Key K, Agent B, T, Ticket|} \
- \ \\<in> parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
-
- would fail on the K2 and K4 cases.
-*)
-
-Goal "[| Says Kas A \
-\ (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \\<in> set evs; \
-\ Says Kas A' \
-\ (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) \\<in> set evs; \
-\ evs \\<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*K2*)
-by (Blast_tac 1);
-qed "unique_AuthKeys";
-
-(* ServKey uniquely identifies the message from Tgs *)
-Goal "[| Says Tgs A \
-\ (Crypt K {|Key ServKey, Agent B, Tt, X|}) \\<in> set evs; \
-\ Says Tgs A' \
-\ (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) \\<in> set evs; \
-\ evs \\<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*K4*)
-by (Blast_tac 1);
-qed "unique_ServKeys";
-
-
-(*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
-
-Goalw [KeyCryptKey_def] "~ KeyCryptKey AuthKey ServKey []";
-by (Simp_tac 1);
-qed "not_KeyCryptKey_Nil";
-AddIffs [not_KeyCryptKey_Nil];
-
-Goalw [KeyCryptKey_def]
- "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \\<in> set evs; \
-\ evs \\<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs";
-by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
-qed "KeyCryptKeyI";
-
-Goalw [KeyCryptKey_def]
- "KeyCryptKey AuthKey ServKey (Says S A X # evs) = \
-\ (Tgs = S & \
-\ (\\<exists>B tt. X = Crypt AuthKey \
-\ {|Key ServKey, Agent B, tt, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |}) \
-\ | KeyCryptKey AuthKey ServKey evs)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "KeyCryptKey_Says";
-Addsimps [KeyCryptKey_Says];
-
-(*A fresh AuthKey cannot be associated with any other
- (with respect to a given trace). *)
-Goalw [KeyCryptKey_def]
- "[| Key AuthKey \\<notin> used evs; evs \\<in> kerberos |] \
-\ ==> ~ KeyCryptKey AuthKey ServKey evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Asm_full_simp_tac 1);
-by (Blast_tac 1);
-qed "Auth_fresh_not_KeyCryptKey";
-
-(*A fresh ServKey cannot be associated with any other
- (with respect to a given trace). *)
-Goalw [KeyCryptKey_def]
- "Key ServKey \\<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs";
-by (Blast_tac 1);
-qed "Serv_fresh_not_KeyCryptKey";
-
-Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
-\ \\<in> parts (spies evs); evs \\<in> kerberos |] \
-\ ==> ~ KeyCryptKey K AuthKey evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*K4*)
-by (Blast_tac 3);
-(*K2: by freshness*)
-by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2);
-by (ALLGOALS Blast_tac);
-qed "AuthKey_not_KeyCryptKey";
-
-(*A secure serverkey cannot have been used to encrypt others*)
-Goal
- "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\<in> parts (spies evs); \
-\ Key SK \\<notin> analz (spies evs); \
-\ B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> ~ KeyCryptKey SK K evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-(*K4 splits into distinct subcases*)
-by Auto_tac;
-(*ServKey can't have been enclosed in two certificates*)
-by (blast_tac (claset() addDs [unique_CryptKey]) 2);
-(*ServKey is fresh and so could not have been used, by new_keys_not_used*)
-by (force_tac (claset() addSDs [Crypt_imp_invKey_keysFor],
- simpset() addsimps [KeyCryptKey_def]) 1);
-qed "ServKey_not_KeyCryptKey";
-
-(*Long term keys are not issued as ServKeys*)
-Goalw [KeyCryptKey_def]
- "evs \\<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs";
-by (parts_induct_tac 1);
-qed "shrK_not_KeyCryptKey";
-
-(*The Tgs message associates ServKey with AuthKey and therefore not with any
- other key AuthKey.*)
-Goalw [KeyCryptKey_def]
- "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
-\ \\<in> set evs; \
-\ AuthKey' \\<noteq> AuthKey; evs \\<in> kerberos |] \
-\ ==> ~ KeyCryptKey AuthKey' ServKey evs";
-by (blast_tac (claset() addDs [unique_ServKeys]) 1);
-qed "Says_Tgs_KeyCryptKey";
-
-Goal "[| KeyCryptKey AuthKey ServKey evs; evs \\<in> kerberos |] \
-\ ==> ~ KeyCryptKey ServKey K evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by Safe_tac;
-(*K4 splits into subcases*)
-by (ALLGOALS Asm_full_simp_tac);
-by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 4);
-(*ServKey is fresh and so could not have been used, by new_keys_not_used*)
-by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
- Crypt_imp_invKey_keysFor],
- simpset() addsimps [KeyCryptKey_def]) 2);
-(*Others by freshness*)
-by (ALLGOALS Blast_tac);
-qed "KeyCryptKey_not_KeyCryptKey";
-
-(*The only session keys that can be found with the help of session keys are
- those sent by Tgs in step K4. *)
-
-(*We take some pains to express the property
- as a logical equivalence so that the simplifier can apply it.*)
-Goal "P --> (Key K \\<in> analz (Key`KK Un H)) --> (K:KK | Key K \\<in> analz H) \
-\ ==> \
-\ P --> (Key K \\<in> analz (Key`KK Un H)) = (K:KK | Key K \\<in> analz H)";
-by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
-qed "Key_analz_image_Key_lemma";
-
-Goal "[| KeyCryptKey K K' evs; evs \\<in> kerberos |] \
-\ ==> Key K' \\<in> analz (insert (Key K) (spies evs))";
-by (full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
-by (Clarify_tac 1);
-by (dresolve_tac [Says_imp_spies RS analz.Inj RS analz_insertI] 1);
-by Auto_tac;
-qed "KeyCryptKey_analz_insert";
-
-Goal "[| K \\<in> AuthKeys evs Un range shrK; evs \\<in> kerberos |] \
-\ ==> \\<forall>SK. ~ KeyCryptKey SK K evs";
-by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
-by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
-qed "AuthKeys_are_not_KeyCryptKey";
-
-Goal "[| K \\<notin> AuthKeys evs; \
-\ K \\<notin> range shrK; evs \\<in> kerberos |] \
-\ ==> \\<forall>SK. ~ KeyCryptKey K SK evs";
-by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
-by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
-qed "not_AuthKeys_not_KeyCryptKey";
-
-
-(*****************SECRECY THEOREMS****************)
-
-(*For proofs involving analz.*)
-val analz_sees_tac =
- EVERY
- [REPEAT (FIRSTGOAL analz_mono_contra_tac),
- ftac Oops_range_spies2 10,
- ftac Oops_range_spies1 9,
- ftac Says_tgs_message_form 7,
- ftac Says_kas_message_form 5,
- REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
- ORELSE' hyp_subst_tac)];
-
-(*For the Oops2 case of the next theorem*)
-Goal "[| evs \\<in> kerberos; \
-\ Says Tgs A (Crypt AuthKey \
-\ {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
-\ \\<in> set evs |] \
-\ ==> ~ KeyCryptKey ServKey SK evs";
-by (blast_tac (claset() addDs [KeyCryptKeyI, KeyCryptKey_not_KeyCryptKey]) 1);
-qed "Oops2_not_KeyCryptKey";
-
-
-(* 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] *)
-Goal "evs \\<in> kerberos ==> \
-\ (\\<forall>SK KK. KK <= -(range shrK) --> \
-\ (\\<forall>K \\<in> KK. ~ KeyCryptKey K SK evs) --> \
-\ (Key SK \\<in> analz (Key`KK Un (spies evs))) = \
-\ (SK \\<in> KK | Key SK \\<in> analz (spies evs)))";
-by (etac kerberos.induct 1);
-by analz_sees_tac;
-by (REPEAT_FIRST (rtac allI));
-by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI)));
-(*Case-splits for Oops1 & 5: the negated case simplifies using the ind hyp*)
-by (case_tac "KeyCryptKey AuthKey SK evsO1" 11);
-by (case_tac "KeyCryptKey ServKey SK evs5" 8);
-by (ALLGOALS
- (asm_simp_tac
- (analz_image_freshK_ss addsimps
- [KeyCryptKey_Says, shrK_not_KeyCryptKey, Oops2_not_KeyCryptKey,
- Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey,
- Says_Tgs_KeyCryptKey, Spy_analz_shrK])));
-(*Fake*)
-by (spy_analz_tac 1);
-(* Base + K2 done by the simplifier! *)
-(*K3*)
-by (Blast_tac 1);
-(*K4*)
-by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 1);
-(*K5*)
-by (case_tac "Key ServKey \\<in> analz (spies evs5)" 1);
-(*If ServKey is compromised then the result follows directly...*)
-by (asm_simp_tac
- (simpset() addsimps [analz_insert_eq,
- impOfSubs (Un_upper2 RS analz_mono)]) 1);
-(*...therefore ServKey is uncompromised.*)
-(*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*)
-by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)]
- delrules [allE, ballE]) 1);
-(** Level 13: Oops1 **)
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
-qed_spec_mp "Key_analz_image_Key";
-
-
-(* First simplification law for analz: no session keys encrypt *)
-(* authentication keys or shared keys. *)
-Goal "[| evs \\<in> kerberos; K \\<in> (AuthKeys evs) Un range shrK; \
-\ SesKey \\<notin> range shrK |] \
-\ ==> (Key K \\<in> analz (insert (Key SesKey) (spies evs))) = \
-\ (K = SesKey | Key K \\<in> analz (spies evs))";
-by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1);
-by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
-qed "analz_insert_freshK1";
-
-
-(* Second simplification law for analz: no service keys encrypt *)
-(* any other keys. *)
-Goal "[| evs \\<in> kerberos; ServKey \\<notin> (AuthKeys evs); ServKey \\<notin> range shrK|]\
-\ ==> (Key K \\<in> analz (insert (Key ServKey) (spies evs))) = \
-\ (K = ServKey | Key K \\<in> analz (spies evs))";
-by (ftac not_AuthKeys_not_KeyCryptKey 1
- THEN assume_tac 1
- THEN assume_tac 1);
-by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
-qed "analz_insert_freshK2";
-
-
-(* Third simplification law for analz: only one authentication key *)
-(* encrypts a certain service key. *)
-Goal
- "[| Says Tgs A \
-\ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
-\ \\<in> set evs; \
-\ AuthKey \\<noteq> AuthKey'; AuthKey' \\<notin> range shrK; evs \\<in> kerberos |] \
-\ ==> (Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs))) = \
-\ (ServKey = AuthKey' | Key ServKey \\<in> analz (spies evs))";
-by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);
-by (Blast_tac 1);
-by (assume_tac 1);
-by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
-qed "analz_insert_freshK3";
-
-
-(*a weakness of the protocol*)
-Goal "[| Says Tgs A \
-\ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
-\ \\<in> set evs; \
-\ Key AuthKey \\<in> analz (spies evs); evs \\<in> kerberos |] \
-\ ==> Key ServKey \\<in> analz (spies evs)";
-by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
- analz.Decrypt RS analz.Fst],
- simpset()) 1);
-qed "AuthKey_compromises_ServKey";
-
-
-(********************** Guarantees for Kas *****************************)
-Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}\
-\ \\<in> parts (spies evs); \
-\ Key ServKey \\<notin> analz (spies evs); \
-\ B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> ServKey \\<notin> AuthKeys evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "ServKey_notin_AuthKeysD";
-
-
-(** If Spy sees the Authentication Key sent in msg K2, then
- the Key has expired **)
-Goal "[| A \\<notin> bad; evs \\<in> kerberos |] \
-\ ==> 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 --> \
-\ Key AuthKey \\<in> analz (spies evs) --> \
-\ ExpirAuth Tk evs";
-by (etac kerberos.induct 1);
-by analz_sees_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [Says_Kas_message_form, less_SucI,
- analz_insert_eq, not_parts_not_analz,
- analz_insert_freshK1] @ pushes)));
-(*Fake*)
-by (spy_analz_tac 1);
-(*K2*)
-by (Blast_tac 1);
-(*K4*)
-by (Blast_tac 1);
-(*Level 8: K5*)
-by (blast_tac (claset() addDs [ServKey_notin_AuthKeysD, Says_Kas_message_form]
- addIs [less_SucI]) 1);
-(*Oops1*)
-by (blast_tac (claset() addSDs [unique_AuthKeys] addIs [less_SucI]) 1);
-(*Oops2*)
-by (blast_tac (claset() addDs [Says_Tgs_message_form,
- Says_Kas_message_form]) 1);
-val lemma = result() RS mp RS mp RSN(1,rev_notE);
-
-
-Goal "[| Says Kas A \
-\ (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}) \
-\ \\<in> set evs; \
-\ ~ ExpirAuth Tk evs; \
-\ A \\<notin> bad; evs \\<in> kerberos |] \
-\ ==> Key AuthKey \\<notin> analz (spies evs)";
-by (blast_tac (claset() addDs [Says_Kas_message_form, lemma]) 1);
-qed "Confidentiality_Kas";
-
-
-(********************** Guarantees for Tgs *****************************)
-
-(** If Spy sees the Service Key sent in msg K4, then
- the Key has expired **)
-Goal "[| 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; \
-\ Key AuthKey \\<notin> analz (spies evs); \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> Key ServKey \\<in> analz (spies evs) --> \
-\ ExpirServ Tt evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-(*The Oops1 case is unusual: must simplify Authkey \\<notin> analz (spies (ev#evs))
- rather than weakening it to Authkey \\<notin> analz (spies evs), for we then
- conclude AuthKey \\<noteq> AuthKeya.*)
-by (Clarify_tac 9);
-by analz_sees_tac;
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [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)));
-(*Fake*)
-by (spy_analz_tac 1);
-(*K2*)
-by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 1);
-(*K4*)
-by (blast_tac (claset() addDs [A_trusts_AuthTicket, Confidentiality_Kas]) 1);
-by (ALLGOALS Clarify_tac);
-(*Oops2*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj,
- Key_unique_SesKey] addIs [less_SucI]) 3);
-(** Level 10 **)
-(*Oops1*)
-by (blast_tac (claset() addDs [Says_Kas_message_form, Says_Tgs_message_form]
- addIs [less_SucI]) 2);
-(*K5. Not clear how this step could be integrated with the main
- simplification step.*)
-by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
-by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
-by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
- addIs [less_SucI]) 1);
-qed_spec_mp "Confidentiality_lemma";
-
-
-(* In the real world Tgs can't check wheter AuthKey is secure! *)
-Goal "[| Says Tgs A \
-\ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
-\ \\<in> set evs; \
-\ Key AuthKey \\<notin> analz (spies evs); \
-\ ~ ExpirServ Tt evs; \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> Key ServKey \\<notin> analz (spies evs)";
-by (blast_tac
- (claset() addDs [Says_Tgs_message_form, Confidentiality_lemma]) 1);
-qed "Confidentiality_Tgs1";
-
-(* In the real world Tgs CAN check what Kas sends! *)
-Goal "[| Says Kas A \
-\ (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}) \
-\ \\<in> set evs; \
-\ Says Tgs A \
-\ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
-\ \\<in> set evs; \
-\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> Key ServKey \\<notin> analz (spies evs)";
-by (blast_tac (claset() addSDs [Confidentiality_Kas,
- Confidentiality_Tgs1]) 1);
-qed "Confidentiality_Tgs2";
-
-(*Most general form*)
-val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2;
-
-
-(********************** Guarantees for Alice *****************************)
-
-val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas;
-
-Goal
- "[| Says Kas A \
-\ (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \\<in> set evs;\
-\ Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|} \
-\ \\<in> parts (spies evs); \
-\ Key AuthKey \\<notin> analz (spies evs); \
-\ evs \\<in> kerberos |] \
-\==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
-\ \\<in> set evs";
-by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-(*K2 and K4 remain*)
-by (blast_tac (claset() addSDs [unique_CryptKey]) 2);
-by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form,
- AuthKeys_used]) 1);
-qed "A_trusts_K4_bis";
-
-
-Goal "[| 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; ~ ExpirServ Tt evs; \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> Key ServKey \\<notin> analz (spies evs)";
-by (dtac A_trusts_AuthKey 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (blast_tac (claset() addDs [Confidentiality_Kas,
- Says_Kas_message_form,
- A_trusts_K4_bis, Confidentiality_Tgs2]) 1);
-qed "Confidentiality_Serv_A";
-
-
-(********************** Guarantees for Bob *****************************)
-(* Theorems for the refined model have suffix "refined" *)
-
-Goal
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
-\ \\<in> set evs; evs \\<in> kerberos|] \
-\ ==> \\<exists>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 (etac rev_mp 1);
-by (parts_induct_tac 1);
-by Auto_tac;
-by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
- A_trusts_AuthTicket]) 1);
-qed "K4_imp_K2";
-
-Goal
-"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
-\ \\<in> set evs; evs \\<in> kerberos|] \
-\ ==> \\<exists>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 (etac rev_mp 1);
-by (parts_induct_tac 1);
-by Auto_tac;
-by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
- A_trusts_AuthTicket]) 1);
-qed "K4_imp_K2_refined";
-
-Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|} \
-\ \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad; \
-\ evs \\<in> kerberos |] \
-\==> \\<exists>AuthKey. \
-\ Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}) \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "B_trusts_ServKey";
-
-Goal "[| 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_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1);
-qed "B_trusts_ServTicket_Kas";
-
-Goal "[| 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_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1);
-qed "B_trusts_ServTicket_Kas_refined";
-
-Goal "[| 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_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2]) 1);
-qed "B_trusts_ServTicket";
-
-Goal "[| 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_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2_refined]) 1);
-qed "B_trusts_ServTicket_refined";
-
-
-Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |] \
-\ ==> ~ ExpirAuth Tk evs";
-by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1);
-qed "NotExpirServ_NotExpirAuth_refined";
-
-
-Goal "[| 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)";
-by (ftac A_trusts_AuthKey 1);
-by (ftac Confidentiality_Kas 3);
-by (ftac B_trusts_ServTicket 6);
-by (blast_tac (claset() addSDs [Confidentiality_Tgs2]
- addDs [Says_Kas_message_form, A_trusts_K4,
- unique_ServKeys, unique_AuthKeys]) 9);
-by (ALLGOALS assume_tac);
-(*
-The proof above is fast. It can be done in one command in 50 secs:
-by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,
- Says_Kas_message_form, B_trusts_ServTicket,
- unique_ServKeys, unique_AuthKeys,
- Confidentiality_Kas,
- Confidentiality_Tgs2]) 1);
-*)
-qed "Confidentiality_B";
-
-
-(*Most general form -- only for refined model! *)
-Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \
-\ \\<in> parts (spies evs); \
-\ ~ ExpirServ Tt evs; \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> Key ServKey \\<notin> analz (spies evs)";
-by (blast_tac (claset() addDs [B_trusts_ServTicket_refined,
- NotExpirServ_NotExpirAuth_refined,
- Confidentiality_Tgs2]) 1);
-qed "Confidentiality_B_refined";
-
-
-(********************** Authenticity theorems *****************************)
-
-(***1. Session Keys authenticity: they originated with servers.***)
-
-(*Authenticity of AuthKey for A: "A_trusts_AuthKey"*)
-
-(*Authenticity of ServKey for A: "A_trusts_ServKey"*)
-Goal "[| 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_tac (claset() addDs [A_trusts_AuthKey, Confidentiality_Auth_A,
- A_trusts_K4_bis]) 1);
-qed "A_trusts_ServKey";
-(*Note: requires a temporal check*)
-
-
-(*Authenticity of ServKey for B: "B_trusts_ServKey"*)
-
-(***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.***)
-
-(*B checks authenticity of A: theorems "A_Authenticity",
- "A_authenticity_refined" *)
-Goal "[| 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";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by (ftac Says_ticket_in_parts_spies 5);
-by (ftac Says_ticket_in_parts_spies 7);
-by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (Blast_tac 1);
-(*K3*)
-by (blast_tac (claset() addDs [A_trusts_AuthKey,
- Says_Kas_message_form,
- Says_Tgs_message_form]) 1);
-(*K4*)
-by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
-(*K5*)
-by (blast_tac (claset() addDs [Key_unique_SesKey]) 1);
-qed "Says_Auth";
-
-(*The second assumption tells B what kind of key ServKey is.*)
-Goal "[| 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_tac (claset() addIs [Says_Auth]
- addDs [Confidentiality_B, Key_unique_SesKey,
- B_trusts_ServKey]) 1);
-qed "A_Authenticity";
-
-(*Stronger form in the refined model*)
-Goal "[| 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_tac (claset() addDs [Confidentiality_B_refined, B_trusts_ServKey,
- Key_unique_SesKey]
- addIs [Says_Auth]) 1);
-qed "A_Authenticity_refined";
-
-
-(*A checks authenticity of B: theorem "B_authenticity"*)
-
-Goal "[| 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";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by (ftac Says_ticket_in_parts_spies 5);
-by (ftac Says_ticket_in_parts_spies 7);
-by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
-by (Clarify_tac 1);
-by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
-by (Clarify_tac 1); (*PROOF FAILED if omitted*)
-by (blast_tac (claset() addDs [unique_CryptKey]) 1);
-qed "Says_K6";
-
-Goal "[| 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";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "K4_trustworthy";
-
-Goal "[| 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";
-by (ftac A_trusts_AuthKey 1);
-by (ftac Says_Kas_message_form 3);
-by (ftac Confidentiality_Kas 4);
-by (ftac K4_trustworthy 7);
-by (Blast_tac 8);
-by (etac exE 9);
-by (ftac K4_imp_K2 9);
-(*Yes the proof's a mess, but I don't know how to improve it.*)
-by (blast_tac (claset() addDs [Key_unique_SesKey]
- addSIs [Says_K6]
- addDs [Confidentiality_Tgs1]) 10);
-by (ALLGOALS assume_tac);
-qed "B_Authenticity";
-
-
-(***3. Parties' knowledge of session keys. A knows a session key if she
- used it to build a cipher.***)
-
-Goal "[| 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 |] \
-\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
-by (simp_tac (simpset() addsimps [Issues_def]) 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (Simp_tac 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by (ftac Says_ticket_in_parts_spies 5);
-by (ftac Says_ticket_in_parts_spies 7);
-by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (Blast_tac 1);
-(*K6 requires numerous lemmas*)
-by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
-by (blast_tac (claset() addDs [B_trusts_ServTicket,
- impOfSubs parts_spies_takeWhile_mono,
- impOfSubs parts_spies_evs_revD2]
- addIs [Says_K6]) 1);
-qed "B_Knows_B_Knows_ServKey_lemma";
-(*Key ServKey \\<notin> analz (spies evs) could be relaxed by Confidentiality_B
- but this is irrelevant because B knows what he knows! *)
-
-Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set 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; \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
-by (blast_tac (claset() addSDs [Confidentiality_B,
- B_Knows_B_Knows_ServKey_lemma]) 1);
-qed "B_Knows_B_Knows_ServKey";
-
-Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set evs; \
-\ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
-\ \\<in> parts (spies evs);\
-\ ~ ExpirServ Tt evs; \
-\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |] \
-\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
-by (blast_tac (claset() addSDs [Confidentiality_B_refined,
- B_Knows_B_Knows_ServKey_lemma]) 1);
-qed "B_Knows_B_Knows_ServKey_refined";
-
-
-Goal "[| 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 |] \
-\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
-by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A,
- B_Knows_B_Knows_ServKey_lemma]) 1);
-qed "A_Knows_B_Knows_ServKey";
-
-Goal "[| Says A Tgs \
-\ {|AuthTicket, Crypt AuthKey {|Agent A, Number Ta|}, Agent B|}\
-\ \\<in> set evs; \
-\ A \\<notin> bad; evs \\<in> kerberos |] \
-\ ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) \
-\ {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS
- A_trusts_AuthKey]) 1);
-qed "K3_imp_K2";
-
-Goal "[| 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";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
- A_trusts_AuthTicket, unique_AuthKeys]) 1);
-qed "K4_trustworthy'";
-
-Goal "[| 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";
-by (simp_tac (simpset() addsimps [Issues_def]) 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (Simp_tac 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac kerberos.induct 1);
-by (ftac Says_ticket_in_parts_spies 5);
-by (ftac Says_ticket_in_parts_spies 7);
-by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
-by (ALLGOALS Asm_simp_tac);
-by (Clarify_tac 1);
-(*K6*)
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
-(*Level 15: case study necessary because the assumption doesn't state
- the form of ServTicket. The guarantee becomes stronger.*)
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz_Decrypt',
- K3_imp_K2, K4_trustworthy',
- impOfSubs parts_spies_takeWhile_mono,
- impOfSubs parts_spies_evs_revD2]
- addIs [Says_Auth]) 1);
-by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
-qed "A_Knows_A_Knows_ServKey_lemma";
-
-Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
-\ \\<in> set evs; \
-\ 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; ~ ExpirServ Tt 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";
-by (blast_tac (claset() addSDs [Confidentiality_Serv_A,
- A_Knows_A_Knows_ServKey_lemma]) 1);
-qed "A_Knows_A_Knows_ServKey";
-
-Goal "[| 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 |] \
-\ ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
-by (blast_tac (claset() addDs [A_Authenticity, Confidentiality_B,
- A_Knows_A_Knows_ServKey_lemma]) 1);
-qed "B_Knows_A_Knows_ServKey";
-
-
-Goal "[| 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); \
-\ ~ ExpirServ Tt 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";
-by (blast_tac (claset() addDs [A_Authenticity_refined,
- Confidentiality_B_refined,
- A_Knows_A_Knows_ServKey_lemma]) 1);
-qed "B_Knows_A_Knows_ServKey_refined";
--- a/src/HOL/Auth/KerberosIV.thy Thu Sep 04 11:08:24 2003 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Thu Sep 04 11:15:53 2003 +0200
@@ -6,52 +6,53 @@
The Kerberos protocol, version IV.
*)
-KerberosIV = Shared +
+theory KerberosIV = Shared:
syntax
- Kas, Tgs :: agent (*the two servers are translations...*)
+ Kas :: agent
+ Tgs :: agent --{*the two servers are translations...*}
translations
- "Kas" == "Server"
- "Tgs" == "Friend 0"
+ "Kas" == "Server "
+ "Tgs" == "Friend 0"
-rules
- (*Tgs is secure --- we already know that Kas is secure*)
- Tgs_not_bad "Tgs \\<notin> bad"
-
+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!*)
syntax
- CT :: event list=>nat
+ CT :: "event list=>nat"
- ExpirAuth :: [nat, event list] => bool
+ ExpirAuth :: "[nat, event list] => bool"
- ExpirServ :: [nat, event list] => bool
+ ExpirServ :: "[nat, event list] => bool"
- ExpirAutc :: [nat, event list] => bool
+ ExpirAutc :: "[nat, event list] => bool"
- RecentResp :: [nat, nat] => bool
+ RecentResp :: "[nat, nat] => bool"
constdefs
(* AuthKeys are those contained in an AuthTicket *)
- AuthKeys :: event list => key set
- "AuthKeys evs == {AuthKey. \\<exists>A Peer Tk. Says Kas A
- (Crypt (shrK A) {|Key AuthKey, Agent Peer, Tk,
+ AuthKeys :: "event list => key set"
+ "AuthKeys evs == {AuthKey. \<exists>A Peer Tk. Says Kas A
+ (Crypt (shrK A) {|Key AuthKey, Agent Peer, Tk,
(Crypt (shrK Peer) {|Agent A, Agent Peer, Key AuthKey, Tk|})
- |}) \\<in> set evs}"
-
+ |}) \<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)))"
+ 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)))"
consts
-
(*Duration of the authentication key*)
AuthLife :: nat
@@ -62,16 +63,26 @@
AutcLife :: nat
(*Upper bound on the time of reaction of a server*)
- RespLife :: nat
+ RespLife :: nat
+
+specification (AuthLife)
+ AuthLife_LB [iff]: "2 \<le> AuthLife"
+ by blast
-rules
- AuthLife_LB "2 <= AuthLife"
- ServLife_LB "2 <= ServLife"
- AutcLife_LB "Suc 0 <= AutcLife"
- RespLife_LB "Suc 0 <= RespLife"
+specification (ServLife)
+ ServLife_LB [iff]: "2 \<le> ServLife"
+ by blast
+
+specification (AutcLife)
+ AutcLife_LB [iff]: "Suc 0 \<le> AutcLife"
+ by blast
+
+specification (RespLife)
+ RespLife_LB [iff]: "Suc 0 \<le> RespLife"
+ by blast
translations
- "CT" == "length"
+ "CT" == "length "
"ExpirAuth T evs" == "AuthLife + T < CT evs"
@@ -85,151 +96,1461 @@
(* Predicate formalising the association between AuthKeys and ServKeys *)
-constdefs
- KeyCryptKey :: [key, key, event list] => bool
+constdefs
+ KeyCryptKey :: "[key, key, event list] => bool"
"KeyCryptKey AuthKey ServKey evs ==
- \\<exists>A B tt.
+ \<exists>A B tt.
Says Tgs A (Crypt AuthKey
{|Key ServKey, Agent B, tt,
Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
- \\<in> set evs"
+ \<in> set evs"
consts
-kerberos :: event list set
+kerberos :: "event list set"
inductive "kerberos"
- intrs
-
- Nil "[] \\<in> kerberos"
+ intros
- Fake "[| evsf \\<in> kerberos; X \\<in> synth (analz (spies evsf)) |]
- ==> Says Spy B X # evsf \\<in> kerberos"
+ Nil: "[] \<in> kerberos"
+
+ Fake: "[| evsf \<in> kerberos; X \<in> synth (analz (spies evsf)) |]
+ ==> Says Spy B X # evsf \<in> kerberos"
(* FROM the initiator *)
- K1 "[| evs1 \\<in> kerberos |]
- ==> Says A Kas {|Agent A, Agent Tgs, Number (CT evs1)|} # evs1
- \\<in> kerberos"
+ K1: "[| evs1 \<in> kerberos |]
+ ==> Says A Kas {|Agent A, Agent Tgs, Number (CT evs1)|} # evs1
+ \<in> kerberos"
(* 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.
+ 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;
- Says A' Kas {|Agent A, Agent Tgs, Number Ta|} \\<in> set evs2 |]
+ K2: "[| evs2 \<in> kerberos; Key AuthKey \<notin> used evs2;
+ Says A' Kas {|Agent A, Agent Tgs, Number Ta|} \<in> set evs2 |]
==> Says Kas A
- (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2),
- (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
- Number (CT evs2)|})|}) # evs2 \\<in> kerberos"
-(*
+ (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2),
+ (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
+ Number (CT evs2)|})|}) # evs2 \<in> kerberos"
+(*
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
+ will be used by the initiator in K3; the one inside the
AuthTicket by Tgs in K4.
*)
(*---------------------------------------------------------------------*)
(* FROM the initiator *)
- K3 "[| evs3 \\<in> kerberos;
- Says A Kas {|Agent A, Agent Tgs, Number Ta|} \\<in> set evs3;
- Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
- AuthTicket|}) \\<in> set evs3;
+ K3: "[| evs3 \<in> kerberos;
+ Says A Kas {|Agent A, Agent Tgs, Number Ta|} \<in> set evs3;
+ Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
+ AuthTicket|}) \<in> set evs3;
RecentResp Tk Ta
|]
- ==> Says A Tgs {|AuthTicket,
- (Crypt AuthKey {|Agent A, Number (CT evs3)|}),
- Agent B|} # evs3 \\<in> kerberos"
-(*The two events amongst the premises allow A to accept only those AuthKeys
+ ==> Says A Tgs {|AuthTicket,
+ (Crypt AuthKey {|Agent A, Number (CT evs3)|}),
+ Agent B|} # evs3 \<in> kerberos"
+(*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 strengthens the guarantees assessed by the
protocol. Theorems that exploit it have the suffix `_refined'
-*)
- K4 "[| evs4 \\<in> kerberos; Key ServKey \\<notin> used evs4; B \\<noteq> Tgs;
+*)
+ K4: "[| evs4 \<in> kerberos; Key ServKey \<notin> used evs4; B \<noteq> Tgs;
Says A' Tgs {|
(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
Number Tk|}),
(Crypt AuthKey {|Agent A, Number Ta1|}), Agent B|}
- \\<in> set evs4;
+ \<in> set evs4;
~ ExpirAuth Tk evs4;
- ~ ExpirAutc Ta1 evs4;
+ ~ ExpirAutc Ta1 evs4;
ServLife + (CT evs4) <= AuthLife + Tk
|]
- ==> Says Tgs A
- (Crypt AuthKey {|Key ServKey, Agent B, Number (CT evs4),
+ ==> Says Tgs A
+ (Crypt AuthKey {|Key ServKey, Agent B, Number (CT evs4),
Crypt (shrK B) {|Agent A, Agent B, Key ServKey,
Number (CT evs4)|} |})
- # evs4 \\<in> kerberos"
-(* Tgs creates a new session key per each request for a service, without
+ # evs4 \<in> kerberos"
+(* Tgs creates a new session key per each request for a service, without
checking if there is still a fresh one for that service.
The cipher under Tgs' key is the AuthTicket, the cipher under B's key
is the ServTicket, which is built now.
NOTE that the last temporal check is not present in the MIT specification.
-
+
*)
(*---------------------------------------------------------------------*)
(* FROM the initiator *)
- K5 "[| evs5 \\<in> kerberos;
- Says A Tgs
- {|AuthTicket, (Crypt AuthKey {|Agent A, Number Ta1|} ),
+ K5: "[| evs5 \<in> kerberos;
+ Says A Tgs
+ {|AuthTicket, (Crypt AuthKey {|Agent A, Number Ta1|}),
Agent B|}
- \\<in> set evs5;
- Says Tgs' A
- (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} )
- \\<in> set evs5;
+ \<in> set evs5;
+ Says Tgs' A
+ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs5;
RecentResp Tt Ta1 |]
==> Says A B {|ServTicket,
Crypt ServKey {|Agent A, Number (CT evs5)|} |}
- # evs5 \\<in> kerberos"
+ # evs5 \<in> kerberos"
(* Checks similar to those in K3. *)
(*---------------------------------------------------------------------*)
(* FROM the responder*)
- K6 "[| evs6 \\<in> kerberos;
- Says A' B {|
- (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} ),
- (Crypt ServKey {|Agent A, Number Ta2|} )|}
- \\<in> set evs6;
+ K6: "[| evs6 \<in> kerberos;
+ Says A' B {|
+ (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}),
+ (Crypt ServKey {|Agent A, Number Ta2|})|}
+ \<in> set evs6;
~ ExpirServ Tt evs6;
~ ExpirAutc Ta2 evs6
|]
- ==> Says B A (Crypt ServKey (Number Ta2) )
- # evs6 \\<in> kerberos"
+ ==> Says B A (Crypt ServKey (Number Ta2))
+ # evs6 \<in> kerberos"
(* Checks similar to those in K4. *)
(*---------------------------------------------------------------------*)
(* Leaking an AuthKey... *)
- Oops1 "[| evsO1 \\<in> kerberos; A \\<noteq> Spy;
+ Oops1: "[| evsO1 \<in> kerberos; A \<noteq> Spy;
Says Kas A
- (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
- AuthTicket|}) \\<in> set evsO1;
+ (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,
+ AuthTicket|}) \<in> set evsO1;
ExpirAuth Tk evsO1 |]
- ==> Says A Spy {|Agent A, Agent Tgs, Number Tk, Key AuthKey|}
- # evsO1 \\<in> kerberos"
+ ==> Says A Spy {|Agent A, Agent Tgs, Number Tk, Key AuthKey|}
+ # evsO1 \<in> kerberos"
(*---------------------------------------------------------------------*)
(*Leaking a ServKey... *)
- Oops2 "[| evsO2 \\<in> kerberos; A \\<noteq> Spy;
- Says Tgs A
+ Oops2: "[| evsO2 \<in> kerberos; A \<noteq> Spy;
+ Says Tgs A
(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
- \\<in> set evsO2;
+ \<in> set evsO2;
ExpirServ Tt evsO2 |]
- ==> Says A Spy {|Agent A, Agent B, Number Tt, Key ServKey|}
- # evsO2 \\<in> kerberos"
+ ==> Says A Spy {|Agent A, Agent B, Number Tt, Key ServKey|}
+ # evsO2 \<in> kerberos"
(*---------------------------------------------------------------------*)
+declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
+declare analz_subset_parts [THEN subsetD, dest]
+declare Fake_parts_insert [THEN subsetD, dest]
+
+
+subsection{*Lemmas about Lists*}
+
+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
+
+lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
+apply (induct_tac "evs")
+apply (induct_tac [2] "a", auto)
+done
+
+lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
+ (if A:bad then insert X (spies evs) else spies evs)"
+apply (induct_tac "evs")
+apply (induct_tac [2] "a", auto)
+done
+
+lemma spies_evs_rev: "spies evs = spies (rev evs)"
+apply (induct_tac "evs")
+apply (induct_tac [2] "a")
+apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
+done
+
+lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
+
+lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs"
+apply (induct_tac "evs")
+apply (induct_tac [2] "a", auto)
+txt{* Resembles @{text"used_subset_append"} in theory Event.*}
+done
+
+lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
+
+
+subsection{*Lemmas about @{term AuthKeys}*}
+
+lemma AuthKeys_empty: "AuthKeys [] = {}"
+apply (unfold AuthKeys_def)
+apply (simp (no_asm))
+done
+
+lemma AuthKeys_not_insert:
+ "(\<forall>A Tk akey Peer.
+ ev \<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,
+ (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))
+ ==> AuthKeys (ev # evs) = AuthKeys evs"
+apply (unfold AuthKeys_def, auto)
+done
+
+lemma AuthKeys_insert:
+ "AuthKeys
+ (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk,
+ (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs)
+ = insert K (AuthKeys evs)"
+apply (unfold AuthKeys_def, auto)
+done
+
+lemma AuthKeys_simp:
+ "K \<in> AuthKeys
+ (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk,
+ (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs)
+ ==> K = K' | K \<in> AuthKeys evs"
+apply (unfold AuthKeys_def, auto)
+done
+
+lemma AuthKeysI:
+ "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk,
+ (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \<in> set evs
+ ==> K \<in> AuthKeys evs"
+apply (unfold AuthKeys_def, auto)
+done
+
+lemma AuthKeys_used: "K \<in> AuthKeys evs ==> Key K \<in> used evs"
+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|})
+ \<in> set evs ==> AuthTicket \<in> parts (spies evs)"
+by blast
+
+lemma Oops_range_spies1:
+ "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|})
+ \<in> set evs ;
+ evs \<in> kerberos |] ==> AuthKey \<notin> range shrK"
+apply (erule rev_mp)
+apply (erule kerberos.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|})
+ \<in> set evs ==> ServTicket \<in> parts (spies evs)"
+apply blast
+done
+
+lemma Oops_range_spies2:
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ \<in> set evs ;
+ evs \<in> kerberos |] ==> ServKey \<notin> range shrK"
+apply (erule rev_mp)
+apply (erule kerberos.induct, auto)
+done
+
+lemma Says_ticket_in_parts_spies:
+ "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \<in> set evs
+ ==> Ticket \<in> parts (spies evs)"
+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)"
+apply (erule kerberos.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)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[| Key (shrK A) \<in> parts (spies evs); evs \<in> kerberos |] ==> 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 [rule_format, simp]:
+ "evs \<in> kerberos ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (spies 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)
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*Others*}
+apply (blast+)
+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; Key K \<notin> used evs|] ==> K \<notin> keysFor (analz (spies evs))"
+by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
+
+
+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*}
+lemma Says_Kas_message_form:
+ "[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|})
+ \<in> set evs;
+ evs \<in> kerberos |]
+ ==> AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs &
+ AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}) &
+ K = shrK A & Peer = Tgs"
+apply (erule rev_mp)
+apply (erule kerberos.induct)
+apply (simp_all (no_asm) add: AuthKeys_def AuthKeys_insert)
+apply (blast+)
+done
+
+(*This lemma is essential for proving Says_Tgs_message_form:
+
+ the session key AuthKey
+ supplied by Kas in the authentication ticket
+ cannot be a long-term key!
+
+ Generalised to any session keys (both AuthKey and ServKey).
+*)
+lemma SesKey_is_session_key:
+ "[| Crypt (shrK Tgs_B) {|Agent A, Agent Tgs_B, Key SesKey, Number T|}
+ \<in> parts (spies evs); Tgs_B \<notin> bad;
+ evs \<in> kerberos |]
+ ==> SesKey \<notin> range shrK"
+apply (erule rev_mp)
+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)
+done
+
+lemma A_trusts_AuthTicket:
+ "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
+ \<in> parts (spies evs);
+ evs \<in> kerberos |]
+ ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk,
+ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule kerberos.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:
+ "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}
+ \<in> parts (spies evs);
+ evs \<in> kerberos |]
+ ==> AuthKey \<in> AuthKeys evs"
+apply (frule A_trusts_AuthTicket, assumption)
+apply (simp (no_asm) add: AuthKeys_def)
+apply blast
+done
+
+text{*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*}
+lemma Says_Tgs_message_form:
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ \<in> set evs;
+ evs \<in> kerberos |]
+ ==> B \<noteq> Tgs & ServKey \<notin> range shrK & ServKey \<notin> AuthKeys evs &
+ ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) &
+ AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs"
+apply (erule rev_mp)
+apply (erule kerberos.induct)
+apply (simp_all add: AuthKeys_insert AuthKeys_not_insert AuthKeys_empty AuthKeys_simp, blast, auto)
+txt{*Three subcases of Message 4*}
+apply (blast dest!: AuthKeys_used Says_Kas_message_form)
+apply (blast dest!: SesKey_is_session_key)
+apply (blast dest: AuthTicket_crypt_AuthKey)
+done
+
+text{*Authenticity of AuthKey for A:
+ If a certain encrypted message appears then it originated with Kas*}
+lemma A_trusts_AuthKey:
+ "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}
+ \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> kerberos |]
+ ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule kerberos.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])
+done
+
+
+text{*If a certain encrypted message appears then it originated with Tgs*}
+lemma A_trusts_K4:
+ "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, 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, Tt, 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)
+txt{*Fake*}
+apply blast
+txt{*K2*}
+apply blast
+txt{*K4*}
+apply auto
+done
+
+lemma AuthTicket_form:
+ "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}
+ \<in> parts (spies evs);
+ A \<notin> bad;
+ evs \<in> kerberos |]
+ ==> AuthKey \<notin> range shrK &
+ AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}"
+apply (erule rev_mp)
+apply (erule kerberos.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:
+ "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
+ \<in> parts (spies evs);
+ Key AuthKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
+ ==> ServKey \<notin> range shrK &
+ (\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})"
+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)
+done
+
+text{* Essentially the same as @{text AuthTicket_form} *}
+lemma Says_kas_message_form:
+ "[| Says Kas' A (Crypt (shrK A)
+ {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \<in> set evs;
+ evs \<in> kerberos |]
+ ==> AuthKey \<notin> range shrK &
+ AuthTicket =
+ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
+ | AuthTicket \<in> analz (spies evs)"
+by (blast dest: Says_imp_spies [THEN analz.Inj] AuthTicket_form)
+
+lemma Says_tgs_message_form:
+ "[| Says Tgs' A (Crypt AuthKey
+ {|Key ServKey, Agent B, Tt, ServTicket|}) \<in> set evs;
+ evs \<in> kerberos |]
+ ==> ServKey \<notin> range shrK &
+ (\<exists>A. ServTicket =
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})
+ | ServTicket \<in> analz (spies evs)"
+by (blast dest: Says_imp_spies [THEN analz.Inj] ServTicket_form)
+
+
+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. *}
+
+lemma unique_CryptKey:
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key SesKey, T|}
+ \<in> parts (spies evs);
+ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}
+ \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
+ ==> 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 (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.
+ A ServKey is encrypted by one and only one AuthKey.
+*}
+lemma Key_unique_SesKey:
+ "[| Crypt K {|Key SesKey, Agent B, T, Ticket|}
+ \<in> parts (spies evs);
+ Crypt K' {|Key SesKey, Agent B', T', Ticket'|}
+ \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
+ ==> 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 (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
+
+
+(*
+ 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.
+ Similarly, at reception of any message mentioning an AuthKey
+ (a legitimate user could make several requests to Tgs - by K3), Tgs
+ associates it with a new ServKey.
+
+ Therefore, a goal like
+
+ "evs \<in> kerberos
+ ==> Key Kc \<notin> analz (spies evs) -->
+ (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket.
+ Crypt Kc {|Key K, Agent B, T, Ticket|}
+ \<in> parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')"
+
+ would fail on the K2 and K4 cases.
+*)
+
+lemma unique_AuthKeys:
+ "[| Says Kas A
+ (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \<in> set evs;
+ Says Kas A'
+ (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) \<in> set evs;
+ evs \<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerberos.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 *}
+lemma unique_ServKeys:
+ "[| Says Tgs A
+ (Crypt K {|Key ServKey, Agent B, Tt, X|}) \<in> set evs;
+ Says Tgs A'
+ (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) \<in> set evs;
+ evs \<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerberos.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
+
+
+subsection{*Lemmas About the Predicate @{term KeyCryptKey}*}
+
+lemma not_KeyCryptKey_Nil [iff]: "~ KeyCryptKey AuthKey ServKey []"
+by (simp add: KeyCryptKey_def)
+
+lemma KeyCryptKeyI:
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \<in> set evs;
+ evs \<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs"
+apply (unfold KeyCryptKey_def)
+apply (blast dest: Says_Tgs_message_form)
+done
+
+lemma KeyCryptKey_Says [simp]:
+ "KeyCryptKey AuthKey ServKey (Says S A X # evs) =
+ (Tgs = S &
+ (\<exists>B tt. X = Crypt AuthKey
+ {|Key ServKey, Agent B, tt,
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
+ | KeyCryptKey AuthKey ServKey evs)"
+apply (unfold KeyCryptKey_def)
+apply (simp (no_asm))
+apply blast
+done
+
+(*A fresh AuthKey cannot be associated with any other
+ (with respect to a given trace). *)
+lemma Auth_fresh_not_KeyCryptKey:
+ "[| Key AuthKey \<notin> used evs; evs \<in> kerberos |]
+ ==> ~ KeyCryptKey AuthKey ServKey evs"
+apply (unfold KeyCryptKey_def)
+apply (erule rev_mp)
+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)
+done
+
+(*A fresh ServKey cannot be associated with any other
+ (with respect to a given trace). *)
+lemma Serv_fresh_not_KeyCryptKey:
+ "Key ServKey \<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs"
+apply (unfold KeyCryptKey_def, blast)
+done
+
+lemma AuthKey_not_KeyCryptKey:
+ "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}
+ \<in> parts (spies evs); evs \<in> kerberos |]
+ ==> ~ KeyCryptKey K AuthKey evs"
+apply (erule rev_mp)
+apply (erule kerberos.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)
+txt{*K4*}
+apply (blast+)
+done
+
+text{*A secure serverkey cannot have been used to encrypt others*}
+lemma ServKey_not_KeyCryptKey:
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \<in> parts (spies evs);
+ Key SK \<notin> analz (spies evs);
+ B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> ~ KeyCryptKey SK K 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, blast)
+txt{*K4 splits into distinct subcases*}
+apply auto
+txt{*ServKey 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
+ @{text new_keys_not_used}*}
+apply (force dest!: Crypt_imp_invKey_keysFor simp add: KeyCryptKey_def)
+done
+
+text{*Long term keys are not issued as ServKeys*}
+lemma shrK_not_KeyCryptKey:
+ "evs \<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs"
+apply (unfold KeyCryptKey_def)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+done
+
+text{*The Tgs message associates ServKey with AuthKey and therefore not with any
+ other key AuthKey.*}
+lemma Says_Tgs_KeyCryptKey:
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |})
+ \<in> set evs;
+ AuthKey' \<noteq> AuthKey; evs \<in> kerberos |]
+ ==> ~ KeyCryptKey AuthKey' ServKey evs"
+apply (unfold KeyCryptKey_def)
+apply (blast dest: unique_ServKeys)
+done
+
+lemma KeyCryptKey_not_KeyCryptKey:
+ "[| KeyCryptKey AuthKey ServKey evs; evs \<in> kerberos |]
+ ==> ~ KeyCryptKey ServKey K evs"
+apply (erule rev_mp)
+apply (erule kerberos.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)
+txt{*ServKey is fresh and so could not have been used, by
+ @{text new_keys_not_used}*}
+ prefer 2
+ apply (force dest!: Says_imp_spies [THEN parts.Inj] Crypt_imp_invKey_keysFor simp add: KeyCryptKey_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 --> (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:
+ "[| KeyCryptKey K K' evs; evs \<in> kerberos |]
+ ==> Key K' \<in> analz (insert (Key K) (spies evs))"
+apply (simp (no_asm_use) add: KeyCryptKey_def)
+apply clarify
+apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
+done
+
+lemma AuthKeys_are_not_KeyCryptKey:
+ "[| K \<in> AuthKeys evs Un range shrK; evs \<in> kerberos |]
+ ==> \<forall>SK. ~ KeyCryptKey SK K evs"
+apply (simp add: KeyCryptKey_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:
+ "[| evs \<in> kerberos;
+ Says Tgs A (Crypt AuthKey
+ {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs |]
+ ==> ~ KeyCryptKey ServKey SK evs"
+apply (blast dest: KeyCryptKeyI KeyCryptKey_not_KeyCryptKey)
+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 ==>
+ (\<forall>SK KK. KK <= -(range shrK) -->
+ (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs) -->
+ (Key SK \<in> analz (Key`KK Un (spies evs))) =
+ (SK \<in> KK | Key SK \<in> analz (spies evs)))"
+apply (erule kerberos.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 [8] "KeyCryptKey ServKey SK evs5")
+apply (simp_all del: image_insert
+ add: analz_image_freshK_simps KeyCryptKey_Says shrK_not_KeyCryptKey
+ Oops2_not_KeyCryptKey Auth_fresh_not_KeyCryptKey
+ Serv_fresh_not_KeyCryptKey Says_Tgs_KeyCryptKey Spy_analz_shrK)
+ --{*18 seconds on a 1.8GHz machine??*}
+txt{*Fake*}
+apply spy_analz
+txt{*K4*}
+apply (blast dest!: AuthKey_not_KeyCryptKey)
+txt{*K5*}
+apply (case_tac "Key ServKey \<in> analz (spies evs5) ")
+txt{*If ServKey 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{*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*}
+apply (blast elim!: ServKey_not_KeyCryptKey [THEN [2] rev_notE] del: allE ballE)
+txt{*Oops1*}
+apply simp
+apply (blast dest!: KeyCryptKey_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;
+ SesKey \<notin> range shrK |]
+ ==> (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 (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|]
+ ==> (Key K \<in> analz (insert (Key ServKey) (spies evs))) =
+ (K = ServKey | Key K \<in> analz (spies evs))"
+apply (frule not_AuthKeys_not_KeyCryptKey, 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
+certain service key.*}
+lemma analz_insert_freshK3:
+ "[| Says Tgs A
+ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs;
+ AuthKey \<noteq> AuthKey'; AuthKey' \<notin> range shrK; evs \<in> kerberos |]
+ ==> (Key ServKey \<in> analz (insert (Key AuthKey') (spies evs))) =
+ (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
+
+
+text{*a weakness of the protocol*}
+lemma AuthKey_compromises_ServKey:
+ "[| Says Tgs A
+ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs;
+ Key AuthKey \<in> analz (spies evs); evs \<in> kerberos |]
+ ==> Key ServKey \<in> analz (spies evs)"
+apply (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
+done
+
+
+subsection{* Guarantees for Kas *}
+lemma ServKey_notin_AuthKeysD:
+ "[| Crypt AuthKey {|Key ServKey, Agent B, Tt,
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}
+ \<in> parts (spies evs);
+ Key ServKey \<notin> analz (spies evs);
+ B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> ServKey \<notin> AuthKeys evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+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]:
+ "[| A \<notin> bad; evs \<in> kerberos |]
+ ==> 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 -->
+ Key AuthKey \<in> analz (spies evs) -->
+ ExpirAuth Tk evs"
+apply (erule kerberos.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)
+apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
+txt{*Fake*}
+apply spy_analz
+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)
+txt{*Oops1*}
+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
+ (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})
+ \<in> set evs;
+ ~ ExpirAuth Tk evs;
+ A \<notin> bad; evs \<in> kerberos |]
+ ==> Key AuthKey \<notin> analz (spies evs)"
+apply (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
+done
+
+
+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
+ (Crypt AuthKey
+ {|Key ServKey, Agent B, Number Tt,
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})
+ \<in> set evs;
+ Key AuthKey \<notin> analz (spies evs);
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> Key ServKey \<in> analz (spies evs) -->
+ ExpirServ Tt evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerberos.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"}.*}
+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)
+txt{*Fake*}
+apply spy_analz
+txt{*K2*}
+apply (blast intro: parts_insertI less_SucI)
+txt{*K4*}
+apply (blast dest: A_trusts_AuthTicket 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
+ simplification step.*}
+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 (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! *}
+lemma Confidentiality_Tgs1:
+ "[| Says Tgs A
+ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs;
+ Key AuthKey \<notin> analz (spies evs);
+ ~ ExpirServ Tt evs;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> Key ServKey \<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:
+ "[| Says Kas A
+ (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})
+ \<in> set evs;
+ Says Tgs A
+ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs;
+ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> Key ServKey \<notin> analz (spies evs)"
+apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs1)
+done
+
+text{*Most general form*}
+lemmas Confidentiality_Tgs3 = A_trusts_AuthTicket [THEN Confidentiality_Tgs2]
+
+
+subsection{* Guarantees for Alice *}
+
+lemmas Confidentiality_Auth_A = A_trusts_AuthKey [THEN Confidentiality_Kas]
+
+lemma A_trusts_K4_bis:
+ "[| Says Kas A
+ (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \<in> set evs;
+ Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
+ \<in> parts (spies evs);
+ Key AuthKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
+ ==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ \<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 (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)
+done
+
+
+lemma Confidentiality_Serv_A:
+ "[| 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; ~ ExpirServ Tt evs;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> Key ServKey \<notin> analz (spies evs)"
+apply (drule A_trusts_AuthKey, assumption, assumption)
+apply (blast dest: Confidentiality_Kas Says_Kas_message_form A_trusts_K4_bis Confidentiality_Tgs2)
+done
+
+
+subsection{* Guarantees for Bob *}
+text{* Theorems for the refined model have suffix "refined" *}
+
+lemma K4_imp_K2:
+"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs; evs \<in> kerberos|]
+ ==> \<exists>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"
+apply (erule rev_mp)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
+apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN A_trusts_AuthTicket])
+done
+
+lemma K4_imp_K2_refined:
+"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs; evs \<in> kerberos|]
+ ==> \<exists>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)"
+apply (erule rev_mp)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
+apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN A_trusts_AuthTicket])
+done
+
+text{*Authenticity of ServKey for B*}
+lemma B_trusts_ServKey:
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}
+ \<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad;
+ evs \<in> kerberos |]
+ ==> \<exists>AuthKey.
+ Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|})
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule kerberos.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 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 elim: leE)
+
+
+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.
+*)
+
+
+
+text{*Most general form -- only for refined model! *}
+lemma Confidentiality_B_refined:
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+ \<in> parts (spies evs);
+ ~ ExpirServ Tt evs;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> Key ServKey \<notin> analz (spies evs)"
+apply (blast dest: B_trusts_ServTicket_refined NotExpirServ_NotExpirAuth_refined Confidentiality_Tgs2)
+done
+
+
+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"
+apply (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis)
+done
+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)
+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
+)
+done
+
+
+(***3. Parties' knowledge of session keys. A knows a session key if she
+ used it to build a cipher.***)
+
+lemma B_Knows_B_Knows_ServKey_lemma:
+ "[| 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 |]
+ ==> B Issues A with (Crypt ServKey (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 (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{*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)
+done
+(*Key ServKey \<notin> analz (spies evs) could be relaxed by Confidentiality_B
+ but this is irrelevant because B knows what he knows! *)
+
+lemma B_Knows_B_Knows_ServKey:
+ "[| Says B A (Crypt ServKey (Number Ta)) \<in> set 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;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+apply (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma)
+done
+
+lemma B_Knows_B_Knows_ServKey_refined:
+ "[| Says B A (Crypt ServKey (Number Ta)) \<in> set evs;
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}
+ \<in> parts (spies evs);
+ ~ ExpirServ Tt evs;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+apply (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma)
+done
+
+
+lemma A_Knows_B_Knows_ServKey:
+ "[| 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 |]
+ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
+apply (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma)
+done
+
+lemma K3_imp_K2:
+ "[| Says A Tgs
+ {|AuthTicket, Crypt AuthKey {|Agent A, Number Ta|}, Agent B|}
+ \<in> set evs;
+ A \<notin> bad; evs \<in> kerberos |]
+ ==> \<exists>Tk. Says Kas A (Crypt (shrK A)
+ {|Key AuthKey, Agent Tgs, Tk, AuthTicket|})
+ \<in> set evs"
+apply (erule rev_mp)
+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)
+apply 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 (frule_tac [5] Says_ticket_in_parts_spies)
+apply (frule_tac [7] Says_ticket_in_parts_spies)
+apply (simp_all (no_asm_simp))
+apply clarify
+txt{*K6*}
+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.*}
+apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
+ K3_imp_K2 K4_trustworthy'
+ parts_spies_takeWhile_mono [THEN subsetD]
+ parts_spies_evs_revD2 [THEN subsetD]
+ intro: Says_Auth)
+apply (simp add: takeWhile_tail)
+done
+
+lemma A_Knows_A_Knows_ServKey:
+ "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|}
+ \<in> set evs;
+ 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; ~ ExpirServ Tt 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 (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma)
+done
+
+lemma B_Knows_A_Knows_ServKey:
+ "[| 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 |]
+ ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
+apply (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma)
+done
+
+
+lemma B_Knows_A_Knows_ServKey_refined:
+ "[| 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);
+ ~ ExpirServ Tt 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 (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma)
+done
end