Now with Andy Gordon's treatment of freshness to replace newN/K
authorpaulson
Fri Jan 17 12:49:31 1997 +0100 (1997-01-17)
changeset 25164d68fbe6378b
parent 2515 6ff9bd353121
child 2517 2af078382853
Now with Andy Gordon's treatment of freshness to replace newN/K
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -18,16 +18,6 @@
     1.4      Simp_tac i;
     1.5  
     1.6  
     1.7 -
     1.8 -(*GOALS.ML??*)
     1.9 -fun prlim n = (goals_limit:=n; pr());
    1.10 -
    1.11 -(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    1.12 -goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    1.13 -by (fast_tac (!claset addEs [equalityE]) 1);
    1.14 -val subset_range_iff = result();
    1.15 -
    1.16 -
    1.17  open Message;
    1.18  
    1.19  AddIffs (msg.inject);
    1.20 @@ -44,49 +34,6 @@
    1.21  Addsimps [invKey, invKey_eq];
    1.22  
    1.23  
    1.24 -(**** Freeness laws for HPair ****)
    1.25 -
    1.26 -goalw thy [HPair_def] "Agent A ~= HPair X Y";
    1.27 -by (Simp_tac 1);
    1.28 -qed "Agent_neq_HPair";
    1.29 -
    1.30 -goalw thy [HPair_def] "Nonce N ~= HPair X Y";
    1.31 -by (Simp_tac 1);
    1.32 -qed "Nonce_neq_HPair";
    1.33 -
    1.34 -goalw thy [HPair_def] "Key K ~= HPair X Y";
    1.35 -by (Simp_tac 1);
    1.36 -qed "Key_neq_HPair";
    1.37 -
    1.38 -goalw thy [HPair_def] "Hash Z ~= HPair X Y";
    1.39 -by (Simp_tac 1);
    1.40 -qed "Hash_neq_HPair";
    1.41 -
    1.42 -goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
    1.43 -by (Simp_tac 1);
    1.44 -qed "Crypt_neq_HPair";
    1.45 -
    1.46 -val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
    1.47 -		  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
    1.48 -
    1.49 -AddIffs HPair_neqs;
    1.50 -AddIffs (HPair_neqs RL [not_sym]);
    1.51 -
    1.52 -goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
    1.53 -by (Simp_tac 1);
    1.54 -qed "HPair_eq";
    1.55 -
    1.56 -goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
    1.57 -by (Simp_tac 1);
    1.58 -qed "MPair_eq_HPair";
    1.59 -
    1.60 -goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
    1.61 -by (Auto_tac());
    1.62 -qed "HPair_eq_MPair";
    1.63 -
    1.64 -AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
    1.65 -
    1.66 -
    1.67  (**** keysFor operator ****)
    1.68  
    1.69  goalw thy [keysFor_def] "keysFor {} = {}";
    1.70 @@ -133,7 +80,7 @@
    1.71  
    1.72  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    1.73            keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
    1.74 -	  keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    1.75 +          keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    1.76  
    1.77  goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    1.78  by (Fast_tac 1);
    1.79 @@ -282,8 +229,8 @@
    1.80  
    1.81  fun parts_tac i =
    1.82    EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
    1.83 -	 etac parts.induct i,
    1.84 -	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.85 +         etac parts.induct i,
    1.86 +         REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.87  
    1.88  goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
    1.89  by (parts_tac 1);
    1.90 @@ -410,8 +357,8 @@
    1.91  
    1.92  fun analz_tac i =
    1.93    EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
    1.94 -	 etac analz.induct i,
    1.95 -	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.96 +         etac analz.induct i,
    1.97 +         REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.98  
    1.99  goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   1.100  by (analz_tac 1);
   1.101 @@ -488,7 +435,7 @@
   1.102  qed "analz_Crypt_if";
   1.103  
   1.104  Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
   1.105 -	  analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   1.106 +          analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   1.107  
   1.108  (*This rule supposes "for the sake of argument" that we have the key.*)
   1.109  goal thy  "analz (insert (Crypt K X) H) <=  \
   1.110 @@ -587,7 +534,7 @@
   1.111    but can synth a pair or encryption from its components...*)
   1.112  val mk_cases = synth.mk_cases msg.simps;
   1.113  
   1.114 -(*NO Agent_synth, as any Agent name can be synthd*)
   1.115 +(*NO Agent_synth, as any Agent name can be synthesized*)
   1.116  val Nonce_synth = mk_cases "Nonce n : synth H";
   1.117  val Key_synth   = mk_cases "Key K : synth H";
   1.118  val Hash_synth  = mk_cases "Hash X : synth H";
   1.119 @@ -752,17 +699,6 @@
   1.120  by (Fast_tac 1);
   1.121  qed "Fake_analz_insert";
   1.122  
   1.123 -(*Needed????????????????*)
   1.124 -goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
   1.125 -\              analz (insert X H) <= synth (analz H) Un analz H";
   1.126 -by (rtac subsetI 1);
   1.127 -by (subgoal_tac "x : analz (synth (analz H))" 1);
   1.128 -by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.129 -                      addSEs [impOfSubs analz_mono]) 2);
   1.130 -by (Full_simp_tac 1);
   1.131 -by (Fast_tac 1);
   1.132 -qed "Fake_analz_insert_old";
   1.133 -
   1.134  goal thy "(X: analz H & X: parts H) = (X: analz H)";
   1.135  by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   1.136  val analz_conj_parts = result();
   1.137 @@ -788,8 +724,8 @@
   1.138  qed "Crypt_synth_analz";
   1.139  
   1.140  
   1.141 -goal thy "!!K. Key K ~: analz H \
   1.142 -\   ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)";
   1.143 +goal thy "!!K. X ~: synth (analz H) \
   1.144 +\   ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
   1.145  by (Fast_tac 1);
   1.146  qed "Hash_synth_analz";
   1.147  Addsimps [Hash_synth_analz];
   1.148 @@ -799,41 +735,41 @@
   1.149  
   1.150  (*** Freeness ***)
   1.151  
   1.152 -goalw thy [HPair_def] "Agent A ~= HPair X Y";
   1.153 +goalw thy [HPair_def] "Agent A ~= Hash[X] Y";
   1.154  by (Simp_tac 1);
   1.155  qed "Agent_neq_HPair";
   1.156  
   1.157 -goalw thy [HPair_def] "Nonce N ~= HPair X Y";
   1.158 +goalw thy [HPair_def] "Nonce N ~= Hash[X] Y";
   1.159  by (Simp_tac 1);
   1.160  qed "Nonce_neq_HPair";
   1.161  
   1.162 -goalw thy [HPair_def] "Key K ~= HPair X Y";
   1.163 +goalw thy [HPair_def] "Key K ~= Hash[X] Y";
   1.164  by (Simp_tac 1);
   1.165  qed "Key_neq_HPair";
   1.166  
   1.167 -goalw thy [HPair_def] "Hash Z ~= HPair X Y";
   1.168 +goalw thy [HPair_def] "Hash Z ~= Hash[X] Y";
   1.169  by (Simp_tac 1);
   1.170  qed "Hash_neq_HPair";
   1.171  
   1.172 -goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
   1.173 +goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y";
   1.174  by (Simp_tac 1);
   1.175  qed "Crypt_neq_HPair";
   1.176  
   1.177  val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
   1.178 -		  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
   1.179 +                  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
   1.180  
   1.181  AddIffs HPair_neqs;
   1.182  AddIffs (HPair_neqs RL [not_sym]);
   1.183  
   1.184 -goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
   1.185 +goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
   1.186  by (Simp_tac 1);
   1.187  qed "HPair_eq";
   1.188  
   1.189 -goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   1.190 +goalw thy [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   1.191  by (Simp_tac 1);
   1.192  qed "MPair_eq_HPair";
   1.193  
   1.194 -goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   1.195 +goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   1.196  by (Auto_tac());
   1.197  qed "HPair_eq_MPair";
   1.198  
   1.199 @@ -842,31 +778,31 @@
   1.200  
   1.201  (*** Specialized laws, proved in terms of those for Hash and MPair ***)
   1.202  
   1.203 -goalw thy [HPair_def] "keysFor (insert (HPair X Y) H) = keysFor H";
   1.204 +goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
   1.205  by (Simp_tac 1);
   1.206  qed "keysFor_insert_HPair";
   1.207  
   1.208  goalw thy [HPair_def]
   1.209 -    "parts (insert (HPair X Y) H) = \
   1.210 -\    insert (HPair X Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   1.211 +    "parts (insert (Hash[X] Y) H) = \
   1.212 +\    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   1.213  by (Simp_tac 1);
   1.214  qed "parts_insert_HPair";
   1.215  
   1.216  goalw thy [HPair_def]
   1.217 -    "analz (insert (HPair X Y) H) = \
   1.218 -\    insert (HPair X Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   1.219 +    "analz (insert (Hash[X] Y) H) = \
   1.220 +\    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   1.221  by (Simp_tac 1);
   1.222  qed "analz_insert_HPair";
   1.223  
   1.224  goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
   1.225 -\   ==> (HPair X Y : synth (analz H)) = \
   1.226 +\   ==> (Hash[X] Y : synth (analz H)) = \
   1.227  \       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
   1.228  by (Simp_tac 1);
   1.229  by (Fast_tac 1);
   1.230  qed "HPair_synth_analz";
   1.231  
   1.232  Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
   1.233 -	  HPair_synth_analz, HPair_synth_analz];
   1.234 +          HPair_synth_analz, HPair_synth_analz];
   1.235  
   1.236  
   1.237  (*We do NOT want Crypt... messages broken up in protocols!!*)
   1.238 @@ -881,7 +817,7 @@
   1.239  
   1.240  val pushKeys = map (insComm thy "Key ?K") 
   1.241                     ["Agent ?C", "Nonce ?N", "Hash ?X", 
   1.242 -		    "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.243 +                    "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.244  
   1.245  val pushCrypts = map (insComm thy "Crypt ?X ?K") 
   1.246                       ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
   1.247 @@ -898,7 +834,7 @@
   1.248  
   1.249  val Fake_insert_tac = 
   1.250      dresolve_tac [impOfSubs Fake_analz_insert,
   1.251 -		  impOfSubs Fake_parts_insert] THEN'
   1.252 +                  impOfSubs Fake_parts_insert] THEN'
   1.253      eresolve_tac [asm_rl, synth.Inj];
   1.254  
   1.255  (*Analysis of Fake cases and of messages that forward unknown parts.
   1.256 @@ -916,9 +852,9 @@
   1.257         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
   1.258         DEPTH_SOLVE 
   1.259           (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
   1.260 -	  THEN
   1.261 -	  IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
   1.262 -						 impOfSubs analz_subset_parts]) 2 1))
   1.263 +          THEN
   1.264 +          IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
   1.265 +                                                 impOfSubs analz_subset_parts]) 2 1))
   1.266         ]) i);
   1.267  
   1.268  (** Useful in many uniqueness proofs **)
   1.269 @@ -929,10 +865,10 @@
   1.270    their standard form*)
   1.271  fun prove_unique_tac lemma = 
   1.272    EVERY' [dtac lemma,
   1.273 -	  REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   1.274 -	  (*Duplicate the assumption*)
   1.275 -	  forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   1.276 -	  fast_tac (!claset addSDs [spec])];
   1.277 +          REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   1.278 +          (*Duplicate the assumption*)
   1.279 +          forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   1.280 +          fast_tac (!claset addSDs [spec])];
   1.281  
   1.282  
   1.283  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
     2.1 --- a/src/HOL/Auth/Message.thy	Fri Jan 17 11:50:09 1997 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Fri Jan 17 12:49:31 1997 +0100
     2.3 @@ -41,7 +41,7 @@
     2.4  
     2.5  (*Allows messages of the form {|A,B,NA|}, etc...*)
     2.6  syntax
     2.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(2{|_,/ _|})")
     2.8 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     2.9  
    2.10  translations
    2.11    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    2.12 @@ -50,8 +50,8 @@
    2.13  
    2.14  constdefs
    2.15    (*Message Y, paired with a MAC computed with the help of X*)
    2.16 -  HPair :: "[msg,msg]=>msg"
    2.17 -    "HPair X Y == {| Hash{|X,Y|}, Y|}"
    2.18 +  HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
    2.19 +    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    2.20  
    2.21    (*Keys useful to decrypt elements of a message set*)
    2.22    keysFor :: msg set => key set
     3.1 --- a/src/HOL/Auth/NS_Public.ML	Fri Jan 17 11:50:09 1997 +0100
     3.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Jan 17 12:49:31 1997 +0100
     3.3 @@ -11,7 +11,6 @@
     3.4  
     3.5  proof_timing:=true;
     3.6  HOL_quantifiers := false;
     3.7 -Pretty.setdepth 20;
     3.8  
     3.9  AddIffs [Spy_in_lost];
    3.10  
    3.11 @@ -26,10 +25,7 @@
    3.12  \                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    3.13  by (REPEAT (resolve_tac [exI,bexI] 1));
    3.14  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    3.15 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    3.16 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    3.17 -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
    3.18 -				    addss (!simpset setsolver safe_solver))));
    3.19 +by possibility_tac;
    3.20  result();
    3.21  
    3.22  
    3.23 @@ -84,9 +80,9 @@
    3.24  
    3.25  
    3.26  fun analz_induct_tac i = 
    3.27 -    etac ns_public.induct i	THEN
    3.28 +    etac ns_public.induct i     THEN
    3.29      ALLGOALS (asm_simp_tac 
    3.30 -	      (!simpset addsimps [not_parts_not_analz]
    3.31 +              (!simpset addsimps [not_parts_not_analz]
    3.32                          setloop split_tac [expand_if]));
    3.33  
    3.34  (**** Authenticity properties obtained from NS2 ****)
    3.35 @@ -105,9 +101,9 @@
    3.36  by (fast_tac (!claset addSEs partsEs) 3);
    3.37  (*Fake*)
    3.38  by (best_tac (!claset addIs [analz_insertI]
    3.39 -		      addDs [impOfSubs analz_subset_parts,
    3.40 -			     impOfSubs Fake_parts_insert]
    3.41 -	              addss (!simpset)) 2);
    3.42 +                      addDs [impOfSubs analz_subset_parts,
    3.43 +                             impOfSubs Fake_parts_insert]
    3.44 +                      addss (!simpset)) 2);
    3.45  (*Base*)
    3.46  by (fast_tac (!claset addss (!simpset)) 1);
    3.47  bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
    3.48 @@ -132,8 +128,8 @@
    3.49  by (step_tac (!claset addSIs [analz_insertI]) 1);
    3.50  by (ex_strip_tac 1);
    3.51  by (best_tac (!claset delrules [conjI]
    3.52 -		      addSDs [impOfSubs Fake_parts_insert]
    3.53 -	              addDs  [impOfSubs analz_subset_parts]
    3.54 +                      addSDs [impOfSubs Fake_parts_insert]
    3.55 +                      addDs  [impOfSubs analz_subset_parts]
    3.56                        addss (!simpset)) 1);
    3.57  val lemma = result();
    3.58  
    3.59 @@ -158,7 +154,7 @@
    3.60                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    3.61  (*NS1*)
    3.62  by (fast_tac (!claset addSEs partsEs
    3.63 -		      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    3.64 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    3.65                        addIs  [impOfSubs analz_subset_parts]) 2);
    3.66  (*Fake*)
    3.67  by (spy_analz_tac 1);
    3.68 @@ -191,9 +187,9 @@
    3.69  by (fast_tac (!claset addss (!simpset)) 1);
    3.70  by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
    3.71  by (best_tac (!claset addSIs [disjI2]
    3.72 -		      addSDs [impOfSubs Fake_parts_insert]
    3.73 -		      addDs  [impOfSubs analz_subset_parts]
    3.74 -	              addss (!simpset)) 1);
    3.75 +                      addSDs [impOfSubs Fake_parts_insert]
    3.76 +                      addDs  [impOfSubs analz_subset_parts]
    3.77 +                      addss (!simpset)) 1);
    3.78  qed_spec_mp "NA_decrypt_imp_B_msg";
    3.79  
    3.80  (*Corollary: if A receives B's message NS2 and the nonce NA agrees
    3.81 @@ -219,10 +215,10 @@
    3.82  by (analz_induct_tac 1);
    3.83  (*Fake*)
    3.84  by (best_tac (!claset addSIs [disjI2]
    3.85 -		      addSDs [impOfSubs Fake_parts_insert]
    3.86 -		      addIs  [analz_insertI]
    3.87 -		      addDs  [impOfSubs analz_subset_parts]
    3.88 -	              addss (!simpset)) 2);
    3.89 +                      addSDs [impOfSubs Fake_parts_insert]
    3.90 +                      addIs  [analz_insertI]
    3.91 +                      addDs  [impOfSubs analz_subset_parts]
    3.92 +                      addss (!simpset)) 2);
    3.93  (*Base*)
    3.94  by (fast_tac (!claset addss (!simpset)) 1);
    3.95  qed_spec_mp "B_trusts_NS1";
    3.96 @@ -252,9 +248,9 @@
    3.97  by (step_tac (!claset addSIs [analz_insertI]) 1);
    3.98  by (ex_strip_tac 1);
    3.99  by (best_tac (!claset delrules [conjI]
   3.100 -	              addSDs [impOfSubs Fake_parts_insert]
   3.101 -	              addDs  [impOfSubs analz_subset_parts] 
   3.102 -	              addss (!simpset)) 1);
   3.103 +                      addSDs [impOfSubs Fake_parts_insert]
   3.104 +                      addDs  [impOfSubs analz_subset_parts] 
   3.105 +                      addss (!simpset)) 1);
   3.106  val lemma = result();
   3.107  
   3.108  goal thy 
   3.109 @@ -317,14 +313,14 @@
   3.110  by (fast_tac (!claset addss (!simpset)) 1);
   3.111  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   3.112  by (best_tac (!claset addSIs [disjI2]
   3.113 -		      addSDs [impOfSubs Fake_parts_insert]
   3.114 -	              addDs  [impOfSubs analz_subset_parts] 
   3.115 -	              addss (!simpset)) 1);
   3.116 +                      addSDs [impOfSubs Fake_parts_insert]
   3.117 +                      addDs  [impOfSubs analz_subset_parts] 
   3.118 +                      addss (!simpset)) 1);
   3.119  (*NS3*)
   3.120  by (Step_tac 1);
   3.121  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   3.122  by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   3.123 -	              addDs  [unique_NB]) 1);
   3.124 +                      addDs  [unique_NB]) 1);
   3.125  qed_spec_mp "NB_decrypt_imp_A_msg";
   3.126  
   3.127  (*Corollary: if B receives message NS3 and the nonce NB agrees,
   3.128 @@ -363,14 +359,14 @@
   3.129  by (fast_tac (!claset addss (!simpset)) 1);
   3.130  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   3.131  by (best_tac (!claset addSIs [disjI2]
   3.132 -		      addDs [impOfSubs analz_subset_parts,
   3.133 -			     impOfSubs Fake_parts_insert]
   3.134 -	              addss (!simpset)) 1);
   3.135 +                      addDs [impOfSubs analz_subset_parts,
   3.136 +                             impOfSubs Fake_parts_insert]
   3.137 +                      addss (!simpset)) 1);
   3.138  (*NS3*)
   3.139  by (Step_tac 1);
   3.140  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   3.141  by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   3.142 -	              addDs  [unique_NB]) 1);
   3.143 +                      addDs  [unique_NB]) 1);
   3.144  val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp);
   3.145  
   3.146  goal thy 
     4.1 --- a/src/HOL/Auth/NS_Public.thy	Fri Jan 17 11:50:09 1997 +0100
     4.2 +++ b/src/HOL/Auth/NS_Public.thy	Fri Jan 17 12:49:31 1997 +0100
     4.3 @@ -37,9 +37,9 @@
     4.4  
     4.5           (*Alice proves her existence by sending NB back to Bob.*)
     4.6      NS3  "[| evs: ns_public;  A ~= B;
     4.7 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
     4.8 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
     4.9                 : set_of_list evs;
    4.10 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.11 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    4.12                 : set_of_list evs |]
    4.13            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    4.14  
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Jan 17 11:50:09 1997 +0100
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Jan 17 12:49:31 1997 +0100
     5.3 @@ -15,7 +15,6 @@
     5.4  
     5.5  proof_timing:=true;
     5.6  HOL_quantifiers := false;
     5.7 -Pretty.setdepth 20;
     5.8  
     5.9  AddIffs [Spy_in_lost];
    5.10  
    5.11 @@ -30,10 +29,7 @@
    5.12  \                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    5.13  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.14  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    5.15 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    5.16 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    5.17 -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
    5.18 -				    addss (!simpset setsolver safe_solver))));
    5.19 +by possibility_tac;
    5.20  result();
    5.21  
    5.22  
    5.23 @@ -88,9 +84,9 @@
    5.24  
    5.25  
    5.26  fun analz_induct_tac i = 
    5.27 -    etac ns_public.induct i	THEN
    5.28 +    etac ns_public.induct i     THEN
    5.29      ALLGOALS (asm_simp_tac 
    5.30 -	      (!simpset addsimps [not_parts_not_analz]
    5.31 +              (!simpset addsimps [not_parts_not_analz]
    5.32                          setloop split_tac [expand_if]));
    5.33  
    5.34  
    5.35 @@ -110,9 +106,9 @@
    5.36  by (fast_tac (!claset addSEs partsEs) 3);
    5.37  (*Fake*)
    5.38  by (best_tac (!claset addIs [analz_insertI]
    5.39 -		      addDs [impOfSubs analz_subset_parts,
    5.40 -			     impOfSubs Fake_parts_insert]
    5.41 -	              addss (!simpset)) 2);
    5.42 +                      addDs [impOfSubs analz_subset_parts,
    5.43 +                             impOfSubs Fake_parts_insert]
    5.44 +                      addss (!simpset)) 2);
    5.45  (*Base*)
    5.46  by (fast_tac (!claset addss (!simpset)) 1);
    5.47  bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
    5.48 @@ -137,8 +133,8 @@
    5.49  by (step_tac (!claset addSIs [analz_insertI]) 1);
    5.50  by (ex_strip_tac 1);
    5.51  by (best_tac (!claset delrules [conjI]
    5.52 -		      addSDs [impOfSubs Fake_parts_insert]
    5.53 -	              addDs  [impOfSubs analz_subset_parts]
    5.54 +                      addSDs [impOfSubs Fake_parts_insert]
    5.55 +                      addDs  [impOfSubs analz_subset_parts]
    5.56                        addss (!simpset)) 1);
    5.57  val lemma = result();
    5.58  
    5.59 @@ -163,7 +159,7 @@
    5.60                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    5.61  (*NS1*)
    5.62  by (fast_tac (!claset addSEs partsEs
    5.63 -		      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    5.64 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    5.65                        addIs  [impOfSubs analz_subset_parts]) 2);
    5.66  (*Fake*)
    5.67  by (spy_analz_tac 1);
    5.68 @@ -193,9 +189,9 @@
    5.69  by (fast_tac (!claset addss (!simpset)) 1);
    5.70  by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
    5.71  by (best_tac (!claset addSIs [disjI2]
    5.72 -		      addSDs [impOfSubs Fake_parts_insert]
    5.73 -		      addDs  [impOfSubs analz_subset_parts]
    5.74 -	              addss (!simpset)) 1);
    5.75 +                      addSDs [impOfSubs Fake_parts_insert]
    5.76 +                      addDs  [impOfSubs analz_subset_parts]
    5.77 +                      addss (!simpset)) 1);
    5.78  (*NS2*)
    5.79  by (Step_tac 1);
    5.80  by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
    5.81 @@ -225,10 +221,10 @@
    5.82  by (analz_induct_tac 1);
    5.83  (*Fake*)
    5.84  by (best_tac (!claset addSIs [disjI2]
    5.85 -		      addSDs [impOfSubs Fake_parts_insert]
    5.86 -		      addIs  [analz_insertI]
    5.87 -		      addDs  [impOfSubs analz_subset_parts]
    5.88 -	              addss (!simpset)) 2);
    5.89 +                      addSDs [impOfSubs Fake_parts_insert]
    5.90 +                      addIs  [analz_insertI]
    5.91 +                      addDs  [impOfSubs analz_subset_parts]
    5.92 +                      addss (!simpset)) 2);
    5.93  (*Base*)
    5.94  by (fast_tac (!claset addss (!simpset)) 1);
    5.95  qed_spec_mp "B_trusts_NS1";
    5.96 @@ -257,9 +253,9 @@
    5.97  by (step_tac (!claset addSIs [analz_insertI]) 1);
    5.98  by (ex_strip_tac 1);
    5.99  by (best_tac (!claset delrules [conjI]
   5.100 -	              addSDs [impOfSubs Fake_parts_insert]
   5.101 -	              addDs  [impOfSubs analz_subset_parts] 
   5.102 -	              addss (!simpset)) 1);
   5.103 +                      addSDs [impOfSubs Fake_parts_insert]
   5.104 +                      addDs  [impOfSubs analz_subset_parts] 
   5.105 +                      addss (!simpset)) 1);
   5.106  val lemma = result();
   5.107  
   5.108  goal thy 
   5.109 @@ -316,18 +312,18 @@
   5.110  (*Fake*)
   5.111  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   5.112  by (fast_tac (!claset addss (!simpset)) 1);
   5.113 -br (ccontr RS disjI2) 1;
   5.114 +by (rtac (ccontr RS disjI2) 1);
   5.115  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   5.116  by (Fast_tac 1);
   5.117  by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   5.118 -	              addDs  [impOfSubs analz_subset_parts] 
   5.119 -	              addss (!simpset)) 1);
   5.120 +                      addDs  [impOfSubs analz_subset_parts] 
   5.121 +                      addss (!simpset)) 1);
   5.122  (*NS3*)
   5.123  by (Step_tac 1);
   5.124  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1));
   5.125  by (Fast_tac 1);
   5.126  by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   5.127 -	              addDs  [unique_NB]) 1);
   5.128 +                      addDs  [unique_NB]) 1);
   5.129  qed_spec_mp "NB_decrypt_imp_A_msg";
   5.130  
   5.131  
     6.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Jan 17 11:50:09 1997 +0100
     6.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Jan 17 12:49:31 1997 +0100
     6.3 @@ -41,9 +41,9 @@
     6.4  
     6.5           (*Alice proves her existence by sending NB back to Bob.*)
     6.6      NS3  "[| evs: ns_public;  A ~= B;
     6.7 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
     6.8 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
     6.9                 : set_of_list evs;
    6.10 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    6.11 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    6.12                 : set_of_list evs |]
    6.13            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    6.14  
     7.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Jan 17 11:50:09 1997 +0100
     7.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Jan 17 12:49:31 1997 +0100
     7.3 @@ -22,10 +22,9 @@
     7.4  \        ==> EX N K. EX evs: ns_shared lost.          \
     7.5  \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs";
     7.6  by (REPEAT (resolve_tac [exI,bexI] 1));
     7.7 -by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
     7.8 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
     7.9 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    7.10 -by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    7.11 +by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
    7.12 +          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
    7.13 +by possibility_tac;
    7.14  result();
    7.15  
    7.16  
    7.17 @@ -52,15 +51,13 @@
    7.18  (*For reasoning about the encrypted portion of message NS3*)
    7.19  goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
    7.20  \                ==> X : parts (sees lost Spy evs)";
    7.21 -by (fast_tac (!claset addSEs partsEs
    7.22 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    7.23 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    7.24  qed "NS3_msg_in_parts_sees_Spy";
    7.25                                
    7.26  goal thy
    7.27      "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
    7.28  \           ==> K : parts (sees lost Spy evs)";
    7.29 -by (fast_tac (!claset addSEs partsEs
    7.30 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    7.31 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    7.32  qed "Oops_parts_sees_Spy";
    7.33  
    7.34  val parts_Fake_tac = 
    7.35 @@ -107,72 +104,18 @@
    7.36  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    7.37  
    7.38  
    7.39 -(*** Future keys can't be seen or used! ***)
    7.40 -
    7.41 -(*Nobody can have SEEN keys that will be generated in the future. *)
    7.42 +(*Nobody can have used non-existent keys!*)
    7.43  goal thy "!!evs. evs : ns_shared lost ==>      \
    7.44 -\               length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
    7.45 -by (parts_induct_tac 1);
    7.46 -by (ALLGOALS (fast_tac (!claset addEs [leD RS notE]
    7.47 -				addDs [impOfSubs analz_subset_parts,
    7.48 -                                       impOfSubs parts_insert_subset_Un,
    7.49 -                                       Suc_leD]
    7.50 -                                addss (!simpset))));
    7.51 -qed_spec_mp "new_keys_not_seen";
    7.52 -Addsimps [new_keys_not_seen];
    7.53 -
    7.54 -(*Variant: old messages must contain old keys!*)
    7.55 -goal thy 
    7.56 - "!!evs. [| Says A B X : set_of_list evs;          \
    7.57 -\           Key (newK i) : parts {X};              \
    7.58 -\           evs : ns_shared lost                   \
    7.59 -\        |] ==> i < length evs";
    7.60 -by (rtac ccontr 1);
    7.61 -by (dtac leI 1);
    7.62 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    7.63 -                      addIs  [impOfSubs parts_mono]) 1);
    7.64 -qed "Says_imp_old_keys";
    7.65 -
    7.66 -
    7.67 -
    7.68 -(*** Future nonces can't be seen or used! ***)
    7.69 -
    7.70 -goal thy "!!evs. evs : ns_shared lost ==>     \
    7.71 -\             length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
    7.72 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    7.73  by (parts_induct_tac 1);
    7.74 -by (REPEAT_FIRST
    7.75 -    (fast_tac (!claset addSEs partsEs
    7.76 -                       addSDs  [Says_imp_sees_Spy RS parts.Inj]
    7.77 -                       addEs [leD RS notE]
    7.78 -				addDs  [impOfSubs analz_subset_parts,
    7.79 -                               impOfSubs parts_insert_subset_Un, Suc_leD]
    7.80 -                       addss (!simpset))));
    7.81 -qed_spec_mp "new_nonces_not_seen";
    7.82 -Addsimps [new_nonces_not_seen];
    7.83 -
    7.84 -
    7.85 -(*Nobody can have USED keys that will be generated in the future.
    7.86 -  ...very like new_keys_not_seen*)
    7.87 -goal thy "!!evs. evs : ns_shared lost ==>      \
    7.88 -\                length evs <= i -->           \
    7.89 -\                newK i ~: keysFor (parts (sees lost Spy evs))";
    7.90 -by (parts_induct_tac 1);
    7.91 -(*NS1 and NS2*)
    7.92 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]));
    7.93 -(*Fake and NS3*)
    7.94 -by (EVERY 
    7.95 -    (map
    7.96 -     (best_tac
    7.97 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    7.98 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    7.99 -                      Suc_leD]
   7.100 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   7.101 -               addss (!simpset)))
   7.102 -     [2,1]));
   7.103 -(*NS4 and NS5: nonce exchange*)
   7.104 -by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
   7.105 -                                  addIs  [less_SucI, impOfSubs keysFor_mono]
   7.106 -                                  addss (!simpset addsimps [le_def])) 1));
   7.107 +(*Fake*)
   7.108 +by (best_tac
   7.109 +      (!claset addIs [impOfSubs analz_subset_parts]
   7.110 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   7.111 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   7.112 +               addss (!simpset)) 1);
   7.113 +(*NS2, NS4, NS5*)
   7.114 +by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
   7.115  qed_spec_mp "new_keys_not_used";
   7.116  
   7.117  bind_thm ("new_keys_not_analzd",
   7.118 @@ -186,14 +129,15 @@
   7.119  
   7.120  (*Describes the form of K, X and K' when the Server sends this message.*)
   7.121  goal thy 
   7.122 - "!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \
   7.123 -\           evs : ns_shared lost |]                       \
   7.124 -\        ==> (EX i. K = Key(newK i) &                     \
   7.125 -\                   X = (Crypt (shrK B) {|K, Agent A|}) & \
   7.126 -\                   K' = shrK A)";
   7.127 + "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
   7.128 +\             : set_of_list evs;                              \
   7.129 +\           evs : ns_shared lost |]                           \
   7.130 +\        ==> K ~: range shrK &                                \
   7.131 +\            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
   7.132 +\            K' = shrK A";
   7.133  by (etac rev_mp 1);
   7.134  by (etac ns_shared.induct 1);
   7.135 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   7.136 +by (Auto_tac());
   7.137  qed "Says_Server_message_form";
   7.138  
   7.139  
   7.140 @@ -219,16 +163,14 @@
   7.141  goal thy 
   7.142   "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
   7.143  \            : set_of_list evs;  evs : ns_shared lost |]                   \
   7.144 -\        ==> (EX i. K = newK i & i < length evs &                  \
   7.145 -\                   X = (Crypt (shrK B) {|Key K, Agent A|}))       \
   7.146 -\          | X : analz (sees lost Spy evs)";
   7.147 +\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))  \
   7.148 +\            | X : analz (sees lost Spy evs)";
   7.149  by (case_tac "A : lost" 1);
   7.150  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   7.151                        addss (!simpset)) 1);
   7.152  by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
   7.153  by (fast_tac (!claset addEs  partsEs
   7.154                        addSDs [A_trusts_NS2, Says_Server_message_form]
   7.155 -                      addIs [Says_imp_old_keys]
   7.156                        addss (!simpset)) 1);
   7.157  qed "Says_S_message_form";
   7.158  
   7.159 @@ -237,14 +179,13 @@
   7.160  val analz_Fake_tac = 
   7.161      forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
   7.162      forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
   7.163 -    Full_simp_tac 7 THEN
   7.164 -    REPEAT_FIRST (eresolve_tac [asm_rl, exE, disjE] ORELSE' hyp_subst_tac);
   7.165 +    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   7.166  
   7.167  
   7.168  (****
   7.169   The following is to prove theorems of the form
   7.170  
   7.171 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   7.172 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   7.173    Key K : analz (sees lost Spy evs)
   7.174  
   7.175   A more general formula must be proved inductively.
   7.176 @@ -256,8 +197,8 @@
   7.177    to encrypt messages containing other keys, in the actual protocol.
   7.178    We require that agents should behave like this subsequently also.*)
   7.179  goal thy 
   7.180 - "!!evs. evs : ns_shared lost ==> \
   7.181 -\        (Crypt (newK i) X) : parts (sees lost Spy evs) & \
   7.182 + "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==> \
   7.183 +\        (Crypt KAB X) : parts (sees lost Spy evs) & \
   7.184  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   7.185  by (etac ns_shared.induct 1);
   7.186  by parts_Fake_tac;
   7.187 @@ -276,31 +217,28 @@
   7.188  (*The equality makes the induction hypothesis easier to apply*)
   7.189  goal thy  
   7.190   "!!evs. evs : ns_shared lost ==> \
   7.191 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   7.192 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   7.193 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
   7.194 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   7.195 +\            (K : KK | Key K : analz (sees lost Spy evs))";
   7.196  by (etac ns_shared.induct 1);
   7.197  by analz_Fake_tac;
   7.198 -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   7.199 -by (ALLGOALS (*Takes 18 secs*)
   7.200 -    (asm_simp_tac 
   7.201 -     (!simpset addsimps [Un_assoc RS sym, 
   7.202 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   7.203 -               setloop split_tac [expand_if])));
   7.204 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   7.205 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   7.206 +(*Takes 24 secs*)
   7.207 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   7.208  (*NS4, Fake*) 
   7.209 -by (EVERY (map spy_analz_tac [5,2]));
   7.210 -(*NS3, NS2, Base*)
   7.211 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   7.212 -qed_spec_mp "analz_image_newK";
   7.213 +by (EVERY (map spy_analz_tac [3,2]));
   7.214 +(*Base*)
   7.215 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   7.216 +qed_spec_mp "analz_image_freshK";
   7.217  
   7.218  
   7.219  goal thy
   7.220 - "!!evs. evs : ns_shared lost ==>                               \
   7.221 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   7.222 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
   7.223 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   7.224 -                                   insert_Key_singleton]) 1);
   7.225 -by (Fast_tac 1);
   7.226 -qed "analz_insert_Key_newK";
   7.227 + "!!evs. [| evs : ns_shared lost;  KAB ~: range shrK |] ==>     \
   7.228 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   7.229 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
   7.230 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   7.231 +qed "analz_insert_freshK";
   7.232  
   7.233  
   7.234  (** The session key K uniquely identifies the message, if encrypted
   7.235 @@ -320,8 +258,8 @@
   7.236  (*NS2: it can't be a new key*)
   7.237  by (expand_case_tac "K = ?y" 1);
   7.238  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   7.239 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   7.240 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   7.241 +by (fast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
   7.242 +                      addSEs sees_Spy_partsEs
   7.243                        addss (!simpset addsimps [parts_insertI])) 1);
   7.244  val lemma = result();
   7.245  
   7.246 @@ -352,15 +290,14 @@
   7.247  by analz_Fake_tac;
   7.248  by (ALLGOALS 
   7.249      (asm_simp_tac 
   7.250 -     (!simpset addsimps ([not_parts_not_analz,
   7.251 -                          analz_insert_Key_newK] @ pushes)
   7.252 +     (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
   7.253                 setloop split_tac [expand_if])));
   7.254 +(*NS4, Fake*) 
   7.255 +by (EVERY (map spy_analz_tac [4,1]));
   7.256  (*NS2*)
   7.257 -by (fast_tac (!claset addIs [parts_insertI]
   7.258 -                      addEs [Says_imp_old_keys RS less_irrefl]
   7.259 -                      addss (!simpset)) 2);
   7.260 -(*NS4, Fake*) 
   7.261 -by (EVERY (map spy_analz_tac [3,1]));
   7.262 +by (fast_tac (!claset addSEs sees_Spy_partsEs
   7.263 +                      addIs [parts_insertI, impOfSubs analz_subset_parts]
   7.264 +                      addss (!simpset)) 1);
   7.265  (*NS3 and Oops subcases*) (**LEVEL 5 **)
   7.266  by (step_tac (!claset delrules [impCE]) 1);
   7.267  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   7.268 @@ -382,10 +319,10 @@
   7.269  (*Final version: Server's message in the most abstract form*)
   7.270  goal thy 
   7.271   "!!evs. [| Says Server A                                               \
   7.272 -\            (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs;        \
   7.273 -\           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
   7.274 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   7.275 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   7.276  \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   7.277 -\        |] ==> K ~: analz (sees lost Spy evs)";
   7.278 +\        |] ==> Key K ~: analz (sees lost Spy evs)";
   7.279  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   7.280  by (fast_tac (!claset addSEs [lemma]) 1);
   7.281  qed "Spy_not_see_encrypted_key";
   7.282 @@ -394,10 +331,10 @@
   7.283  goal thy 
   7.284   "!!evs. [| C ~: {A,B,Server};                                          \
   7.285  \           Says Server A                                               \
   7.286 -\            (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs;        \
   7.287 -\           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
   7.288 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   7.289 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   7.290  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   7.291 -\        ==> K ~: analz (sees lost C evs)";
   7.292 +\        ==> Key K ~: analz (sees lost C evs)";
   7.293  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   7.294  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   7.295  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   7.296 @@ -449,8 +386,8 @@
   7.297                        addDs [impOfSubs analz_subset_parts]) 1);
   7.298  by (Fast_tac 2);
   7.299  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   7.300 -(*Contradiction from the assumption   
   7.301 -   Crypt (newK(length evsa)) (Nonce NB) : parts (sees lost Spy evsa) *)
   7.302 +(*Subgoal 1: contradiction from the assumptions  
   7.303 +  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
   7.304  by (dtac Crypt_imp_invKey_keysFor 1);
   7.305  (**LEVEL 10**)
   7.306  by (Asm_full_simp_tac 1);
   7.307 @@ -460,7 +397,7 @@
   7.308  by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
   7.309  by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN 
   7.310      REPEAT (assume_tac 1));
   7.311 -by (fast_tac (!claset addDs [unique_session_keys]) 1);
   7.312 +by (best_tac (!claset addDs [unique_session_keys]) 1);
   7.313  val lemma = result();
   7.314  
   7.315  goal thy
     8.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Jan 17 11:50:09 1997 +0100
     8.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Jan 17 12:49:31 1997 +0100
     8.3 @@ -26,20 +26,20 @@
     8.4            ==> Says Spy B X # evs : ns_shared lost"
     8.5  
     8.6           (*Alice initiates a protocol run, requesting to talk to any B*)
     8.7 -    NS1  "[| evs: ns_shared lost;  A ~= Server |]
     8.8 -          ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|}
     8.9 -                  # evs  :  ns_shared lost"
    8.10 +    NS1  "[| evs: ns_shared lost;  A ~= Server;  Nonce NA ~: used evs |]
    8.11 +          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
    8.12 +                :  ns_shared lost"
    8.13  
    8.14           (*Server's response to Alice's message.
    8.15             !! It may respond more than once to A's request !!
    8.16  	   Server doesn't know who the true sender is, hence the A' in
    8.17                 the sender field.*)
    8.18 -    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
    8.19 +    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    8.20               Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    8.21            ==> Says Server A 
    8.22                  (Crypt (shrK A)
    8.23 -                   {|Nonce NA, Agent B, Key (newK(length evs)),   
    8.24 -                    (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) 
    8.25 +                   {|Nonce NA, Agent B, Key KAB,
    8.26 +                     (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
    8.27                  # evs : ns_shared lost"
    8.28  
    8.29            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    8.30 @@ -52,9 +52,9 @@
    8.31  
    8.32           (*Bob's nonce exchange.  He does not know who the message came
    8.33             from, but responds to A because she is mentioned inside.*)
    8.34 -    NS4  "[| evs: ns_shared lost;  A ~= B;  
    8.35 +    NS4  "[| evs: ns_shared lost;  A ~= B;  Nonce NB ~: used evs;
    8.36               Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
    8.37 -          ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs
    8.38 +          ==> Says B A (Crypt K (Nonce NB)) # evs
    8.39                  : ns_shared lost"
    8.40  
    8.41           (*Alice responds with Nonce NB if she has seen the key before.
     9.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Jan 17 11:50:09 1997 +0100
     9.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Jan 17 12:49:31 1997 +0100
     9.3 @@ -26,9 +26,7 @@
     9.4  \                 : set_of_list evs";
     9.5  by (REPEAT (resolve_tac [exI,bexI] 1));
     9.6  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
     9.7 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
     9.8 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
     9.9 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    9.10 +by possibility_tac;
    9.11  result();
    9.12  
    9.13  
    9.14 @@ -59,15 +57,14 @@
    9.15  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    9.16  qed "OR2_analz_sees_Spy";
    9.17  
    9.18 -goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs \
    9.19 +goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
    9.20  \                ==> X : analz (sees lost Spy evs)";
    9.21  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    9.22  qed "OR4_analz_sees_Spy";
    9.23  
    9.24  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    9.25  \                 ==> K : parts (sees lost Spy evs)";
    9.26 -by (fast_tac (!claset addSEs partsEs
    9.27 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    9.28 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
    9.29  qed "Oops_parts_sees_Spy";
    9.30  
    9.31  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    9.32 @@ -84,9 +81,9 @@
    9.33    harder to complete, since simplification does less for us.*)
    9.34  val parts_Fake_tac = 
    9.35      let val tac = forw_inst_tac [("lost","lost")] 
    9.36 -    in  tac OR2_parts_sees_Spy 4 THEN 
    9.37 -        tac OR4_parts_sees_Spy 6 THEN
    9.38 -        tac Oops_parts_sees_Spy 7
    9.39 +    in  tac OR2_parts_sees_Spy     4 THEN 
    9.40 +        tac OR4_parts_sees_Spy     6 THEN
    9.41 +        tac Oops_parts_sees_Spy    7
    9.42      end;
    9.43  
    9.44  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    9.45 @@ -128,77 +125,18 @@
    9.46  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    9.47  
    9.48  
    9.49 -(*** Future keys can't be seen or used! ***)
    9.50 -
    9.51 -(*Nobody can have SEEN keys that will be generated in the future. *)
    9.52 -goal thy "!!i. evs : otway lost ==>          \
    9.53 -\              length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
    9.54 -by (parts_induct_tac 1);
    9.55 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    9.56 -                                    addDs [impOfSubs analz_subset_parts,
    9.57 -                                           impOfSubs parts_insert_subset_Un,
    9.58 -                                           Suc_leD]
    9.59 -                                    addss (!simpset))));
    9.60 -qed_spec_mp "new_keys_not_seen";
    9.61 -Addsimps [new_keys_not_seen];
    9.62 -
    9.63 -(*Variant: old messages must contain old keys!*)
    9.64 -goal thy 
    9.65 - "!!evs. [| Says A B X : set_of_list evs;          \
    9.66 -\           Key (newK i) : parts {X};    \
    9.67 -\           evs : otway lost                       \
    9.68 -\        |] ==> i < length evs";
    9.69 -by (rtac ccontr 1);
    9.70 -by (dtac leI 1);
    9.71 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    9.72 -                      addIs  [impOfSubs parts_mono]) 1);
    9.73 -qed "Says_imp_old_keys";
    9.74 -
    9.75 -
    9.76 -(*** Future nonces can't be seen or used! ***)
    9.77 -
    9.78 -goal thy "!!evs. evs : otway lost ==>         \
    9.79 -\                length evs <= i --> \
    9.80 -\                Nonce (newN i) ~: parts (sees lost Spy evs)";
    9.81 +(*Nobody can have used non-existent keys!*)
    9.82 +goal thy "!!evs. evs : otway lost ==>          \
    9.83 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    9.84  by (parts_induct_tac 1);
    9.85 -by (REPEAT_FIRST (fast_tac (!claset 
    9.86 -                              addSEs partsEs
    9.87 -                              addSDs [Says_imp_sees_Spy RS parts.Inj]
    9.88 -                              addEs  [leD RS notE]
    9.89 -                              addDs  [impOfSubs analz_subset_parts,
    9.90 -                                      impOfSubs parts_insert_subset_Un,
    9.91 -                                      Suc_leD]
    9.92 -                              addss (!simpset))));
    9.93 -qed_spec_mp "new_nonces_not_seen";
    9.94 -Addsimps [new_nonces_not_seen];
    9.95 -
    9.96 -(*Variant: old messages must contain old nonces!*)
    9.97 -goal thy "!!evs. [| Says A B X : set_of_list evs;            \
    9.98 -\                   Nonce (newN i) : parts {X};    \
    9.99 -\                   evs : otway lost                         \
   9.100 -\                |] ==> i < length evs";
   9.101 -by (rtac ccontr 1);
   9.102 -by (dtac leI 1);
   9.103 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   9.104 -                      addIs  [impOfSubs parts_mono]) 1);
   9.105 -qed "Says_imp_old_nonces";
   9.106 -
   9.107 -
   9.108 -(*Nobody can have USED keys that will be generated in the future.
   9.109 -  ...very like new_keys_not_seen*)
   9.110 -goal thy "!!i. evs : otway lost ==>          \
   9.111 -\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
   9.112 -by (parts_induct_tac 1);
   9.113 -(*OR1 and OR3*)
   9.114 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   9.115 -(*Fake, OR2, OR4: these messages send unknown (X) components*)
   9.116 -by (REPEAT
   9.117 -    (best_tac
   9.118 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   9.119 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   9.120 -                      Suc_leD]
   9.121 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   9.122 -               addss (!simpset)) 1));
   9.123 +(*Fake*)
   9.124 +by (best_tac
   9.125 +      (!claset addIs [impOfSubs analz_subset_parts]
   9.126 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   9.127 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   9.128 +               addss (!simpset)) 1);
   9.129 +(*OR1-3*)
   9.130 +by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
   9.131  qed_spec_mp "new_keys_not_used";
   9.132  
   9.133  bind_thm ("new_keys_not_analzd",
   9.134 @@ -214,11 +152,10 @@
   9.135  (*Describes the form of K and NA when the Server sends this message.  Also
   9.136    for Oops case.*)
   9.137  goal thy 
   9.138 - "!!evs. [| Says Server B \
   9.139 -\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;       \
   9.140 + "!!evs. [| Says Server B                                                 \
   9.141 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;   \
   9.142  \           evs : otway lost |]                                           \
   9.143 -\        ==> (EX n. K = Key(newK n)) &                                    \
   9.144 -\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   9.145 +\     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   9.146  by (etac rev_mp 1);
   9.147  by (etac otway.induct 1);
   9.148  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   9.149 @@ -230,14 +167,14 @@
   9.150      dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
   9.151      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   9.152      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   9.153 -    assume_tac 7 THEN Full_simp_tac 7 THEN
   9.154 +    assume_tac 7 THEN
   9.155      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   9.156  
   9.157  
   9.158  (****
   9.159   The following is to prove theorems of the form
   9.160  
   9.161 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   9.162 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   9.163    Key K : analz (sees lost Spy evs)
   9.164  
   9.165   A more general formula must be proved inductively.
   9.166 @@ -248,32 +185,28 @@
   9.167  
   9.168  (*The equality makes the induction hypothesis easier to apply*)
   9.169  goal thy  
   9.170 - "!!evs. evs : otway lost ==> \
   9.171 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   9.172 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   9.173 + "!!evs. evs : otway lost ==>                                         \
   9.174 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
   9.175 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   9.176 +\            (K : KK | Key K : analz (sees lost Spy evs))";
   9.177  by (etac otway.induct 1);
   9.178  by analz_Fake_tac;
   9.179 -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   9.180 -by (ALLGOALS (*Takes 11 secs*)
   9.181 -    (asm_simp_tac 
   9.182 -     (!simpset addsimps [Un_assoc RS sym, 
   9.183 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   9.184 -               setloop split_tac [expand_if])));
   9.185 -(*OR4, OR2, Fake*) 
   9.186 -by (EVERY (map spy_analz_tac [5,3,2]));
   9.187 -(*Oops, OR3, Base*)
   9.188 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   9.189 -qed_spec_mp "analz_image_newK";
   9.190 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   9.191 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   9.192 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   9.193 +(*Base*)
   9.194 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   9.195 +(*Fake, OR2, OR4*) 
   9.196 +by (REPEAT (spy_analz_tac 1));
   9.197 +qed_spec_mp "analz_image_freshK";
   9.198  
   9.199  
   9.200  goal thy
   9.201 - "!!evs. evs : otway lost ==>                               \
   9.202 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   9.203 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
   9.204 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   9.205 -                                   insert_Key_singleton]) 1);
   9.206 -by (Fast_tac 1);
   9.207 -qed "analz_insert_Key_newK";
   9.208 + "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
   9.209 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   9.210 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
   9.211 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   9.212 +qed "analz_insert_freshK";
   9.213  
   9.214  
   9.215  (*** The Key K uniquely identifies the Server's  message. **)
   9.216 @@ -291,8 +224,8 @@
   9.217  by (Fast_tac 2);
   9.218  by (expand_case_tac "K = ?y" 1);
   9.219  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   9.220 -(*...we assume X is a very new message, and handle this case by contradiction*)
   9.221 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   9.222 +(*...we assume X is a recent message, and handle this case by contradiction*)
   9.223 +by (fast_tac (!claset addSEs sees_Spy_partsEs
   9.224                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
   9.225                        addss (!simpset addsimps [parts_insertI])) 1);
   9.226  val lemma = result();
   9.227 @@ -333,8 +266,7 @@
   9.228  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   9.229  (*OR1: creation of new Nonce.  Move assertion into global context*)
   9.230  by (expand_case_tac "NA = ?y" 1);
   9.231 -by (best_tac (!claset addSEs partsEs
   9.232 -                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   9.233 +by (best_tac (!claset addSEs sees_Spy_partsEs) 1);
   9.234  val lemma = result();
   9.235  
   9.236  goal thy 
   9.237 @@ -346,8 +278,6 @@
   9.238  qed "unique_NA";
   9.239  
   9.240  
   9.241 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   9.242 -
   9.243  (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   9.244    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   9.245    over-simplified version of this protocol: see OtwayRees_Bad.*)
   9.246 @@ -358,7 +288,7 @@
   9.247  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   9.248  \             ~: parts (sees lost Spy evs)";
   9.249  by (parts_induct_tac 1);
   9.250 -by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
   9.251 +by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs
   9.252                                addSDs  [impOfSubs parts_insert_subset_Un]
   9.253                                addss (!simpset)) 1));
   9.254  qed_spec_mp"no_nonce_OR1_OR2";
   9.255 @@ -380,16 +310,14 @@
   9.256  by (parts_induct_tac 1);
   9.257  (*OR1: it cannot be a new Nonce, contradiction.*)
   9.258  by (fast_tac (!claset addSIs [parts_insertI]
   9.259 -                      addSEs partsEs
   9.260 -                      addEs [Says_imp_old_nonces RS less_irrefl]
   9.261 +                      addSEs sees_Spy_partsEs
   9.262                        addss (!simpset)) 1);
   9.263  (*OR3 and OR4*) 
   9.264  (*OR4*)
   9.265  by (REPEAT (Safe_step_tac 2));
   9.266  by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   9.267  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   9.268 -                      addEs  partsEs
   9.269 -                      addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   9.270 +                      addEs  sees_Spy_partsEs) 2);
   9.271  (*OR3*)  (** LEVEL 5 **)
   9.272  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   9.273  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   9.274 @@ -420,8 +348,7 @@
   9.275  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   9.276  \                       : set_of_list evs";
   9.277  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   9.278 -                      addEs  partsEs
   9.279 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   9.280 +                      addEs  sees_Spy_partsEs) 1);
   9.281  qed "A_trusts_OR4";
   9.282  
   9.283  
   9.284 @@ -439,11 +366,13 @@
   9.285  by (etac otway.induct 1);
   9.286  by analz_Fake_tac;
   9.287  by (ALLGOALS
   9.288 -    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
   9.289 -				      analz_insert_Key_newK] 
   9.290 -		            setloop split_tac [expand_if])));
   9.291 +    (asm_simp_tac (!simpset addcongs [conj_cong] 
   9.292 +                            addsimps [not_parts_not_analz, analz_insert_freshK]
   9.293 +                            setloop split_tac [expand_if])));
   9.294  (*OR3*)
   9.295 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   9.296 +by (fast_tac (!claset delrules [impCE]
   9.297 +                      addSEs sees_Spy_partsEs
   9.298 +                      addIs [impOfSubs analz_subset_parts]
   9.299                        addss (!simpset addsimps [parts_insert2])) 3);
   9.300  (*OR4, OR2, Fake*) 
   9.301  by (REPEAT_FIRST spy_analz_tac);
   9.302 @@ -453,12 +382,12 @@
   9.303  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   9.304  
   9.305  goal thy 
   9.306 - "!!evs. [| Says Server B \
   9.307 -\            {|NA, Crypt (shrK A) {|NA, K|},                             \
   9.308 -\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   9.309 -\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   9.310 + "!!evs. [| Says Server B                                                \
   9.311 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   9.312 +\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   9.313 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   9.314  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   9.315 -\        ==> K ~: analz (sees lost Spy evs)";
   9.316 +\        ==> Key K ~: analz (sees lost Spy evs)";
   9.317  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   9.318  by (fast_tac (!claset addSEs [lemma]) 1);
   9.319  qed "Spy_not_see_encrypted_key";
   9.320 @@ -467,11 +396,11 @@
   9.321  goal thy 
   9.322   "!!evs. [| C ~: {A,B,Server};                                           \
   9.323  \           Says Server B                                                \
   9.324 -\            {|NA, Crypt (shrK A) {|NA, K|},                             \
   9.325 -\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   9.326 -\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   9.327 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   9.328 +\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   9.329 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   9.330  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   9.331 -\        ==> K ~: analz (sees lost C evs)";
   9.332 +\        ==> Key K ~: analz (sees lost C evs)";
   9.333  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   9.334  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   9.335  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   9.336 @@ -507,7 +436,7 @@
   9.337  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   9.338  (*OR2: creation of new Nonce.  Move assertion into global context*)
   9.339  by (expand_case_tac "NB = ?y" 1);
   9.340 -by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   9.341 +by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1);
   9.342  val lemma = result();
   9.343  
   9.344  goal thy 
   9.345 @@ -537,8 +466,7 @@
   9.346  by (parts_induct_tac 1);
   9.347  (*OR1: it cannot be a new Nonce, contradiction.*)
   9.348  by (fast_tac (!claset addSIs [parts_insertI]
   9.349 -                      addSEs partsEs
   9.350 -                      addEs [Says_imp_old_nonces RS less_irrefl]
   9.351 +                      addSEs sees_Spy_partsEs
   9.352                        addss (!simpset)) 1);
   9.353  (*OR4*)
   9.354  by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   9.355 @@ -570,8 +498,7 @@
   9.356  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   9.357  \                   : set_of_list evs";
   9.358  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   9.359 -                      addEs  partsEs
   9.360 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   9.361 +                      addEs  sees_Spy_partsEs) 1);
   9.362  qed "B_trusts_OR3";
   9.363  
   9.364  
    10.1 --- a/src/HOL/Auth/OtwayRees.thy	Fri Jan 17 11:50:09 1997 +0100
    10.2 +++ b/src/HOL/Auth/OtwayRees.thy	Fri Jan 17 12:49:31 1997 +0100
    10.3 @@ -28,27 +28,26 @@
    10.4            ==> Says Spy B X  # evs : otway lost"
    10.5  
    10.6           (*Alice initiates a protocol run*)
    10.7 -    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
    10.8 -          ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, 
    10.9 -                         Crypt (shrK A)
   10.10 -                           {|Nonce (newN(length evs)), Agent A, Agent B|} |} 
   10.11 +    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
   10.12 +          ==> Says A B {|Nonce NA, Agent A, Agent B, 
   10.13 +                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
   10.14                   # evs : otway lost"
   10.15  
   10.16           (*Bob's response to Alice's message.  Bob doesn't know who 
   10.17  	   the sender is, hence the A' in the sender field.
   10.18             Note that NB is encrypted.*)
   10.19 -    OR2  "[| evs: otway lost;  B ~= Server;
   10.20 +    OR2  "[| evs: otway lost;  B ~= Server;  Nonce NB ~: used evs;
   10.21               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
   10.22            ==> Says B Server 
   10.23                    {|Nonce NA, Agent A, Agent B, X, 
   10.24                      Crypt (shrK B)
   10.25 -                      {|Nonce NA, Nonce(newN(length evs)), Agent A, Agent B|}|}
   10.26 +                      {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
   10.27                   # evs : otway lost"
   10.28  
   10.29           (*The Server receives Bob's message and checks that the three NAs
   10.30             match.  Then he sends a new session key to Bob with a packet for
   10.31             forwarding to Alice.*)
   10.32 -    OR3  "[| evs: otway lost;  B ~= Server;
   10.33 +    OR3  "[| evs: otway lost;  B ~= Server;  Key KAB ~: used evs;
   10.34               Says B' Server 
   10.35                    {|Nonce NA, Agent A, Agent B, 
   10.36                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
   10.37 @@ -56,18 +55,18 @@
   10.38                 : set_of_list evs |]
   10.39            ==> Says Server B 
   10.40                    {|Nonce NA, 
   10.41 -                    Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
   10.42 -                    Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
   10.43 +                    Crypt (shrK A) {|Nonce NA, Key KAB|},
   10.44 +                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
   10.45                   # evs : otway lost"
   10.46  
   10.47           (*Bob receives the Server's (?) message and compares the Nonces with
   10.48  	   those in the message he previously sent the Server.*)
   10.49      OR4  "[| evs: otway lost;  A ~= B;  
   10.50 -             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   10.51 -               : set_of_list evs;
   10.52               Says B Server {|Nonce NA, Agent A, Agent B, X', 
   10.53                               Crypt (shrK B)
   10.54                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
   10.55 +               : set_of_list evs;
   10.56 +             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   10.57                 : set_of_list evs |]
   10.58            ==> Says B A {|Nonce NA, X|} # evs : otway lost"
   10.59  
    11.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 17 11:50:09 1997 +0100
    11.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 17 12:49:31 1997 +0100
    11.3 @@ -26,9 +26,7 @@
    11.4  \             : set_of_list evs";
    11.5  by (REPEAT (resolve_tac [exI,bexI] 1));
    11.6  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    11.7 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    11.8 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    11.9 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
   11.10 +by possibility_tac;
   11.11  result();
   11.12  
   11.13  
   11.14 @@ -54,15 +52,14 @@
   11.15  
   11.16  (** For reasoning about the encrypted portion of messages **)
   11.17  
   11.18 -goal thy "!!evs. Says S B {|X, X'|} : set_of_list evs ==> \
   11.19 +goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
   11.20  \                X : analz (sees lost Spy evs)";
   11.21  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   11.22  qed "OR4_analz_sees_Spy";
   11.23  
   11.24  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
   11.25  \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
   11.26 -by (fast_tac (!claset addSEs partsEs
   11.27 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   11.28 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
   11.29  qed "Oops_parts_sees_Spy";
   11.30  
   11.31  (*OR4_analz_sees_Spy lets us treat those cases using the same 
   11.32 @@ -81,9 +78,9 @@
   11.33  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   11.34  fun parts_induct_tac i = SELECT_GOAL
   11.35      (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
   11.36 -	     (*Fake message*)
   11.37 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   11.38 -					   impOfSubs Fake_parts_insert]
   11.39 +             (*Fake message*)
   11.40 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   11.41 +                                           impOfSubs Fake_parts_insert]
   11.42                                      addss (!simpset)) 2)) THEN
   11.43       (*Base case*)
   11.44       fast_tac (!claset addss (!simpset)) 1 THEN
   11.45 @@ -117,49 +114,18 @@
   11.46  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   11.47  
   11.48  
   11.49 -(*** Future keys can't be seen or used! ***)
   11.50 -
   11.51 -(*Nobody can have SEEN keys that will be generated in the future. *)
   11.52 -goal thy "!!i. evs : otway lost ==>             \
   11.53 -\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   11.54 +(*Nobody can have used non-existent keys!*)
   11.55 +goal thy "!!evs. evs : otway lost ==>          \
   11.56 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   11.57  by (parts_induct_tac 1);
   11.58 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   11.59 -				    addDs [impOfSubs analz_subset_parts,
   11.60 -                                           impOfSubs parts_insert_subset_Un,
   11.61 -                                           Suc_leD]
   11.62 -                                    addss (!simpset))));
   11.63 -qed_spec_mp "new_keys_not_seen";
   11.64 -Addsimps [new_keys_not_seen];
   11.65 -
   11.66 -(*Variant: old messages must contain old keys!*)
   11.67 -goal thy 
   11.68 - "!!evs. [| Says A B X : set_of_list evs;          \
   11.69 -\           Key (newK i) : parts {X};              \
   11.70 -\           evs : otway lost                       \
   11.71 -\        |] ==> i < length evs";
   11.72 -by (rtac ccontr 1);
   11.73 -by (dtac leI 1);
   11.74 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   11.75 -                      addIs  [impOfSubs parts_mono]) 1);
   11.76 -qed "Says_imp_old_keys";
   11.77 -
   11.78 -
   11.79 -(*Nobody can have USED keys that will be generated in the future.
   11.80 -  ...very like new_keys_not_seen*)
   11.81 -goal thy "!!i. evs : otway lost ==>          \
   11.82 -\           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
   11.83 -by (parts_induct_tac 1);
   11.84 -(*Fake, OR4: these messages send unknown (X) components*)
   11.85 -by (EVERY
   11.86 -    (map 
   11.87 -     (best_tac
   11.88 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   11.89 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   11.90 -                      Suc_leD]
   11.91 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   11.92 -               addss (!simpset))) [5,1]));
   11.93 -(*Remaining subgoals*)
   11.94 -by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
   11.95 +(*Fake*)
   11.96 +by (best_tac
   11.97 +      (!claset addIs [impOfSubs analz_subset_parts]
   11.98 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   11.99 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
  11.100 +               addss (!simpset)) 1);
  11.101 +(*OR3*)
  11.102 +by (fast_tac (!claset addss (!simpset)) 1);
  11.103  qed_spec_mp "new_keys_not_used";
  11.104  
  11.105  bind_thm ("new_keys_not_analzd",
  11.106 @@ -174,12 +140,12 @@
  11.107  
  11.108  (*Describes the form of K and NA when the Server sends this message.*)
  11.109  goal thy 
  11.110 - "!!evs. [| Says Server B \
  11.111 -\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
  11.112 -\             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
  11.113 -\           evs : otway lost |]                                               \
  11.114 -\        ==> (EX n. K = Key(newK n)) &                                        \
  11.115 -\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
  11.116 + "!!evs. [| Says Server B                                           \
  11.117 +\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
  11.118 +\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
  11.119 +\             : set_of_list evs;                                    \
  11.120 +\           evs : otway lost |]                                     \
  11.121 +\        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
  11.122  by (etac rev_mp 1);
  11.123  by (etac otway.induct 1);
  11.124  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  11.125 @@ -190,18 +156,17 @@
  11.126  val analz_Fake_tac = 
  11.127      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
  11.128      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
  11.129 -    assume_tac 7 THEN Full_simp_tac 7 THEN
  11.130 +    assume_tac 7 THEN
  11.131      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
  11.132  
  11.133  
  11.134  (****
  11.135   The following is to prove theorems of the form
  11.136  
  11.137 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
  11.138 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
  11.139    Key K : analz (sees lost Spy evs)
  11.140  
  11.141   A more general formula must be proved inductively.
  11.142 -
  11.143  ****)
  11.144  
  11.145  
  11.146 @@ -210,31 +175,28 @@
  11.147  (*The equality makes the induction hypothesis easier to apply*)
  11.148  goal thy  
  11.149   "!!evs. evs : otway lost ==>                                         \
  11.150 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
  11.151 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
  11.152 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
  11.153 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  11.154 +\            (K : KK | Key K : analz (sees lost Spy evs))";
  11.155  by (etac otway.induct 1);
  11.156  by analz_Fake_tac;
  11.157 -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
  11.158 -by (ALLGOALS (*Takes 18 secs*)
  11.159 -    (asm_simp_tac 
  11.160 -     (!simpset addsimps [Un_assoc RS sym, 
  11.161 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
  11.162 -               setloop split_tac [expand_if])));
  11.163 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
  11.164 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  11.165 +(*14 seconds*)
  11.166 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  11.167  (*OR4, Fake*) 
  11.168 -by (EVERY (map spy_analz_tac [4,2]));
  11.169 -(*Oops, OR3, Base*)
  11.170 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
  11.171 -qed_spec_mp "analz_image_newK";
  11.172 +by (EVERY (map spy_analz_tac [3,2]));
  11.173 +(*Base*)
  11.174 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  11.175 +qed_spec_mp "analz_image_freshK";
  11.176  
  11.177  
  11.178  goal thy
  11.179 - "!!evs. evs : otway lost ==>                                          \
  11.180 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
  11.181 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
  11.182 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
  11.183 -                                   insert_Key_singleton]) 1);
  11.184 -by (Fast_tac 1);
  11.185 -qed "analz_insert_Key_newK";
  11.186 + "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
  11.187 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
  11.188 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
  11.189 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  11.190 +qed "analz_insert_freshK";
  11.191  
  11.192  
  11.193  (*** The Key K uniquely identifies the Server's  message. **)
  11.194 @@ -254,8 +216,8 @@
  11.195  by (Fast_tac 2);
  11.196  by (expand_case_tac "K = ?y" 1);
  11.197  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  11.198 -(*...we assume X is a very new message, and handle this case by contradiction*)
  11.199 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
  11.200 +(*...we assume X is a recent message and handle this case by contradiction*)
  11.201 +by (fast_tac (!claset addSEs sees_Spy_partsEs
  11.202                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
  11.203                        addss (!simpset addsimps [parts_insertI])) 1);
  11.204  val lemma = result();
  11.205 @@ -306,8 +268,7 @@
  11.206  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
  11.207  \                   : set_of_list evs";
  11.208  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
  11.209 -                      addEs  partsEs
  11.210 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
  11.211 +                      addEs  sees_Spy_partsEs) 1);
  11.212  qed "A_trusts_OR4";
  11.213  
  11.214  
  11.215 @@ -326,38 +287,43 @@
  11.216  by (etac otway.induct 1);
  11.217  by analz_Fake_tac;
  11.218  by (ALLGOALS
  11.219 -    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
  11.220 -				      analz_insert_Key_newK]
  11.221 -		            setloop split_tac [expand_if])));
  11.222 +    (asm_simp_tac (!simpset addcongs [conj_cong] 
  11.223 +                            addsimps [not_parts_not_analz,
  11.224 +                                      analz_insert_freshK]
  11.225 +                            setloop split_tac [expand_if])));
  11.226  (*OR3*)
  11.227 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
  11.228 +by (fast_tac (!claset delrules [impCE]
  11.229 +                      addSEs sees_Spy_partsEs
  11.230 +                      addIs [impOfSubs analz_subset_parts]
  11.231                        addss (!simpset addsimps [parts_insert2])) 2);
  11.232 +(*Oops*) 
  11.233 +by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
  11.234  (*OR4, Fake*) 
  11.235  by (REPEAT_FIRST spy_analz_tac);
  11.236 -(*Oops*) 
  11.237 -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
  11.238  val lemma = result() RS mp RS mp RSN(2,rev_notE);
  11.239  
  11.240  goal thy 
  11.241 - "!!evs. [| Says Server B                                                     \
  11.242 -\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
  11.243 -\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
  11.244 -\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
  11.245 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
  11.246 -\        ==> K ~: analz (sees lost Spy evs)";
  11.247 + "!!evs. [| Says Server B                                           \
  11.248 +\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
  11.249 +\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
  11.250 +\             : set_of_list evs;                                    \
  11.251 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
  11.252 +\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
  11.253 +\        ==> Key K ~: analz (sees lost Spy evs)";
  11.254  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  11.255  by (fast_tac (!claset addSEs [lemma]) 1);
  11.256  qed "Spy_not_see_encrypted_key";
  11.257  
  11.258  
  11.259  goal thy 
  11.260 - "!!evs. [| C ~: {A,B,Server};                                                \
  11.261 -\           Says Server B                                                     \
  11.262 -\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
  11.263 -\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
  11.264 -\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
  11.265 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
  11.266 -\        ==> K ~: analz (sees lost C evs)";
  11.267 + "!!evs. [| C ~: {A,B,Server};                                      \
  11.268 +\           Says Server B                                           \
  11.269 +\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
  11.270 +\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
  11.271 +\             : set_of_list evs;                                    \
  11.272 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
  11.273 +\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
  11.274 +\        ==> Key K ~: analz (sees lost C evs)";
  11.275  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  11.276  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
  11.277  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
  11.278 @@ -394,6 +360,5 @@
  11.279  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
  11.280  \                     : set_of_list evs";
  11.281  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
  11.282 -                      addEs  partsEs
  11.283 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
  11.284 +                      addEs  sees_Spy_partsEs) 1);
  11.285  qed "B_trusts_OR3";
    12.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Jan 17 11:50:09 1997 +0100
    12.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Jan 17 12:49:31 1997 +0100
    12.3 @@ -7,6 +7,11 @@
    12.4  
    12.5  Simplified version with minimal encryption but explicit messages
    12.6  
    12.7 +Note that the formalization does not even assume that nonces are fresh.
    12.8 +This is because the protocol does not rely on uniqueness of nonces for
    12.9 +security, only for freshness, and the proof script does not prove freshness
   12.10 +properties.
   12.11 +
   12.12  From page 11 of
   12.13    Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
   12.14    IEEE Trans. SE 22 (1), 1996
   12.15 @@ -29,36 +34,31 @@
   12.16  
   12.17           (*Alice initiates a protocol run*)
   12.18      OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
   12.19 -          ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|}
   12.20 -                 # evs : otway lost"
   12.21 +          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost"
   12.22  
   12.23           (*Bob's response to Alice's message.  Bob doesn't know who 
   12.24  	   the sender is, hence the A' in the sender field.*)
   12.25      OR2  "[| evs: otway lost;  B ~= Server;
   12.26               Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
   12.27 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, 
   12.28 -                              Nonce (newN(length evs))|}
   12.29 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   12.30                   # evs : otway lost"
   12.31  
   12.32           (*The Server receives Bob's message.  Then he sends a new
   12.33             session key to Bob with a packet for forwarding to Alice.*)
   12.34 -    OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;
   12.35 +    OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
   12.36               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   12.37                 : set_of_list evs |]
   12.38            ==> Says Server B 
   12.39 -               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, 
   12.40 -                                  Key(newK(length evs))|},
   12.41 -                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 
   12.42 -                                  Key(newK(length evs))|}|}
   12.43 +               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
   12.44 +                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
   12.45                # evs : otway lost"
   12.46  
   12.47           (*Bob receives the Server's (?) message and compares the Nonces with
   12.48  	   those in the message he previously sent the Server.*)
   12.49      OR4  "[| evs: otway lost;  A ~= B;
   12.50 -             Says S B {|X, 
   12.51 -                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
   12.52 +             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   12.53                 : set_of_list evs;
   12.54 -             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   12.55 +             Says S B {|X, Crypt(shrK B){|Nonce NB, Agent A, Agent B, Key K|}|}
   12.56                 : set_of_list evs |]
   12.57            ==> Says B A X # evs : otway lost"
   12.58  
    13.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jan 17 11:50:09 1997 +0100
    13.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jan 17 12:49:31 1997 +0100
    13.3 @@ -29,24 +29,12 @@
    13.4  \                 : set_of_list evs";
    13.5  by (REPEAT (resolve_tac [exI,bexI] 1));
    13.6  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    13.7 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    13.8 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    13.9 -by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
   13.10 +by possibility_tac;
   13.11  result();
   13.12  
   13.13  
   13.14  (**** Inductive proofs about otway ****)
   13.15  
   13.16 -(*The Spy can see more than anybody else, except for their initial state*)
   13.17 -goal thy 
   13.18 - "!!evs. evs : otway ==> \
   13.19 -\     sees lost A evs <= initState lost A Un sees lost Spy evs";
   13.20 -by (etac otway.induct 1);
   13.21 -by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
   13.22 -                                addss (!simpset))));
   13.23 -qed "sees_agent_subset_sees_Spy";
   13.24 -
   13.25 -
   13.26  (*Nobody sends themselves messages*)
   13.27  goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
   13.28  by (etac otway.induct 1);
   13.29 @@ -63,15 +51,14 @@
   13.30  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   13.31  qed "OR2_analz_sees_Spy";
   13.32  
   13.33 -goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
   13.34 +goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
   13.35  \                X : analz (sees lost Spy evs)";
   13.36  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   13.37  qed "OR4_analz_sees_Spy";
   13.38  
   13.39  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
   13.40  \                 ==> K : parts (sees lost Spy evs)";
   13.41 -by (fast_tac (!claset addSEs partsEs
   13.42 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   13.43 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
   13.44  qed "Oops_parts_sees_Spy";
   13.45  
   13.46  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
   13.47 @@ -92,9 +79,9 @@
   13.48  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   13.49  fun parts_induct_tac i = SELECT_GOAL
   13.50      (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
   13.51 -	     (*Fake message*)
   13.52 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   13.53 -					   impOfSubs Fake_parts_insert]
   13.54 +             (*Fake message*)
   13.55 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   13.56 +                                           impOfSubs Fake_parts_insert]
   13.57                                      addss (!simpset)) 2)) THEN
   13.58       (*Base case*)
   13.59       fast_tac (!claset addss (!simpset)) 1 THEN
   13.60 @@ -129,76 +116,18 @@
   13.61  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   13.62  
   13.63  
   13.64 -(*** Future keys can't be seen or used! ***)
   13.65 -
   13.66 -(*Nobody can have SEEN keys that will be generated in the future. *)
   13.67 -goal thy "!!i. evs : otway ==>               \
   13.68 -\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   13.69 -by (parts_induct_tac 1);
   13.70 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   13.71 -				    addDs [impOfSubs analz_subset_parts,
   13.72 -					   impOfSubs parts_insert_subset_Un,
   13.73 -					   Suc_leD]
   13.74 -                                addss (!simpset))));
   13.75 -qed_spec_mp "new_keys_not_seen";
   13.76 -Addsimps [new_keys_not_seen];
   13.77 -
   13.78 -(*Variant: old messages must contain old keys!*)
   13.79 -goal thy 
   13.80 - "!!evs. [| Says A B X : set_of_list evs;          \
   13.81 -\           Key (newK i) : parts {X};    \
   13.82 -\           evs : otway                            \
   13.83 -\        |] ==> i < length evs";
   13.84 -by (rtac ccontr 1);
   13.85 -by (dtac leI 1);
   13.86 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   13.87 -                      addIs  [impOfSubs parts_mono]) 1);
   13.88 -qed "Says_imp_old_keys";
   13.89 -
   13.90 -
   13.91 -(*** Future nonces can't be seen or used! ***)
   13.92 -
   13.93 -goal thy "!!i. evs : otway ==>               \
   13.94 -\              length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
   13.95 +(*Nobody can have used non-existent keys!*)
   13.96 +goal thy "!!evs. evs : otway ==>          \
   13.97 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   13.98  by (parts_induct_tac 1);
   13.99 -by (REPEAT_FIRST
  13.100 -    (fast_tac (!claset addSEs partsEs
  13.101 -	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
  13.102 -		       addEs [leD RS notE]
  13.103 -		       addDs  [impOfSubs analz_subset_parts,
  13.104 -			       impOfSubs parts_insert_subset_Un, Suc_leD]
  13.105 -		       addss (!simpset))));
  13.106 -qed_spec_mp "new_nonces_not_seen";
  13.107 -Addsimps [new_nonces_not_seen];
  13.108 -
  13.109 -(*Variant: old messages must contain old nonces!*)
  13.110 -goal thy 
  13.111 - "!!evs. [| Says A B X : set_of_list evs;            \
  13.112 -\           Nonce (newN i) : parts {X};    \
  13.113 -\           evs : otway                              \
  13.114 -\        |] ==> i < length evs";
  13.115 -by (rtac ccontr 1);
  13.116 -by (dtac leI 1);
  13.117 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
  13.118 -                      addIs  [impOfSubs parts_mono]) 1);
  13.119 -qed "Says_imp_old_nonces";
  13.120 -
  13.121 -
  13.122 -(*Nobody can have USED keys that will be generated in the future.
  13.123 -  ...very like new_keys_not_seen*)
  13.124 -goal thy "!!i. evs : otway ==>               \
  13.125 -\           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
  13.126 -by (parts_induct_tac 1);
  13.127 -(*OR1 and OR3*)
  13.128 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
  13.129 -(*Fake, OR2, OR4: these messages send unknown (X) components*)
  13.130 -by (REPEAT
  13.131 -    (best_tac
  13.132 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
  13.133 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
  13.134 -                      Suc_leD]
  13.135 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
  13.136 -               addss (!simpset)) 1));
  13.137 +(*Fake*)
  13.138 +by (best_tac
  13.139 +      (!claset addIs [impOfSubs analz_subset_parts]
  13.140 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
  13.141 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
  13.142 +               addss (!simpset)) 1);
  13.143 +(*OR1-3*)
  13.144 +by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
  13.145  qed_spec_mp "new_keys_not_used";
  13.146  
  13.147  bind_thm ("new_keys_not_analzd",
  13.148 @@ -214,11 +143,10 @@
  13.149  (*Describes the form of K and NA when the Server sends this message.  Also
  13.150    for Oops case.*)
  13.151  goal thy 
  13.152 - "!!evs. [| Says Server B \
  13.153 -\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
  13.154 -\           evs : otway |]                                           \
  13.155 -\        ==> (EX n. K = Key(newK n)) &                               \
  13.156 -\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
  13.157 + "!!evs. [| Says Server B                                                 \
  13.158 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;   \
  13.159 +\           evs : otway |]                                                \
  13.160 +\     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
  13.161  by (etac rev_mp 1);
  13.162  by (etac otway.induct 1);
  13.163  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  13.164 @@ -229,61 +157,46 @@
  13.165  val analz_Fake_tac = 
  13.166      dtac OR2_analz_sees_Spy 4 THEN 
  13.167      dtac OR4_analz_sees_Spy 6 THEN
  13.168 -    forward_tac [Says_Server_message_form] 7 THEN
  13.169 -    assume_tac 7 THEN Full_simp_tac 7 THEN
  13.170 +    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
  13.171      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
  13.172  
  13.173  
  13.174  (****
  13.175   The following is to prove theorems of the form
  13.176  
  13.177 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
  13.178 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
  13.179    Key K : analz (sees lost Spy evs)
  13.180  
  13.181   A more general formula must be proved inductively.
  13.182 -
  13.183  ****)
  13.184  
  13.185  
  13.186  (** Session keys are not used to encrypt other session keys **)
  13.187  
  13.188 -(*Lemma for the trivial direction of the if-and-only-if*)
  13.189 -goal thy  
  13.190 - "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
  13.191 -\         (K : nE | Key K : analz sEe)  ==>     \
  13.192 -\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
  13.193 -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
  13.194 -val lemma = result();
  13.195 -
  13.196 -
  13.197  (*The equality makes the induction hypothesis easier to apply*)
  13.198  goal thy  
  13.199   "!!evs. evs : otway ==> \
  13.200 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
  13.201 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
  13.202 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
  13.203 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  13.204 +\            (K : KK | Key K : analz (sees lost Spy evs))";
  13.205  by (etac otway.induct 1);
  13.206  by analz_Fake_tac;
  13.207 -by (REPEAT_FIRST (ares_tac [allI, lemma]));
  13.208 -by (ALLGOALS (*Takes 18 secs*)
  13.209 -    (asm_simp_tac 
  13.210 -     (!simpset addsimps [Un_assoc RS sym, 
  13.211 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
  13.212 -               setloop split_tac [expand_if])));
  13.213 -(*OR4, OR2, Fake*) 
  13.214 -by (EVERY (map spy_analz_tac [5,3,2]));
  13.215 -(*Oops, OR3, Base*)
  13.216 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
  13.217 -qed_spec_mp "analz_image_newK";
  13.218 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
  13.219 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  13.220 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  13.221 +(*Base*)
  13.222 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  13.223 +(*Fake, OR2, OR4*) 
  13.224 +by (REPEAT (spy_analz_tac 1));
  13.225 +qed_spec_mp "analz_image_freshK";
  13.226  
  13.227  
  13.228  goal thy
  13.229 - "!!evs. evs : otway ==>                               \
  13.230 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
  13.231 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
  13.232 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
  13.233 -                                   insert_Key_singleton]) 1);
  13.234 -by (Fast_tac 1);
  13.235 -qed "analz_insert_Key_newK";
  13.236 + "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>              \
  13.237 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
  13.238 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
  13.239 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  13.240 +qed "analz_insert_freshK";
  13.241  
  13.242  
  13.243  (*** The Key K uniquely identifies the Server's  message. **)
  13.244 @@ -301,8 +214,8 @@
  13.245  by (Fast_tac 2);
  13.246  by (expand_case_tac "K = ?y" 1);
  13.247  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  13.248 -(*...we assume X is a very new message, and handle this case by contradiction*)
  13.249 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
  13.250 +(*...we assume X is a recent message, and handle this case by contradiction*)
  13.251 +by (fast_tac (!claset addSEs sees_Spy_partsEs
  13.252                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
  13.253                        addss (!simpset addsimps [parts_insertI])) 1);
  13.254  val lemma = result();
  13.255 @@ -328,27 +241,28 @@
  13.256  by (etac otway.induct 1);
  13.257  by analz_Fake_tac;
  13.258  by (ALLGOALS
  13.259 -    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
  13.260 -				      analz_insert_Key_newK]
  13.261 -		            setloop split_tac [expand_if])));
  13.262 +    (asm_simp_tac (!simpset addcongs [conj_cong] 
  13.263 +                            addsimps [not_parts_not_analz, analz_insert_freshK]
  13.264 +                            setloop split_tac [expand_if])));
  13.265  (*OR3*)
  13.266 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
  13.267 +by (fast_tac (!claset delrules [impCE]
  13.268 +                      addSEs sees_Spy_partsEs
  13.269 +                      addIs [impOfSubs analz_subset_parts]
  13.270                        addss (!simpset addsimps [parts_insert2])) 3);
  13.271  (*OR4, OR2, Fake*) 
  13.272  by (REPEAT_FIRST spy_analz_tac);
  13.273  (*Oops*) (** LEVEL 5 **)
  13.274  by (fast_tac (!claset delrules [disjE]
  13.275 -		      addDs [unique_session_keys] addss (!simpset)) 1);
  13.276 +                      addDs [unique_session_keys] addss (!simpset)) 1);
  13.277  val lemma = result() RS mp RS mp RSN(2,rev_notE);
  13.278  
  13.279 -
  13.280  goal thy 
  13.281 - "!!evs. [| Says Server B                                         \
  13.282 -\            {|NA, Crypt (shrK A) {|NA, K|},                      \
  13.283 -\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
  13.284 -\            Says B Spy {|NA, NB, K|} ~: set_of_list evs;         \
  13.285 + "!!evs. [| Says Server B                                                \
  13.286 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
  13.287 +\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
  13.288 +\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
  13.289  \           A ~: lost;  B ~: lost;  evs : otway |]                \
  13.290 -\        ==> K ~: analz (sees lost Spy evs)";
  13.291 +\        ==> Key K ~: analz (sees lost Spy evs)";
  13.292  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  13.293  by (fast_tac (!claset addSEs [lemma]) 1);
  13.294  qed "Spy_not_see_encrypted_key";
  13.295 @@ -359,9 +273,9 @@
  13.296  (*Only OR1 can have caused such a part of a message to appear.
  13.297    I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
  13.298    Perhaps it's because OR2 has two similar-looking encrypted messages in
  13.299 -	this version.*)
  13.300 +        this version.*)
  13.301  goal thy 
  13.302 - "!!evs. [| A ~: lost;  A ~= B; evs : otway |]                 \
  13.303 + "!!evs. [| A ~: lost;  A ~= B;  evs : otway |]                \
  13.304  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
  13.305  \             : parts (sees lost Spy evs) -->                  \
  13.306  \            Says A B {|NA, Agent A, Agent B,                  \
  13.307 @@ -390,15 +304,13 @@
  13.308  by (parts_induct_tac 1);
  13.309  (*OR1: it cannot be a new Nonce, contradiction.*)
  13.310  by (fast_tac (!claset addSIs [parts_insertI]
  13.311 -                      addSEs partsEs
  13.312 -                      addEs [Says_imp_old_nonces RS less_irrefl]
  13.313 +                      addSEs sees_Spy_partsEs
  13.314                        addss (!simpset)) 1);
  13.315  (*OR4*)
  13.316  by (REPEAT (Safe_step_tac 2));
  13.317  by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
  13.318  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
  13.319 -                      addEs  partsEs
  13.320 -                      addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
  13.321 +                      addEs  sees_Spy_partsEs) 2);
  13.322  (*OR3*)  (** LEVEL 5 **)
  13.323  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
  13.324  by (step_tac (!claset delrules [disjCI, impCE]) 1);
    14.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Jan 17 11:50:09 1997 +0100
    14.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Jan 17 12:49:31 1997 +0100
    14.3 @@ -27,26 +27,25 @@
    14.4            ==> Says Spy B X  # evs : otway"
    14.5  
    14.6           (*Alice initiates a protocol run*)
    14.7 -    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    14.8 -          ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, 
    14.9 -                         Crypt (shrK A) 
   14.10 -                            {|Nonce (newN(length evs)), Agent A, Agent B|} |} 
   14.11 +    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
   14.12 +          ==> Says A B {|Nonce NA, Agent A, Agent B, 
   14.13 +                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
   14.14                   # evs : otway"
   14.15  
   14.16           (*Bob's response to Alice's message.  Bob doesn't know who 
   14.17  	   the sender is, hence the A' in the sender field.
   14.18             We modify the published protocol by NOT encrypting NB.*)
   14.19 -    OR2  "[| evs: otway;  B ~= Server;
   14.20 +    OR2  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
   14.21               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
   14.22            ==> Says B Server 
   14.23 -                  {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)), 
   14.24 +                  {|Nonce NA, Agent A, Agent B, X, Nonce NB,
   14.25                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   14.26                   # evs : otway"
   14.27  
   14.28           (*The Server receives Bob's message and checks that the three NAs
   14.29             match.  Then he sends a new session key to Bob with a packet for
   14.30             forwarding to Alice.*)
   14.31 -    OR3  "[| evs: otway;  B ~= Server;
   14.32 +    OR3  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
   14.33               Says B' Server 
   14.34                    {|Nonce NA, Agent A, Agent B, 
   14.35                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
   14.36 @@ -55,16 +54,16 @@
   14.37                 : set_of_list evs |]
   14.38            ==> Says Server B 
   14.39                    {|Nonce NA, 
   14.40 -                    Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
   14.41 -                    Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
   14.42 +                    Crypt (shrK A) {|Nonce NA, Key KAB|},
   14.43 +                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
   14.44                   # evs : otway"
   14.45  
   14.46           (*Bob receives the Server's (?) message and compares the Nonces with
   14.47  	   those in the message he previously sent the Server.*)
   14.48      OR4  "[| evs: otway;  A ~= B;
   14.49 -             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   14.50 +             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
   14.51                 : set_of_list evs;
   14.52 -             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
   14.53 +             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   14.54                 : set_of_list evs |]
   14.55            ==> Says B A {|Nonce NA, X|} # evs : otway"
   14.56  
    15.1 --- a/src/HOL/Auth/Public.ML	Fri Jan 17 11:50:09 1997 +0100
    15.2 +++ b/src/HOL/Auth/Public.ML	Fri Jan 17 12:49:31 1997 +0100
    15.3 @@ -158,18 +158,20 @@
    15.4  AddIffs [Nonce_notin_initState];
    15.5  
    15.6  goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
    15.7 -be (impOfSubs parts_mono) 1;
    15.8 +by (etac (impOfSubs parts_mono) 1);
    15.9  by (Fast_tac 1);
   15.10  qed "usedI";
   15.11  
   15.12  AddIs [usedI];
   15.13  
   15.14 -(*Yields a supply of fresh nonces for possibility theorems.*)
   15.15 +(** A supply of fresh nonces for possibility theorems. **)
   15.16 +
   15.17  goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   15.18  by (list.induct_tac "evs" 1);
   15.19  by (res_inst_tac [("x","0")] exI 1);
   15.20  by (Step_tac 1);
   15.21  by (Full_simp_tac 1);
   15.22 +(*Inductive step*)
   15.23  by (event.induct_tac "a" 1);
   15.24  by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
   15.25  by (msg.induct_tac "msg" 1);
   15.26 @@ -184,11 +186,18 @@
   15.27  val lemma = result();
   15.28  
   15.29  goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
   15.30 -br (lemma RS exE) 1;
   15.31 -br selectI 1;
   15.32 +by (rtac (lemma RS exE) 1);
   15.33 +by (rtac selectI 1);
   15.34  by (Fast_tac 1);
   15.35  qed "Nonce_supply";
   15.36  
   15.37 +(*Tactic for possibility theorems*)
   15.38 +val possibility_tac =
   15.39 +    REPEAT 
   15.40 +    (ALLGOALS (simp_tac (!simpset setsolver safe_solver))
   15.41 +     THEN
   15.42 +     REPEAT_FIRST (eq_assume_tac ORELSE' 
   15.43 +                   resolve_tac [refl, conjI, Nonce_supply]));
   15.44  
   15.45  (** Power of the Spy **)
   15.46  
    16.1 --- a/src/HOL/Auth/Recur.ML	Fri Jan 17 11:50:09 1997 +0100
    16.2 +++ b/src/HOL/Auth/Recur.ML	Fri Jan 17 12:49:31 1997 +0100
    16.3 @@ -10,29 +10,26 @@
    16.4  
    16.5  proof_timing:=true;
    16.6  HOL_quantifiers := false;
    16.7 -Pretty.setdepth 25;
    16.8 +Pretty.setdepth 30;
    16.9  
   16.10  
   16.11  (** Possibility properties: traces that reach the end 
   16.12 -	ONE theorem would be more elegant and faster!
   16.13 -	By induction on a list of agents (no repetitions)
   16.14 +        ONE theorem would be more elegant and faster!
   16.15 +        By induction on a list of agents (no repetitions)
   16.16  **)
   16.17  
   16.18 +
   16.19  (*Simplest case: Alice goes directly to the server*)
   16.20  goal thy
   16.21   "!!A. A ~= Server   \
   16.22  \ ==> EX K NA. EX evs: recur lost.          \
   16.23 -\     Says Server A {|Agent A,              \
   16.24 -\                     Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
   16.25 +\     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
   16.26  \                       Agent Server|}      \
   16.27  \         : set_of_list evs";
   16.28  by (REPEAT (resolve_tac [exI,bexI] 1));
   16.29  by (rtac (recur.Nil RS recur.RA1 RS 
   16.30 -	  (respond.One RSN (4,recur.RA3))) 2);
   16.31 -by (REPEAT
   16.32 -    (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
   16.33 -     THEN
   16.34 -     REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
   16.35 +          (respond.One RSN (4,recur.RA3))) 2);
   16.36 +by possibility_tac;
   16.37  result();
   16.38  
   16.39  
   16.40 @@ -40,44 +37,42 @@
   16.41  goal thy
   16.42   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
   16.43  \ ==> EX K. EX NA. EX evs: recur lost.          \
   16.44 -\       Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   16.45 +\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   16.46  \                       Agent Server|}                          \
   16.47  \         : set_of_list evs";
   16.48 +by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
   16.49 +by (REPEAT (eresolve_tac [exE, conjE] 1));
   16.50  by (REPEAT (resolve_tac [exI,bexI] 1));
   16.51  by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
   16.52 -	  (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
   16.53 -	  recur.RA4) 2);
   16.54 -bw HPair_def;
   16.55 -by (REPEAT
   16.56 -    (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
   16.57 -     THEN
   16.58 -     ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
   16.59 +          (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
   16.60 +          recur.RA4) 2);
   16.61 +by basic_possibility_tac;
   16.62 +by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
   16.63 +			       less_not_refl2 RS not_sym] 1));
   16.64  result();
   16.65  
   16.66  
   16.67 -(*Case three: Alice, Bob, Charlie and the server*)
   16.68 +(*Case three: Alice, Bob, Charlie and the server
   16.69  goal thy
   16.70 - "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
   16.71 + "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
   16.72  \ ==> EX K. EX NA. EX evs: recur lost.          \
   16.73 -\       Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   16.74 +\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   16.75  \                       Agent Server|}                          \
   16.76  \         : set_of_list evs";
   16.77 +by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
   16.78 +by (REPEAT (eresolve_tac [exE, conjE] 1));
   16.79  by (REPEAT (resolve_tac [exI,bexI] 1));
   16.80  by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
   16.81 -	  (respond.One RS respond.Cons RS respond.Cons RSN
   16.82 -	   (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
   16.83 -bw HPair_def;
   16.84 -by (REPEAT	(*SLOW: 37 seconds*)
   16.85 -    (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
   16.86 -     THEN
   16.87 -     ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
   16.88 -by (ALLGOALS 
   16.89 -    (SELECT_GOAL (DEPTH_SOLVE
   16.90 -		  (swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND 
   16.91 -		   etac not_sym 1))));
   16.92 +          (respond.One RS respond.Cons RS respond.Cons RSN
   16.93 +           (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
   16.94 +(*SLOW: 70 seconds*)
   16.95 +by basic_possibility_tac;
   16.96 +by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
   16.97 +		 ORELSE
   16.98 +		 eresolve_tac [asm_rl, less_not_refl2, 
   16.99 +			       less_not_refl2 RS not_sym] 1));
  16.100  result();
  16.101 -
  16.102 -
  16.103 +****************)
  16.104  
  16.105  (**** Inductive proofs about recur ****)
  16.106  
  16.107 @@ -99,10 +94,30 @@
  16.108  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
  16.109  
  16.110  
  16.111 +
  16.112 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
  16.113 +by (etac respond.induct 1);
  16.114 +by (ALLGOALS Simp_tac);
  16.115 +qed "respond_Key_in_parts";
  16.116 +
  16.117 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
  16.118 +by (etac respond.induct 1);
  16.119 +by (REPEAT (assume_tac 1));
  16.120 +qed "respond_imp_not_used";
  16.121 +
  16.122 +goal thy
  16.123 + "!!evs. [| Key K : parts {RB};  (PB,RB,K') : respond evs |] \
  16.124 +\        ==> Key K ~: used evs";
  16.125 +by (etac rev_mp 1);
  16.126 +by (etac respond.induct 1);
  16.127 +by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
  16.128 +             !simpset));
  16.129 +qed_spec_mp "Key_in_parts_respond";
  16.130 +
  16.131  (*Simple inductive reasoning about responses*)
  16.132 -goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i";
  16.133 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
  16.134  by (etac respond.induct 1);
  16.135 -by (REPEAT (ares_tac responses.intrs 1));
  16.136 +by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
  16.137  qed "respond_imp_responses";
  16.138  
  16.139  
  16.140 @@ -110,7 +125,7 @@
  16.141  
  16.142  val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
  16.143  
  16.144 -goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
  16.145 +goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \
  16.146  \                ==> RA : analz (sees lost Spy evs)";
  16.147  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
  16.148  qed "RA4_analz_sees_Spy";
  16.149 @@ -131,8 +146,8 @@
  16.150      let val tac = forw_inst_tac [("lost","lost")] 
  16.151      in  tac RA2_parts_sees_Spy 4              THEN
  16.152          etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
  16.153 -	forward_tac [respond_imp_responses] 5 THEN
  16.154 -	tac RA4_parts_sees_Spy 6
  16.155 +        forward_tac [respond_imp_responses] 5 THEN
  16.156 +        tac RA4_parts_sees_Spy 6
  16.157      end;
  16.158  
  16.159  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
  16.160 @@ -153,14 +168,6 @@
  16.161  (** Spy never sees another agent's long-term key (unless initially lost) **)
  16.162  
  16.163  goal thy 
  16.164 - "!!evs. (j,PB,RB) : respond i \
  16.165 -\  ==> Key K : parts {RB} --> (EX j'. K = newK2(i,j') & j<=j')";
  16.166 -be respond.induct 1;
  16.167 -by (Auto_tac());
  16.168 -by (best_tac (!claset addDs [Suc_leD]) 1);
  16.169 -qed_spec_mp "Key_in_parts_respond";
  16.170 -
  16.171 -goal thy 
  16.172   "!!evs. evs : recur lost \
  16.173  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
  16.174  by (parts_induct_tac 1);
  16.175 @@ -189,115 +196,30 @@
  16.176  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
  16.177  
  16.178  
  16.179 -(*** Future keys can't be seen or used! ***)
  16.180 +
  16.181 +(** Nobody can have used non-existent keys! **)
  16.182  
  16.183 -(*Nobody can have SEEN keys that will be generated in the future. *)
  16.184 -goal thy "!!evs. evs : recur lost ==> \
  16.185 -\                length evs <= i -->   \
  16.186 -\                Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
  16.187 -by (parts_induct_tac 1);
  16.188 -(*RA2*)
  16.189 -by (best_tac (!claset addSEs partsEs 
  16.190 -	              addSDs [parts_cut]
  16.191 -                      addDs  [Suc_leD]
  16.192 -                      addss  (!simpset)) 3);
  16.193 -(*Fake*)
  16.194 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
  16.195 -			     impOfSubs parts_insert_subset_Un,
  16.196 -			     Suc_leD]
  16.197 -		      addss (!simpset)) 1);
  16.198 -(*For RA3*)
  16.199 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
  16.200 -(*RA1-RA4*)
  16.201 -by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
  16.202 -		              addss (!simpset)) 1));
  16.203 -qed_spec_mp "new_keys_not_seen";
  16.204 -Addsimps [new_keys_not_seen];
  16.205 -
  16.206 -(*Variant: old messages must contain old keys!*)
  16.207 -goal thy 
  16.208 - "!!evs. [| Says A B X : set_of_list evs;     \
  16.209 -\           Key (newK2(i,j)) : parts {X};     \
  16.210 -\           evs : recur lost                 \
  16.211 -\        |] ==> i < length evs";
  16.212 -by (rtac ccontr 1);
  16.213 -by (dtac leI 1);
  16.214 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
  16.215 -                      addIs  [impOfSubs parts_mono]) 1);
  16.216 -qed "Says_imp_old_keys";
  16.217 -
  16.218 -
  16.219 -(*** Future nonces can't be seen or used! ***)
  16.220 -
  16.221 -goal thy 
  16.222 - "!!evs. (j, PB, RB) : respond i \
  16.223 -\        ==> Nonce N : parts {RB} --> Nonce N : parts {PB}";
  16.224 -be respond.induct 1;
  16.225 +goal thy
  16.226 + "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
  16.227 +\        ==> K : range shrK";
  16.228 +by (etac rev_mp 1);
  16.229 +by (etac (respond_imp_responses RS responses.induct) 1);
  16.230  by (Auto_tac());
  16.231 -qed_spec_mp "Nonce_in_parts_respond";
  16.232 +qed_spec_mp "Key_in_keysFor_parts";
  16.233  
  16.234  
  16.235 -goal thy "!!i. evs : recur lost ==> \
  16.236 -\              length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
  16.237 -by (parts_induct_tac 1);
  16.238 -(*For RA3*)
  16.239 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
  16.240 -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  16.241 -                        addDs  [Nonce_in_parts_respond, parts_cut, Suc_leD]
  16.242 -			addss (!simpset)) 0 4);
  16.243 -(*Fake*)
  16.244 -by (fast_tac (!claset addDs  [impOfSubs analz_subset_parts,
  16.245 -			      impOfSubs parts_insert_subset_Un,
  16.246 -			      Suc_leD]
  16.247 -		      addss (!simpset)) 1);
  16.248 -(*RA1, RA2, RA4*)
  16.249 -by (REPEAT_FIRST  (fast_tac (!claset 
  16.250 -                              addSEs partsEs
  16.251 -                              addEs [leD RS notE]
  16.252 -                              addDs [Suc_leD]
  16.253 -                              addss (!simpset))));
  16.254 -qed_spec_mp "new_nonces_not_seen";
  16.255 -Addsimps [new_nonces_not_seen];
  16.256 -
  16.257 -(*Variant: old messages must contain old nonces!*)
  16.258 -goal thy "!!evs. [| Says A B X : set_of_list evs;    \
  16.259 -\                   Nonce (newN i) : parts {X};      \
  16.260 -\                   evs : recur lost                 \
  16.261 -\                |] ==> i < length evs";
  16.262 -by (rtac ccontr 1);
  16.263 -by (dtac leI 1);
  16.264 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
  16.265 -                      addIs  [impOfSubs parts_mono]) 1);
  16.266 -qed "Says_imp_old_nonces";
  16.267 -
  16.268 -
  16.269 -(** Nobody can have USED keys that will be generated in the future. **)
  16.270 -
  16.271 -goal thy
  16.272 - "!!evs. (j,PB,RB) : respond i \
  16.273 -\        ==> K : keysFor (parts {RB}) --> (EX A. K = shrK A)";
  16.274 -be (respond_imp_responses RS responses.induct) 1;
  16.275 -by (Auto_tac());
  16.276 -qed_spec_mp "Key_in_keysFor_parts_respond";
  16.277 -
  16.278 -
  16.279 -goal thy "!!i. evs : recur lost ==>          \
  16.280 -\       length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
  16.281 +goal thy "!!evs. evs : recur lost ==>          \
  16.282 +\       Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
  16.283  by (parts_induct_tac 1);
  16.284  (*RA3*)
  16.285 -by (fast_tac (!claset addDs  [Key_in_keysFor_parts_respond, Suc_leD]
  16.286 -		      addss  (!simpset addsimps [parts_insert_sees])) 4);
  16.287 -(*RA2*)
  16.288 -by (fast_tac (!claset addSEs partsEs 
  16.289 -	              addDs  [Suc_leD] addss (!simpset)) 3);
  16.290 -(*Fake, RA1, RA4*)
  16.291 -by (REPEAT 
  16.292 -    (best_tac
  16.293 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
  16.294 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
  16.295 -                      Suc_leD]
  16.296 -               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
  16.297 -               addss (!simpset)) 1));
  16.298 +by (best_tac (!claset addDs  [Key_in_keysFor_parts]
  16.299 +                      addss  (!simpset addsimps [parts_insert_sees])) 2);
  16.300 +(*Fake*)
  16.301 +by (best_tac
  16.302 +      (!claset addIs [impOfSubs analz_subset_parts]
  16.303 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
  16.304 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
  16.305 +               addss (!simpset)) 1);
  16.306  qed_spec_mp "new_keys_not_used";
  16.307  
  16.308  
  16.309 @@ -319,86 +241,82 @@
  16.310      dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
  16.311  
  16.312  
  16.313 -Delsimps [image_insert];
  16.314 -
  16.315  (** Session keys are not used to encrypt other session keys **)
  16.316  
  16.317  (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
  16.318    Note that it holds for *any* set H (not just "sees lost Spy evs")
  16.319    satisfying the inductive hypothesis.*)
  16.320  goal thy  
  16.321 - "!!evs. [| RB : responses i;                             \
  16.322 -\           ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
  16.323 -\           (K : newK``I | Key K : analz H) |]                \
  16.324 -\       ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \
  16.325 -\           (K : newK``I | Key K : analz (insert RB H))";
  16.326 -be responses.induct 1;
  16.327 -by (ALLGOALS
  16.328 -    (asm_simp_tac 
  16.329 -     (!simpset addsimps [insert_Key_singleton, insert_Key_image, 
  16.330 -			 Un_assoc RS sym, pushKey_newK]
  16.331 -               setloop split_tac [expand_if])));
  16.332 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  16.333 -qed "resp_analz_image_newK_lemma";
  16.334 + "!!evs. [| RB : responses evs;                             \
  16.335 +\           ALL K KK. KK <= Compl (range shrK) -->          \
  16.336 +\                     (Key K : analz (Key``KK Un H)) =      \
  16.337 +\                     (K : KK | Key K : analz H) |]         \
  16.338 +\       ==> ALL K KK. KK <= Compl (range shrK) -->          \
  16.339 +\                     (Key K : analz (insert RB (Key``KK Un H))) = \
  16.340 +\                     (K : KK | Key K : analz (insert RB H))";
  16.341 +by (etac responses.induct 1);
  16.342 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  16.343 +qed "resp_analz_image_freshK_lemma";
  16.344  
  16.345  (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
  16.346  goal thy  
  16.347 - "!!evs. evs : recur lost ==>                                            \
  16.348 -\  ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
  16.349 -\           (K : newK``I | Key K : analz (sees lost Spy evs))";
  16.350 + "!!evs. evs : recur lost ==>                                   \
  16.351 +\  ALL K KK. KK <= Compl (range shrK) -->                       \
  16.352 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  16.353 +\            (K : KK | Key K : analz (sees lost Spy evs))";
  16.354  by (etac recur.induct 1);
  16.355  by analz_Fake_tac;
  16.356 -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
  16.357 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
  16.358 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
  16.359 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  16.360 +by (ALLGOALS 
  16.361 +    (asm_simp_tac
  16.362 +     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
  16.363  (*Base*)
  16.364  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  16.365  (*RA4, RA2, Fake*) 
  16.366  by (REPEAT (spy_analz_tac 1));
  16.367 -val raw_analz_image_newK = result();
  16.368 -qed_spec_mp "analz_image_newK";
  16.369 +val raw_analz_image_freshK = result();
  16.370 +qed_spec_mp "analz_image_freshK";
  16.371  
  16.372  
  16.373  (*Instance of the lemma with H replaced by (sees lost Spy evs):
  16.374 -   [| RB : responses i;  evs : recur lost |]
  16.375 -   ==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) =
  16.376 -       (xa : newK``x | Key xa : analz (insert RB (sees lost Spy evs))) 
  16.377 +   [| RB : responses evs;  evs : recur lost; |]
  16.378 +   ==> KK <= Compl (range shrK) --> 
  16.379 +       Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
  16.380 +       (K : KK | Key K : analz (insert RB (sees lost Spy evs))) 
  16.381  *)
  16.382 -bind_thm ("resp_analz_image_newK",
  16.383 -	  raw_analz_image_newK RSN
  16.384 -	    (2, resp_analz_image_newK_lemma) RS spec RS spec);
  16.385 +bind_thm ("resp_analz_image_freshK",
  16.386 +          raw_analz_image_freshK RSN
  16.387 +            (2, resp_analz_image_freshK_lemma) RS spec RS spec);
  16.388  
  16.389  goal thy
  16.390 - "!!evs. evs : recur lost ==>                               \
  16.391 -\        Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \
  16.392 -\        (K = newK x | Key K : analz (sees lost Spy evs))";
  16.393 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
  16.394 -                                   insert_Key_singleton]) 1);
  16.395 -by (Fast_tac 1);
  16.396 -qed "analz_insert_Key_newK";
  16.397 + "!!evs. [| evs : recur lost;  KAB ~: range shrK |] ==>              \
  16.398 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =      \
  16.399 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
  16.400 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  16.401 +qed "analz_insert_freshK";
  16.402  
  16.403  
  16.404 -(*This is more general than proving Hash_new_nonces_not_seen: we don't prove
  16.405 -  that "future nonces" can't be hashed, but that everything that's hashed is
  16.406 -  already in past traffic. *)
  16.407 +(*Everything that's hashed is already in past traffic. *)
  16.408  goal thy "!!i. [| evs : recur lost;  A ~: lost |] ==>              \
  16.409  \              Hash {|Key(shrK A), X|} : parts (sees lost Spy evs) -->  \
  16.410  \              X : parts (sees lost Spy evs)";
  16.411 -be recur.induct 1;
  16.412 +by (etac recur.induct 1);
  16.413  by parts_Fake_tac;
  16.414  (*RA3 requires a further induction*)
  16.415 -be responses.induct 5;
  16.416 +by (etac responses.induct 5);
  16.417  by (ALLGOALS Asm_simp_tac);
  16.418  (*Fake*)
  16.419  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
  16.420 -			     impOfSubs Fake_parts_insert]
  16.421 -	              addss (!simpset addsimps [parts_insert_sees])) 2);
  16.422 +                             impOfSubs Fake_parts_insert]
  16.423 +                      addss (!simpset addsimps [parts_insert_sees])) 2);
  16.424  (*Two others*)
  16.425  by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
  16.426  bind_thm ("Hash_imp_body", result() RSN (2, rev_mp));
  16.427  
  16.428  
  16.429  (** The Nonce NA uniquely identifies A's message. 
  16.430 -    This theorem applies to rounds RA1 and RA2!
  16.431 +    This theorem applies to steps RA1 and RA2!
  16.432  
  16.433    Unicity is not used in other proofs but is desirable in its own right.
  16.434  **)
  16.435 @@ -409,29 +327,20 @@
  16.436  \        Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
  16.437  \          : parts (sees lost Spy evs)  -->  B=B' & P=P'";
  16.438  by (parts_induct_tac 1);
  16.439 -be responses.induct 3;
  16.440 +by (etac responses.induct 3);
  16.441  by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
  16.442  by (step_tac (!claset addSEs partsEs) 1);
  16.443 -(*RA1: creation of new Nonce.  Move assertion into global context*)
  16.444 -by (expand_case_tac "NA = ?y" 1);
  16.445 -by (best_tac (!claset addSIs [exI]
  16.446 -                      addSDs [Hash_imp_body]
  16.447 -		      addSEs (new_nonces_not_seen::partsEs)
  16.448 -		      addss (!simpset)) 1);
  16.449 -by (best_tac (!claset addss  (!simpset)) 1);
  16.450 -(*RA2: creation of new Nonce*)
  16.451 -by (expand_case_tac "NA = ?y" 1);
  16.452 -by (best_tac (!claset addSIs [exI]
  16.453 -		      addSDs [Hash_imp_body]
  16.454 -		      addSEs (new_nonces_not_seen::partsEs)
  16.455 -		      addss  (!simpset)) 1);
  16.456 -by (best_tac (!claset addss  (!simpset)) 1);
  16.457 +(*RA1,2: creation of new Nonce.  Move assertion into global context*)
  16.458 +by (ALLGOALS (expand_case_tac "NA = ?y"));
  16.459 +by (REPEAT_FIRST (ares_tac [exI]));
  16.460 +by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
  16.461 +                              addSEs sees_Spy_partsEs) 1));
  16.462  val lemma = result();
  16.463  
  16.464  goalw thy [HPair_def]
  16.465 - "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|}   \
  16.466 + "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}   \
  16.467  \            : parts (sees lost Spy evs);                          \
  16.468 -\          HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
  16.469 +\          Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \
  16.470  \            : parts (sees lost Spy evs);                          \
  16.471  \          evs : recur lost;  A ~: lost |]                         \
  16.472  \        ==> B=B' & P=P'";
  16.473 @@ -445,39 +354,36 @@
  16.474  ***)
  16.475  
  16.476  goal thy
  16.477 - "!!evs. [| RB : responses i;  evs : recur lost |] \
  16.478 + "!!evs. [| RB : responses evs;  evs : recur lost |] \
  16.479  \ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
  16.480 -be responses.induct 1;
  16.481 +by (etac responses.induct 1);
  16.482  by (ALLGOALS
  16.483      (asm_simp_tac 
  16.484 -     (!simpset addsimps [resp_analz_image_newK, insert_Key_singleton]
  16.485 -               setloop split_tac [expand_if])));
  16.486 +     (analz_image_freshK_ss addsimps [Spy_analz_shrK,
  16.487 +                                      resp_analz_image_freshK])));
  16.488  qed "shrK_in_analz_respond";
  16.489  Addsimps [shrK_in_analz_respond];
  16.490  
  16.491  
  16.492  goal thy  
  16.493 - "!!evs. [| RB : responses i;                             \
  16.494 -\           ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
  16.495 -\           (K : newK``I | Key K : analz H) |]                \
  16.496 + "!!evs. [| RB : responses evs;                             \
  16.497 +\           ALL K KK. KK <= Compl (range shrK) -->          \
  16.498 +\                     (Key K : analz (Key``KK Un H)) =      \
  16.499 +\                     (K : KK | Key K : analz H) |]         \
  16.500  \       ==> (Key K : analz (insert RB H)) --> \
  16.501 -\                  (Key K : parts{RB} | Key K : analz H)";
  16.502 -be responses.induct 1;
  16.503 +\           (Key K : parts{RB} | Key K : analz H)";
  16.504 +by (etac responses.induct 1);
  16.505  by (ALLGOALS
  16.506      (asm_simp_tac 
  16.507 -     (!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert,
  16.508 -			 resp_analz_image_newK_lemma,
  16.509 -			 insert_Key_singleton, insert_Key_image, 
  16.510 -			 Un_assoc RS sym, pushKey_newK]
  16.511 -               setloop split_tac [expand_if])));
  16.512 -(*The "Message" simpset gives the standard treatment of "image"*)
  16.513 -by (simp_tac (simpset_of "Message") 1);
  16.514 +     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
  16.515 +(*Simplification using two distinct treatments of "image"*)
  16.516 +by (simp_tac (!simpset addsimps [parts_insert2]) 1);
  16.517  by (fast_tac (!claset delrules [allE]) 1);
  16.518  qed "resp_analz_insert_lemma";
  16.519  
  16.520  bind_thm ("resp_analz_insert",
  16.521 -	  raw_analz_image_newK RSN
  16.522 -	    (2, resp_analz_insert_lemma) RSN(2, rev_mp));
  16.523 +          raw_analz_image_freshK RSN
  16.524 +            (2, resp_analz_insert_lemma) RSN(2, rev_mp));
  16.525  
  16.526  
  16.527  (*The Server does not send such messages.  This theorem lets us avoid
  16.528 @@ -487,44 +393,51 @@
  16.529  \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
  16.530  \                  ~: set_of_list evs";
  16.531  by (etac recur.induct 1);
  16.532 -be (respond.induct) 5;
  16.533 +by (etac (respond.induct) 5);
  16.534  by (Auto_tac());
  16.535  qed_spec_mp "Says_Server_not";
  16.536  AddSEs [Says_Server_not RSN (2,rev_notE)];
  16.537  
  16.538  
  16.539 +(*The last key returned by respond indeed appears in a certificate*)
  16.540  goal thy 
  16.541 - "!!i. (j,PB,RB) : respond i               \
  16.542 -\  ==> EX A' B'. ALL A B N.                \
  16.543 + "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
  16.544 +\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
  16.545 +by (etac respond.elim 1);
  16.546 +by (ALLGOALS Asm_full_simp_tac);
  16.547 +qed "respond_certificate";
  16.548 +
  16.549 +
  16.550 +goal thy 
  16.551 + "!!K'. (PB,RB,KXY) : respond evs               \
  16.552 +\  ==> EX A' B'. ALL A B N.              \
  16.553  \        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
  16.554  \          -->   (A'=A & B'=B) | (A'=B & B'=A)";
  16.555 -be respond.induct 1;
  16.556 +by (etac respond.induct 1);
  16.557  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
  16.558  (*Base case*)
  16.559  by (Fast_tac 1);
  16.560  by (Step_tac 1);
  16.561 +(*Case analysis on K=KBC*)
  16.562  by (expand_case_tac "K = ?y" 1);
  16.563 +by (dtac respond_Key_in_parts 1);
  16.564  by (best_tac (!claset addSIs [exI]
  16.565                        addSEs partsEs
  16.566 -                      addDs [Key_in_parts_respond]
  16.567 -                      addss (!simpset)) 1);
  16.568 +                      addDs [Key_in_parts_respond]) 1);
  16.569 +(*Case analysis on K=KAB*)
  16.570  by (expand_case_tac "K = ?y" 1);
  16.571  by (REPEAT (ares_tac [exI] 2));
  16.572  by (ex_strip_tac 1);
  16.573 -be respond.elim 1;
  16.574 -by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac));
  16.575 -by (ALLGOALS (asm_full_simp_tac 
  16.576 -	      (!simpset addsimps [all_conj_distrib, ex_disj_distrib]))); 
  16.577 -by (Fast_tac 1);
  16.578 +by (dtac respond_certificate 1);
  16.579  by (Fast_tac 1);
  16.580  val lemma = result();
  16.581  
  16.582  goal thy 
  16.583   "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};    \
  16.584  \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
  16.585 -\          (j,PB,RB) : respond i |]               \
  16.586 +\          (PB,RB,KXY) : respond evs |]               \
  16.587  \ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
  16.588 -by (prove_unique_tac lemma 1);	(*50 seconds??, due to the disjunctions*)
  16.589 +by (prove_unique_tac lemma 1);  (*50 seconds??, due to the disjunctions*)
  16.590  qed "unique_session_keys";
  16.591  
  16.592  
  16.593 @@ -533,47 +446,34 @@
  16.594      the premises, e.g. by having A=Spy **)
  16.595  
  16.596  goal thy 
  16.597 - "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
  16.598 -\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
  16.599 -be respond.elim 1;
  16.600 -by (ALLGOALS Asm_full_simp_tac);
  16.601 -qed "newK2_respond_lemma";
  16.602 -
  16.603 -
  16.604 -goal thy 
  16.605 - "!!evs. [| (j,PB,RB) : respond (length evs);  evs : recur lost |]       \
  16.606 + "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur lost |]       \
  16.607  \        ==> ALL A A' N. A ~: lost & A' ~: lost -->  \
  16.608  \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
  16.609  \            Key K ~: analz (insert RB (sees lost Spy evs))";
  16.610 -be respond.induct 1;
  16.611 +by (etac respond.induct 1);
  16.612  by (forward_tac [respond_imp_responses] 2);
  16.613 -by (ALLGOALS (*4 MINUTES???*)
  16.614 +by (forward_tac [respond_imp_not_used] 2);
  16.615 +by (ALLGOALS (*43 seconds*)
  16.616      (asm_simp_tac 
  16.617 -     (!simpset addsimps 
  16.618 -	  ([analz_image_newK, not_parts_not_analz,
  16.619 -	    read_instantiate [("H", "?ff``?xx")] parts_insert,
  16.620 -	    Un_assoc RS sym, resp_analz_image_newK,
  16.621 -	    insert_Key_singleton, analz_insert_Key_newK])
  16.622 -      setloop split_tac [expand_if])));
  16.623 -by (ALLGOALS (simp_tac (simpset_of "Message")));
  16.624 -by (Fast_tac 1);
  16.625 +     (analz_image_freshK_ss addsimps 
  16.626 +          [analz_image_freshK, not_parts_not_analz,
  16.627 +           shrK_in_analz_respond,
  16.628 +           read_instantiate [("H", "?ff``?xx")] parts_insert,
  16.629 +           resp_analz_image_freshK, analz_insert_freshK])));
  16.630 +by (ALLGOALS Simp_tac);
  16.631 +by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
  16.632  by (step_tac (!claset addSEs [MPair_parts]) 1);
  16.633 -(** LEVEL 6 **)
  16.634 -by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond]
  16.635 -                      addSEs [new_keys_not_seen RS not_parts_not_analz 
  16.636 -			      RSN(2,rev_notE)]
  16.637 -                      addss (!simpset)) 4);
  16.638 -by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3);
  16.639 +(** LEVEL 7 **)
  16.640 +by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
  16.641 +                      addDs  [impOfSubs analz_subset_parts]) 4);
  16.642 +by (fast_tac (!claset addSDs [respond_certificate]) 3);
  16.643  by (best_tac (!claset addSEs partsEs
  16.644                        addDs [Key_in_parts_respond]
  16.645                        addss (!simpset)) 2);
  16.646 -by (thin_tac "ALL x.?P(x)" 1);
  16.647 -be respond.elim 1;
  16.648 -by (fast_tac (!claset addss (!simpset)) 1);
  16.649 -by (step_tac (!claset addss (!simpset)) 1);
  16.650 -by (best_tac (!claset addSEs partsEs
  16.651 -                      addDs [Key_in_parts_respond]
  16.652 -                      addss (!simpset)) 1);
  16.653 +by (dtac unique_session_keys 1);
  16.654 +by (etac respond_certificate 1);
  16.655 +by (assume_tac 1);
  16.656 +by (Fast_tac 1);
  16.657  qed_spec_mp "respond_Spy_not_see_encrypted_key";
  16.658  
  16.659  
  16.660 @@ -586,7 +486,7 @@
  16.661  by analz_Fake_tac;
  16.662  by (ALLGOALS
  16.663      (asm_simp_tac
  16.664 -     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] 
  16.665 +     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] 
  16.666                 setloop split_tac [expand_if])));
  16.667  (*RA4*)
  16.668  by (spy_analz_tac 4);
  16.669 @@ -596,13 +496,14 @@
  16.670  (*RA2*)
  16.671  by (spy_analz_tac 1);
  16.672  (*RA3, case 2: K is an old key*)
  16.673 -by (fast_tac (!claset addSDs [resp_analz_insert]
  16.674 -		      addSEs partsEs
  16.675 -                      addDs [Key_in_parts_respond]
  16.676 -	              addEs [Says_imp_old_keys RS less_irrefl]) 2);
  16.677 +by (best_tac (!claset addSDs [resp_analz_insert]
  16.678 +                      addSEs partsEs
  16.679 +                      addDs [Key_in_parts_respond, 
  16.680 +                             Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)]
  16.681 +                      addss (!simpset)) 2);
  16.682  (*RA3, case 1: use lemma previously proved by induction*)
  16.683  by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
  16.684 -			      (2,rev_notE)]) 1);
  16.685 +                              (2,rev_notE)]) 1);
  16.686  bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
  16.687  
  16.688  
  16.689 @@ -622,34 +523,29 @@
  16.690  (**** Authenticity properties for Agents ****)
  16.691  
  16.692  (*The response never contains Hashes*)
  16.693 -(*NEEDED????????????????*)
  16.694  goal thy
  16.695 - "!!evs. (j,PB,RB) : respond i \
  16.696 + "!!evs. (PB,RB,K) : respond evs \
  16.697  \        ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
  16.698  \            Hash {|Key (shrK B), M|} : parts H";
  16.699 -be (respond_imp_responses RS responses.induct) 1;
  16.700 +by (etac (respond_imp_responses RS responses.induct) 1);
  16.701  by (Auto_tac());
  16.702  bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
  16.703  
  16.704 -(*NEEDED????????????????*)
  16.705  (*Only RA1 or RA2 can have caused such a part of a message to appear.*)
  16.706  goalw thy [HPair_def]
  16.707   "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
  16.708  \             : parts (sees lost Spy evs);                        \
  16.709  \            A ~: lost;  evs : recur lost |]                        \
  16.710 -\        ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|})  \
  16.711 +\        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
  16.712  \             : set_of_list evs";
  16.713 -be rev_mp 1;
  16.714 +by (etac rev_mp 1);
  16.715  by (parts_induct_tac 1);
  16.716  (*RA3*)
  16.717  by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
  16.718  qed_spec_mp "Hash_auth_sender";
  16.719  
  16.720  
  16.721 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
  16.722 -
  16.723 -
  16.724 -(** These two results should subsume (for all agents) the guarantees proved
  16.725 +(** These two results subsume (for all agents) the guarantees proved
  16.726      separately for A and B in the Otway-Rees protocol.
  16.727  **)
  16.728  
    17.1 --- a/src/HOL/Auth/Recur.thy	Fri Jan 17 11:50:09 1997 +0100
    17.2 +++ b/src/HOL/Auth/Recur.thy	Fri Jan 17 12:49:31 1997 +0100
    17.3 @@ -8,56 +8,47 @@
    17.4  
    17.5  Recur = Shared +
    17.6  
    17.7 -syntax
    17.8 -  newK2    :: "nat*nat => key"
    17.9 -
   17.10 -translations
   17.11 -  "newK2 x"  == "newK(nPair x)"
   17.12 -
   17.13  (*Two session keys are distributed to each agent except for the initiator,
   17.14 -	who receives one.
   17.15 +        who receives one.
   17.16    Perhaps the two session keys could be bundled into a single message.
   17.17  *)
   17.18 -consts     respond :: "nat => (nat*msg*msg)set"
   17.19 -inductive "respond i"	(*Server's response to the nested message*)
   17.20 +consts     respond :: "event list => (msg*msg*key)set"
   17.21 +inductive "respond evs" (*Server's response to the nested message*)
   17.22    intrs
   17.23      (*The message "Agent Server" marks the end of a list.*)
   17.24  
   17.25 -    One  "A ~= Server
   17.26 -          ==> (j, HPair (Key(shrK A)) 
   17.27 +    One  "[| A ~= Server;  Key KAB ~: used evs |]
   17.28 +          ==> (Hash[Key(shrK A)] 
   17.29                          {|Agent A, Agent B, Nonce NA, Agent Server|}, 
   17.30 -                  {|Agent A, 
   17.31 -                    Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|}, 
   17.32 -                    Agent Server|})
   17.33 -              : respond i"
   17.34 +               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
   17.35 +               KAB)   : respond evs"
   17.36  
   17.37      (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
   17.38 -    Cons "[| (Suc j, PA, RA) : respond i;
   17.39 -             PA = HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|};
   17.40 +    Cons "[| (PA, RA, KAB) : respond evs;  
   17.41 +             Key KBC ~: used evs;  Key KBC ~: parts {RA};
   17.42 +             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
   17.43               B ~= Server |]
   17.44 -          ==> (j, HPair (Key(shrK B)) {|Agent B, Agent C, Nonce NB, PA|}, 
   17.45 -                  {|Agent B, 
   17.46 -                    Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|},
   17.47 -                    Agent B, 
   17.48 -                    Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|}, 
   17.49 -                    RA|})
   17.50 -              : respond i"
   17.51 +          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
   17.52 +               {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
   17.53 +                 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
   17.54 +                 RA|},
   17.55 +               KBC)
   17.56 +              : respond evs"
   17.57  
   17.58  
   17.59  (*Induction over "respond" can be difficult due to the complexity of the
   17.60    subgoals.  The "responses" relation formalizes the general form of its
   17.61    third component.
   17.62  *)
   17.63 -consts     responses :: nat => msg set
   17.64 -inductive "responses i" 	
   17.65 +consts     responses :: event list => msg set
   17.66 +inductive "responses evs"       
   17.67    intrs
   17.68      (*Server terminates lists*)
   17.69 -    Nil  "Agent Server : responses i"
   17.70 +    Nil  "Agent Server : responses evs"
   17.71  
   17.72 -    Cons "RA : responses i
   17.73 -          ==> {|Agent B, 
   17.74 -                Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|},
   17.75 -                RA|}  : responses i"
   17.76 +    Cons "[| RA : responses evs;  Key KAB ~: used evs |]
   17.77 +          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
   17.78 +                RA|}  : responses evs"
   17.79  
   17.80  
   17.81  consts     recur   :: agent set => event list set
   17.82 @@ -75,40 +66,36 @@
   17.83  
   17.84           (*Alice initiates a protocol run.
   17.85             "Agent Server" is just a placeholder, to terminate the nesting.*)
   17.86 -    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server |]
   17.87 +    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
   17.88            ==> Says A B 
   17.89 -                (HPair (Key(shrK A)) 
   17.90 -                 {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|})
   17.91 +                (Hash[Key(shrK A)] 
   17.92 +                 {|Agent A, Agent B, Nonce NA, Agent Server|})
   17.93                # evs : recur lost"
   17.94  
   17.95           (*Bob's response to Alice's message.  C might be the Server.
   17.96             XA should be the Hash of the remaining components with KA, but
   17.97 -		Bob cannot check that.
   17.98 +                Bob cannot check that.
   17.99             P is the previous recur message from Alice's caller.
  17.100             NOTE: existing proofs don't need PA and are complicated by its
  17.101 -		presence!  See parts_Fake_tac.*)
  17.102 -    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
  17.103 +                presence!  See parts_Fake_tac.*)
  17.104 +    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
  17.105               Says A' B PA : set_of_list evs;  
  17.106               PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
  17.107 -          ==> Says B C 
  17.108 -                (HPair (Key(shrK B))
  17.109 -                 {|Agent B, Agent C, Nonce (newN(length evs)), PA|})
  17.110 +          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
  17.111                # evs : recur lost"
  17.112  
  17.113           (*The Server receives and decodes Bob's message.  Then he generates
  17.114             a new session key and a response.*)
  17.115      RA3  "[| evs: recur lost;  B ~= Server;
  17.116               Says B' Server PB : set_of_list evs;
  17.117 -             (0,PB,RB) : respond (length evs) |]
  17.118 +             (PB,RB,K) : respond evs |]
  17.119            ==> Says Server B RB # evs : recur lost"
  17.120  
  17.121           (*Bob receives the returned message and compares the Nonces with
  17.122 -	   those in the message he previously sent the Server.*)
  17.123 +           those in the message he previously sent the Server.*)
  17.124      RA4  "[| evs: recur lost;  A ~= B;  
  17.125 -             Says C' B {|Agent B, 
  17.126 -                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
  17.127 -                         Agent B, 
  17.128 -                         Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|}
  17.129 +             Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
  17.130 +                         Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
  17.131                 : set_of_list evs;
  17.132               Says B  C {|XH, Agent B, Agent C, Nonce NB, 
  17.133                           XA, Agent A, Agent B, Nonce NA, P|} 
    18.1 --- a/src/HOL/Auth/Shared.ML	Fri Jan 17 11:50:09 1997 +0100
    18.2 +++ b/src/HOL/Auth/Shared.ML	Fri Jan 17 12:49:31 1997 +0100
    18.3 @@ -28,18 +28,16 @@
    18.4  
    18.5  (*Injectiveness and freshness of new keys and nonces*)
    18.6  AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, 
    18.7 -	 inj_newK RS inj_eq, inj_nPair RS inj_eq];
    18.8 +         inj_newK RS inj_eq, inj_nPair RS inj_eq];
    18.9  
   18.10  (* invKey (shrK A) = shrK A *)
   18.11 -bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
   18.12 +bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys);
   18.13  
   18.14 -(* invKey (newK i) = newK i *)
   18.15 -bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
   18.16 -Addsimps [invKey_shrK, invKey_newK];
   18.17 +Addsimps [invKey_id];
   18.18  
   18.19  goal thy "!!K. newK i = invKey K ==> newK i = K";
   18.20  by (rtac (invKey_eq RS iffD1) 1);
   18.21 -by (Simp_tac 1);
   18.22 +by (Full_simp_tac 1);
   18.23  val newK_invKey = result();
   18.24  
   18.25  AddSDs [newK_invKey, sym RS newK_invKey];
   18.26 @@ -54,12 +52,7 @@
   18.27  by (Auto_tac ());
   18.28  qed "newK_notin_initState";
   18.29  
   18.30 -goal thy "Nonce (newN i) ~: parts (initState lost B)";
   18.31 -by (agent.induct_tac "B" 1);
   18.32 -by (Auto_tac ());
   18.33 -qed "newN_notin_initState";
   18.34 -
   18.35 -AddIffs [newK_notin_initState, newN_notin_initState];
   18.36 +AddIffs [newK_notin_initState];
   18.37  
   18.38  goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
   18.39  by (agent.induct_tac "C" 1);
   18.40 @@ -156,6 +149,10 @@
   18.41  by (Auto_tac ());
   18.42  qed_spec_mp "Says_imp_sees_Spy";
   18.43  
   18.44 +(*Use with addSEs to derive contradictions from old Says events containing
   18.45 +  items known to be fresh*)
   18.46 +val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
   18.47 +
   18.48  goal thy  
   18.49   "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
   18.50  \        ==> X : analz (sees lost Spy evs)";
   18.51 @@ -194,6 +191,181 @@
   18.52  Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
   18.53  
   18.54  
   18.55 +(*** Fresh nonces ***)
   18.56 +
   18.57 +goal thy "Nonce N ~: parts (initState lost B)";
   18.58 +by (agent.induct_tac "B" 1);
   18.59 +by (Auto_tac ());
   18.60 +qed "Nonce_notin_initState";
   18.61 +
   18.62 +AddIffs [Nonce_notin_initState];
   18.63 +
   18.64 +goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
   18.65 +by (etac (impOfSubs parts_mono) 1);
   18.66 +by (Fast_tac 1);
   18.67 +qed "usedI";
   18.68 +
   18.69 +AddIs [usedI];
   18.70 +
   18.71 +(** Fresh keys never clash with long-term shared keys **)
   18.72 +
   18.73 +goal thy "Key (shrK A) : used evs";
   18.74 +by (Best_tac 1);
   18.75 +qed "shrK_in_used";
   18.76 +AddIffs [shrK_in_used];
   18.77 +
   18.78 +(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
   18.79 +  from long-term shared keys*)
   18.80 +goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
   18.81 +by (Best_tac 1);
   18.82 +qed "Key_not_used";
   18.83 +
   18.84 +(*A session key cannot clash with a long-term shared key*)
   18.85 +goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
   18.86 +by (Fast_tac 1);
   18.87 +qed "shrK_neq";
   18.88 +
   18.89 +Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
   18.90 +
   18.91 +
   18.92 +goal thy "used (Says A B X # evs) = parts{X} Un used evs";
   18.93 +by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
   18.94 +qed "used_Says";
   18.95 +Addsimps [used_Says];
   18.96 +
   18.97 +goal thy "used [] <= used l";
   18.98 +by (list.induct_tac "l" 1);
   18.99 +by (event.induct_tac "a" 2);
  18.100 +by (ALLGOALS Asm_simp_tac);
  18.101 +by (Best_tac 1);
  18.102 +qed "used_nil_subset";
  18.103 +
  18.104 +goal thy "used l <= used (l@l')";
  18.105 +by (list.induct_tac "l" 1);
  18.106 +by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
  18.107 +by (event.induct_tac "a" 1);
  18.108 +by (Asm_simp_tac 1);
  18.109 +by (Best_tac 1);
  18.110 +qed "used_subset_append";
  18.111 +
  18.112 +
  18.113 +(*** Supply fresh nonces for possibility theorems. ***)
  18.114 +
  18.115 +goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
  18.116 +by (list.induct_tac "evs" 1);
  18.117 +by (res_inst_tac [("x","0")] exI 1);
  18.118 +by (Step_tac 1);
  18.119 +by (Full_simp_tac 1);
  18.120 +(*Inductive step*)
  18.121 +by (event.induct_tac "a" 1);
  18.122 +by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
  18.123 +by (msg.induct_tac "msg" 1);
  18.124 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
  18.125 +by (Step_tac 1);
  18.126 +(*MPair case*)
  18.127 +by (res_inst_tac [("x","Na+Nb")] exI 2);
  18.128 +by (fast_tac (!claset addSEs [add_leE]) 2);
  18.129 +(*Nonce case*)
  18.130 +by (res_inst_tac [("x","N + Suc nat")] exI 1);
  18.131 +by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
  18.132 +val lemma = result();
  18.133 +
  18.134 +goal thy "EX N. Nonce N ~: used evs";
  18.135 +by (rtac (lemma RS exE) 1);
  18.136 +by (Fast_tac 1);
  18.137 +qed "Nonce_supply1";
  18.138 +
  18.139 +goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
  18.140 +by (cut_inst_tac [("evs","evs")] lemma 1);
  18.141 +by (cut_inst_tac [("evs","evs'")] lemma 1);
  18.142 +by (Step_tac 1);
  18.143 +by (res_inst_tac [("x","N")] exI 1);
  18.144 +by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
  18.145 +by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
  18.146 +				     le_add2, le_add1, 
  18.147 +				     le_eq_less_Suc RS sym]) 1);
  18.148 +qed "Nonce_supply2";
  18.149 +
  18.150 +goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
  18.151 +\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
  18.152 +by (cut_inst_tac [("evs","evs")] lemma 1);
  18.153 +by (cut_inst_tac [("evs","evs'")] lemma 1);
  18.154 +by (cut_inst_tac [("evs","evs''")] lemma 1);
  18.155 +by (Step_tac 1);
  18.156 +by (res_inst_tac [("x","N")] exI 1);
  18.157 +by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
  18.158 +by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
  18.159 +by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
  18.160 +				     le_add2, le_add1, 
  18.161 +				     le_eq_less_Suc RS sym]) 1);
  18.162 +by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
  18.163 +by (stac (le_eq_less_Suc RS sym) 1);
  18.164 +by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
  18.165 +by (REPEAT (rtac le_add1 1));
  18.166 +qed "Nonce_supply3";
  18.167 +
  18.168 +goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
  18.169 +by (rtac (lemma RS exE) 1);
  18.170 +by (rtac selectI 1);
  18.171 +by (Fast_tac 1);
  18.172 +qed "Nonce_supply";
  18.173 +
  18.174 +(*** Supply fresh keys for possibility theorems. ***)
  18.175 +
  18.176 +goal thy "EX K. Key K ~: used evs";
  18.177 +by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
  18.178 +by (Fast_tac 1);
  18.179 +qed "Key_supply1";
  18.180 +
  18.181 +val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
  18.182 +
  18.183 +goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
  18.184 +by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
  18.185 +by (etac exE 1);
  18.186 +by (cut_inst_tac [("evs","evs'")] 
  18.187 +    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
  18.188 +by (Auto_tac());
  18.189 +qed "Key_supply2";
  18.190 +
  18.191 +goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
  18.192 +\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
  18.193 +by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
  18.194 +by (etac exE 1);
  18.195 +by (cut_inst_tac [("evs","evs'")] 
  18.196 +    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
  18.197 +by (etac exE 1);
  18.198 +by (cut_inst_tac [("evs","evs''")] 
  18.199 +    (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
  18.200 +by (Step_tac 1);
  18.201 +by (Full_simp_tac 1);
  18.202 +by (fast_tac (!claset addSEs [allE]) 1);
  18.203 +qed "Key_supply3";
  18.204 +
  18.205 +goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
  18.206 +by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
  18.207 +by (rtac selectI 1);
  18.208 +by (Fast_tac 1);
  18.209 +qed "Key_supply";
  18.210 +
  18.211 +(*** Tactics for possibility theorems ***)
  18.212 +
  18.213 +val possibility_tac =
  18.214 +    REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
  18.215 +    (ALLGOALS (simp_tac 
  18.216 +               (!simpset delsimps [used_Says] setsolver safe_solver))
  18.217 +     THEN
  18.218 +     REPEAT_FIRST (eq_assume_tac ORELSE' 
  18.219 +                   resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
  18.220 +
  18.221 +(*For harder protocols (such as Recur) where we have to set up some
  18.222 +  nonces and keys initially*)
  18.223 +val basic_possibility_tac =
  18.224 +    REPEAT 
  18.225 +    (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
  18.226 +     THEN
  18.227 +     REPEAT_FIRST (resolve_tac [refl, conjI]));
  18.228 +
  18.229 +
  18.230  (** Power of the Spy **)
  18.231  
  18.232  (*The Spy can see more than anybody else, except for their initial state*)
  18.233 @@ -227,25 +399,35 @@
  18.234  (*Push newK applications in, allowing other keys to be pulled out*)
  18.235  val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
  18.236  
  18.237 -Delsimps [image_insert];
  18.238 -Addsimps [image_insert RS sym];
  18.239 -
  18.240 -Delsimps [image_Un];
  18.241 -Addsimps [image_Un RS sym];
  18.242 -
  18.243 -goal thy "insert (Key (newK x)) H = Key `` (newK``{x}) Un H";
  18.244 +goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
  18.245  by (Fast_tac 1);
  18.246 -qed "insert_Key_singleton";
  18.247 +qed "subset_Compl_range";
  18.248  
  18.249  goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
  18.250  \         Key `` (f `` (insert x E)) Un C";
  18.251  by (Fast_tac 1);
  18.252  qed "insert_Key_image";
  18.253  
  18.254 +goal thy "insert (Key K) H = Key `` {K} Un H";
  18.255 +by (Fast_tac 1);
  18.256 +qed "insert_Key_singleton";
  18.257 +
  18.258 +goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
  18.259 +by (Fast_tac 1);
  18.260 +qed "insert_Key_image'";
  18.261 +
  18.262 +val analz_image_freshK_ss = 
  18.263 +     !simpset delsimps [image_insert, image_Un]
  18.264 +              addsimps ([image_insert RS sym, image_Un RS sym,
  18.265 +                         Key_not_used, 
  18.266 +                         insert_Key_singleton, subset_Compl_range,
  18.267 +                         insert_Key_image', Un_assoc RS sym]
  18.268 +                        @disj_comms)
  18.269 +              setloop split_tac [expand_if];
  18.270  
  18.271  (*Lemma for the trivial direction of the if-and-only-if*)
  18.272  goal thy  
  18.273   "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
  18.274  \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
  18.275  by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
  18.276 -qed "analz_image_newK_lemma";
  18.277 +qed "analz_image_freshK_lemma";
    19.1 --- a/src/HOL/Auth/Shared.thy	Fri Jan 17 11:50:09 1997 +0100
    19.2 +++ b/src/HOL/Auth/Shared.thy	Fri Jan 17 12:49:31 1997 +0100
    19.3 @@ -8,13 +8,14 @@
    19.4  Server keys; initial states of agents; new nonces and keys; function "sees" 
    19.5  *)
    19.6  
    19.7 -Shared = Message + List + 
    19.8 +Shared = Message + List + Finite +
    19.9  
   19.10  consts
   19.11    shrK    :: agent => key  (*symmetric keys*)
   19.12  
   19.13  rules
   19.14 -  isSym_shrK "isSymKey (shrK A)"
   19.15 +  (*ALL keys are symmetric*)
   19.16 +  isSym_keys "isSymKey K"
   19.17  
   19.18  consts  (*Initial states of agents -- parameter of the construction*)
   19.19    initState :: [agent set, agent] => msg set
   19.20 @@ -44,6 +45,23 @@
   19.21    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
   19.22  
   19.23  
   19.24 +constdefs
   19.25 +  (*Set of items that might be visible to somebody: complement of the set
   19.26 +        of fresh items*)
   19.27 +  used :: event list => msg set
   19.28 +    "used evs == parts (UN lost B. sees lost B evs)"
   19.29 +
   19.30 +
   19.31 +rules
   19.32 +  (*Unlike the corresponding property of nonces, this cannot be proved.
   19.33 +    We have infinitely many agents and there is nothing to stop their
   19.34 +    long-term keys from exhausting all the natural numbers.  The axiom
   19.35 +    assumes that their keys are dispersed so as to leave room for infinitely
   19.36 +    many fresh session keys.  We could, alternatively, restrict agents to
   19.37 +    an unspecified finite number.*)
   19.38 +  Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
   19.39 +
   19.40 +
   19.41  (*Agents generate random (symmetric) keys and nonces.
   19.42    The numeric argument is typically the length of the current trace.
   19.43    An injective pairing function allows multiple keys/nonces to be generated
   19.44 @@ -63,6 +81,5 @@
   19.45    inj_newK        "inj newK"
   19.46  
   19.47    newK_neq_shrK   "newK i ~= shrK A" 
   19.48 -  isSym_newK      "isSymKey (newK i)"
   19.49  
   19.50  end
    20.1 --- a/src/HOL/Auth/WooLam.ML	Fri Jan 17 11:50:09 1997 +0100
    20.2 +++ b/src/HOL/Auth/WooLam.ML	Fri Jan 17 12:49:31 1997 +0100
    20.3 @@ -25,10 +25,11 @@
    20.4  \                 : set_of_list evs";
    20.5  by (REPEAT (resolve_tac [exI,bexI] 1));
    20.6  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
    20.7 -	  woolam.WL4 RS woolam.WL5) 2);
    20.8 +          woolam.WL4 RS woolam.WL5) 2);
    20.9  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
   20.10  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
   20.11 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
   20.12 +by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
   20.13 +                                    addss (!simpset setsolver safe_solver))));
   20.14  result();
   20.15  
   20.16  
   20.17 @@ -94,23 +95,6 @@
   20.18  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   20.19  
   20.20  
   20.21 -(*** Future nonces can't be seen or used! ***)
   20.22 -
   20.23 -goal thy "!!i. evs : woolam ==>             \
   20.24 -\             length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)";
   20.25 -by (parts_induct_tac 1);
   20.26 -by (REPEAT_FIRST (fast_tac (!claset 
   20.27 -                              addSEs partsEs
   20.28 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   20.29 -                              addEs [leD RS notE]
   20.30 -			      addDs  [impOfSubs analz_subset_parts,
   20.31 -                                      impOfSubs parts_insert_subset_Un,
   20.32 -                                      Suc_leD]
   20.33 -                              addss (!simpset))));
   20.34 -qed_spec_mp "new_nonces_not_seen";
   20.35 -Addsimps [new_nonces_not_seen];
   20.36 -
   20.37 -
   20.38  (**** Autheticity properties for Woo-Lam ****)
   20.39  
   20.40  
   20.41 @@ -201,6 +185,5 @@
   20.42  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   20.43  by (parts_induct_tac 1);
   20.44  by (Step_tac 1);
   20.45 -by (best_tac (!claset addSEs partsEs
   20.46 -                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   20.47 +by (best_tac (!claset addSEs partsEs) 1);
   20.48  **)
    21.1 --- a/src/HOL/Auth/WooLam.thy	Fri Jan 17 11:50:09 1997 +0100
    21.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Jan 17 12:49:31 1997 +0100
    21.3 @@ -35,16 +35,16 @@
    21.4            ==> Says A B (Agent A) # evs : woolam"
    21.5  
    21.6           (*Bob responds to Alice's message with a challenge.*)
    21.7 -    WL2  "[| evs: woolam;  A ~= B;
    21.8 +    WL2  "[| evs: woolam;  A ~= B;  
    21.9               Says A' B (Agent A) : set_of_list evs |]
   21.10 -          ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
   21.11 +          ==> Says B A (Nonce NB) # evs : woolam"
   21.12  
   21.13           (*Alice responds to Bob's challenge by encrypting NB with her key.
   21.14             B is *not* properly determined -- Alice essentially broadcasts
   21.15             her reply.*)
   21.16      WL3  "[| evs: woolam;  A ~= B;
   21.17 -             Says B' A (Nonce NB) : set_of_list evs;
   21.18 -             Says A  B (Agent A)  : set_of_list evs |]
   21.19 +             Says A  B (Agent A)  : set_of_list evs;
   21.20 +             Says B' A (Nonce NB) : set_of_list evs |]
   21.21            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
   21.22  
   21.23           (*Bob forwards Alice's response to the Server.*)
    22.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Jan 17 11:50:09 1997 +0100
    22.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jan 17 12:49:31 1997 +0100
    22.3 @@ -14,7 +14,7 @@
    22.4  
    22.5  proof_timing:=true;
    22.6  HOL_quantifiers := false;
    22.7 -Pretty.setdepth 20;
    22.8 +Pretty.setdepth 25;
    22.9  
   22.10  
   22.11  (*A "possibility property": there are traces that reach the end*)
   22.12 @@ -23,9 +23,9 @@
   22.13  \        ==> EX X NB K. EX evs: yahalom lost.          \
   22.14  \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
   22.15  by (REPEAT (resolve_tac [exI,bexI] 1));
   22.16 -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
   22.17 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
   22.18 -by (ALLGOALS Fast_tac);
   22.19 +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
   22.20 +          yahalom.YM4) 2);
   22.21 +by possibility_tac;
   22.22  result();
   22.23  
   22.24  
   22.25 @@ -115,64 +115,20 @@
   22.26  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   22.27  
   22.28  
   22.29 -(*** Future keys can't be seen or used! ***)
   22.30 -
   22.31 -(*Nobody can have SEEN keys that will be generated in the future. *)
   22.32 -goal thy "!!i. evs : yahalom lost ==>        \
   22.33 -\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   22.34 +(*Nobody can have used non-existent keys!*)
   22.35 +goal thy "!!evs. evs : yahalom lost ==>          \
   22.36 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   22.37  by (parts_induct_tac 1);
   22.38 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   22.39 -				    addDs [impOfSubs analz_subset_parts,
   22.40 -                                           impOfSubs parts_insert_subset_Un,
   22.41 -                                           Suc_leD]
   22.42 -                                    addss (!simpset))));
   22.43 -qed_spec_mp "new_keys_not_seen";
   22.44 -Addsimps [new_keys_not_seen];
   22.45 -
   22.46 -(*Variant: old messages must contain old keys!*)
   22.47 -goal thy 
   22.48 - "!!evs. [| Says A B X : set_of_list evs;          \
   22.49 -\           Key (newK i) : parts {X};    \
   22.50 -\           evs : yahalom lost                     \
   22.51 -\        |] ==> i < length evs";
   22.52 -by (rtac ccontr 1);
   22.53 -by (dtac leI 1);
   22.54 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   22.55 -                      addIs  [impOfSubs parts_mono]) 1);
   22.56 -qed "Says_imp_old_keys";
   22.57 -
   22.58 -
   22.59 -(*Ready-made for the classical reasoner*)
   22.60 -goal thy "!!evs. [| Says A B {|Crypt K {|b,Key(newK(length evs)),na,nb|}, X|}\
   22.61 -\                   : set_of_list evs;  evs : yahalom lost |]              \
   22.62 -\                ==> R";
   22.63 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   22.64 -                      addss (!simpset addsimps [parts_insertI])) 1);
   22.65 -qed "Says_too_new_key";
   22.66 -AddSEs [Says_too_new_key];
   22.67 -
   22.68 -
   22.69 -(*Nobody can have USED keys that will be generated in the future.
   22.70 -  ...very like new_keys_not_seen*)
   22.71 -goal thy "!!i. evs : yahalom lost ==>        \
   22.72 -\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
   22.73 -by (parts_induct_tac 1);
   22.74 -(*YM1, YM2 and YM3*)
   22.75 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   22.76 -(*Fake and Oops: these messages send unknown (X) components*)
   22.77 -by (EVERY
   22.78 -    (map (fast_tac
   22.79 -          (!claset addDs [impOfSubs analz_subset_parts,
   22.80 -                          impOfSubs (analz_subset_parts RS keysFor_mono),
   22.81 -                          impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   22.82 -                          Suc_leD]
   22.83 -                   addss (!simpset))) [3,1]));
   22.84 -(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
   22.85 -by (fast_tac
   22.86 -      (!claset addSEs partsEs
   22.87 -               addSDs [Says_imp_sees_Spy RS parts.Inj]
   22.88 -               addEs [new_keys_not_seen RSN(2,rev_notE)]
   22.89 -               addDs [Suc_leD]) 1);
   22.90 +(*YM4: Key K is not fresh!*)
   22.91 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
   22.92 +(*YM3*)
   22.93 +by (fast_tac (!claset addss (!simpset)) 2);
   22.94 +(*Fake*)
   22.95 +by (best_tac
   22.96 +      (!claset addIs [impOfSubs analz_subset_parts]
   22.97 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   22.98 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   22.99 +               addss (!simpset)) 1);
  22.100  qed_spec_mp "new_keys_not_used";
  22.101  
  22.102  bind_thm ("new_keys_not_analzd",
  22.103 @@ -185,10 +141,10 @@
  22.104  (*Describes the form of K when the Server sends this message.  Useful for
  22.105    Oops as well as main secrecy property.*)
  22.106  goal thy 
  22.107 - "!!evs. [| Says Server A                                                    \
  22.108 -\            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
  22.109 -\           evs : yahalom lost |]                                            \
  22.110 -\        ==> EX i. K = Key(newK i)";
  22.111 + "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
  22.112 +\             : set_of_list evs;                                           \
  22.113 +\           evs : yahalom lost |]                                          \
  22.114 +\        ==> K ~: range shrK";
  22.115  by (etac rev_mp 1);
  22.116  by (etac yahalom.induct 1);
  22.117  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  22.118 @@ -199,68 +155,42 @@
  22.119  val analz_Fake_tac = 
  22.120      forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
  22.121      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
  22.122 -    assume_tac 7 THEN Full_simp_tac 7 THEN
  22.123 -    REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
  22.124 +    assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
  22.125  
  22.126  
  22.127  (****
  22.128   The following is to prove theorems of the form
  22.129  
  22.130 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
  22.131 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
  22.132    Key K : analz (sees lost Spy evs)
  22.133  
  22.134   A more general formula must be proved inductively.
  22.135 -
  22.136  ****)
  22.137  
  22.138 -
  22.139 -(*NOT useful in this form, but it says that session keys are not used
  22.140 -  to encrypt messages containing other keys, in the actual protocol.
  22.141 -  We require that agents should behave like this subsequently also.*)
  22.142 -goal thy 
  22.143 - "!!evs. evs : yahalom lost ==> \
  22.144 -\        (Crypt (newK i) X) : parts (sees lost Spy evs) & \
  22.145 -\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
  22.146 -by (etac yahalom.induct 1);
  22.147 -by parts_Fake_tac;
  22.148 -by (ALLGOALS Asm_simp_tac);
  22.149 -(*Deals with Faked messages*)
  22.150 -by (best_tac (!claset addSEs partsEs
  22.151 -                      addDs [impOfSubs parts_insert_subset_Un]
  22.152 -                      addss (!simpset)) 2);
  22.153 -(*Base case*)
  22.154 -by (Auto_tac());
  22.155 -result();
  22.156 -
  22.157 -
  22.158  (** Session keys are not used to encrypt other session keys **)
  22.159  
  22.160  goal thy  
  22.161   "!!evs. evs : yahalom lost ==> \
  22.162 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
  22.163 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
  22.164 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
  22.165 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  22.166 +\            (K : KK | Key K : analz (sees lost Spy evs))";
  22.167  by (etac yahalom.induct 1);
  22.168  by analz_Fake_tac;
  22.169 -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
  22.170 -by (ALLGOALS (*Takes 11 secs*)
  22.171 -    (asm_simp_tac 
  22.172 -     (!simpset addsimps [Un_assoc RS sym, 
  22.173 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
  22.174 -               setloop split_tac [expand_if])));
  22.175 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
  22.176 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  22.177 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  22.178 +(*Base*)
  22.179 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  22.180  (*YM4, Fake*) 
  22.181 -by (EVERY (map spy_analz_tac [4, 2]));
  22.182 -(*Oops, YM3, Base*)
  22.183 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
  22.184 -qed_spec_mp "analz_image_newK";
  22.185 +by (REPEAT (spy_analz_tac 1));
  22.186 +qed_spec_mp "analz_image_freshK";
  22.187  
  22.188  goal thy
  22.189 - "!!evs. evs : yahalom lost ==>                               \
  22.190 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
  22.191 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
  22.192 -by (asm_simp_tac (HOL_ss addsimps [analz_image_newK, 
  22.193 -                                   insert_Key_singleton]) 1);
  22.194 -by (Fast_tac 1);
  22.195 -qed "analz_insert_Key_newK";
  22.196 + "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
  22.197 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
  22.198 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
  22.199 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  22.200 +qed "analz_insert_freshK";
  22.201  
  22.202  
  22.203  (*** The Key K uniquely identifies the Server's  message. **)
  22.204 @@ -279,8 +209,10 @@
  22.205  (*Remaining case: YM3*)
  22.206  by (expand_case_tac "K = ?y" 1);
  22.207  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  22.208 -(*...we assume X is a very new message, and handle this case by contradiction*)
  22.209 -by (Fast_tac 1);  (*uses Says_too_new_key*)
  22.210 +(*...we assume X is a recent message and handle this case by contradiction*)
  22.211 +by (fast_tac (!claset addSEs sees_Spy_partsEs
  22.212 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
  22.213 +                      addss (!simpset addsimps [parts_insertI])) 1);
  22.214  val lemma = result();
  22.215  
  22.216  goal thy 
  22.217 @@ -324,10 +256,13 @@
  22.218  by analz_Fake_tac;
  22.219  by (ALLGOALS
  22.220      (asm_simp_tac 
  22.221 -     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
  22.222 +     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
  22.223                 setloop split_tac [expand_if])));
  22.224  (*YM3*)
  22.225 -by (Fast_tac 2);  (*uses Says_too_new_key*)
  22.226 +by (fast_tac (!claset delrules [impCE]
  22.227 +                      addSEs sees_Spy_partsEs
  22.228 +                      addIs [impOfSubs analz_subset_parts]
  22.229 +                      addss (!simpset addsimps [parts_insert2])) 2);
  22.230  (*OR4, Fake*) 
  22.231  by (REPEAT_FIRST spy_analz_tac);
  22.232  (*Oops*)
  22.233 @@ -339,25 +274,27 @@
  22.234  
  22.235  (*Final version: Server's message in the most abstract form*)
  22.236  goal thy 
  22.237 - "!!evs. [| Says Server A                                               \
  22.238 -\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
  22.239 -\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
  22.240 -\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
  22.241 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
  22.242 -\     K ~: analz (sees lost Spy evs)";
  22.243 + "!!evs. [| Says Server A                                         \
  22.244 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
  22.245 +\                Crypt (shrK B) {|Agent A, Key K|}|}              \
  22.246 +\             : set_of_list evs;                                  \
  22.247 +\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
  22.248 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  22.249 +\        ==> Key K ~: analz (sees lost Spy evs)";
  22.250  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  22.251  by (fast_tac (!claset addSEs [lemma]) 1);
  22.252  qed "Spy_not_see_encrypted_key";
  22.253  
  22.254  
  22.255  goal thy 
  22.256 - "!!evs. [| C ~: {A,B,Server};                                          \
  22.257 -\           Says Server A                                               \
  22.258 -\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
  22.259 -\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
  22.260 -\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
  22.261 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
  22.262 -\     K ~: analz (sees lost C evs)";
  22.263 + "!!evs. [| C ~: {A,B,Server};                                    \
  22.264 +\           Says Server A                                         \
  22.265 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
  22.266 +\                Crypt (shrK B) {|Agent A, Key K|}|}              \
  22.267 +\             : set_of_list evs;                                  \
  22.268 +\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
  22.269 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  22.270 +\        ==> Key K ~: analz (sees lost C evs)";
  22.271  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  22.272  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
  22.273  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
  22.274 @@ -374,7 +311,7 @@
  22.275  \           B ~: lost;  evs : yahalom lost |]                           \
  22.276  \        ==> EX NA NB. Says Server A                                    \
  22.277  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
  22.278 -\                                  Nonce NA, Nonce NB|},                \
  22.279 +\                                           Nonce NA, Nonce NB|},       \
  22.280  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  22.281  \                       : set_of_list evs";
  22.282  by (etac rev_mp 1);
  22.283 @@ -384,40 +321,8 @@
  22.284  qed "B_trusts_YM4_shrK";
  22.285  
  22.286  
  22.287 -(*** General properties of nonces ***)
  22.288 -
  22.289 -goal thy "!!evs. evs : yahalom lost ==>       \
  22.290 -\                length evs <= i --> \
  22.291 -\                Nonce (newN i) ~: parts (sees lost Spy evs)";
  22.292 -by (parts_induct_tac 1);
  22.293 -by (REPEAT_FIRST (fast_tac (!claset 
  22.294 -                              addSEs partsEs
  22.295 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
  22.296 -                              addEs  [leD RS notE]
  22.297 -			      addDs  [impOfSubs analz_subset_parts,
  22.298 -                                      impOfSubs parts_insert_subset_Un,
  22.299 -                                      Suc_leD]
  22.300 -                              addss (!simpset))));
  22.301 -qed_spec_mp "new_nonces_not_seen";
  22.302 -Addsimps [new_nonces_not_seen];
  22.303 -
  22.304 -(*Variant: old messages must contain old nonces!*)
  22.305 -goal thy 
  22.306 - "!!evs. [| Says A B X : set_of_list evs;              \
  22.307 -\           Nonce (newN i) : parts {X};      \
  22.308 -\           evs : yahalom lost                         \
  22.309 -\        |] ==> i < length evs";
  22.310 -by (rtac ccontr 1);
  22.311 -by (dtac leI 1);
  22.312 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
  22.313 -                      addIs  [impOfSubs parts_mono]) 1);
  22.314 -qed "Says_imp_old_nonces";
  22.315 -
  22.316 -
  22.317  (** The Nonce NB uniquely identifies B's message. **)
  22.318  
  22.319 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
  22.320 -
  22.321  goal thy 
  22.322   "!!evs. evs : yahalom lost ==> \
  22.323  \   EX NA' A' B'. ALL NA A B. \
  22.324 @@ -427,14 +332,15 @@
  22.325  (*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
  22.326  by (REPEAT (etac exE 2) THEN 
  22.327      best_tac (!claset addSIs [exI]
  22.328 -		      addDs [impOfSubs Fake_parts_insert]
  22.329 -      	              addss (!simpset)) 2);
  22.330 +                      addDs [impOfSubs Fake_parts_insert]
  22.331 +                      addss (!simpset)) 2);
  22.332  (*Base case*)
  22.333  by (fast_tac (!claset addss (!simpset)) 1);
  22.334  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
  22.335  (*YM2: creation of new Nonce.  Move assertion into global context*)
  22.336  by (expand_case_tac "NB = ?y" 1);
  22.337 -by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
  22.338 +by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
  22.339 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
  22.340  val lemma = result();
  22.341  
  22.342  goal thy 
  22.343 @@ -447,16 +353,6 @@
  22.344  by (prove_unique_tac lemma 1);
  22.345  qed "unique_NB";
  22.346  
  22.347 -(*OLD VERSION
  22.348 -fun lost_tac s =
  22.349 -    case_tac ("(" ^ s ^ ") : lost") THEN'
  22.350 -    SELECT_GOAL 
  22.351 -      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
  22.352 -       REPEAT_DETERM (etac MPair_analz 1) THEN
  22.353 -       dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
  22.354 -       assume_tac 1 THEN Fast_tac 1);
  22.355 -*)
  22.356 -
  22.357  fun lost_tac s =
  22.358      case_tac ("(" ^ s ^ ") : lost") THEN'
  22.359      SELECT_GOAL 
  22.360 @@ -502,7 +398,6 @@
  22.361  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
  22.362                        addSIs [parts_insertI]
  22.363                        addSEs partsEs
  22.364 -                      addEs [Says_imp_old_nonces RS less_irrefl]
  22.365                        addss (!simpset)) 1);
  22.366  val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
  22.367  
  22.368 @@ -518,8 +413,8 @@
  22.369  \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
  22.370  \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
  22.371  \            (EX A B NA. Says Server A                                  \
  22.372 -\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
  22.373 -\                                  Nonce NA, Nonce NB|},       \
  22.374 +\                        {|Crypt (shrK A) {|Agent B, Key K,             \
  22.375 +\                                  Nonce NA, Nonce NB|},                \
  22.376  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  22.377  \                       : set_of_list evs)";
  22.378  by (etac yahalom.induct 1);
  22.379 @@ -602,81 +497,97 @@
  22.380  
  22.381  val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
  22.382  
  22.383 -fun grind_tac i = 
  22.384 - SELECT_GOAL
  22.385 -  (REPEAT_FIRST 
  22.386 -   (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
  22.387 -    assume_tac ORELSE'
  22.388 -    depth_tac (!claset delrules [conjI]
  22.389 -                       addSIs [exI, analz_insertI,
  22.390 -                               impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
  22.391  
  22.392  (*The only nonces that can be found with the help of session keys are
  22.393    those distributed as nonce NB by the Server.  The form of the theorem
  22.394 -  recalls analz_image_newK, but it is much more complicated.*)
  22.395 +  recalls analz_image_freshK, but it is much more complicated.*)
  22.396 +
  22.397 +(*As with analz_image_freshK, we take some pains to express the property
  22.398 +  as a logical equivalence so that the simplifier can apply it.*)
  22.399 +goal thy  
  22.400 + "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
  22.401 +\        P --> (X : analz (G Un H)) = (X : analz H)";
  22.402 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
  22.403 +qed "Nonce_secrecy_lemma";
  22.404 +
  22.405  goal thy 
  22.406 - "!!evs. evs : yahalom lost ==>                                           \
  22.407 -\     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
  22.408 -\     (EX K: newK``E. EX A B na X.                                        \
  22.409 -\            Says Server A                                                \
  22.410 -\                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}   \
  22.411 -\            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
  22.412 + "!!evs. evs : yahalom lost ==>                                          \
  22.413 +\        (ALL KK. KK <= Compl (range shrK) -->                               \
  22.414 +\             (ALL K: KK. ALL A B na X.                                       \
  22.415 +\                 Says Server A                                              \
  22.416 +\                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
  22.417 +\                 ~: set_of_list evs)   -->  \
  22.418 +\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =      \
  22.419 +\             (Nonce NB : analz (sees lost Spy evs)))";
  22.420  by (etac yahalom.induct 1);
  22.421  by analz_Fake_tac;
  22.422 +by (REPEAT_FIRST (resolve_tac [impI RS allI]));
  22.423 +by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
  22.424 +by (rtac ccontr 7);
  22.425 +by (subgoal_tac "ALL A B na X.                                       \
  22.426 +\                 Says Server A                                              \
  22.427 +\                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
  22.428 +\                 ~: set_of_list evsa" 7);
  22.429 +by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
  22.430 +by (subgoal_tac "ALL A B na X.                                       \
  22.431 +\                 Says Server A                                              \
  22.432 +\                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
  22.433 +\                 ~: set_of_list evsa" 5);
  22.434  by (ALLGOALS  (*22 seconds*)
  22.435      (asm_simp_tac 
  22.436 -     (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
  22.437 -                          insert_Key_singleton, insert_Key_image]
  22.438 -                         @ pushes)
  22.439 -               setloop split_tac [expand_if])));
  22.440 +     (analz_image_freshK_ss  addsimps
  22.441 +             ([all_conj_distrib, 
  22.442 +               not_parts_not_analz, analz_image_freshK]
  22.443 +              @ pushes @ ball_simps))));
  22.444  (*Base*)
  22.445  by (fast_tac (!claset addss (!simpset)) 1);
  22.446 -(*Fake*) (** LEVEL 4 **)
  22.447 +(*Fake*) (** LEVEL 10 **)
  22.448  by (spy_analz_tac 1);
  22.449 -(*YM1-YM3*) (*24 seconds*)
  22.450 -by (EVERY (map grind_tac [3,2,1]));
  22.451 +(*YM3*)
  22.452 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
  22.453  (*Oops*)
  22.454 -by (Full_simp_tac 2);
  22.455 -by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
  22.456 -by (grind_tac 2);
  22.457 -by (fast_tac (!claset delrules [bexI] 
  22.458 -                      addDs [unique_session_keys]
  22.459 +(*20 secs*)
  22.460 +by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
  22.461                        addss (!simpset)) 2);
  22.462  (*YM4*)
  22.463 -(** LEVEL 10 **)
  22.464 -by (rtac (impI RS allI) 1);
  22.465 +(** LEVEL 13 **)
  22.466 +by (REPEAT (resolve_tac [impI, allI] 1));
  22.467  by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
  22.468 +by (stac insert_commute 1);
  22.469  by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
  22.470 -by (asm_simp_tac (!simpset addsimps [analz_image_newK]
  22.471 -                           setloop split_tac [expand_if]) 1);
  22.472 -(** LEVEL 14 **)
  22.473 -by (grind_tac 1);
  22.474 -by (REPEAT (dtac not_analz_insert 1));
  22.475 +by (asm_simp_tac (analz_image_freshK_ss 
  22.476 +                  addsimps [analz_insertI, analz_image_freshK]) 1);
  22.477 +by (step_tac (!claset addSDs [not_analz_insert]) 1);
  22.478  by (lost_tac "A" 1);
  22.479 +(** LEVEL 20 **)
  22.480  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
  22.481      THEN REPEAT (assume_tac 1));
  22.482 -by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
  22.483 -by (fast_tac (!claset delrules [conjI]
  22.484 -                      addIs [analz_insertI]
  22.485 -                      addss (!simpset)) 1);
  22.486 -val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
  22.487 +by (thin_tac "All ?PP" 1);
  22.488 +by (Fast_tac 1);
  22.489 +qed_spec_mp "Nonce_secrecy";
  22.490  
  22.491  
  22.492  (*Version required below: if NB can be decrypted using a session key then it
  22.493    was distributed with that key.  The more general form above is required
  22.494    for the induction to carry through.*)
  22.495  goal thy 
  22.496 - "!!evs. [| Says Server A                                                   \
  22.497 -\            {|Crypt (shrK A) {|Agent B, Key (newK i), na, Nonce NB'|}, X|} \
  22.498 -\           : set_of_list evs;                                              \
  22.499 -\           Nonce NB : analz (insert (Key (newK i)) (sees lost Spy evs));   \
  22.500 -\           evs : yahalom lost |]                                           \
  22.501 -\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
  22.502 -by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
  22.503 -by (dtac Nonce_secrecy 1 THEN assume_tac 1);
  22.504 -by (fast_tac (!claset addDs [unique_session_keys]
  22.505 -                      addss (!simpset)) 1);
  22.506 -val single_Nonce_secrecy = result();
  22.507 + "!!evs. [| Says Server A                                              \
  22.508 +\            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
  22.509 +\           : set_of_list evs;                                         \
  22.510 +\           Nonce NB : analz (insert (Key KAB) (sees lost Spy evs));   \
  22.511 +\           Nonce NB ~: analz (sees lost Spy evs);                     \
  22.512 +\           KAB ~: range shrK;  evs : yahalom lost |]                  \
  22.513 +\        ==>  NB = NB'";
  22.514 +by (rtac ccontr 1);
  22.515 +by (subgoal_tac "ALL A B na X.                                       \
  22.516 +\                 Says Server A                                              \
  22.517 +\                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
  22.518 +\                 ~: set_of_list evs" 1);
  22.519 +by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
  22.520 +by (asm_simp_tac (analz_image_freshK_ss 
  22.521 +                  addsimps ([Nonce_secrecy] @ ball_simps)) 1);
  22.522 +by (auto_tac (!claset addDs [unique_session_keys], (!simpset)));
  22.523 +qed "single_Nonce_secrecy";
  22.524  
  22.525  
  22.526  goal thy 
  22.527 @@ -691,46 +602,41 @@
  22.528  by (ALLGOALS
  22.529      (asm_simp_tac 
  22.530       (!simpset addsimps ([not_parts_not_analz,
  22.531 -                          analz_insert_Key_newK] @ pushes)
  22.532 +                          analz_insert_freshK] @ pushes)
  22.533                 setloop split_tac [expand_if])));
  22.534  by (fast_tac (!claset addSIs [parts_insertI]
  22.535 -                      addSEs partsEs
  22.536 -                      addEs [Says_imp_old_nonces RS less_irrefl]
  22.537 +                      addSEs sees_Spy_partsEs
  22.538                        addss (!simpset)) 2);
  22.539  (*Proof of YM2*) (** LEVEL 4 **)
  22.540 -by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); 
  22.541 -by (fast_tac (!claset addIs [parts_insertI]
  22.542 -                      addSEs partsEs
  22.543 -                      addEs [Says_imp_old_nonces RS less_irrefl]
  22.544 -                      addss (!simpset)) 3);
  22.545 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
  22.546 +by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
  22.547 +                               impOfSubs analz_subset_parts]
  22.548 +                        addSEs partsEs) 3 2);
  22.549  (*Prove YM3 by showing that no NB can also be an NA*)
  22.550  by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
  22.551  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
  22.552  (*Fake*)
  22.553  by (spy_analz_tac 1);
  22.554 -(*YM4*) (** LEVEL 10 **)
  22.555 +(*YM4*) (** LEVEL 8 **)
  22.556  by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
  22.557  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
  22.558 +(*43 secs??*)
  22.559  by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
  22.560 -(** LEVEL 13 **)
  22.561  by (lost_tac "Aa" 1);
  22.562  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
  22.563  by (forward_tac [Says_Server_message_form] 3);
  22.564  by (forward_tac [Says_Server_imp_YM2] 4);
  22.565 +(** LEVEL 15 **)
  22.566  by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
  22.567 -by (Full_simp_tac 1);
  22.568 -by (REPEAT_FIRST hyp_subst_tac);
  22.569 -(** LEVEL 20 **)
  22.570  by (lost_tac "Ba" 1);
  22.571  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
  22.572  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  22.573                        addSEs [MPair_parts]) 1);
  22.574  by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
  22.575 +(** LEVEL 20 **)
  22.576  by (dtac Spy_not_see_encrypted_key 1);
  22.577  by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
  22.578  by (spy_analz_tac 1);
  22.579 -(*Oops case*) (** LEVEL 27 **)
  22.580 +(*Oops case*) (** LEVEL 23 **)
  22.581  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
  22.582  by (step_tac (!claset delrules [disjE, conjI]) 1);
  22.583  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
  22.584 @@ -738,7 +644,7 @@
  22.585  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
  22.586  by (rtac conjI 1);
  22.587  by (no_nonce_tac 1);
  22.588 -(** LEVEL 34 **)
  22.589 +(** LEVEL 30 **)
  22.590  by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
  22.591  by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
  22.592  val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
  22.593 @@ -750,16 +656,16 @@
  22.594    ALL POSSIBLE keys instead of our particular K (though at least the
  22.595    nonces are forced to agree with NA and NB). *)
  22.596  goal thy 
  22.597 - "!!evs. [| Says B Server                                        \
  22.598 + "!!evs. [| Says B Server                                               \
  22.599  \            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
  22.600  \           : set_of_list evs;       \
  22.601  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
  22.602  \                       Crypt K (Nonce NB)|} : set_of_list evs;         \
  22.603  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
  22.604  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
  22.605 -\         ==> Says Server A                                       \
  22.606 -\                     {|Crypt (shrK A) {|Agent B, Key K,                         \
  22.607 -\                               Nonce NA, Nonce NB|},          \
  22.608 +\         ==> Says Server A                                             \
  22.609 +\                     {|Crypt (shrK A) {|Agent B, Key K,                \
  22.610 +\                               Nonce NA, Nonce NB|},                   \
  22.611  \                       Crypt (shrK B) {|Agent A, Key K|}|}             \
  22.612  \                   : set_of_list evs";
  22.613  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
  22.614 @@ -771,4 +677,3 @@
  22.615  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
  22.616  by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
  22.617  qed "B_trusts_YM4";
  22.618 -
    23.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Jan 17 11:50:09 1997 +0100
    23.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Jan 17 12:49:31 1997 +0100
    23.3 @@ -26,30 +26,26 @@
    23.4            ==> Says Spy B X  # evs : yahalom lost"
    23.5  
    23.6           (*Alice initiates a protocol run*)
    23.7 -    YM1  "[| evs: yahalom lost;  A ~= B |]
    23.8 -          ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs
    23.9 -                : yahalom lost"
   23.10 +    YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
   23.11 +          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
   23.12  
   23.13           (*Bob's response to Alice's message.  Bob doesn't know who 
   23.14  	   the sender is, hence the A' in the sender field.*)
   23.15 -    YM2  "[| evs: yahalom lost;  B ~= Server;
   23.16 +    YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
   23.17               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
   23.18            ==> Says B Server 
   23.19 -                  {|Agent B, 
   23.20 -                    Crypt (shrK B)
   23.21 -                      {|Agent A, Nonce NA, Nonce (newN(length evs))|}|}
   23.22 -                 # evs : yahalom lost"
   23.23 +                  {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   23.24 +                # evs : yahalom lost"
   23.25  
   23.26           (*The Server receives Bob's message.  He responds by sending a
   23.27              new session key to Alice, with a packet for forwarding to Bob.*)
   23.28 -    YM3  "[| evs: yahalom lost;  A ~= Server;
   23.29 +    YM3  "[| evs: yahalom lost;  A ~= Server;  Key KAB ~: used evs;
   23.30               Says B' Server 
   23.31                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   23.32                 : set_of_list evs |]
   23.33            ==> Says Server A
   23.34 -                  {|Crypt (shrK A) {|Agent B, Key (newK(length evs)), 
   23.35 -                            Nonce NA, Nonce NB|},
   23.36 -                    Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|}
   23.37 +                  {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
   23.38 +                    Crypt (shrK B) {|Agent A, Key KAB|}|}
   23.39                   # evs : yahalom lost"
   23.40  
   23.41           (*Alice receives the Server's (?) message, checks her Nonce, and
    24.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Jan 17 11:50:09 1997 +0100
    24.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jan 17 12:49:31 1997 +0100
    24.3 @@ -24,9 +24,9 @@
    24.4  \        ==> EX X NB K. EX evs: yahalom lost.          \
    24.5  \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    24.6  by (REPEAT (resolve_tac [exI,bexI] 1));
    24.7 -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    24.8 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    24.9 -by (ALLGOALS Fast_tac);
   24.10 +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
   24.11 +          yahalom.YM4) 2);
   24.12 +by possibility_tac;
   24.13  result();
   24.14  
   24.15  
   24.16 @@ -91,87 +91,45 @@
   24.17  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   24.18      sends messages containing X! **)
   24.19  
   24.20 -(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
   24.21 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   24.22  goal thy 
   24.23 - "!!evs. [| evs : yahalom lost;  A ~: lost |]    \
   24.24 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
   24.25 + "!!evs. evs : yahalom lost \
   24.26 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   24.27  by (parts_induct_tac 1);
   24.28  by (Auto_tac());
   24.29 -qed "Spy_not_see_shrK";
   24.30 -
   24.31 -bind_thm ("Spy_not_analz_shrK",
   24.32 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   24.33 -
   24.34 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   24.35 +qed "Spy_see_shrK";
   24.36 +Addsimps [Spy_see_shrK];
   24.37  
   24.38 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
   24.39 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
   24.40 -val major::prems = 
   24.41 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   24.42 -\             evs : yahalom lost;                               \
   24.43 -\             A:lost ==> R                                  \
   24.44 -\           |] ==> R";
   24.45 -by (rtac ccontr 1);
   24.46 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   24.47 -by (swap_res_tac prems 2);
   24.48 -by (ALLGOALS (fast_tac (!claset addIs prems)));
   24.49 -qed "Spy_see_shrK_E";
   24.50 +goal thy 
   24.51 + "!!evs. evs : yahalom lost \
   24.52 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   24.53 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   24.54 +qed "Spy_analz_shrK";
   24.55 +Addsimps [Spy_analz_shrK];
   24.56  
   24.57 -bind_thm ("Spy_analz_shrK_E", 
   24.58 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   24.59 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   24.60 +\                  evs : yahalom lost |] ==> A:lost";
   24.61 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   24.62 +qed "Spy_see_shrK_D";
   24.63  
   24.64 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   24.65 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   24.66 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   24.67  
   24.68  
   24.69 -(*** Future keys can't be seen or used! ***)
   24.70 -
   24.71 -(*Nobody can have SEEN keys that will be generated in the future. *)
   24.72 -goal thy "!!i. evs : yahalom lost ==> \
   24.73 -\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   24.74 +(*Nobody can have used non-existent keys!*)
   24.75 +goal thy "!!evs. evs : yahalom lost ==>          \
   24.76 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   24.77  by (parts_induct_tac 1);
   24.78 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   24.79 -				    addDs [impOfSubs analz_subset_parts,
   24.80 -                                           impOfSubs parts_insert_subset_Un,
   24.81 -                                           Suc_leD]
   24.82 -                                    addss (!simpset))));
   24.83 -qed_spec_mp "new_keys_not_seen";
   24.84 -Addsimps [new_keys_not_seen];
   24.85 -
   24.86 -(*Variant: old messages must contain old keys!*)
   24.87 -goal thy 
   24.88 - "!!evs. [| Says A B X : set_of_list evs;  \
   24.89 -\           Key (newK i) : parts {X};    \
   24.90 -\           evs : yahalom lost                 \
   24.91 -\        |] ==> i < length evs";
   24.92 -by (rtac ccontr 1);
   24.93 -by (dtac leI 1);
   24.94 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   24.95 -                      addIs  [impOfSubs parts_mono]) 1);
   24.96 -qed "Says_imp_old_keys";
   24.97 -
   24.98 -
   24.99 -(*Nobody can have USED keys that will be generated in the future.
  24.100 -  ...very like new_keys_not_seen*)
  24.101 -goal thy "!!i. evs : yahalom lost ==> \
  24.102 -\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
  24.103 -by (parts_induct_tac 1);
  24.104 -by (dtac YM4_Key_parts_sees_Spy 5);
  24.105 -(*YM1, YM2 and YM3*)
  24.106 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
  24.107 -(*Fake and Oops: these messages send unknown (X) components*)
  24.108 -by (EVERY
  24.109 -    (map (fast_tac
  24.110 -          (!claset addDs [impOfSubs analz_subset_parts,
  24.111 -                          impOfSubs (analz_subset_parts RS keysFor_mono),
  24.112 -                          impOfSubs (parts_insert_subset_Un RS keysFor_mono),
  24.113 -                          Suc_leD]
  24.114 -                   addss (!simpset))) [3,1]));
  24.115 -(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
  24.116 -by (fast_tac
  24.117 -      (!claset addSEs partsEs
  24.118 -               addSDs [Says_imp_sees_Spy RS parts.Inj]
  24.119 -               addEs [new_keys_not_seen RSN(2,rev_notE)]
  24.120 -               addDs [Suc_leD]) 1);
  24.121 +(*YM4: Key K is not fresh!*)
  24.122 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
  24.123 +(*YM3*)
  24.124 +by (fast_tac (!claset addss (!simpset)) 2);
  24.125 +(*Fake*)
  24.126 +by (best_tac
  24.127 +      (!claset addIs [impOfSubs analz_subset_parts]
  24.128 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
  24.129 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
  24.130 +               addss (!simpset)) 1);
  24.131  qed_spec_mp "new_keys_not_used";
  24.132  
  24.133  bind_thm ("new_keys_not_analzd",
  24.134 @@ -184,10 +142,10 @@
  24.135  (*Describes the form of K when the Server sends this message.  Useful for
  24.136    Oops as well as main secrecy property.*)
  24.137  goal thy 
  24.138 - "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
  24.139 + "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
  24.140  \            : set_of_list evs;                                         \
  24.141  \           evs : yahalom lost |]                                       \
  24.142 -\        ==> (EX i. K = Key(newK i)) & A ~= B";
  24.143 +\        ==> K ~: range shrK & A ~= B";
  24.144  by (etac rev_mp 1);
  24.145  by (etac yahalom.induct 1);
  24.146  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  24.147 @@ -198,14 +156,14 @@
  24.148  val analz_Fake_tac = 
  24.149      dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
  24.150      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
  24.151 -    assume_tac 7 THEN Full_simp_tac 7 THEN
  24.152 -    REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7);
  24.153 +    assume_tac 7 THEN
  24.154 +    REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
  24.155  
  24.156  
  24.157  (****
  24.158   The following is to prove theorems of the form
  24.159  
  24.160 -          Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
  24.161 +          Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
  24.162            Key K : analz (sees lost Spy evs)
  24.163  
  24.164   A more general formula must be proved inductively.
  24.165 @@ -216,30 +174,26 @@
  24.166  
  24.167  goal thy  
  24.168   "!!evs. evs : yahalom lost ==> \
  24.169 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
  24.170 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
  24.171 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
  24.172 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
  24.173 +\            (K : KK | Key K : analz (sees lost Spy evs))";
  24.174  by (etac yahalom.induct 1);
  24.175  by analz_Fake_tac;
  24.176 -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
  24.177 -by (ALLGOALS (*Takes 11 secs*)
  24.178 -    (asm_simp_tac 
  24.179 -     (!simpset addsimps [Un_assoc RS sym, 
  24.180 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
  24.181 -               setloop split_tac [expand_if])));
  24.182 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
  24.183 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  24.184 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  24.185 +(*Base*)
  24.186 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  24.187  (*YM4, Fake*) 
  24.188 -by (EVERY (map spy_analz_tac [4, 2]));
  24.189 -(*Oops, YM3, Base*)
  24.190 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
  24.191 -qed_spec_mp "analz_image_newK";
  24.192 +by (REPEAT (spy_analz_tac 1));
  24.193 +qed_spec_mp "analz_image_freshK";
  24.194  
  24.195  goal thy
  24.196 - "!!evs. evs : yahalom lost ==>                               \
  24.197 -\        Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \
  24.198 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
  24.199 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
  24.200 -                                   insert_Key_singleton]) 1);
  24.201 -by (Fast_tac 1);
  24.202 -qed "analz_insert_Key_newK";
  24.203 + "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
  24.204 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
  24.205 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
  24.206 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  24.207 +qed "analz_insert_freshK";
  24.208  
  24.209  
  24.210  (*** The Key K uniquely identifies the Server's  message. **)
  24.211 @@ -256,8 +210,8 @@
  24.212  (*Remaining case: YM3*)
  24.213  by (expand_case_tac "K = ?y" 1);
  24.214  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  24.215 -(*...we assume X is a very new message, and handle this case by contradiction*)
  24.216 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
  24.217 +(*...we assume X is a recent message and handle this case by contradiction*)
  24.218 +by (fast_tac (!claset addSEs sees_Spy_partsEs
  24.219                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
  24.220                        addss (!simpset addsimps [parts_insertI])) 1);
  24.221  val lemma = result();
  24.222 @@ -290,12 +244,13 @@
  24.223  by analz_Fake_tac;
  24.224  by (ALLGOALS
  24.225      (asm_simp_tac 
  24.226 -     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
  24.227 +     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
  24.228                 setloop split_tac [expand_if])));
  24.229  (*YM3*)
  24.230 -by (fast_tac (!claset addIs [parts_insertI]
  24.231 -                      addEs [Says_imp_old_keys RS less_irrefl]
  24.232 -                      addss (!simpset)) 2);
  24.233 +by (fast_tac (!claset delrules [impCE]
  24.234 +                      addSEs sees_Spy_partsEs
  24.235 +                      addIs [impOfSubs analz_subset_parts]
  24.236 +                      addss (!simpset addsimps [parts_insert2])) 2);
  24.237  (*OR4, Fake*) 
  24.238  by (REPEAT_FIRST spy_analz_tac);
  24.239  (*Oops*)
  24.240 @@ -308,12 +263,12 @@
  24.241  (*Final version: Server's message in the most abstract form*)
  24.242  goal thy 
  24.243   "!!evs. [| Says Server A                                         \
  24.244 -\              {|NB, Crypt (shrK A) {|Agent B, K, NA|},           \
  24.245 -\                    Crypt (shrK B) {|NB, K, Agent A|}|}          \
  24.246 +\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
  24.247 +\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}      \
  24.248  \           : set_of_list evs;                                    \
  24.249 -\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
  24.250 +\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
  24.251  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  24.252 -\        ==> K ~: analz (sees lost Spy evs)";
  24.253 +\        ==> Key K ~: analz (sees lost Spy evs)";
  24.254  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  24.255  by (fast_tac (!claset addSEs [lemma]) 1);
  24.256  qed "Spy_not_see_encrypted_key";
  24.257 @@ -322,12 +277,12 @@
  24.258  goal thy 
  24.259   "!!evs. [| C ~: {A,B,Server};                                    \
  24.260  \           Says Server A                                         \
  24.261 -\              {|NB, Crypt (shrK A) {|Agent B, K, NA|},           \
  24.262 -\                    Crypt (shrK B) {|NB, K, Agent A|}|}          \
  24.263 +\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
  24.264 +\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}      \
  24.265  \           : set_of_list evs;                                    \
  24.266 -\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
  24.267 +\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
  24.268  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  24.269 -\        ==> K ~: analz (sees lost C evs)";
  24.270 +\        ==> Key K ~: analz (sees lost C evs)";
  24.271  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  24.272  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
  24.273  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    25.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Jan 17 11:50:09 1997 +0100
    25.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Jan 17 12:49:31 1997 +0100
    25.3 @@ -30,26 +30,26 @@
    25.4            ==> Says Spy B X  # evs : yahalom lost"
    25.5  
    25.6           (*Alice initiates a protocol run*)
    25.7 -    YM1  "[| evs: yahalom lost;  A ~= B |]
    25.8 -          ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost"
    25.9 +    YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
   25.10 +          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
   25.11  
   25.12           (*Bob's response to Alice's message.  Bob doesn't know who 
   25.13  	   the sender is, hence the A' in the sender field.*)
   25.14 -    YM2  "[| evs: yahalom lost;  B ~= Server;
   25.15 +    YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
   25.16               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
   25.17 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|}
   25.18 -                 # evs : yahalom lost"
   25.19 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs
   25.20 +                : yahalom lost"
   25.21  
   25.22           (*The Server receives Bob's message.  He responds by sending a
   25.23             new session key to Alice, with a packet for forwarding to Bob.
   25.24             Fields are reversed in the 2nd packet to prevent attacks.*)
   25.25 -    YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;
   25.26 +    YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
   25.27               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   25.28                 : set_of_list evs |]
   25.29            ==> Says Server A
   25.30                 {|Nonce NB, 
   25.31 -                 Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|},
   25.32 -                 Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|}
   25.33 +                 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
   25.34 +                 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
   25.35                   # evs : yahalom lost"
   25.36  
   25.37           (*Alice receives the Server's (?) message, checks her Nonce, and