src/HOL/Auth/Event.ML
changeset 1933 8b24773de6db
parent 1930 cdf9bcd53749
child 1942 6c9c1a42a869
     1.1 --- a/src/HOL/Auth/Event.ML	Wed Aug 21 11:43:37 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Wed Aug 21 13:22:23 1996 +0200
     1.3 @@ -395,11 +395,10 @@
     1.4  	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
     1.5  	      addss (!simpset)))
     1.6      [2,1];
     1.7 -(*NS4*)
     1.8 -by (step_tac (!claset addSDs [Suc_leD, newK_invKey]) 1);
     1.9 -by (deepen_tac (!claset addIs [impOfSubs keysFor_mono]) 0 2);
    1.10 -by (fast_tac (!claset addDs [Says_imp_old_keys]
    1.11 -	              addss (!simpset addsimps [le_def])) 1);
    1.12 +(*NS4 and NS5: nonce exchange*)
    1.13 +by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
    1.14 +	                          addIs  [less_SucI, impOfSubs keysFor_mono]
    1.15 +		                  addss (!simpset addsimps [le_def])) 0));
    1.16  val lemma = result();
    1.17  
    1.18  goal thy 
    1.19 @@ -561,7 +560,7 @@
    1.20  ****)
    1.21  
    1.22  
    1.23 -(*Not useful in this form, but it says that session keys are not used
    1.24 +(*NOT useful in this form, but it says that session keys are not used
    1.25    to encrypt messages containing other keys, in the actual protocol.
    1.26    We require that agents should behave like this subsequently also.*)
    1.27  goal thy 
    1.28 @@ -576,7 +575,8 @@
    1.29  		      addDs [impOfSubs analz_subset_parts,
    1.30                               impOfSubs parts_insert_subset_Un]
    1.31                        addss (!simpset)) 1);
    1.32 -by (fast_tac (!claset addss (!simpset)) 1);
    1.33 +(*NS4 and NS5*)
    1.34 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.35  result();
    1.36  
    1.37