src/HOL/Auth/OtwayRees.ML
changeset 2064 5a5e508e2a2b
parent 2053 6c0594bfa726
child 2071 0debdc018d26
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Oct 07 10:47:01 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Oct 07 10:55:51 1996 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    Proc. Royal Soc. 426 (1989)
     1.5  *)
     1.6  
     1.7 -
     1.8  open OtwayRees;
     1.9  
    1.10  proof_timing:=true;
    1.11 @@ -89,20 +88,26 @@
    1.12          tac Reveal_parts_sees_Spy 7
    1.13      end;
    1.14  
    1.15 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.16 +fun parts_induct_tac i = SELECT_GOAL
    1.17 +    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    1.18 +	     (*Fake message*)
    1.19 +	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.20 +					   impOfSubs Fake_parts_insert]
    1.21 +                                    addss (!simpset)) 2)) THEN
    1.22 +     (*Base case*)
    1.23 +     fast_tac (!claset addss (!simpset)) 1 THEN
    1.24 +     ALLGOALS Asm_simp_tac) i;
    1.25  
    1.26  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.27      sends messages containing X! **)
    1.28  
    1.29 -(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
    1.30 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.31  goal thy 
    1.32   "!!evs. [| evs : otway lost;  A ~: lost |]    \
    1.33  \        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.34 -by (etac otway.induct 1);
    1.35 -by parts_Fake_tac;
    1.36 +by (parts_induct_tac 1);
    1.37  by (Auto_tac());
    1.38 -(*Deals with Fake message*)
    1.39 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.40 -                             impOfSubs Fake_parts_insert]) 1);
    1.41  qed "Spy_not_see_shrK";
    1.42  
    1.43  bind_thm ("Spy_not_analz_shrK",
    1.44 @@ -139,10 +144,7 @@
    1.45  goal thy "!!evs. evs : otway lost ==> \
    1.46  \                length evs <= length evs' --> \
    1.47  \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    1.48 -by (etac otway.induct 1);
    1.49 -by parts_Fake_tac;
    1.50 -(*auto_tac does not work here, as it performs safe_tac first*)
    1.51 -by (ALLGOALS Asm_simp_tac);
    1.52 +by (parts_induct_tac 1);
    1.53  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.54                                             impOfSubs parts_insert_subset_Un,
    1.55                                             Suc_leD]
    1.56 @@ -214,9 +216,7 @@
    1.57  goal thy "!!evs. evs : otway lost ==> \
    1.58  \                length evs <= length evs' --> \
    1.59  \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    1.60 -by (etac otway.induct 1);
    1.61 -by parts_Fake_tac;
    1.62 -by (ALLGOALS Asm_simp_tac);
    1.63 +by (parts_induct_tac 1);
    1.64  (*OR1 and OR3*)
    1.65  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    1.66  (*Fake, OR2, OR4: these messages send unknown (X) components*)
    1.67 @@ -248,7 +248,43 @@
    1.68  Addsimps [new_keys_not_used, new_keys_not_analzd];
    1.69  
    1.70  
    1.71 -(** Lemmas concerning the form of items passed in messages **)
    1.72 +
    1.73 +(*** Proofs involving analz ***)
    1.74 +
    1.75 +(*Describes the form of Key K when the following message is sent.  The use of
    1.76 +  "parts" strengthens the induction hyp for proving the Fake case.  The
    1.77 +  assumption A ~: lost prevents its being a Faked message.  (Based
    1.78 +  on NS_Shared/Says_S_message_form) *)
    1.79 +goal thy
    1.80 + "!!evs. evs: otway lost ==>                                           \
    1.81 +\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) &   \
    1.82 +\          A ~: lost -->                                               \
    1.83 +\        (EX evt: otway lost. K = newK evt)";
    1.84 +by (parts_induct_tac 1);
    1.85 +by (Auto_tac());
    1.86 +qed_spec_mp "Reveal_message_lemma";
    1.87 +
    1.88 +(*EITHER describes the form of Key K when the following message is sent, 
    1.89 +  OR     reduces it to the Fake case.*)
    1.90 +
    1.91 +goal thy 
    1.92 + "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
    1.93 +\           evs : otway lost |]                      \
    1.94 +\        ==> (EX evt: otway lost. K = newK evt)          \
    1.95 +\          | Key K : analz (sees lost Spy evs)";
    1.96 +br (Reveal_message_lemma RS disjCI) 1;
    1.97 +ba 1;
    1.98 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    1.99 +                      addDs [impOfSubs analz_subset_parts]
   1.100 +                      addss (!simpset)) 1);
   1.101 +qed "Reveal_message_form";
   1.102 +
   1.103 +
   1.104 +(*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.105 +val analz_Fake_tac = 
   1.106 +    dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
   1.107 +    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   1.108 +    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   1.109  
   1.110  
   1.111  (****
   1.112 @@ -283,51 +319,13 @@
   1.113  
   1.114  (** Session keys are not used to encrypt other session keys **)
   1.115  
   1.116 -(*Describes the form of Key K when the following message is sent.  The use of
   1.117 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.118 -  assumptions on A are needed to prevent its being a Faked message.  (Based
   1.119 -  on NS_Shared/Says_S_message_form) *)
   1.120 -goal thy
   1.121 - "!!evs. evs: otway lost ==>                                           \
   1.122 -\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
   1.123 -\          A ~: lost -->                                           \
   1.124 -\        (EX evt: otway lost. K = newK evt)";
   1.125 -by (etac otway.induct 1);
   1.126 -by parts_Fake_tac;
   1.127 -by (ALLGOALS Asm_simp_tac);
   1.128 -(*Deals with Fake message*)
   1.129 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.130 -                             impOfSubs Fake_parts_insert]) 2);
   1.131 -by (Auto_tac());
   1.132 -val lemma = result() RS mp;
   1.133 -
   1.134 -
   1.135 -(*EITHER describes the form of Key K when the following message is sent, 
   1.136 -  OR     reduces it to the Fake case.*)
   1.137 -goal thy 
   1.138 - "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   1.139 -\           evs : otway lost |]                      \
   1.140 -\        ==> (EX evt: otway lost. K = newK evt)          \
   1.141 -\          | Key K : analz (sees lost Spy evs)";
   1.142 -by (excluded_middle_tac "A : lost" 1);
   1.143 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.144 -                      addss (!simpset)) 2);
   1.145 -by (forward_tac [lemma] 1);
   1.146 -by (fast_tac (!claset addEs  partsEs
   1.147 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.148 -by (Fast_tac 1);
   1.149 -qed "Reveal_message_form";
   1.150 -
   1.151 -
   1.152  (*The equality makes the induction hypothesis easier to apply*)
   1.153  goal thy  
   1.154   "!!evs. evs : otway lost ==> \
   1.155  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.156  \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.157  by (etac otway.induct 1);
   1.158 -by (dtac OR2_analz_sees_Spy 4);
   1.159 -by (dtac OR4_analz_sees_Spy 6);
   1.160 -by (dtac Reveal_message_form 7);
   1.161 +by analz_Fake_tac;
   1.162  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.163  by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   1.164  by (ALLGOALS (*Takes 28 secs*)
   1.165 @@ -339,7 +337,7 @@
   1.166  (*Reveal case 2, OR4, OR2, Fake*) 
   1.167  by (EVERY (map spy_analz_tac [7,5,3,2]));
   1.168  (*Reveal case 1, OR3, Base*)
   1.169 -by (Auto_tac());
   1.170 +by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.171  qed_spec_mp "analz_image_newK";
   1.172  
   1.173  
   1.174 @@ -370,9 +368,8 @@
   1.175  (*Remaining cases: OR3 and OR4*)
   1.176  by (ex_strip_tac 2);
   1.177  by (Fast_tac 2);
   1.178 -by (excluded_middle_tac "K = Key(newK evsa)" 1);
   1.179 -by (Asm_simp_tac 1);
   1.180 -by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   1.181 +by (expand_case_tac "K = ?y" 1);
   1.182 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.183  (*...we assume X is a very new message, and handle this case by contradiction*)
   1.184  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.185                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.186 @@ -403,42 +400,27 @@
   1.187  
   1.188  (*Only OR1 can have caused such a part of a message to appear.*)
   1.189  goal thy 
   1.190 - "!!evs. [| A ~: lost;  evs : otway lost |]               \
   1.191 -\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   1.192 -\             : parts (sees lost Spy evs) -->                  \
   1.193 -\            Says A B {|NA, Agent A, Agent B,               \
   1.194 + "!!evs. [| A ~: lost;  evs : otway lost |]                        \
   1.195 +\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)               \
   1.196 +\             : parts (sees lost Spy evs) -->                      \
   1.197 +\            Says A B {|NA, Agent A, Agent B,                      \
   1.198  \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   1.199  \             : set_of_list evs";
   1.200 -by (etac otway.induct 1);
   1.201 -by parts_Fake_tac;
   1.202 -by (ALLGOALS Asm_simp_tac);
   1.203 -(*Fake*)
   1.204 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.205 -                              impOfSubs Fake_parts_insert]) 2);
   1.206 -by (Auto_tac());
   1.207 +by (parts_induct_tac 1);
   1.208  qed_spec_mp "Crypt_imp_OR1";
   1.209  
   1.210  
   1.211 -(** The Nonce NA uniquely identifies A's  message. **)
   1.212 +(** The Nonce NA uniquely identifies A's message. **)
   1.213  
   1.214  goal thy 
   1.215   "!!evs. [| evs : otway lost; A ~: lost |]               \
   1.216  \ ==> EX B'. ALL B.    \
   1.217  \        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
   1.218  \        --> B = B'";
   1.219 -by (etac otway.induct 1);
   1.220 -by parts_Fake_tac;
   1.221 -by (ALLGOALS Asm_simp_tac);
   1.222 -(*Fake*)
   1.223 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.224 -                              impOfSubs Fake_parts_insert]) 2);
   1.225 -(*Base case*)
   1.226 -by (fast_tac (!claset addss (!simpset)) 1);
   1.227 -by (Step_tac 1);
   1.228 +by (parts_induct_tac 1);
   1.229 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.230  (*OR1: creation of new Nonce.  Move assertion into global context*)
   1.231 -by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
   1.232 -by (Asm_simp_tac 1);
   1.233 -by (Fast_tac 1);
   1.234 +by (expand_case_tac "NA = ?y" 1);
   1.235  by (best_tac (!claset addSEs partsEs
   1.236                        addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   1.237  val lemma = result();
   1.238 @@ -497,26 +479,21 @@
   1.239  \                   Crypt {|NA, Key K|} (shrK A),                      \
   1.240  \                   Crypt {|NB, Key K|} (shrK B)|}                     \
   1.241  \                   : set_of_list evs)";
   1.242 -by (etac otway.induct 1);
   1.243 -by parts_Fake_tac;
   1.244 -by (ALLGOALS Asm_simp_tac);
   1.245 -(*Fake*)
   1.246 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.247 -                              impOfSubs Fake_parts_insert]) 1);
   1.248 +by (parts_induct_tac 1);
   1.249  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.250  by (fast_tac (!claset addSIs [parts_insertI]
   1.251                        addSEs partsEs
   1.252                        addEs [Says_imp_old_nonces RS less_irrefl]
   1.253                        addss (!simpset)) 1);
   1.254 -(*OR3 and OR4*)  (** LEVEL 5 **)
   1.255 +(*OR3 and OR4*) 
   1.256  (*OR4*)
   1.257  by (REPEAT (Safe_step_tac 2));
   1.258  by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   1.259  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   1.260                        addEs  partsEs
   1.261                        addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   1.262 -(*OR3*)  (** LEVEL 8 **)
   1.263 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.264 +(*OR3*)  (** LEVEL 5 **)
   1.265 +by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.266  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.267  by (fast_tac (!claset addSEs [MPair_parts]
   1.268                        addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.269 @@ -547,7 +524,7 @@
   1.270  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.271                        addEs  partsEs
   1.272                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.273 -qed "A_can_trust";
   1.274 +qed "A_trust_OR4";
   1.275  
   1.276  
   1.277  (*Describes the form of K and NA when the Server sends this message.*)
   1.278 @@ -577,9 +554,7 @@
   1.279  \            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
   1.280  \            Key K ~: analz (sees lost Spy evs)";
   1.281  by (etac otway.induct 1);
   1.282 -by (dtac OR2_analz_sees_Spy 4);
   1.283 -by (dtac OR4_analz_sees_Spy 6);
   1.284 -by (forward_tac [Reveal_message_form] 7);
   1.285 +by analz_Fake_tac;
   1.286  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.287  by (ALLGOALS
   1.288      (asm_full_simp_tac 
   1.289 @@ -599,7 +574,7 @@
   1.290  by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   1.291  by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   1.292  (*So now we have  Aa ~: lost *)
   1.293 -by (dtac A_can_trust 1);
   1.294 +by (dtac A_trust_OR4 1);
   1.295  by (REPEAT (assume_tac 1));
   1.296  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.297  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.298 @@ -643,13 +618,8 @@
   1.299  \             {|NA, Agent A, Agent B, X',                      \
   1.300  \               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
   1.301  \             : set_of_list evs)";
   1.302 -by (etac otway.induct 1);
   1.303 -by parts_Fake_tac;
   1.304 -by (ALLGOALS Asm_simp_tac);
   1.305 -(*Fake*)
   1.306 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.307 -                              impOfSubs Fake_parts_insert]) 2);
   1.308 -by (Auto_tac());
   1.309 +by (parts_induct_tac 1);
   1.310 +by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   1.311  qed_spec_mp "Crypt_imp_OR2";
   1.312  
   1.313  
   1.314 @@ -657,23 +627,13 @@
   1.315  
   1.316  goal thy 
   1.317   "!!evs. [| evs : otway lost; B ~: lost |]               \
   1.318 -\ ==> EX NA' A'. ALL NA A.                              \
   1.319 +\ ==> EX NA' A'. ALL NA A.                               \
   1.320  \      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
   1.321  \      --> NA = NA' & A = A'";
   1.322 -by (etac otway.induct 1);
   1.323 -by parts_Fake_tac;
   1.324 -by (ALLGOALS Asm_simp_tac);
   1.325 -(*Fake*)
   1.326 -by (best_tac (!claset delrules [conjI,conjE]
   1.327 -		      addSDs [impOfSubs analz_subset_parts,
   1.328 -                              impOfSubs Fake_parts_insert]) 2);
   1.329 -(*Base case*)
   1.330 -by (fast_tac (!claset addss (!simpset)) 1);
   1.331 -by (Step_tac 1);
   1.332 +by (parts_induct_tac 1);
   1.333 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.334  (*OR2: creation of new Nonce.  Move assertion into global context*)
   1.335 -by (excluded_middle_tac "NB = Nonce (newN evsa)" 1);
   1.336 -by (Asm_simp_tac 1);
   1.337 -by (fast_tac (!claset addSIs [exI]) 1);
   1.338 +by (expand_case_tac "NB = ?y" 1);
   1.339  by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   1.340  val lemma = result();
   1.341  
   1.342 @@ -706,12 +666,7 @@
   1.343  \                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
   1.344  \                        Crypt {|NB, Key K|} (shrK B)|}                  \
   1.345  \                   : set_of_list evs)";
   1.346 -by (etac otway.induct 1);
   1.347 -by parts_Fake_tac;
   1.348 -by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   1.349 -(*Fake*)
   1.350 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.351 -                              impOfSubs Fake_parts_insert]) 1);
   1.352 +by (parts_induct_tac 1);
   1.353  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.354  by (fast_tac (!claset addSIs [parts_insertI]
   1.355                        addSEs partsEs
   1.356 @@ -753,10 +708,10 @@
   1.357  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.358                        addEs  partsEs
   1.359                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.360 -qed "B_can_trust";
   1.361 +qed "B_trust_OR3";
   1.362  
   1.363  
   1.364 -B_can_trust RS Spy_not_see_encrypted_key;
   1.365 +B_trust_OR3 RS Spy_not_see_encrypted_key;
   1.366  
   1.367  
   1.368  (** A session key uniquely identifies a pair of senders in the message
   1.369 @@ -769,8 +724,7 @@
   1.370  \         C=A | C=B";
   1.371  by (Simp_tac 1);        (*Miniscoping*)
   1.372  by (etac otway.induct 1);
   1.373 -by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4);
   1.374 -by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6);
   1.375 +by analz_Fake_tac;
   1.376  (*spy_analz_tac just does not work here: it is an entirely different proof!*)
   1.377  by (ALLGOALS 
   1.378      (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   1.379 @@ -778,9 +732,8 @@
   1.380                                        parts_insert2])));
   1.381  by (REPEAT_FIRST (etac exE));
   1.382  (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
   1.383 -by (excluded_middle_tac "K = newK evsa" 4);
   1.384 -by (Asm_simp_tac 4);
   1.385 -by (REPEAT (ares_tac [exI] 4));
   1.386 +by (expand_case_tac "K = ?y" 4);
   1.387 +by (REPEAT (ares_tac [exI] 5));
   1.388  (*...we prove this case by contradiction: the key is too new!*)
   1.389  by (fast_tac (!claset addSEs partsEs
   1.390                        addEs [Says_imp_old_keys RS less_irrefl]