src/HOL/Auth/Kerberos_BAN.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 8741 61bc5ed22b62
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Auth/Kerberos_BAN
     2     ID:         $Id$
     3     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Kerberos protocol, BAN version.
     7 
     8 From page 251 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 
    12   Confidentiality (secrecy) and authentication properties rely on 
    13   temporal checks: strong guarantees in a little abstracted - but
    14   very realistic - model (see .thy).
    15 
    16 Tidied by lcp.
    17 *)
    18 
    19 AddEs spies_partsEs;
    20 AddDs [impOfSubs analz_subset_parts];
    21 AddDs [impOfSubs Fake_parts_insert];
    22 
    23 AddIffs [SesKeyLife_LB, AutLife_LB];
    24 
    25 
    26 (*A "possibility property": there are traces that reach the end.*)
    27 Goal "EX Timestamp K. EX evs: kerberos_ban.    \
    28 \            Says B A (Crypt K (Number Timestamp)) \
    29 \                 : set evs";
    30 by (cut_facts_tac [SesKeyLife_LB] 1);
    31 by (REPEAT (resolve_tac [exI,bexI] 1));
    32 by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
    33           kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
    34 by possibility_tac;
    35 by (ALLGOALS Asm_simp_tac);
    36 result();
    37 
    38 
    39 
    40 (**** Inductive proofs about kerberos_ban ****)
    41 
    42 (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
    43 Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
    44 \             ==> X : parts (spies evs)";
    45 by (Blast_tac 1);
    46 qed "Kb3_msg_in_parts_spies";
    47                               
    48 Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
    49 \        ==> K : parts (spies evs)";
    50 by (Blast_tac 1);
    51 qed "Oops_parts_spies";
    52 
    53 (*For proving the easier theorems about X ~: parts (spies evs).*)
    54 fun parts_induct_tac i = 
    55     etac kerberos_ban.induct i  THEN 
    56     ftac Oops_parts_spies (i+6)  THEN
    57     ftac Kb3_msg_in_parts_spies (i+4)     THEN
    58     prove_simple_subgoals_tac i;
    59 
    60 
    61 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    62 Goal "evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    63 by (parts_induct_tac 1);
    64 by (ALLGOALS Blast_tac);
    65 qed "Spy_see_shrK";
    66 Addsimps [Spy_see_shrK];
    67 
    68 
    69 Goal "evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    70 by Auto_tac;
    71 qed "Spy_analz_shrK";
    72 Addsimps [Spy_analz_shrK];
    73 
    74 Goal  "[| Key (shrK A) : parts (spies evs);       \
    75 \               evs : kerberos_ban |] ==> A:bad";
    76 by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    77 qed "Spy_see_shrK_D";
    78 
    79 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    80 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    81 
    82 
    83 (*Nobody can have used non-existent keys!*)
    84 Goal "evs : kerberos_ban ==>      \
    85 \      Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    86 by (parts_induct_tac 1);
    87 (*Fake*)
    88 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    89 (*Kb2, Kb3, Kb4*)
    90 by (ALLGOALS Blast_tac);
    91 qed_spec_mp "new_keys_not_used";
    92 
    93 bind_thm ("new_keys_not_analzd",
    94           [analz_subset_parts RS keysFor_mono,
    95            new_keys_not_used] MRS contra_subsetD);
    96 
    97 Addsimps [new_keys_not_used, new_keys_not_analzd];
    98 
    99 
   100 (** Lemmas concerning the form of items passed in messages **)
   101 
   102 (*Describes the form of K, X and K' when the Server sends this message.*)
   103 Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
   104 \        : set evs; evs : kerberos_ban |]                           \
   105 \     ==> K ~: range shrK &                                         \
   106 \         X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &      \
   107 \         K' = shrK A";
   108 by (etac rev_mp 1);
   109 by (etac kerberos_ban.induct 1);
   110 by Auto_tac;
   111 qed "Says_Server_message_form";
   112 
   113 
   114 (*If the encrypted message appears then it originated with the Server
   115   PROVIDED that A is NOT compromised!
   116 
   117   This shows implicitly the FRESHNESS OF THE SESSION KEY to A
   118 *)
   119 Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
   120 \          : parts (spies evs);                          \
   121 \        A ~: bad;  evs : kerberos_ban |]                \
   122 \      ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   123 \            : set evs";
   124 by (etac rev_mp 1);
   125 by (parts_induct_tac 1);
   126 by (Blast_tac 1);
   127 qed "A_trusts_K_by_Kb2";
   128 
   129 
   130 (*If the TICKET appears then it originated with the Server*)
   131 (*FRESHNESS OF THE SESSION KEY to B*)
   132 Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
   133 \        B ~: bad;  evs : kerberos_ban |]                        \
   134 \      ==> Says Server A                                         \
   135 \           (Crypt (shrK A) {|Number Ts, Agent B, Key K,                   \
   136 \                         Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})  \
   137 \          : set evs";
   138 by (etac rev_mp 1);
   139 by (parts_induct_tac 1);
   140 by (Blast_tac 1);
   141 qed "B_trusts_K_by_Kb3";
   142 
   143 
   144 (*EITHER describes the form of X when the following message is sent, 
   145   OR     reduces it to the Fake case.
   146   Use Says_Server_message_form if applicable.*)
   147 Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
   148 \           : set evs;                                                  \
   149 \        evs : kerberos_ban |]                                          \
   150 \==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
   151 \         | X : analz (spies evs)";
   152 by (case_tac "A : bad" 1);
   153 by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
   154                       addss (simpset())) 1);
   155 by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   156 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 
   157 				Says_Server_message_form]) 1);
   158 qed "Says_S_message_form";
   159 
   160 
   161 (*For proofs involving analz.*)
   162 val analz_spies_tac = 
   163     ftac Says_Server_message_form 7 THEN
   164     ftac Says_S_message_form 5 THEN 
   165     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   166 
   167 
   168 (****
   169  The following is to prove theorems of the form
   170 
   171   Key K : analz (insert (Key KAB) (spies evs)) ==>
   172   Key K : analz (spies evs)
   173 
   174  A more general formula must be proved inductively.
   175 
   176 ****)
   177 
   178 
   179 (** Session keys are not used to encrypt other session keys **)
   180 
   181 Goal "evs : kerberos_ban ==>                          \
   182 \  ALL K KK. KK <= - (range shrK) -->                 \
   183 \         (Key K : analz (Key``KK Un (spies evs))) =  \
   184 \         (K : KK | Key K : analz (spies evs))";
   185 by (etac kerberos_ban.induct 1);
   186 by analz_spies_tac;
   187 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   188 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   189 (*Takes 5 secs*)
   190 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   191 (*Fake*) 
   192 by (spy_analz_tac 1);
   193 qed_spec_mp "analz_image_freshK";
   194 
   195 
   196 Goal "[| evs : kerberos_ban;  KAB ~: range shrK |] ==>     \
   197 \     Key K : analz (insert (Key KAB) (spies evs)) =       \
   198 \     (K = KAB | Key K : analz (spies evs))";
   199 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   200 qed "analz_insert_freshK";
   201 
   202 
   203 (** The session key K uniquely identifies the message **)
   204 
   205 Goal "evs : kerberos_ban ==>                                         \
   206 \   EX A' Ts' B' X'. ALL A Ts B X.                                   \
   207 \    Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   208 \          : set evs \
   209 \    -->         A=A' & Ts=Ts' & B=B' & X=X'";
   210 by (etac kerberos_ban.induct 1);
   211 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   212 by Safe_tac;
   213 (*Kb2: it can't be a new key*)
   214 by (expand_case_tac "K = ?y" 1);
   215 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   216 by (blast_tac (claset() delrules [conjI]) 1);
   217 val lemma = result();
   218 
   219 (*In messages of this form, the session key uniquely identifies the rest*)
   220 Goal "[| Says Server A                                    \
   221 \          (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ 
   222 \        Says Server A'                                   \
   223 \         (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\
   224 \        evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
   225 by (prove_unique_tac lemma 1);
   226 qed "unique_session_keys";
   227 
   228 
   229 (** Lemma: the session key sent in msg Kb2 would be EXPIRED
   230     if the spy could see it!
   231 **)
   232 
   233 Goal "[| A ~: bad;  B ~: bad;  evs : kerberos_ban |]           \
   234 \ ==> Says Server A                                            \
   235 \         (Crypt (shrK A) {|Number Ts, Agent B, Key K,         \
   236 \                           Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
   237 \        : set evs -->                                         \
   238 \     Key K : analz (spies evs) --> Expired Ts evs"; 
   239 by (etac kerberos_ban.induct 1);
   240 by analz_spies_tac;
   241 by (ALLGOALS
   242     (asm_simp_tac (simpset() addsimps [analz_insert_eq, analz_insert_freshK]
   243 				      @ pushes)));
   244 (*Oops*)
   245 by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
   246 (*Kb2*)
   247 by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
   248 (*Fake*) 
   249 by (spy_analz_tac 1);
   250 (**LEVEL 6 **)
   251 (*Kb3*)
   252 by (case_tac "Aa : bad" 1);
   253 by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2);
   254 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
   255                                Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
   256                         addIs [less_SucI]) 1);
   257 qed_spec_mp "lemma2";
   258 
   259 
   260 (** CONFIDENTIALITY for the SERVER:
   261                      Spy does not see the keys sent in msg Kb2 
   262                      as long as they have NOT EXPIRED
   263 **)
   264 Goal "[| Says Server A                                           \
   265 \         (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs;  \
   266 \        ~ Expired T evs;                                        \
   267 \        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   268 \     |] ==> Key K ~: analz (spies evs)";
   269 by (ftac Says_Server_message_form 1 THEN assume_tac 1);
   270 by (blast_tac (claset() addIs [lemma2]) 1);
   271 qed "Confidentiality_S";
   272 
   273 (**** THE COUNTERPART OF CONFIDENTIALITY 
   274       [|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs)
   275       WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
   276 
   277 
   278 (** CONFIDENTIALITY for ALICE: **)
   279 (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
   280 Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\
   281 \        ~ Expired T evs;          \
   282 \        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   283 \     |] ==> Key K ~: analz (spies evs)";
   284 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1);
   285 qed "Confidentiality_A";
   286 
   287 
   288 (** CONFIDENTIALITY for BOB: **)
   289 (** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
   290 Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
   291 \         : parts (spies evs);              \
   292 \       ~ Expired Tk evs;          \
   293 \       A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   294 \     |] ==> Key K ~: analz (spies evs)";             
   295 by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
   296                                 Confidentiality_S]) 1);
   297 qed "Confidentiality_B";
   298 
   299 
   300 Goal "[| B ~: bad;  evs : kerberos_ban |]                        \
   301 \     ==> Key K ~: analz (spies evs) -->                    \
   302 \         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   303 \         : set evs -->                                             \
   304 \         Crypt K (Number Ta) : parts (spies evs) -->        \
   305 \         Says B A (Crypt K (Number Ta)) : set evs";
   306 by (etac kerberos_ban.induct 1);
   307 by (ftac Says_S_message_form 5 THEN assume_tac 5);     
   308 by (dtac Kb3_msg_in_parts_spies 5);
   309 by (ftac Oops_parts_spies 7);
   310 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   311 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   312 (**LEVEL 6**)
   313 by (Blast_tac 1);
   314 by (Clarify_tac 1);
   315 (*
   316 Subgoal 1: contradiction from the assumptions  
   317 Key K ~: used evs2  and Crypt K (Number Ta) : parts (spies evs2)
   318 *)
   319 by (dtac Crypt_imp_invKey_keysFor 1);
   320 by (Asm_full_simp_tac 1);
   321 (* the two tactics above detect the contradiction*)
   322 by (case_tac "Ba : bad" 1);  (*splits up the subgoal by the stated case*)
   323 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 
   324                               B_trusts_K_by_Kb3, 
   325 			      unique_session_keys]) 2);
   326 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS 
   327 			      Crypt_Spy_analz_bad]) 1);
   328 val lemma_B = result();
   329 
   330 
   331 (*AUTHENTICATION OF B TO A*)
   332 Goal "[| Crypt K (Number Ta) : parts (spies evs);           \
   333 \        Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
   334 \        : parts (spies evs);                               \
   335 \        ~ Expired Ts evs;                                  \
   336 \        A ~: bad;  B ~: bad;  evs : kerberos_ban |]        \
   337 \     ==> Says B A (Crypt K (Number Ta)) : set evs";
   338 by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
   339                         addSIs [lemma_B RS mp RS mp RS mp]
   340                         addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
   341 qed "Authentication_B";
   342 
   343 
   344 Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |]      ==>         \ 
   345 \        Key K ~: analz (spies evs) -->         \
   346 \        Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
   347 \        : set evs -->  \
   348 \         Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\
   349 \        Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
   350 \            : set evs";
   351 by (etac kerberos_ban.induct 1);
   352 by (ftac Says_S_message_form 5 THEN assume_tac 5);     
   353 by (ftac Kb3_msg_in_parts_spies 5);
   354 by (ftac Oops_parts_spies 7);
   355 by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   356 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   357 (**LEVEL 6**)
   358 by (Blast_tac 1);
   359 by (Clarify_tac 1);
   360 by (dtac Crypt_imp_invKey_keysFor 1);
   361 by (Asm_full_simp_tac 1);
   362 by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
   363 val lemma_A = result();
   364 
   365 
   366 (*AUTHENTICATION OF A TO B*)
   367 Goal "[| Crypt K {|Agent A, Number Ta|} : parts (spies evs);  \
   368 \        Crypt (shrK B) {|Number Ts, Agent A, Key K|}         \
   369 \        : parts (spies evs);                                 \
   370 \        ~ Expired Ts evs;                                    \
   371 \        A ~: bad;  B ~: bad;  evs : kerberos_ban |]          \
   372 \     ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \    
   373 \                    Crypt K {|Agent A, Number Ta|}|} : set evs";
   374 by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
   375                         addSIs [lemma_A RS mp RS mp RS mp]
   376                         addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
   377 qed "Authentication_A";