--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Jun 19 10:34:33 1998 +0200
@@ -0,0 +1,450 @@
+(* Title: HOL/Auth/Kerberos_BAN
+ ID: $Id$
+ Author: Giampaolo Bella, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Kerberos protocol, BAN version.
+
+From page 251 of
+ Burrows, Abadi and Needham. A Logic of Authentication.
+ Proc. Royal Soc. 426 (1989)
+*)
+
+open Kerberos_BAN;
+
+(*
+ Confidentiality (secrecy) and authentication properties rely on
+ temporal checks: strong guarantees in a little abstracted - but
+ very realistic - model (see .thy).
+
+ Total execution time: 158s
+*)
+
+proof_timing:=true;
+HOL_quantifiers := false;
+
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
+AddSIs [SesKeyLife_LB, AutLife_LB];
+
+Addsimps [SesKeyLife_LB, AutLife_LB];
+
+
+(*A "possibility property": there are traces that reach the end.*)
+goal thy
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+\ ==> EX Timestamp K. EX evs: kerberos_ban. \
+\ Says B A (Crypt K (Number Timestamp)) \
+\ : set evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS
+ kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
+by possibility_tac;
+by (ALLGOALS (simp_tac (simpset() addsimps [leD]))); (*from NatDef.ML!!!!*)
+by (cut_facts_tac [SesKeyLife_LB] 1);
+by (trans_tac 1);
+result();
+
+
+
+(**** Inductive proofs about kerberos_ban ****)
+
+(*Nobody sends themselves messages*)
+goal thy "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
+by (etac kerberos_ban.induct 1);
+by Auto_tac;
+qed_spec_mp "not_Says_to_self";
+Addsimps [not_Says_to_self];
+AddSEs [not_Says_to_self RSN (2, rev_notE)];
+
+
+(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
+goal thy "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
+\ ==> X : parts (spies evs)";
+by (Blast_tac 1);
+qed "Kb3_msg_in_parts_spies";
+
+goal thy
+ "!!evs. Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
+\ ==> K : parts (spies evs)";
+by (Blast_tac 1);
+qed "Oops_parts_spies";
+
+(*For proving the easier theorems about X ~: parts (spies evs).*)
+fun parts_induct_tac i =
+ etac kerberos_ban.induct i THEN
+ forward_tac [Oops_parts_spies] (i+6) THEN
+ forward_tac [Kb3_msg_in_parts_spies] (i+4) THEN
+ prove_simple_subgoals_tac i;
+
+
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+goal thy
+"!!evs. evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+by (parts_induct_tac 1);
+by (ALLGOALS Blast_tac);
+qed "Spy_see_shrK";
+Addsimps [Spy_see_shrK];
+
+
+goal thy
+"!!evs. evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+by Auto_tac;
+qed "Spy_analz_shrK";
+Addsimps [Spy_analz_shrK];
+
+goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
+\ evs : kerberos_ban |] ==> 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 thy "!!evs. evs : kerberos_ban ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+by (parts_induct_tac 1);
+(*Fake*)
+by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
+(*Kb2, Kb3, Kb4*)
+by (ALLGOALS Blast_tac);
+qed_spec_mp "new_keys_not_used";
+
+bind_thm ("new_keys_not_analzd",
+ [analz_subset_parts RS keysFor_mono,
+ new_keys_not_used] MRS contra_subsetD);
+
+Addsimps [new_keys_not_used, new_keys_not_analzd];
+
+
+(** Lemmas concerning the form of items passed in messages **)
+
+(*Describes the form of K, X and K' when the Server sends this message.*)
+goal thy
+ "!!evs. [| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \
+\ : set evs; evs : kerberos_ban |] \
+\ ==> K ~: range shrK & \
+\ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \
+\ K' = shrK A";
+by (etac rev_mp 1);
+by (etac kerberos_ban.induct 1);
+by Auto_tac;
+qed "Says_Server_message_form";
+
+
+(*If the encrypted message appears then it originated with the Server
+ PROVIDED that A is NOT compromised!
+
+ This shows implicitly the FRESHNESS OF THE SESSION KEY to A
+*)
+goal thy
+ "!!evs. [| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
+\ : parts (spies evs); \
+\ A ~: bad; evs : kerberos_ban |] \
+\ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
+\ : set evs";
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (Blast_tac 1);
+qed "A_trusts_K_by_Kb2";
+
+
+(*If the TICKET appears then it originated with the Server*)
+(*FRESHNESS OF THE SESSION KEY to B*)
+goal thy
+ "!!evs. [| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
+\ B ~: bad; evs : kerberos_ban |] \
+\ ==> Says Server A \
+\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \
+\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \
+\ : set evs";
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (Blast_tac 1);
+qed "B_trusts_K_by_Kb3";
+
+
+(*EITHER describes the form of X when the following message is sent,
+ OR reduces it to the Fake case.
+ Use Says_Server_message_form if applicable.*)
+goal thy
+ "!!evs. [| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
+\ : set evs; \
+\ evs : kerberos_ban |] \
+\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
+\ | X : analz (spies evs)";
+by (case_tac "A : bad" 1);
+by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
+ addss (simpset())) 1);
+by (forward_tac [Says_imp_spies RS parts.Inj] 1);
+by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2,
+ Says_Server_message_form]) 1);
+qed "Says_S_message_form";
+
+
+(*For proofs involving analz.*)
+val analz_spies_tac =
+ forward_tac [Says_Server_message_form] 7 THEN
+ forward_tac [Says_S_message_form] 5 THEN
+ REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
+
+
+(****
+ The following is to prove theorems of the form
+
+ Key K : analz (insert (Key KAB) (spies evs)) ==>
+ Key K : analz (spies evs)
+
+ A more general formula must be proved inductively.
+
+****)
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+goal thy
+ "!!evs. evs : kerberos_ban ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
+by (etac kerberos_ban.induct 1);
+by analz_spies_tac;
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
+(*Takes 5 secs*)
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Fake*)
+by (spy_analz_tac 1);
+qed_spec_mp "analz_image_freshK";
+
+
+goal thy
+ "!!evs. [| evs : kerberos_ban; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
+
+
+(** The session key K uniquely identifies the message **)
+
+goal thy
+ "!!evs. evs : kerberos_ban ==> \
+\ EX A' Ts' B' X'. ALL A Ts B X. \
+\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
+\ : set evs \
+\ --> A=A' & Ts=Ts' & B=B' & X=X'";
+by (etac kerberos_ban.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
+by Safe_tac;
+(*Kb2: it can't be a new key*)
+by (expand_case_tac "K = ?y" 1);
+by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
+by (blast_tac (claset() delrules [conjI]) 1);
+val lemma = result();
+
+(*In messages of this form, the session key uniquely identifies the rest*)
+goal thy
+ "!!evs. [| Says Server A \
+\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \
+\ Says Server A' \
+\ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\
+\ evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
+by (prove_unique_tac lemma 1);
+qed "unique_session_keys";
+
+
+(** Lemma: the session key sent in msg Kb2 would be EXPIRED
+ if the spy could see it!
+**)
+
+goal thy
+ "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] \
+\ ==> Says Server A \
+\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \
+\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
+\ : set evs --> \
+\ Key K : analz (spies evs) --> Expired Ts evs";
+by (etac kerberos_ban.induct 1);
+by analz_spies_tac;
+by (ALLGOALS
+ (asm_simp_tac (simpset()
+ addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes @ split_ifs))));
+(*Oops*)
+by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
+(*Kb2*)
+by (fast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
+(**LEVEL 6 **)
+by (clarify_tac (claset() delrules [impCE]) 1);
+by (case_tac "Ba : bad" 1);
+by (blast_tac (claset() addIs [less_SucI]) 2);
+(**LEVEL 9**)
+by (rotate_tac 10 1);
+by (forward_tac [mp] 1 THEN assume_tac 1);
+by (etac disjE 1);
+by (blast_tac (claset() addIs [less_SucI]) 2);
+(**LEVEL 13**)
+by (Clarify_tac 1);
+by (case_tac "Aa : bad" 1);
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj,
+ A_trusts_K_by_Kb2, unique_session_keys]) 2);
+(**LEVEL 16**)
+by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
+ Crypt_Spy_analz_bad RS analz.Snd RS
+ analz.Snd RS analz.Fst]
+ addIs [less_SucI]) 1);
+val lemma = result() RS mp RS mp RSN(1,rev_notE);
+
+
+(** CONFIDENTIALITY for the SERVER:
+ Spy does not see the keys sent in msg Kb2
+ as long as they have NOT EXPIRED
+**)
+goal thy
+ "!!evs. [| Says Server A \
+\ (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs; \
+\ ~ Expired T evs; \
+\ A ~: bad; B ~: bad; evs : kerberos_ban \
+\ |] ==> Key K ~: analz (spies evs)";
+by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
+by (Clarify_tac 1);
+by (rtac ccontr 1);
+by (blast_tac (claset() addSEs [lemma]) 1);
+qed "Confidentiality_S";
+
+(**** THE COUNTERPART OF CONFIDENTIALITY
+ [|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs)
+ WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****)
+
+
+(** CONFIDENTIALITY for ALICE: **)
+(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
+goal thy
+"!!evs. [| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\
+\ ~ Expired T evs; \
+\ A ~: bad; B ~: bad; evs : kerberos_ban \
+\ |] ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2,
+ Confidentiality_S]) 1);
+qed "Confidentiality_A";
+
+
+(** CONFIDENTIALITY for BOB: **)
+(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
+goal thy
+"!!evs. [| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
+\ : parts (spies evs); \
+\ ~ Expired Tk evs; \
+\ A ~: bad; B ~: bad; evs : kerberos_ban \
+\ |] ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3,
+ Confidentiality_S]) 1);
+qed "Confidentiality_B";
+
+
+goal thy
+ "!!evs. [| B ~: bad; evs : kerberos_ban |] \
+\ ==> Key K ~: analz (spies evs) --> \
+\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
+\ : set evs --> \
+\ Crypt K (Number Ta) : parts (spies evs) --> \
+\ Says B A (Crypt K (Number Ta)) : set evs";
+by (etac kerberos_ban.induct 1);
+by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
+by (dtac Kb3_msg_in_parts_spies 5);
+by (forward_tac [Oops_parts_spies] 7);
+by (TRYALL (rtac impI));
+by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
+(**LEVEL 7**)
+by (Blast_tac 1);
+by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
+(*
+Subgoal 1: contradiction from the assumptions
+Key K ~: used evs2 and Crypt K (Number Ta) : parts (spies evs2)
+*)
+by (dtac Crypt_imp_invKey_keysFor 1);
+by (Asm_full_simp_tac 1);
+(* the two tactics above detectthe contradiction*)
+by (rtac disjI1 1);
+by (thin_tac "?PP-->?QQ" 1); (*deletes the matching assumptions*)
+by (case_tac "Ba : bad" 1); (*splits up the subgoal by the stated case*)
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
+ B_trusts_K_by_Kb3,
+ unique_session_keys]) 2);
+by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS
+ Crypt_Spy_analz_bad]) 1);
+val lemma_B = result();
+
+
+(*AUTHENTICATION OF B TO A*)
+goal thy
+ "!!evs. [| Crypt K (Number Ta) : parts (spies evs); \
+\ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
+\ : parts (spies evs); \
+\ ~ Expired Ts evs; \
+\ A ~: bad; B ~: bad; evs : kerberos_ban |] \
+\ ==> Says B A (Crypt K (Number Ta)) : set evs";
+by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
+ addSIs [lemma_B RS mp RS mp RS mp]
+ addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
+qed "Authentication_B";
+
+
+goal thy
+ "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] ==> \
+\ Key K ~: analz (spies evs) --> \
+\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
+\ : set evs --> \
+\ Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\
+\ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \
+\ : set evs";
+by (etac kerberos_ban.induct 1);
+by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
+by (forward_tac [Kb3_msg_in_parts_spies] 5);
+by (forward_tac [Oops_parts_spies] 7);
+by (TRYALL (rtac impI));
+by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
+(**LEVEL 7**)
+by (Blast_tac 1);
+by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
+by (dtac Crypt_imp_invKey_keysFor 1);
+by (Asm_full_simp_tac 1);
+by (rtac disjI1 1);
+(*Last Subgoal! ...to be refined...*)
+by (thin_tac "Says ?A Server ?X : set evs3" 1);
+by (dresolve_tac [Says_imp_spies RS parts.Inj] 1);
+by (dresolve_tac [Says_imp_spies RS parts.Inj] 1);
+by (dtac A_trusts_K_by_Kb2 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (dtac A_trusts_K_by_Kb2 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (dtac unique_session_keys 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (Blast_tac 1);
+val lemma_A = result();
+
+
+(*AUTHENTICATION OF A TO B*)
+goal thy
+ "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \
+\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \
+\ : parts (spies evs); \
+\ ~ Expired Ts evs; \
+\ A ~: bad; B ~: bad; evs : kerberos_ban |] \
+\ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \
+\ Crypt K {|Agent A, Number Ta|}|} : set evs";
+by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
+ addSIs [lemma_A RS mp RS mp RS mp]
+ addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
+qed "Authentication_A";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Kerberos_BAN.thy Fri Jun 19 10:34:33 1998 +0200
@@ -0,0 +1,97 @@
+(* Title: HOL/Auth/Kerberos_BAN
+ ID: $Id$
+ Author: Giampaolo Bella, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Kerberos protocol, BAN version.
+
+From page 251 of
+ Burrows, Abadi and Needham. A Logic of Authentication.
+ Proc. Royal Soc. 426 (1989)
+*)
+
+Kerberos_BAN = Shared +
+
+(* Temporal modelization: session keys can be leaked
+ ONLY when they have expired *)
+
+syntax
+ CT :: event list=>nat
+ Expired :: [nat, event list] => bool
+ RecentAuth :: [nat, event list] => bool
+
+consts
+
+ (*Duration of the session key*)
+ SesKeyLife :: nat
+
+ (*Duration of the authenticator*)
+ AutLife :: nat
+
+rules
+ (*The ticket should remain fresh for two journeys on the network at least*)
+ SesKeyLife_LB "2 <= SesKeyLife"
+
+ (*The authenticator only for one journey*)
+ AutLife_LB "1 <= AutLife"
+
+translations
+ "CT" == "length"
+
+ "Expired T evs" == "SesKeyLife + T < CT evs"
+
+ "RecentAuth T evs" == "CT evs <= AutLife + T"
+
+consts kerberos_ban :: event list set
+inductive "kerberos_ban"
+ intrs
+
+ Nil "[]: kerberos_ban"
+
+
+ Fake "[| evs: kerberos_ban; B ~= Spy;
+ X: synth (analz (spies evs)) |]
+ ==> Says Spy B X # evs : kerberos_ban"
+
+
+ Kb1 "[| evs1: kerberos_ban; A ~= Server |]
+ ==> Says A Server {|Agent A, Agent B|} # evs1
+ : kerberos_ban"
+
+
+ Kb2 "[| evs2: kerberos_ban; A ~= B; A ~= Server; Key KAB ~: used evs2;
+ Says A' Server {|Agent A, Agent B|} : set evs2 |]
+ ==> Says Server A
+ (Crypt (shrK A)
+ {|Number (CT evs2), Agent B, Key KAB,
+ (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|})
+ # evs2 : kerberos_ban"
+
+
+ Kb3 "[| evs3: kerberos_ban; A ~= B;
+ Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ : set evs3;
+ Says A Server {|Agent A, Agent B|} : set evs3;
+ ~ Expired Ts evs3 |]
+ ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |}
+ # evs3 : kerberos_ban"
+
+
+ Kb4 "[| evs4: kerberos_ban; A ~= B;
+ Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
+ (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
+ ~ Expired Ts evs4;
+ RecentAuth Ta evs4|]
+ ==> Says B A (Crypt K (Number Ta)) # evs4
+ : kerberos_ban"
+
+
+(*The session key has EXPIRED when it gets lost *)
+ Oops "[| evso: kerberos_ban; A ~= Spy;
+ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ : set evso;
+ Expired Ts evso |]
+ ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
+
+
+end