src/HOL/Auth/Kerberos_BAN.ML

 
 AddIffs [SesKeyLife_LB, AutLife_LB];
 
 
 (*A "possibility property": there are traces that reach the end.*)
-goal thy 
+Goal 
  "!!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));

 
 
 (**** Inductive proofs about kerberos_ban ****)
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
+Goal "!!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 \
+Goal "!!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
+Goal
     "!!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";
 

     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 
+Goal 
 "!!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 
+Goal 
 "!!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);       \
+Goal  "!!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 ==>      \
+Goal "!!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*)

 
 
 (** 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 
+Goal 
  "!!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";

 (*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
+Goal
  "!!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";

 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
+Goal
  "!!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|}|})  \

 
 
 (*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 
+Goal 
  "!!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)";

 ****)
 
 
 (** Session keys are not used to encrypt other session keys **)
 
-goal thy  
+Goal  
  "!!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);

 (*Fake*) 
 by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 
-goal thy
+Goal
  "!!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 
+Goal 
  "!!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 (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 
+Goal 
  "!!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'";

 
 (** Lemma: the session key sent in msg Kb2 would be EXPIRED
     if the spy could see it!
 **)
 
-goal thy 
+Goal 
  "!!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 -->                                         \

 
 (** CONFIDENTIALITY for the SERVER:
                      Spy does not see the keys sent in msg Kb2 
                      as long as they have NOT EXPIRED
 **)
-goal thy 
+Goal 
  "!!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)";

       WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
 
 
 (** CONFIDENTIALITY for ALICE: **)
 (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
-goal thy 
+Goal 
 "!!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
+Goal
 "!!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
+Goal
  "!!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) -->        \

 			      Crypt_Spy_analz_bad]) 1);
 val lemma_B = result();
 
 
 (*AUTHENTICATION OF B TO A*)
-goal thy
+Goal
  "!!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 |]        \

                         addSIs [lemma_B RS mp RS mp RS mp]
                         addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
 qed "Authentication_B";
 
 
-goal thy
+Goal
  "!!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) -->\

 by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
 val lemma_A = result();
 
 
 (*AUTHENTICATION OF A TO B*)
-goal thy
+Goal
  "!!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 |]          \