src/HOL/Auth/Kerberos_BAN.ML

Added functions Suml and Sumr which are useful for constructing
datatypes involving function types.

(*  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)

  Confidentiality (secrecy) and authentication properties rely on 
  temporal checks: strong guarantees in a little abstracted - but
  very realistic - model (see .thy).

Tidied by lcp.
*)

AddDs  [Says_imp_knows_Spy RS parts.Inj, parts.Body];
AddDs  [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];

AddIffs [SesKeyLife_LB, AutLife_LB];


(*A "possibility property": there are traces that reach the end.*)
Goal "\\<exists>Timestamp K. \\<exists>evs \\<in> kerberos_ban.    \
\            Says B A (Crypt K (Number Timestamp)) \
\                 \\<in> set evs";
by (cut_facts_tac [SesKeyLife_LB] 1);
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 Asm_simp_tac);
result();



(**** Inductive proofs about kerberos_ban ****)

(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) \\<in> set evs \
\             ==> X \\<in> parts (spies evs)";
by (Blast_tac 1);
qed "Kb3_msg_in_parts_spies";
                              
Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \\<in> set evs \
\        ==> K \\<in> parts (spies evs)";
by (Blast_tac 1);
qed "Oops_parts_spies";

(*For proving the easier theorems about X \\<notin> parts (spies evs).*)
fun parts_induct_tac i = 
    etac kerberos_ban.induct i  THEN 
    ftac Oops_parts_spies (i+6)  THEN
    ftac 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 "evs \\<in> kerberos_ban ==> (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_ban ==> (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_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 "evs \\<in> kerberos_ban ==>      \
\      Key K \\<notin> used evs --> K \\<notin> 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";
Addsimps [new_keys_not_used];

(** Lemmas concerning the form of items passed in messages **)

(*Describes the form of K, X and K' when the Server sends this message.*)
Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
\        \\<in> set evs; evs \\<in> kerberos_ban |]                           \
\     ==> K \\<notin> 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 "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
\          \\<in> parts (spies evs);                          \
\        A \\<notin> bad;  evs \\<in> kerberos_ban |]                \
\      ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
\            \\<in> 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 "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \\<in> parts (spies evs); \
\        B \\<notin> bad;  evs \\<in> kerberos_ban |]                        \
\      ==> Says Server A                                         \
\           (Crypt (shrK A) {|Number Ts, Agent B, Key K,                   \
\                         Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})  \
\          \\<in> 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 "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
\           \\<in> set evs;                                                  \
\        evs \\<in> kerberos_ban |]                                          \
\==> (K \\<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
\         | X \\<in> analz (spies evs)";
by (case_tac "A \\<in> 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 = 
    ftac Says_Server_message_form 7 THEN
    ftac 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 \\<in> analz (insert (Key KAB) (spies evs)) ==>
  Key K \\<in> analz (spies evs)

 A more general formula must be proved inductively.

****)


(** Session keys are not used to encrypt other session keys **)

Goal "evs \\<in> kerberos_ban ==>                          \
\  \\<forall>K KK. KK <= - (range shrK) -->                 \
\         (Key K \\<in> analz (Key`KK Un (spies evs))) =  \
\         (K \\<in> KK | Key K \\<in> 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 "[| evs \\<in> kerberos_ban;  KAB \\<notin> range shrK |] ==>     \
\     (Key K \\<in> analz (insert (Key KAB) (spies evs))) =       \
\     (K = KAB | Key K \\<in> 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 "[| Says Server A                                    \
\          (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \\<in> set evs; \ 
\        Says Server A'                                   \
\         (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \\<in> set evs;\
\        evs \\<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*Kb2: it can't be a new key*)
by (Blast_tac 1);
qed "unique_session_keys";


(** Lemma: the session key sent in msg Kb2 would be EXPIRED
    if the spy could see it!
**)

Goal "[| A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban |]           \
\ ==> Says Server A                                            \
\         (Crypt (shrK A) {|Number Ts, Agent B, Key K,         \
\                           Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
\        \\<in> set evs -->                                         \
\     Key K \\<in> analz (spies evs) --> Expired Ts evs"; 
by (etac kerberos_ban.induct 1);
by analz_spies_tac;
by (ALLGOALS
    (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq, 
				       analz_insert_freshK] @ pushes)));
(*Oops: PROOF FAILED if addIs below*)
by (blast_tac (claset() addDs [unique_session_keys] addSIs [less_SucI]) 4);
(*Kb2*)
by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
(*Fake*) 
by (spy_analz_tac 1);
(**LEVEL 6 **)
(*Kb3*)
by (case_tac "Aa \\<in> bad" 1);
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2);
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
                               Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
                        addIs [less_SucI]) 1);
qed_spec_mp "lemma2";


(** CONFIDENTIALITY for the SERVER:
                     Spy does not see the keys sent in msg Kb2 
                     as long as they have NOT EXPIRED
**)
Goal "[| Says Server A                                           \
\         (Crypt K' {|Number T, Agent B, Key K, X|}) \\<in> set evs;  \
\        ~ Expired T evs;                                        \
\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban                \
\     |] ==> Key K \\<notin> analz (spies evs)";
by (ftac Says_Server_message_form 1 THEN assume_tac 1);
by (blast_tac (claset() addIs [lemma2]) 1);
qed "Confidentiality_S";

(**** THE COUNTERPART OF CONFIDENTIALITY 
      [|...; Expired Ts evs; ...|] ==> Key K \\<in> 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 "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \\<in> parts (spies evs);\
\        ~ Expired T evs;          \
\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban                \
\     |] ==> Key K \\<notin> 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 "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
\         \\<in> parts (spies evs);              \
\       ~ Expired Tk evs;          \
\       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban                \
\     |] ==> Key K \\<notin> analz (spies evs)";             
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
                                Confidentiality_S]) 1);
qed "Confidentiality_B";


Goal "[| B \\<notin> bad;  evs \\<in> kerberos_ban |]                        \
\     ==> Key K \\<notin> analz (spies evs) -->                    \
\         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
\         \\<in> set evs -->                                             \
\         Crypt K (Number Ta) \\<in> parts (spies evs) -->        \
\         Says B A (Crypt K (Number Ta)) \\<in> set evs";
by (etac kerberos_ban.induct 1);
by (ftac Says_S_message_form 5 THEN assume_tac 5);     
by (dtac Kb3_msg_in_parts_spies 5);
by (ftac Oops_parts_spies 7);
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
(**LEVEL 6**)
by (Blast_tac 1);
by (Clarify_tac 1);
(*
Subgoal 1: contradiction from the assumptions  
Key K \\<notin> used evs2  and Crypt K (Number Ta) \\<in> parts (spies evs2)
*)
by (dtac Crypt_imp_invKey_keysFor 1);
by (Asm_full_simp_tac 1);
(* the two tactics above detect the contradiction*)
by (case_tac "Ba \\<in> 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 "[| Crypt K (Number Ta) \\<in> parts (spies evs);           \
\        Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
\        \\<in> parts (spies evs);                               \
\        ~ Expired Ts evs;                                  \
\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban |]        \
\     ==> Says B A (Crypt K (Number Ta)) \\<in> 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 "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |]      ==>         \ 
\        Key K \\<notin> analz (spies evs) -->         \
\        Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
\        \\<in> set evs -->  \
\         Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs) -->\
\        Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
\            \\<in> set evs";
by (etac kerberos_ban.induct 1);
by (ftac Says_S_message_form 5 THEN assume_tac 5);     
by (ftac Kb3_msg_in_parts_spies 5);
by (ftac Oops_parts_spies 7);
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
(**LEVEL 6**)
by (Blast_tac 1);
by (Clarify_tac 1);
by (dtac Crypt_imp_invKey_keysFor 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
val lemma_A = result();


(*AUTHENTICATION OF A TO B*)
Goal "[| Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs);  \
\        Crypt (shrK B) {|Number Ts, Agent A, Key K|}         \
\        \\<in> parts (spies evs);                                 \
\        ~ Expired Ts evs;                                    \
\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban |]          \
\     ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \    
\                    Crypt K {|Agent A, Number Ta|}|} \\<in> 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";