src/HOL/Auth/Recur.ML
changeset 2516 4d68fbe6378b
parent 2485 c4368c967c56
child 2533 2d5604a51562
     1.1 --- a/src/HOL/Auth/Recur.ML	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Recur.ML	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -10,29 +10,26 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 -Pretty.setdepth 25;
     1.8 +Pretty.setdepth 30;
     1.9  
    1.10  
    1.11  (** Possibility properties: traces that reach the end 
    1.12 -	ONE theorem would be more elegant and faster!
    1.13 -	By induction on a list of agents (no repetitions)
    1.14 +        ONE theorem would be more elegant and faster!
    1.15 +        By induction on a list of agents (no repetitions)
    1.16  **)
    1.17  
    1.18 +
    1.19  (*Simplest case: Alice goes directly to the server*)
    1.20  goal thy
    1.21   "!!A. A ~= Server   \
    1.22  \ ==> EX K NA. EX evs: recur lost.          \
    1.23 -\     Says Server A {|Agent A,              \
    1.24 -\                     Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
    1.25 +\     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
    1.26  \                       Agent Server|}      \
    1.27  \         : set_of_list evs";
    1.28  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.29  by (rtac (recur.Nil RS recur.RA1 RS 
    1.30 -	  (respond.One RSN (4,recur.RA3))) 2);
    1.31 -by (REPEAT
    1.32 -    (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
    1.33 -     THEN
    1.34 -     REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
    1.35 +          (respond.One RSN (4,recur.RA3))) 2);
    1.36 +by possibility_tac;
    1.37  result();
    1.38  
    1.39  
    1.40 @@ -40,44 +37,42 @@
    1.41  goal thy
    1.42   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.43  \ ==> EX K. EX NA. EX evs: recur lost.          \
    1.44 -\       Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    1.45 +\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    1.46  \                       Agent Server|}                          \
    1.47  \         : set_of_list evs";
    1.48 +by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
    1.49 +by (REPEAT (eresolve_tac [exE, conjE] 1));
    1.50  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.51  by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
    1.52 -	  (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
    1.53 -	  recur.RA4) 2);
    1.54 -bw HPair_def;
    1.55 -by (REPEAT
    1.56 -    (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
    1.57 -     THEN
    1.58 -     ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
    1.59 +          (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
    1.60 +          recur.RA4) 2);
    1.61 +by basic_possibility_tac;
    1.62 +by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
    1.63 +			       less_not_refl2 RS not_sym] 1));
    1.64  result();
    1.65  
    1.66  
    1.67 -(*Case three: Alice, Bob, Charlie and the server*)
    1.68 +(*Case three: Alice, Bob, Charlie and the server
    1.69  goal thy
    1.70 - "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.71 + "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
    1.72  \ ==> EX K. EX NA. EX evs: recur lost.          \
    1.73 -\       Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    1.74 +\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    1.75  \                       Agent Server|}                          \
    1.76  \         : set_of_list evs";
    1.77 +by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
    1.78 +by (REPEAT (eresolve_tac [exE, conjE] 1));
    1.79  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.80  by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
    1.81 -	  (respond.One RS respond.Cons RS respond.Cons RSN
    1.82 -	   (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
    1.83 -bw HPair_def;
    1.84 -by (REPEAT	(*SLOW: 37 seconds*)
    1.85 -    (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
    1.86 -     THEN
    1.87 -     ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
    1.88 -by (ALLGOALS 
    1.89 -    (SELECT_GOAL (DEPTH_SOLVE
    1.90 -		  (swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND 
    1.91 -		   etac not_sym 1))));
    1.92 +          (respond.One RS respond.Cons RS respond.Cons RSN
    1.93 +           (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
    1.94 +(*SLOW: 70 seconds*)
    1.95 +by basic_possibility_tac;
    1.96 +by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
    1.97 +		 ORELSE
    1.98 +		 eresolve_tac [asm_rl, less_not_refl2, 
    1.99 +			       less_not_refl2 RS not_sym] 1));
   1.100  result();
   1.101 -
   1.102 -
   1.103 +****************)
   1.104  
   1.105  (**** Inductive proofs about recur ****)
   1.106  
   1.107 @@ -99,10 +94,30 @@
   1.108  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   1.109  
   1.110  
   1.111 +
   1.112 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
   1.113 +by (etac respond.induct 1);
   1.114 +by (ALLGOALS Simp_tac);
   1.115 +qed "respond_Key_in_parts";
   1.116 +
   1.117 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
   1.118 +by (etac respond.induct 1);
   1.119 +by (REPEAT (assume_tac 1));
   1.120 +qed "respond_imp_not_used";
   1.121 +
   1.122 +goal thy
   1.123 + "!!evs. [| Key K : parts {RB};  (PB,RB,K') : respond evs |] \
   1.124 +\        ==> Key K ~: used evs";
   1.125 +by (etac rev_mp 1);
   1.126 +by (etac respond.induct 1);
   1.127 +by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
   1.128 +             !simpset));
   1.129 +qed_spec_mp "Key_in_parts_respond";
   1.130 +
   1.131  (*Simple inductive reasoning about responses*)
   1.132 -goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i";
   1.133 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
   1.134  by (etac respond.induct 1);
   1.135 -by (REPEAT (ares_tac responses.intrs 1));
   1.136 +by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
   1.137  qed "respond_imp_responses";
   1.138  
   1.139  
   1.140 @@ -110,7 +125,7 @@
   1.141  
   1.142  val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
   1.143  
   1.144 -goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
   1.145 +goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \
   1.146  \                ==> RA : analz (sees lost Spy evs)";
   1.147  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   1.148  qed "RA4_analz_sees_Spy";
   1.149 @@ -131,8 +146,8 @@
   1.150      let val tac = forw_inst_tac [("lost","lost")] 
   1.151      in  tac RA2_parts_sees_Spy 4              THEN
   1.152          etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
   1.153 -	forward_tac [respond_imp_responses] 5 THEN
   1.154 -	tac RA4_parts_sees_Spy 6
   1.155 +        forward_tac [respond_imp_responses] 5 THEN
   1.156 +        tac RA4_parts_sees_Spy 6
   1.157      end;
   1.158  
   1.159  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   1.160 @@ -153,14 +168,6 @@
   1.161  (** Spy never sees another agent's long-term key (unless initially lost) **)
   1.162  
   1.163  goal thy 
   1.164 - "!!evs. (j,PB,RB) : respond i \
   1.165 -\  ==> Key K : parts {RB} --> (EX j'. K = newK2(i,j') & j<=j')";
   1.166 -be respond.induct 1;
   1.167 -by (Auto_tac());
   1.168 -by (best_tac (!claset addDs [Suc_leD]) 1);
   1.169 -qed_spec_mp "Key_in_parts_respond";
   1.170 -
   1.171 -goal thy 
   1.172   "!!evs. evs : recur lost \
   1.173  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   1.174  by (parts_induct_tac 1);
   1.175 @@ -189,115 +196,30 @@
   1.176  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   1.177  
   1.178  
   1.179 -(*** Future keys can't be seen or used! ***)
   1.180 +
   1.181 +(** Nobody can have used non-existent keys! **)
   1.182  
   1.183 -(*Nobody can have SEEN keys that will be generated in the future. *)
   1.184 -goal thy "!!evs. evs : recur lost ==> \
   1.185 -\                length evs <= i -->   \
   1.186 -\                Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
   1.187 -by (parts_induct_tac 1);
   1.188 -(*RA2*)
   1.189 -by (best_tac (!claset addSEs partsEs 
   1.190 -	              addSDs [parts_cut]
   1.191 -                      addDs  [Suc_leD]
   1.192 -                      addss  (!simpset)) 3);
   1.193 -(*Fake*)
   1.194 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.195 -			     impOfSubs parts_insert_subset_Un,
   1.196 -			     Suc_leD]
   1.197 -		      addss (!simpset)) 1);
   1.198 -(*For RA3*)
   1.199 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
   1.200 -(*RA1-RA4*)
   1.201 -by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
   1.202 -		              addss (!simpset)) 1));
   1.203 -qed_spec_mp "new_keys_not_seen";
   1.204 -Addsimps [new_keys_not_seen];
   1.205 -
   1.206 -(*Variant: old messages must contain old keys!*)
   1.207 -goal thy 
   1.208 - "!!evs. [| Says A B X : set_of_list evs;     \
   1.209 -\           Key (newK2(i,j)) : parts {X};     \
   1.210 -\           evs : recur lost                 \
   1.211 -\        |] ==> i < length evs";
   1.212 -by (rtac ccontr 1);
   1.213 -by (dtac leI 1);
   1.214 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   1.215 -                      addIs  [impOfSubs parts_mono]) 1);
   1.216 -qed "Says_imp_old_keys";
   1.217 -
   1.218 -
   1.219 -(*** Future nonces can't be seen or used! ***)
   1.220 -
   1.221 -goal thy 
   1.222 - "!!evs. (j, PB, RB) : respond i \
   1.223 -\        ==> Nonce N : parts {RB} --> Nonce N : parts {PB}";
   1.224 -be respond.induct 1;
   1.225 +goal thy
   1.226 + "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
   1.227 +\        ==> K : range shrK";
   1.228 +by (etac rev_mp 1);
   1.229 +by (etac (respond_imp_responses RS responses.induct) 1);
   1.230  by (Auto_tac());
   1.231 -qed_spec_mp "Nonce_in_parts_respond";
   1.232 +qed_spec_mp "Key_in_keysFor_parts";
   1.233  
   1.234  
   1.235 -goal thy "!!i. evs : recur lost ==> \
   1.236 -\              length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
   1.237 -by (parts_induct_tac 1);
   1.238 -(*For RA3*)
   1.239 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
   1.240 -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.241 -                        addDs  [Nonce_in_parts_respond, parts_cut, Suc_leD]
   1.242 -			addss (!simpset)) 0 4);
   1.243 -(*Fake*)
   1.244 -by (fast_tac (!claset addDs  [impOfSubs analz_subset_parts,
   1.245 -			      impOfSubs parts_insert_subset_Un,
   1.246 -			      Suc_leD]
   1.247 -		      addss (!simpset)) 1);
   1.248 -(*RA1, RA2, RA4*)
   1.249 -by (REPEAT_FIRST  (fast_tac (!claset 
   1.250 -                              addSEs partsEs
   1.251 -                              addEs [leD RS notE]
   1.252 -                              addDs [Suc_leD]
   1.253 -                              addss (!simpset))));
   1.254 -qed_spec_mp "new_nonces_not_seen";
   1.255 -Addsimps [new_nonces_not_seen];
   1.256 -
   1.257 -(*Variant: old messages must contain old nonces!*)
   1.258 -goal thy "!!evs. [| Says A B X : set_of_list evs;    \
   1.259 -\                   Nonce (newN i) : parts {X};      \
   1.260 -\                   evs : recur lost                 \
   1.261 -\                |] ==> i < length evs";
   1.262 -by (rtac ccontr 1);
   1.263 -by (dtac leI 1);
   1.264 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   1.265 -                      addIs  [impOfSubs parts_mono]) 1);
   1.266 -qed "Says_imp_old_nonces";
   1.267 -
   1.268 -
   1.269 -(** Nobody can have USED keys that will be generated in the future. **)
   1.270 -
   1.271 -goal thy
   1.272 - "!!evs. (j,PB,RB) : respond i \
   1.273 -\        ==> K : keysFor (parts {RB}) --> (EX A. K = shrK A)";
   1.274 -be (respond_imp_responses RS responses.induct) 1;
   1.275 -by (Auto_tac());
   1.276 -qed_spec_mp "Key_in_keysFor_parts_respond";
   1.277 -
   1.278 -
   1.279 -goal thy "!!i. evs : recur lost ==>          \
   1.280 -\       length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
   1.281 +goal thy "!!evs. evs : recur lost ==>          \
   1.282 +\       Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   1.283  by (parts_induct_tac 1);
   1.284  (*RA3*)
   1.285 -by (fast_tac (!claset addDs  [Key_in_keysFor_parts_respond, Suc_leD]
   1.286 -		      addss  (!simpset addsimps [parts_insert_sees])) 4);
   1.287 -(*RA2*)
   1.288 -by (fast_tac (!claset addSEs partsEs 
   1.289 -	              addDs  [Suc_leD] addss (!simpset)) 3);
   1.290 -(*Fake, RA1, RA4*)
   1.291 -by (REPEAT 
   1.292 -    (best_tac
   1.293 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.294 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.295 -                      Suc_leD]
   1.296 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.297 -               addss (!simpset)) 1));
   1.298 +by (best_tac (!claset addDs  [Key_in_keysFor_parts]
   1.299 +                      addss  (!simpset addsimps [parts_insert_sees])) 2);
   1.300 +(*Fake*)
   1.301 +by (best_tac
   1.302 +      (!claset addIs [impOfSubs analz_subset_parts]
   1.303 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.304 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   1.305 +               addss (!simpset)) 1);
   1.306  qed_spec_mp "new_keys_not_used";
   1.307  
   1.308  
   1.309 @@ -319,86 +241,82 @@
   1.310      dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
   1.311  
   1.312  
   1.313 -Delsimps [image_insert];
   1.314 -
   1.315  (** Session keys are not used to encrypt other session keys **)
   1.316  
   1.317  (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
   1.318    Note that it holds for *any* set H (not just "sees lost Spy evs")
   1.319    satisfying the inductive hypothesis.*)
   1.320  goal thy  
   1.321 - "!!evs. [| RB : responses i;                             \
   1.322 -\           ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
   1.323 -\           (K : newK``I | Key K : analz H) |]                \
   1.324 -\       ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \
   1.325 -\           (K : newK``I | Key K : analz (insert RB H))";
   1.326 -be responses.induct 1;
   1.327 -by (ALLGOALS
   1.328 -    (asm_simp_tac 
   1.329 -     (!simpset addsimps [insert_Key_singleton, insert_Key_image, 
   1.330 -			 Un_assoc RS sym, pushKey_newK]
   1.331 -               setloop split_tac [expand_if])));
   1.332 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.333 -qed "resp_analz_image_newK_lemma";
   1.334 + "!!evs. [| RB : responses evs;                             \
   1.335 +\           ALL K KK. KK <= Compl (range shrK) -->          \
   1.336 +\                     (Key K : analz (Key``KK Un H)) =      \
   1.337 +\                     (K : KK | Key K : analz H) |]         \
   1.338 +\       ==> ALL K KK. KK <= Compl (range shrK) -->          \
   1.339 +\                     (Key K : analz (insert RB (Key``KK Un H))) = \
   1.340 +\                     (K : KK | Key K : analz (insert RB H))";
   1.341 +by (etac responses.induct 1);
   1.342 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.343 +qed "resp_analz_image_freshK_lemma";
   1.344  
   1.345  (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
   1.346  goal thy  
   1.347 - "!!evs. evs : recur lost ==>                                            \
   1.348 -\  ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
   1.349 -\           (K : newK``I | Key K : analz (sees lost Spy evs))";
   1.350 + "!!evs. evs : recur lost ==>                                   \
   1.351 +\  ALL K KK. KK <= Compl (range shrK) -->                       \
   1.352 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   1.353 +\            (K : KK | Key K : analz (sees lost Spy evs))";
   1.354  by (etac recur.induct 1);
   1.355  by analz_Fake_tac;
   1.356 -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.357 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
   1.358 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.359 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   1.360 +by (ALLGOALS 
   1.361 +    (asm_simp_tac
   1.362 +     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
   1.363  (*Base*)
   1.364  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.365  (*RA4, RA2, Fake*) 
   1.366  by (REPEAT (spy_analz_tac 1));
   1.367 -val raw_analz_image_newK = result();
   1.368 -qed_spec_mp "analz_image_newK";
   1.369 +val raw_analz_image_freshK = result();
   1.370 +qed_spec_mp "analz_image_freshK";
   1.371  
   1.372  
   1.373  (*Instance of the lemma with H replaced by (sees lost Spy evs):
   1.374 -   [| RB : responses i;  evs : recur lost |]
   1.375 -   ==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) =
   1.376 -       (xa : newK``x | Key xa : analz (insert RB (sees lost Spy evs))) 
   1.377 +   [| RB : responses evs;  evs : recur lost; |]
   1.378 +   ==> KK <= Compl (range shrK) --> 
   1.379 +       Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
   1.380 +       (K : KK | Key K : analz (insert RB (sees lost Spy evs))) 
   1.381  *)
   1.382 -bind_thm ("resp_analz_image_newK",
   1.383 -	  raw_analz_image_newK RSN
   1.384 -	    (2, resp_analz_image_newK_lemma) RS spec RS spec);
   1.385 +bind_thm ("resp_analz_image_freshK",
   1.386 +          raw_analz_image_freshK RSN
   1.387 +            (2, resp_analz_image_freshK_lemma) RS spec RS spec);
   1.388  
   1.389  goal thy
   1.390 - "!!evs. evs : recur lost ==>                               \
   1.391 -\        Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \
   1.392 -\        (K = newK x | Key K : analz (sees lost Spy evs))";
   1.393 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.394 -                                   insert_Key_singleton]) 1);
   1.395 -by (Fast_tac 1);
   1.396 -qed "analz_insert_Key_newK";
   1.397 + "!!evs. [| evs : recur lost;  KAB ~: range shrK |] ==>              \
   1.398 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =      \
   1.399 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
   1.400 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.401 +qed "analz_insert_freshK";
   1.402  
   1.403  
   1.404 -(*This is more general than proving Hash_new_nonces_not_seen: we don't prove
   1.405 -  that "future nonces" can't be hashed, but that everything that's hashed is
   1.406 -  already in past traffic. *)
   1.407 +(*Everything that's hashed is already in past traffic. *)
   1.408  goal thy "!!i. [| evs : recur lost;  A ~: lost |] ==>              \
   1.409  \              Hash {|Key(shrK A), X|} : parts (sees lost Spy evs) -->  \
   1.410  \              X : parts (sees lost Spy evs)";
   1.411 -be recur.induct 1;
   1.412 +by (etac recur.induct 1);
   1.413  by parts_Fake_tac;
   1.414  (*RA3 requires a further induction*)
   1.415 -be responses.induct 5;
   1.416 +by (etac responses.induct 5);
   1.417  by (ALLGOALS Asm_simp_tac);
   1.418  (*Fake*)
   1.419  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.420 -			     impOfSubs Fake_parts_insert]
   1.421 -	              addss (!simpset addsimps [parts_insert_sees])) 2);
   1.422 +                             impOfSubs Fake_parts_insert]
   1.423 +                      addss (!simpset addsimps [parts_insert_sees])) 2);
   1.424  (*Two others*)
   1.425  by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
   1.426  bind_thm ("Hash_imp_body", result() RSN (2, rev_mp));
   1.427  
   1.428  
   1.429  (** The Nonce NA uniquely identifies A's message. 
   1.430 -    This theorem applies to rounds RA1 and RA2!
   1.431 +    This theorem applies to steps RA1 and RA2!
   1.432  
   1.433    Unicity is not used in other proofs but is desirable in its own right.
   1.434  **)
   1.435 @@ -409,29 +327,20 @@
   1.436  \        Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
   1.437  \          : parts (sees lost Spy evs)  -->  B=B' & P=P'";
   1.438  by (parts_induct_tac 1);
   1.439 -be responses.induct 3;
   1.440 +by (etac responses.induct 3);
   1.441  by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
   1.442  by (step_tac (!claset addSEs partsEs) 1);
   1.443 -(*RA1: creation of new Nonce.  Move assertion into global context*)
   1.444 -by (expand_case_tac "NA = ?y" 1);
   1.445 -by (best_tac (!claset addSIs [exI]
   1.446 -                      addSDs [Hash_imp_body]
   1.447 -		      addSEs (new_nonces_not_seen::partsEs)
   1.448 -		      addss (!simpset)) 1);
   1.449 -by (best_tac (!claset addss  (!simpset)) 1);
   1.450 -(*RA2: creation of new Nonce*)
   1.451 -by (expand_case_tac "NA = ?y" 1);
   1.452 -by (best_tac (!claset addSIs [exI]
   1.453 -		      addSDs [Hash_imp_body]
   1.454 -		      addSEs (new_nonces_not_seen::partsEs)
   1.455 -		      addss  (!simpset)) 1);
   1.456 -by (best_tac (!claset addss  (!simpset)) 1);
   1.457 +(*RA1,2: creation of new Nonce.  Move assertion into global context*)
   1.458 +by (ALLGOALS (expand_case_tac "NA = ?y"));
   1.459 +by (REPEAT_FIRST (ares_tac [exI]));
   1.460 +by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
   1.461 +                              addSEs sees_Spy_partsEs) 1));
   1.462  val lemma = result();
   1.463  
   1.464  goalw thy [HPair_def]
   1.465 - "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|}   \
   1.466 + "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}   \
   1.467  \            : parts (sees lost Spy evs);                          \
   1.468 -\          HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
   1.469 +\          Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \
   1.470  \            : parts (sees lost Spy evs);                          \
   1.471  \          evs : recur lost;  A ~: lost |]                         \
   1.472  \        ==> B=B' & P=P'";
   1.473 @@ -445,39 +354,36 @@
   1.474  ***)
   1.475  
   1.476  goal thy
   1.477 - "!!evs. [| RB : responses i;  evs : recur lost |] \
   1.478 + "!!evs. [| RB : responses evs;  evs : recur lost |] \
   1.479  \ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
   1.480 -be responses.induct 1;
   1.481 +by (etac responses.induct 1);
   1.482  by (ALLGOALS
   1.483      (asm_simp_tac 
   1.484 -     (!simpset addsimps [resp_analz_image_newK, insert_Key_singleton]
   1.485 -               setloop split_tac [expand_if])));
   1.486 +     (analz_image_freshK_ss addsimps [Spy_analz_shrK,
   1.487 +                                      resp_analz_image_freshK])));
   1.488  qed "shrK_in_analz_respond";
   1.489  Addsimps [shrK_in_analz_respond];
   1.490  
   1.491  
   1.492  goal thy  
   1.493 - "!!evs. [| RB : responses i;                             \
   1.494 -\           ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
   1.495 -\           (K : newK``I | Key K : analz H) |]                \
   1.496 + "!!evs. [| RB : responses evs;                             \
   1.497 +\           ALL K KK. KK <= Compl (range shrK) -->          \
   1.498 +\                     (Key K : analz (Key``KK Un H)) =      \
   1.499 +\                     (K : KK | Key K : analz H) |]         \
   1.500  \       ==> (Key K : analz (insert RB H)) --> \
   1.501 -\                  (Key K : parts{RB} | Key K : analz H)";
   1.502 -be responses.induct 1;
   1.503 +\           (Key K : parts{RB} | Key K : analz H)";
   1.504 +by (etac responses.induct 1);
   1.505  by (ALLGOALS
   1.506      (asm_simp_tac 
   1.507 -     (!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert,
   1.508 -			 resp_analz_image_newK_lemma,
   1.509 -			 insert_Key_singleton, insert_Key_image, 
   1.510 -			 Un_assoc RS sym, pushKey_newK]
   1.511 -               setloop split_tac [expand_if])));
   1.512 -(*The "Message" simpset gives the standard treatment of "image"*)
   1.513 -by (simp_tac (simpset_of "Message") 1);
   1.514 +     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
   1.515 +(*Simplification using two distinct treatments of "image"*)
   1.516 +by (simp_tac (!simpset addsimps [parts_insert2]) 1);
   1.517  by (fast_tac (!claset delrules [allE]) 1);
   1.518  qed "resp_analz_insert_lemma";
   1.519  
   1.520  bind_thm ("resp_analz_insert",
   1.521 -	  raw_analz_image_newK RSN
   1.522 -	    (2, resp_analz_insert_lemma) RSN(2, rev_mp));
   1.523 +          raw_analz_image_freshK RSN
   1.524 +            (2, resp_analz_insert_lemma) RSN(2, rev_mp));
   1.525  
   1.526  
   1.527  (*The Server does not send such messages.  This theorem lets us avoid
   1.528 @@ -487,44 +393,51 @@
   1.529  \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
   1.530  \                  ~: set_of_list evs";
   1.531  by (etac recur.induct 1);
   1.532 -be (respond.induct) 5;
   1.533 +by (etac (respond.induct) 5);
   1.534  by (Auto_tac());
   1.535  qed_spec_mp "Says_Server_not";
   1.536  AddSEs [Says_Server_not RSN (2,rev_notE)];
   1.537  
   1.538  
   1.539 +(*The last key returned by respond indeed appears in a certificate*)
   1.540  goal thy 
   1.541 - "!!i. (j,PB,RB) : respond i               \
   1.542 -\  ==> EX A' B'. ALL A B N.                \
   1.543 + "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
   1.544 +\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
   1.545 +by (etac respond.elim 1);
   1.546 +by (ALLGOALS Asm_full_simp_tac);
   1.547 +qed "respond_certificate";
   1.548 +
   1.549 +
   1.550 +goal thy 
   1.551 + "!!K'. (PB,RB,KXY) : respond evs               \
   1.552 +\  ==> EX A' B'. ALL A B N.              \
   1.553  \        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
   1.554  \          -->   (A'=A & B'=B) | (A'=B & B'=A)";
   1.555 -be respond.induct 1;
   1.556 +by (etac respond.induct 1);
   1.557  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
   1.558  (*Base case*)
   1.559  by (Fast_tac 1);
   1.560  by (Step_tac 1);
   1.561 +(*Case analysis on K=KBC*)
   1.562  by (expand_case_tac "K = ?y" 1);
   1.563 +by (dtac respond_Key_in_parts 1);
   1.564  by (best_tac (!claset addSIs [exI]
   1.565                        addSEs partsEs
   1.566 -                      addDs [Key_in_parts_respond]
   1.567 -                      addss (!simpset)) 1);
   1.568 +                      addDs [Key_in_parts_respond]) 1);
   1.569 +(*Case analysis on K=KAB*)
   1.570  by (expand_case_tac "K = ?y" 1);
   1.571  by (REPEAT (ares_tac [exI] 2));
   1.572  by (ex_strip_tac 1);
   1.573 -be respond.elim 1;
   1.574 -by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac));
   1.575 -by (ALLGOALS (asm_full_simp_tac 
   1.576 -	      (!simpset addsimps [all_conj_distrib, ex_disj_distrib]))); 
   1.577 -by (Fast_tac 1);
   1.578 +by (dtac respond_certificate 1);
   1.579  by (Fast_tac 1);
   1.580  val lemma = result();
   1.581  
   1.582  goal thy 
   1.583   "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};    \
   1.584  \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
   1.585 -\          (j,PB,RB) : respond i |]               \
   1.586 +\          (PB,RB,KXY) : respond evs |]               \
   1.587  \ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
   1.588 -by (prove_unique_tac lemma 1);	(*50 seconds??, due to the disjunctions*)
   1.589 +by (prove_unique_tac lemma 1);  (*50 seconds??, due to the disjunctions*)
   1.590  qed "unique_session_keys";
   1.591  
   1.592  
   1.593 @@ -533,47 +446,34 @@
   1.594      the premises, e.g. by having A=Spy **)
   1.595  
   1.596  goal thy 
   1.597 - "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
   1.598 -\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
   1.599 -be respond.elim 1;
   1.600 -by (ALLGOALS Asm_full_simp_tac);
   1.601 -qed "newK2_respond_lemma";
   1.602 -
   1.603 -
   1.604 -goal thy 
   1.605 - "!!evs. [| (j,PB,RB) : respond (length evs);  evs : recur lost |]       \
   1.606 + "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur lost |]       \
   1.607  \        ==> ALL A A' N. A ~: lost & A' ~: lost -->  \
   1.608  \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
   1.609  \            Key K ~: analz (insert RB (sees lost Spy evs))";
   1.610 -be respond.induct 1;
   1.611 +by (etac respond.induct 1);
   1.612  by (forward_tac [respond_imp_responses] 2);
   1.613 -by (ALLGOALS (*4 MINUTES???*)
   1.614 +by (forward_tac [respond_imp_not_used] 2);
   1.615 +by (ALLGOALS (*43 seconds*)
   1.616      (asm_simp_tac 
   1.617 -     (!simpset addsimps 
   1.618 -	  ([analz_image_newK, not_parts_not_analz,
   1.619 -	    read_instantiate [("H", "?ff``?xx")] parts_insert,
   1.620 -	    Un_assoc RS sym, resp_analz_image_newK,
   1.621 -	    insert_Key_singleton, analz_insert_Key_newK])
   1.622 -      setloop split_tac [expand_if])));
   1.623 -by (ALLGOALS (simp_tac (simpset_of "Message")));
   1.624 -by (Fast_tac 1);
   1.625 +     (analz_image_freshK_ss addsimps 
   1.626 +          [analz_image_freshK, not_parts_not_analz,
   1.627 +           shrK_in_analz_respond,
   1.628 +           read_instantiate [("H", "?ff``?xx")] parts_insert,
   1.629 +           resp_analz_image_freshK, analz_insert_freshK])));
   1.630 +by (ALLGOALS Simp_tac);
   1.631 +by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
   1.632  by (step_tac (!claset addSEs [MPair_parts]) 1);
   1.633 -(** LEVEL 6 **)
   1.634 -by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond]
   1.635 -                      addSEs [new_keys_not_seen RS not_parts_not_analz 
   1.636 -			      RSN(2,rev_notE)]
   1.637 -                      addss (!simpset)) 4);
   1.638 -by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3);
   1.639 +(** LEVEL 7 **)
   1.640 +by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
   1.641 +                      addDs  [impOfSubs analz_subset_parts]) 4);
   1.642 +by (fast_tac (!claset addSDs [respond_certificate]) 3);
   1.643  by (best_tac (!claset addSEs partsEs
   1.644                        addDs [Key_in_parts_respond]
   1.645                        addss (!simpset)) 2);
   1.646 -by (thin_tac "ALL x.?P(x)" 1);
   1.647 -be respond.elim 1;
   1.648 -by (fast_tac (!claset addss (!simpset)) 1);
   1.649 -by (step_tac (!claset addss (!simpset)) 1);
   1.650 -by (best_tac (!claset addSEs partsEs
   1.651 -                      addDs [Key_in_parts_respond]
   1.652 -                      addss (!simpset)) 1);
   1.653 +by (dtac unique_session_keys 1);
   1.654 +by (etac respond_certificate 1);
   1.655 +by (assume_tac 1);
   1.656 +by (Fast_tac 1);
   1.657  qed_spec_mp "respond_Spy_not_see_encrypted_key";
   1.658  
   1.659  
   1.660 @@ -586,7 +486,7 @@
   1.661  by analz_Fake_tac;
   1.662  by (ALLGOALS
   1.663      (asm_simp_tac
   1.664 -     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] 
   1.665 +     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] 
   1.666                 setloop split_tac [expand_if])));
   1.667  (*RA4*)
   1.668  by (spy_analz_tac 4);
   1.669 @@ -596,13 +496,14 @@
   1.670  (*RA2*)
   1.671  by (spy_analz_tac 1);
   1.672  (*RA3, case 2: K is an old key*)
   1.673 -by (fast_tac (!claset addSDs [resp_analz_insert]
   1.674 -		      addSEs partsEs
   1.675 -                      addDs [Key_in_parts_respond]
   1.676 -	              addEs [Says_imp_old_keys RS less_irrefl]) 2);
   1.677 +by (best_tac (!claset addSDs [resp_analz_insert]
   1.678 +                      addSEs partsEs
   1.679 +                      addDs [Key_in_parts_respond, 
   1.680 +                             Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)]
   1.681 +                      addss (!simpset)) 2);
   1.682  (*RA3, case 1: use lemma previously proved by induction*)
   1.683  by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
   1.684 -			      (2,rev_notE)]) 1);
   1.685 +                              (2,rev_notE)]) 1);
   1.686  bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
   1.687  
   1.688  
   1.689 @@ -622,34 +523,29 @@
   1.690  (**** Authenticity properties for Agents ****)
   1.691  
   1.692  (*The response never contains Hashes*)
   1.693 -(*NEEDED????????????????*)
   1.694  goal thy
   1.695 - "!!evs. (j,PB,RB) : respond i \
   1.696 + "!!evs. (PB,RB,K) : respond evs \
   1.697  \        ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
   1.698  \            Hash {|Key (shrK B), M|} : parts H";
   1.699 -be (respond_imp_responses RS responses.induct) 1;
   1.700 +by (etac (respond_imp_responses RS responses.induct) 1);
   1.701  by (Auto_tac());
   1.702  bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
   1.703  
   1.704 -(*NEEDED????????????????*)
   1.705  (*Only RA1 or RA2 can have caused such a part of a message to appear.*)
   1.706  goalw thy [HPair_def]
   1.707   "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
   1.708  \             : parts (sees lost Spy evs);                        \
   1.709  \            A ~: lost;  evs : recur lost |]                        \
   1.710 -\        ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|})  \
   1.711 +\        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
   1.712  \             : set_of_list evs";
   1.713 -be rev_mp 1;
   1.714 +by (etac rev_mp 1);
   1.715  by (parts_induct_tac 1);
   1.716  (*RA3*)
   1.717  by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
   1.718  qed_spec_mp "Hash_auth_sender";
   1.719  
   1.720  
   1.721 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   1.722 -
   1.723 -
   1.724 -(** These two results should subsume (for all agents) the guarantees proved
   1.725 +(** These two results subsume (for all agents) the guarantees proved
   1.726      separately for A and B in the Otway-Rees protocol.
   1.727  **)
   1.728