New example Kerberos_BAN by G Bella
authorpaulson
Fri Jun 19 10:34:33 1998 +0200 (1998-06-19)
changeset 505375d20f367e94
parent 5052 bbe3584b515b
child 5054 77cc7e7b50f2
New example Kerberos_BAN by G Bella
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Fri Jun 19 10:34:33 1998 +0200
     1.3 @@ -0,0 +1,450 @@
     1.4 +(*  Title:      HOL/Auth/Kerberos_BAN
     1.5 +    ID:         $Id$
     1.6 +    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +The Kerberos protocol, BAN version.
    1.10 +
    1.11 +From page 251 of
    1.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 +  Proc. Royal Soc. 426 (1989)
    1.14 +*)
    1.15 +
    1.16 +open Kerberos_BAN;
    1.17 +
    1.18 +(*
    1.19 +   Confidentiality (secrecy) and authentication properties rely on 
    1.20 +   temporal checks: strong guarantees in a little abstracted - but
    1.21 +   very realistic - model (see .thy).
    1.22 +
    1.23 +   Total execution time: 158s
    1.24 +*)
    1.25 +
    1.26 +proof_timing:=true;
    1.27 +HOL_quantifiers := false;
    1.28 +
    1.29 +AddEs spies_partsEs;
    1.30 +AddDs [impOfSubs analz_subset_parts];
    1.31 +AddDs [impOfSubs Fake_parts_insert];
    1.32 +
    1.33 +AddSIs [SesKeyLife_LB, AutLife_LB];
    1.34 +
    1.35 +Addsimps [SesKeyLife_LB, AutLife_LB];
    1.36 +
    1.37 +
    1.38 +(*A "possibility property": there are traces that reach the end.*)
    1.39 +goal thy 
    1.40 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
    1.41 +\        ==> EX Timestamp K. EX evs: kerberos_ban.    \
    1.42 +\               Says B A (Crypt K (Number Timestamp)) \
    1.43 +\                    : set evs";
    1.44 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.45 +by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
    1.46 +          kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
    1.47 +by possibility_tac;
    1.48 +by (ALLGOALS (simp_tac (simpset() addsimps [leD]))); (*from NatDef.ML!!!!*)
    1.49 +by (cut_facts_tac [SesKeyLife_LB] 1);
    1.50 +by (trans_tac 1);
    1.51 +result();
    1.52 +
    1.53 +
    1.54 +
    1.55 +(**** Inductive proofs about kerberos_ban ****)
    1.56 +
    1.57 +(*Nobody sends themselves messages*)
    1.58 +goal thy "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
    1.59 +by (etac kerberos_ban.induct 1);
    1.60 +by Auto_tac;
    1.61 +qed_spec_mp "not_Says_to_self";
    1.62 +Addsimps [not_Says_to_self];
    1.63 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.64 +
    1.65 +
    1.66 +(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
    1.67 +goal thy "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
    1.68 +\                ==> X : parts (spies evs)";
    1.69 +by (Blast_tac 1);
    1.70 +qed "Kb3_msg_in_parts_spies";
    1.71 +                              
    1.72 +goal thy
    1.73 +    "!!evs. Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
    1.74 +\           ==> K : parts (spies evs)";
    1.75 +by (Blast_tac 1);
    1.76 +qed "Oops_parts_spies";
    1.77 +
    1.78 +(*For proving the easier theorems about X ~: parts (spies evs).*)
    1.79 +fun parts_induct_tac i = 
    1.80 +    etac kerberos_ban.induct i  THEN 
    1.81 +    forward_tac [Oops_parts_spies] (i+6)  THEN
    1.82 +    forward_tac [Kb3_msg_in_parts_spies] (i+4)     THEN
    1.83 +    prove_simple_subgoals_tac i;
    1.84 +
    1.85 +
    1.86 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.87 +goal thy 
    1.88 +"!!evs. evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.89 +by (parts_induct_tac 1);
    1.90 +by (ALLGOALS Blast_tac);
    1.91 +qed "Spy_see_shrK";
    1.92 +Addsimps [Spy_see_shrK];
    1.93 +
    1.94 +
    1.95 +goal thy 
    1.96 +"!!evs. evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.97 +by Auto_tac;
    1.98 +qed "Spy_analz_shrK";
    1.99 +Addsimps [Spy_analz_shrK];
   1.100 +
   1.101 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
   1.102 +\                  evs : kerberos_ban |] ==> A:bad";
   1.103 +by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
   1.104 +qed "Spy_see_shrK_D";
   1.105 +
   1.106 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   1.107 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   1.108 +
   1.109 +
   1.110 +(*Nobody can have used non-existent keys!*)
   1.111 +goal thy "!!evs. evs : kerberos_ban ==>      \
   1.112 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   1.113 +by (parts_induct_tac 1);
   1.114 +(*Fake*)
   1.115 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   1.116 +(*Kb2, Kb3, Kb4*)
   1.117 +by (ALLGOALS Blast_tac);
   1.118 +qed_spec_mp "new_keys_not_used";
   1.119 +
   1.120 +bind_thm ("new_keys_not_analzd",
   1.121 +          [analz_subset_parts RS keysFor_mono,
   1.122 +           new_keys_not_used] MRS contra_subsetD);
   1.123 +
   1.124 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.125 +
   1.126 +
   1.127 +(** Lemmas concerning the form of items passed in messages **)
   1.128 +
   1.129 +(*Describes the form of K, X and K' when the Server sends this message.*)
   1.130 +goal thy 
   1.131 + "!!evs. [| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
   1.132 +\           : set evs; evs : kerberos_ban |]                           \
   1.133 +\        ==> K ~: range shrK &                                         \
   1.134 +\            X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &      \
   1.135 +\            K' = shrK A";
   1.136 +by (etac rev_mp 1);
   1.137 +by (etac kerberos_ban.induct 1);
   1.138 +by Auto_tac;
   1.139 +qed "Says_Server_message_form";
   1.140 +
   1.141 +
   1.142 +(*If the encrypted message appears then it originated with the Server
   1.143 +  PROVIDED that A is NOT compromised!
   1.144 +
   1.145 +  This shows implicitly the FRESHNESS OF THE SESSION KEY to A
   1.146 +*)
   1.147 +goal thy
   1.148 + "!!evs. [| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
   1.149 +\             : parts (spies evs);                          \
   1.150 +\           A ~: bad;  evs : kerberos_ban |]                \
   1.151 +\         ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   1.152 +\               : set evs";
   1.153 +by (etac rev_mp 1);
   1.154 +by (parts_induct_tac 1);
   1.155 +by (Blast_tac 1);
   1.156 +qed "A_trusts_K_by_Kb2";
   1.157 +
   1.158 +
   1.159 +(*If the TICKET appears then it originated with the Server*)
   1.160 +(*FRESHNESS OF THE SESSION KEY to B*)
   1.161 +goal thy
   1.162 + "!!evs. [| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
   1.163 +\           B ~: bad;  evs : kerberos_ban |]                        \
   1.164 +\         ==> Says Server A                                         \
   1.165 +\              (Crypt (shrK A) {|Number Ts, Agent B, Key K,                   \
   1.166 +\                            Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})  \
   1.167 +\             : set evs";
   1.168 +by (etac rev_mp 1);
   1.169 +by (parts_induct_tac 1);
   1.170 +by (Blast_tac 1);
   1.171 +qed "B_trusts_K_by_Kb3";
   1.172 +
   1.173 +
   1.174 +(*EITHER describes the form of X when the following message is sent, 
   1.175 +  OR     reduces it to the Fake case.
   1.176 +  Use Says_Server_message_form if applicable.*)
   1.177 +goal thy 
   1.178 + "!!evs. [| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
   1.179 +\              : set evs;                                                  \
   1.180 +\           evs : kerberos_ban |]                                          \
   1.181 +\   ==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
   1.182 +\            | X : analz (spies evs)";
   1.183 +by (case_tac "A : bad" 1);
   1.184 +by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
   1.185 +                      addss (simpset())) 1);
   1.186 +by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   1.187 +by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 
   1.188 +				Says_Server_message_form]) 1);
   1.189 +qed "Says_S_message_form";
   1.190 +
   1.191 +
   1.192 +(*For proofs involving analz.*)
   1.193 +val analz_spies_tac = 
   1.194 +    forward_tac [Says_Server_message_form] 7 THEN
   1.195 +    forward_tac [Says_S_message_form] 5 THEN 
   1.196 +    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   1.197 +
   1.198 +
   1.199 +(****
   1.200 + The following is to prove theorems of the form
   1.201 +
   1.202 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
   1.203 +  Key K : analz (spies evs)
   1.204 +
   1.205 + A more general formula must be proved inductively.
   1.206 +
   1.207 +****)
   1.208 +
   1.209 +
   1.210 +(** Session keys are not used to encrypt other session keys **)
   1.211 +
   1.212 +goal thy  
   1.213 + "!!evs. evs : kerberos_ban ==>                          \
   1.214 +\  ALL K KK. KK <= Compl (range shrK) -->                \
   1.215 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
   1.216 +\            (K : KK | Key K : analz (spies evs))";
   1.217 +by (etac kerberos_ban.induct 1);
   1.218 +by analz_spies_tac;
   1.219 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.220 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   1.221 +(*Takes 5 secs*)
   1.222 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.223 +(*Fake*) 
   1.224 +by (spy_analz_tac 1);
   1.225 +qed_spec_mp "analz_image_freshK";
   1.226 +
   1.227 +
   1.228 +goal thy
   1.229 + "!!evs. [| evs : kerberos_ban;  KAB ~: range shrK |] ==>     \
   1.230 +\        Key K : analz (insert (Key KAB) (spies evs)) =       \
   1.231 +\        (K = KAB | Key K : analz (spies evs))";
   1.232 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.233 +qed "analz_insert_freshK";
   1.234 +
   1.235 +
   1.236 +(** The session key K uniquely identifies the message **)
   1.237 +
   1.238 +goal thy 
   1.239 + "!!evs. evs : kerberos_ban ==>                                         \
   1.240 +\      EX A' Ts' B' X'. ALL A Ts B X.                                   \
   1.241 +\       Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   1.242 +\             : set evs \
   1.243 +\       -->         A=A' & Ts=Ts' & B=B' & X=X'";
   1.244 +by (etac kerberos_ban.induct 1);
   1.245 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.246 +by Safe_tac;
   1.247 +(*Kb2: it can't be a new key*)
   1.248 +by (expand_case_tac "K = ?y" 1);
   1.249 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.250 +by (blast_tac (claset() delrules [conjI]) 1);
   1.251 +val lemma = result();
   1.252 +
   1.253 +(*In messages of this form, the session key uniquely identifies the rest*)
   1.254 +goal thy 
   1.255 + "!!evs. [| Says Server A                                    \
   1.256 +\             (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ 
   1.257 +\           Says Server A'                                   \
   1.258 +\            (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\
   1.259 +\           evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
   1.260 +by (prove_unique_tac lemma 1);
   1.261 +qed "unique_session_keys";
   1.262 +
   1.263 +
   1.264 +(** Lemma: the session key sent in msg Kb2 would be EXPIRED
   1.265 +    if the spy could see it!
   1.266 +**)
   1.267 +
   1.268 +goal thy 
   1.269 + "!!evs. [| A ~: bad;  B ~: bad;  evs : kerberos_ban |]               \
   1.270 +\        ==> Says Server A                                            \
   1.271 +\              (Crypt (shrK A) {|Number Ts, Agent B, Key K,           \
   1.272 +\                            Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
   1.273 +\           : set evs -->                                             \
   1.274 +\        Key K : analz (spies evs) --> Expired Ts evs"; 
   1.275 +by (etac kerberos_ban.induct 1);
   1.276 +by analz_spies_tac;
   1.277 +by (ALLGOALS
   1.278 +    (asm_simp_tac (simpset() 
   1.279 +		   addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes @ split_ifs))));
   1.280 +(*Oops*)
   1.281 +by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
   1.282 +(*Kb2*)
   1.283 +by (fast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
   1.284 +(*Fake*) 
   1.285 +by (spy_analz_tac 1);
   1.286 +(**LEVEL 6 **)
   1.287 +by (clarify_tac (claset() delrules [impCE]) 1);
   1.288 +by (case_tac "Ba : bad" 1);
   1.289 +by (blast_tac (claset() addIs [less_SucI]) 2);
   1.290 +(**LEVEL 9**)
   1.291 +by (rotate_tac 10 1);
   1.292 +by (forward_tac [mp] 1 THEN assume_tac 1);
   1.293 +by (etac disjE 1);
   1.294 +by (blast_tac (claset() addIs [less_SucI]) 2);
   1.295 +(**LEVEL 13**)
   1.296 +by (Clarify_tac 1);
   1.297 +by (case_tac "Aa : bad" 1);
   1.298 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj,
   1.299 +                               A_trusts_K_by_Kb2, unique_session_keys]) 2);
   1.300 +(**LEVEL 16**)
   1.301 +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
   1.302 +                               Crypt_Spy_analz_bad RS analz.Snd RS 
   1.303 +                               analz.Snd RS analz.Fst]
   1.304 +                        addIs [less_SucI]) 1);
   1.305 +val lemma = result() RS mp RS mp RSN(1,rev_notE);
   1.306 +
   1.307 +
   1.308 +(** CONFIDENTIALITY for the SERVER:
   1.309 +                     Spy does not see the keys sent in msg Kb2 
   1.310 +                     as long as they have NOT EXPIRED
   1.311 +**)
   1.312 +goal thy 
   1.313 + "!!evs. [| Says Server A                                           \
   1.314 +\            (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs;  \
   1.315 +\           ~ Expired T evs;                                        \
   1.316 +\           A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   1.317 +\        |] ==> Key K ~: analz (spies evs)";
   1.318 +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.319 +by (Clarify_tac 1);
   1.320 +by (rtac ccontr 1);
   1.321 +by (blast_tac (claset() addSEs [lemma]) 1);
   1.322 +qed "Confidentiality_S";
   1.323 +
   1.324 +(**** THE COUNTERPART OF CONFIDENTIALITY 
   1.325 +      [|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs)
   1.326 +      WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
   1.327 +
   1.328 +
   1.329 +(** CONFIDENTIALITY for ALICE: **)
   1.330 +(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
   1.331 +goal thy 
   1.332 +"!!evs. [| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\
   1.333 +\           ~ Expired T evs;          \
   1.334 +\           A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   1.335 +\        |] ==> Key K ~: analz (spies evs)";
   1.336 +by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 
   1.337 +                                Confidentiality_S]) 1);
   1.338 +qed "Confidentiality_A";
   1.339 +
   1.340 +
   1.341 +(** CONFIDENTIALITY for BOB: **)
   1.342 +(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
   1.343 +goal thy
   1.344 +"!!evs. [| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
   1.345 +\            : parts (spies evs);              \
   1.346 +\          ~ Expired Tk evs;          \
   1.347 +\          A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   1.348 +\        |] ==> Key K ~: analz (spies evs)";             
   1.349 +by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
   1.350 +                                Confidentiality_S]) 1);
   1.351 +qed "Confidentiality_B";
   1.352 +
   1.353 +
   1.354 +goal thy
   1.355 + "!!evs. [| B ~: bad;  evs : kerberos_ban |]                        \
   1.356 +\        ==> Key K ~: analz (spies evs) -->                    \
   1.357 +\            Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   1.358 +\            : set evs -->                                             \
   1.359 +\            Crypt K (Number Ta) : parts (spies evs) -->        \
   1.360 +\            Says B A (Crypt K (Number Ta)) : set evs";
   1.361 +by (etac kerberos_ban.induct 1);
   1.362 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.363 +by (dtac Kb3_msg_in_parts_spies 5);
   1.364 +by (forward_tac [Oops_parts_spies] 7);
   1.365 +by (TRYALL (rtac impI));
   1.366 +by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD)));
   1.367 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.368 +(**LEVEL 7**)
   1.369 +by (Blast_tac 1);
   1.370 +by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   1.371 +(*
   1.372 +Subgoal 1: contradiction from the assumptions  
   1.373 +Key K ~: used evs2  and Crypt K (Number Ta) : parts (spies evs2)
   1.374 +*)
   1.375 +by (dtac Crypt_imp_invKey_keysFor 1);
   1.376 +by (Asm_full_simp_tac 1);
   1.377 +(* the two tactics above detectthe contradiction*)
   1.378 +by (rtac disjI1 1);
   1.379 +by (thin_tac "?PP-->?QQ" 1); (*deletes the matching assumptions*)
   1.380 +by (case_tac "Ba : bad" 1);  (*splits up the subgoal by the stated case*)
   1.381 +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 
   1.382 +                              B_trusts_K_by_Kb3, 
   1.383 +			      unique_session_keys]) 2);
   1.384 +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS 
   1.385 +			      Crypt_Spy_analz_bad]) 1);
   1.386 +val lemma_B = result();
   1.387 +
   1.388 +
   1.389 +(*AUTHENTICATION OF B TO A*)
   1.390 +goal thy
   1.391 + "!!evs. [| Crypt K (Number Ta) : parts (spies evs);           \
   1.392 +\           Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
   1.393 +\           : parts (spies evs);                               \
   1.394 +\           ~ Expired Ts evs;                                  \
   1.395 +\           A ~: bad;  B ~: bad;  evs : kerberos_ban |]        \
   1.396 +\        ==> Says B A (Crypt K (Number Ta)) : set evs";
   1.397 +by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
   1.398 +                        addSIs [lemma_B RS mp RS mp RS mp]
   1.399 +                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
   1.400 +qed "Authentication_B";
   1.401 +
   1.402 +
   1.403 +goal thy
   1.404 + "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |]      ==>         \ 
   1.405 +\           Key K ~: analz (spies evs) -->         \
   1.406 +\           Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
   1.407 +\           : set evs -->  \
   1.408 +\            Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\
   1.409 +\           Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
   1.410 +\               : set evs";
   1.411 +by (etac kerberos_ban.induct 1);
   1.412 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.413 +by (forward_tac [Kb3_msg_in_parts_spies] 5);
   1.414 +by (forward_tac [Oops_parts_spies] 7);
   1.415 +by (TRYALL (rtac impI));
   1.416 +by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD)));
   1.417 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.418 +(**LEVEL 7**)
   1.419 +by (Blast_tac 1);
   1.420 +by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   1.421 +by (dtac Crypt_imp_invKey_keysFor 1);
   1.422 +by (Asm_full_simp_tac 1);
   1.423 +by (rtac disjI1 1);
   1.424 +(*Last Subgoal! ...to be refined...*)
   1.425 +by (thin_tac "Says ?A Server ?X : set evs3" 1);
   1.426 +by (dresolve_tac [Says_imp_spies RS parts.Inj] 1);
   1.427 +by (dresolve_tac [Says_imp_spies RS parts.Inj] 1);
   1.428 +by (dtac A_trusts_K_by_Kb2 1);
   1.429 +by (assume_tac 1);
   1.430 +by (assume_tac 1);
   1.431 +by (dtac A_trusts_K_by_Kb2 1);
   1.432 +by (assume_tac 1);
   1.433 +by (assume_tac 1);
   1.434 +by (dtac unique_session_keys 1);
   1.435 +by (assume_tac 1);
   1.436 +by (assume_tac 1);
   1.437 +by (Blast_tac 1);
   1.438 +val lemma_A = result();
   1.439 +
   1.440 +
   1.441 +(*AUTHENTICATION OF A TO B*)
   1.442 +goal thy
   1.443 + "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs);           \
   1.444 +\           Crypt (shrK B) {|Number Ts, Agent A, Key K|}       \
   1.445 +\           : parts (spies evs);                                         \
   1.446 +\           ~ Expired Ts evs;          \
   1.447 +\           A ~: bad;  B ~: bad;  evs : kerberos_ban |]           \
   1.448 +\        ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \       
   1.449 +\                       Crypt K {|Agent A, Number Ta|}|} : set evs";
   1.450 +by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
   1.451 +                        addSIs [lemma_A RS mp RS mp RS mp]
   1.452 +                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
   1.453 +qed "Authentication_A";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Fri Jun 19 10:34:33 1998 +0200
     2.3 @@ -0,0 +1,97 @@
     2.4 +(*  Title:      HOL/Auth/Kerberos_BAN
     2.5 +    ID:         $Id$
     2.6 +    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +The Kerberos protocol, BAN version.
    2.10 +
    2.11 +From page 251 of
    2.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    2.13 +  Proc. Royal Soc. 426 (1989)
    2.14 +*)
    2.15 +
    2.16 +Kerberos_BAN = Shared + 
    2.17 +
    2.18 +(* Temporal modelization: session keys can be leaked 
    2.19 +                          ONLY when they have expired *)
    2.20 +
    2.21 +syntax
    2.22 +    CT :: event list=>nat
    2.23 +    Expired :: [nat, event list] => bool
    2.24 +    RecentAuth :: [nat, event list] => bool
    2.25 +
    2.26 +consts
    2.27 +
    2.28 +    (*Duration of the session key*)
    2.29 +    SesKeyLife   :: nat
    2.30 +
    2.31 +    (*Duration of the authenticator*)
    2.32 +    AutLife :: nat
    2.33 +
    2.34 +rules
    2.35 +    (*The ticket should remain fresh for two journeys on the network at least*)
    2.36 +    SesKeyLife_LB    "2 <= SesKeyLife"
    2.37 +
    2.38 +    (*The authenticator only for one journey*)
    2.39 +    AutLife_LB    "1 <= AutLife"
    2.40 +
    2.41 +translations
    2.42 +   "CT" == "length"
    2.43 +  
    2.44 +   "Expired T evs" == "SesKeyLife + T < CT evs"
    2.45 +
    2.46 +   "RecentAuth T evs" == "CT evs <= AutLife + T"
    2.47 +
    2.48 +consts  kerberos_ban   :: event list set
    2.49 +inductive "kerberos_ban"
    2.50 +  intrs 
    2.51 +
    2.52 +    Nil  "[]: kerberos_ban"
    2.53 +
    2.54 +
    2.55 +    Fake "[| evs: kerberos_ban;  B ~= Spy;  
    2.56 +             X: synth (analz (spies evs)) |]
    2.57 +          ==> Says Spy B X # evs : kerberos_ban"
    2.58 +
    2.59 +
    2.60 +    Kb1  "[| evs1: kerberos_ban;  A ~= Server |]
    2.61 +          ==> Says A Server {|Agent A, Agent B|} # evs1
    2.62 +                :  kerberos_ban"
    2.63 +
    2.64 +
    2.65 +    Kb2  "[| evs2: kerberos_ban;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    2.66 +             Says A' Server {|Agent A, Agent B|} : set evs2 |]
    2.67 +          ==> Says Server A 
    2.68 +                (Crypt (shrK A)
    2.69 +                   {|Number (CT evs2), Agent B, Key KAB,  
    2.70 +                    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
    2.71 +                # evs2 : kerberos_ban"
    2.72 +
    2.73 +
    2.74 +    Kb3  "[| evs3: kerberos_ban;  A ~= B; 
    2.75 +             Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
    2.76 +               : set evs3;
    2.77 +             Says A Server {|Agent A, Agent B|} : set evs3;
    2.78 +             ~ Expired Ts evs3 |]
    2.79 +          ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
    2.80 +               # evs3 : kerberos_ban"
    2.81 +
    2.82 +
    2.83 +    Kb4  "[| evs4: kerberos_ban;  A ~= B;  
    2.84 +             Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
    2.85 +		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    2.86 +             ~ Expired Ts evs4; 
    2.87 +             RecentAuth Ta evs4|]
    2.88 +          ==> Says B A (Crypt K (Number Ta)) # evs4
    2.89 +                : kerberos_ban"
    2.90 +
    2.91 +
    2.92 +(*The session key has EXPIRED when it gets lost *)
    2.93 +    Oops "[| evso: kerberos_ban;  A ~= Spy;
    2.94 +             Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    2.95 +               : set evso;
    2.96 +             Expired Ts evso |]
    2.97 +          ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    2.98 +
    2.99 +
   2.100 +end
     3.1 --- a/src/HOL/Auth/ROOT.ML	Thu Jun 18 18:35:07 1998 +0200
     3.2 +++ b/src/HOL/Auth/ROOT.ML	Fri Jun 19 10:34:33 1998 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4  
     3.5  (*Shared-key protocols*)
     3.6  time_use_thy "NS_Shared";
     3.7 +time_use_thy "Kerberos_BAN";
     3.8  time_use_thy "OtwayRees";
     3.9  time_use_thy "OtwayRees_AN";
    3.10  time_use_thy "OtwayRees_Bad";