src/HOL/Auth/Yahalom.ML
changeset 2516 4d68fbe6378b
parent 2454 92f43ed48935
child 2637 e9b203f854ae
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 -Pretty.setdepth 20;
     1.8 +Pretty.setdepth 25;
     1.9  
    1.10  
    1.11  (*A "possibility property": there are traces that reach the end*)
    1.12 @@ -23,9 +23,9 @@
    1.13  \        ==> EX X NB K. EX evs: yahalom lost.          \
    1.14  \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    1.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.16 -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    1.17 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.18 -by (ALLGOALS Fast_tac);
    1.19 +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    1.20 +          yahalom.YM4) 2);
    1.21 +by possibility_tac;
    1.22  result();
    1.23  
    1.24  
    1.25 @@ -115,64 +115,20 @@
    1.26  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.27  
    1.28  
    1.29 -(*** Future keys can't be seen or used! ***)
    1.30 -
    1.31 -(*Nobody can have SEEN keys that will be generated in the future. *)
    1.32 -goal thy "!!i. evs : yahalom lost ==>        \
    1.33 -\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
    1.34 +(*Nobody can have used non-existent keys!*)
    1.35 +goal thy "!!evs. evs : yahalom lost ==>          \
    1.36 +\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    1.37  by (parts_induct_tac 1);
    1.38 -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    1.39 -				    addDs [impOfSubs analz_subset_parts,
    1.40 -                                           impOfSubs parts_insert_subset_Un,
    1.41 -                                           Suc_leD]
    1.42 -                                    addss (!simpset))));
    1.43 -qed_spec_mp "new_keys_not_seen";
    1.44 -Addsimps [new_keys_not_seen];
    1.45 -
    1.46 -(*Variant: old messages must contain old keys!*)
    1.47 -goal thy 
    1.48 - "!!evs. [| Says A B X : set_of_list evs;          \
    1.49 -\           Key (newK i) : parts {X};    \
    1.50 -\           evs : yahalom lost                     \
    1.51 -\        |] ==> i < length evs";
    1.52 -by (rtac ccontr 1);
    1.53 -by (dtac leI 1);
    1.54 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    1.55 -                      addIs  [impOfSubs parts_mono]) 1);
    1.56 -qed "Says_imp_old_keys";
    1.57 -
    1.58 -
    1.59 -(*Ready-made for the classical reasoner*)
    1.60 -goal thy "!!evs. [| Says A B {|Crypt K {|b,Key(newK(length evs)),na,nb|}, X|}\
    1.61 -\                   : set_of_list evs;  evs : yahalom lost |]              \
    1.62 -\                ==> R";
    1.63 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.64 -                      addss (!simpset addsimps [parts_insertI])) 1);
    1.65 -qed "Says_too_new_key";
    1.66 -AddSEs [Says_too_new_key];
    1.67 -
    1.68 -
    1.69 -(*Nobody can have USED keys that will be generated in the future.
    1.70 -  ...very like new_keys_not_seen*)
    1.71 -goal thy "!!i. evs : yahalom lost ==>        \
    1.72 -\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
    1.73 -by (parts_induct_tac 1);
    1.74 -(*YM1, YM2 and YM3*)
    1.75 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    1.76 -(*Fake and Oops: these messages send unknown (X) components*)
    1.77 -by (EVERY
    1.78 -    (map (fast_tac
    1.79 -          (!claset addDs [impOfSubs analz_subset_parts,
    1.80 -                          impOfSubs (analz_subset_parts RS keysFor_mono),
    1.81 -                          impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.82 -                          Suc_leD]
    1.83 -                   addss (!simpset))) [3,1]));
    1.84 -(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
    1.85 -by (fast_tac
    1.86 -      (!claset addSEs partsEs
    1.87 -               addSDs [Says_imp_sees_Spy RS parts.Inj]
    1.88 -               addEs [new_keys_not_seen RSN(2,rev_notE)]
    1.89 -               addDs [Suc_leD]) 1);
    1.90 +(*YM4: Key K is not fresh!*)
    1.91 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
    1.92 +(*YM3*)
    1.93 +by (fast_tac (!claset addss (!simpset)) 2);
    1.94 +(*Fake*)
    1.95 +by (best_tac
    1.96 +      (!claset addIs [impOfSubs analz_subset_parts]
    1.97 +               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.98 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.99 +               addss (!simpset)) 1);
   1.100  qed_spec_mp "new_keys_not_used";
   1.101  
   1.102  bind_thm ("new_keys_not_analzd",
   1.103 @@ -185,10 +141,10 @@
   1.104  (*Describes the form of K when the Server sends this message.  Useful for
   1.105    Oops as well as main secrecy property.*)
   1.106  goal thy 
   1.107 - "!!evs. [| Says Server A                                                    \
   1.108 -\            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
   1.109 -\           evs : yahalom lost |]                                            \
   1.110 -\        ==> EX i. K = Key(newK i)";
   1.111 + "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
   1.112 +\             : set_of_list evs;                                           \
   1.113 +\           evs : yahalom lost |]                                          \
   1.114 +\        ==> K ~: range shrK";
   1.115  by (etac rev_mp 1);
   1.116  by (etac yahalom.induct 1);
   1.117  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.118 @@ -199,68 +155,42 @@
   1.119  val analz_Fake_tac = 
   1.120      forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   1.121      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.122 -    assume_tac 7 THEN Full_simp_tac 7 THEN
   1.123 -    REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   1.124 +    assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   1.125  
   1.126  
   1.127  (****
   1.128   The following is to prove theorems of the form
   1.129  
   1.130 -  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   1.131 +  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   1.132    Key K : analz (sees lost Spy evs)
   1.133  
   1.134   A more general formula must be proved inductively.
   1.135 -
   1.136  ****)
   1.137  
   1.138 -
   1.139 -(*NOT useful in this form, but it says that session keys are not used
   1.140 -  to encrypt messages containing other keys, in the actual protocol.
   1.141 -  We require that agents should behave like this subsequently also.*)
   1.142 -goal thy 
   1.143 - "!!evs. evs : yahalom lost ==> \
   1.144 -\        (Crypt (newK i) X) : parts (sees lost Spy evs) & \
   1.145 -\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   1.146 -by (etac yahalom.induct 1);
   1.147 -by parts_Fake_tac;
   1.148 -by (ALLGOALS Asm_simp_tac);
   1.149 -(*Deals with Faked messages*)
   1.150 -by (best_tac (!claset addSEs partsEs
   1.151 -                      addDs [impOfSubs parts_insert_subset_Un]
   1.152 -                      addss (!simpset)) 2);
   1.153 -(*Base case*)
   1.154 -by (Auto_tac());
   1.155 -result();
   1.156 -
   1.157 -
   1.158  (** Session keys are not used to encrypt other session keys **)
   1.159  
   1.160  goal thy  
   1.161   "!!evs. evs : yahalom lost ==> \
   1.162 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.163 -\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.164 +\  ALL K KK. KK <= Compl (range shrK) -->                      \
   1.165 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   1.166 +\            (K : KK | Key K : analz (sees lost Spy evs))";
   1.167  by (etac yahalom.induct 1);
   1.168  by analz_Fake_tac;
   1.169 -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   1.170 -by (ALLGOALS (*Takes 11 secs*)
   1.171 -    (asm_simp_tac 
   1.172 -     (!simpset addsimps [Un_assoc RS sym, 
   1.173 -			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.174 -               setloop split_tac [expand_if])));
   1.175 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.176 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   1.177 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.178 +(*Base*)
   1.179 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.180  (*YM4, Fake*) 
   1.181 -by (EVERY (map spy_analz_tac [4, 2]));
   1.182 -(*Oops, YM3, Base*)
   1.183 -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.184 -qed_spec_mp "analz_image_newK";
   1.185 +by (REPEAT (spy_analz_tac 1));
   1.186 +qed_spec_mp "analz_image_freshK";
   1.187  
   1.188  goal thy
   1.189 - "!!evs. evs : yahalom lost ==>                               \
   1.190 -\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   1.191 -\        (K = newK i | Key K : analz (sees lost Spy evs))";
   1.192 -by (asm_simp_tac (HOL_ss addsimps [analz_image_newK, 
   1.193 -                                   insert_Key_singleton]) 1);
   1.194 -by (Fast_tac 1);
   1.195 -qed "analz_insert_Key_newK";
   1.196 + "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   1.197 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   1.198 +\        (K = KAB | Key K : analz (sees lost Spy evs))";
   1.199 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.200 +qed "analz_insert_freshK";
   1.201  
   1.202  
   1.203  (*** The Key K uniquely identifies the Server's  message. **)
   1.204 @@ -279,8 +209,10 @@
   1.205  (*Remaining case: YM3*)
   1.206  by (expand_case_tac "K = ?y" 1);
   1.207  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.208 -(*...we assume X is a very new message, and handle this case by contradiction*)
   1.209 -by (Fast_tac 1);  (*uses Says_too_new_key*)
   1.210 +(*...we assume X is a recent message and handle this case by contradiction*)
   1.211 +by (fast_tac (!claset addSEs sees_Spy_partsEs
   1.212 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.213 +                      addss (!simpset addsimps [parts_insertI])) 1);
   1.214  val lemma = result();
   1.215  
   1.216  goal thy 
   1.217 @@ -324,10 +256,13 @@
   1.218  by analz_Fake_tac;
   1.219  by (ALLGOALS
   1.220      (asm_simp_tac 
   1.221 -     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
   1.222 +     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
   1.223                 setloop split_tac [expand_if])));
   1.224  (*YM3*)
   1.225 -by (Fast_tac 2);  (*uses Says_too_new_key*)
   1.226 +by (fast_tac (!claset delrules [impCE]
   1.227 +                      addSEs sees_Spy_partsEs
   1.228 +                      addIs [impOfSubs analz_subset_parts]
   1.229 +                      addss (!simpset addsimps [parts_insert2])) 2);
   1.230  (*OR4, Fake*) 
   1.231  by (REPEAT_FIRST spy_analz_tac);
   1.232  (*Oops*)
   1.233 @@ -339,25 +274,27 @@
   1.234  
   1.235  (*Final version: Server's message in the most abstract form*)
   1.236  goal thy 
   1.237 - "!!evs. [| Says Server A                                               \
   1.238 -\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
   1.239 -\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
   1.240 -\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
   1.241 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.242 -\     K ~: analz (sees lost Spy evs)";
   1.243 + "!!evs. [| Says Server A                                         \
   1.244 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   1.245 +\                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.246 +\             : set_of_list evs;                                  \
   1.247 +\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   1.248 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.249 +\        ==> Key K ~: analz (sees lost Spy evs)";
   1.250  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.251  by (fast_tac (!claset addSEs [lemma]) 1);
   1.252  qed "Spy_not_see_encrypted_key";
   1.253  
   1.254  
   1.255  goal thy 
   1.256 - "!!evs. [| C ~: {A,B,Server};                                          \
   1.257 -\           Says Server A                                               \
   1.258 -\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
   1.259 -\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
   1.260 -\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
   1.261 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.262 -\     K ~: analz (sees lost C evs)";
   1.263 + "!!evs. [| C ~: {A,B,Server};                                    \
   1.264 +\           Says Server A                                         \
   1.265 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   1.266 +\                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.267 +\             : set_of_list evs;                                  \
   1.268 +\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   1.269 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.270 +\        ==> Key K ~: analz (sees lost C evs)";
   1.271  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.272  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.273  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.274 @@ -374,7 +311,7 @@
   1.275  \           B ~: lost;  evs : yahalom lost |]                           \
   1.276  \        ==> EX NA NB. Says Server A                                    \
   1.277  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.278 -\                                  Nonce NA, Nonce NB|},                \
   1.279 +\                                           Nonce NA, Nonce NB|},       \
   1.280  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.281  \                       : set_of_list evs";
   1.282  by (etac rev_mp 1);
   1.283 @@ -384,40 +321,8 @@
   1.284  qed "B_trusts_YM4_shrK";
   1.285  
   1.286  
   1.287 -(*** General properties of nonces ***)
   1.288 -
   1.289 -goal thy "!!evs. evs : yahalom lost ==>       \
   1.290 -\                length evs <= i --> \
   1.291 -\                Nonce (newN i) ~: parts (sees lost Spy evs)";
   1.292 -by (parts_induct_tac 1);
   1.293 -by (REPEAT_FIRST (fast_tac (!claset 
   1.294 -                              addSEs partsEs
   1.295 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   1.296 -                              addEs  [leD RS notE]
   1.297 -			      addDs  [impOfSubs analz_subset_parts,
   1.298 -                                      impOfSubs parts_insert_subset_Un,
   1.299 -                                      Suc_leD]
   1.300 -                              addss (!simpset))));
   1.301 -qed_spec_mp "new_nonces_not_seen";
   1.302 -Addsimps [new_nonces_not_seen];
   1.303 -
   1.304 -(*Variant: old messages must contain old nonces!*)
   1.305 -goal thy 
   1.306 - "!!evs. [| Says A B X : set_of_list evs;              \
   1.307 -\           Nonce (newN i) : parts {X};      \
   1.308 -\           evs : yahalom lost                         \
   1.309 -\        |] ==> i < length evs";
   1.310 -by (rtac ccontr 1);
   1.311 -by (dtac leI 1);
   1.312 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   1.313 -                      addIs  [impOfSubs parts_mono]) 1);
   1.314 -qed "Says_imp_old_nonces";
   1.315 -
   1.316 -
   1.317  (** The Nonce NB uniquely identifies B's message. **)
   1.318  
   1.319 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   1.320 -
   1.321  goal thy 
   1.322   "!!evs. evs : yahalom lost ==> \
   1.323  \   EX NA' A' B'. ALL NA A B. \
   1.324 @@ -427,14 +332,15 @@
   1.325  (*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
   1.326  by (REPEAT (etac exE 2) THEN 
   1.327      best_tac (!claset addSIs [exI]
   1.328 -		      addDs [impOfSubs Fake_parts_insert]
   1.329 -      	              addss (!simpset)) 2);
   1.330 +                      addDs [impOfSubs Fake_parts_insert]
   1.331 +                      addss (!simpset)) 2);
   1.332  (*Base case*)
   1.333  by (fast_tac (!claset addss (!simpset)) 1);
   1.334  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
   1.335  (*YM2: creation of new Nonce.  Move assertion into global context*)
   1.336  by (expand_case_tac "NB = ?y" 1);
   1.337 -by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   1.338 +by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   1.339 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.340  val lemma = result();
   1.341  
   1.342  goal thy 
   1.343 @@ -447,16 +353,6 @@
   1.344  by (prove_unique_tac lemma 1);
   1.345  qed "unique_NB";
   1.346  
   1.347 -(*OLD VERSION
   1.348 -fun lost_tac s =
   1.349 -    case_tac ("(" ^ s ^ ") : lost") THEN'
   1.350 -    SELECT_GOAL 
   1.351 -      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   1.352 -       REPEAT_DETERM (etac MPair_analz 1) THEN
   1.353 -       dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
   1.354 -       assume_tac 1 THEN Fast_tac 1);
   1.355 -*)
   1.356 -
   1.357  fun lost_tac s =
   1.358      case_tac ("(" ^ s ^ ") : lost") THEN'
   1.359      SELECT_GOAL 
   1.360 @@ -502,7 +398,6 @@
   1.361  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   1.362                        addSIs [parts_insertI]
   1.363                        addSEs partsEs
   1.364 -                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.365                        addss (!simpset)) 1);
   1.366  val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
   1.367  
   1.368 @@ -518,8 +413,8 @@
   1.369  \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   1.370  \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   1.371  \            (EX A B NA. Says Server A                                  \
   1.372 -\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   1.373 -\                                  Nonce NA, Nonce NB|},       \
   1.374 +\                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.375 +\                                  Nonce NA, Nonce NB|},                \
   1.376  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.377  \                       : set_of_list evs)";
   1.378  by (etac yahalom.induct 1);
   1.379 @@ -602,81 +497,97 @@
   1.380  
   1.381  val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
   1.382  
   1.383 -fun grind_tac i = 
   1.384 - SELECT_GOAL
   1.385 -  (REPEAT_FIRST 
   1.386 -   (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
   1.387 -    assume_tac ORELSE'
   1.388 -    depth_tac (!claset delrules [conjI]
   1.389 -                       addSIs [exI, analz_insertI,
   1.390 -                               impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
   1.391  
   1.392  (*The only nonces that can be found with the help of session keys are
   1.393    those distributed as nonce NB by the Server.  The form of the theorem
   1.394 -  recalls analz_image_newK, but it is much more complicated.*)
   1.395 +  recalls analz_image_freshK, but it is much more complicated.*)
   1.396 +
   1.397 +(*As with analz_image_freshK, we take some pains to express the property
   1.398 +  as a logical equivalence so that the simplifier can apply it.*)
   1.399 +goal thy  
   1.400 + "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
   1.401 +\        P --> (X : analz (G Un H)) = (X : analz H)";
   1.402 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   1.403 +qed "Nonce_secrecy_lemma";
   1.404 +
   1.405  goal thy 
   1.406 - "!!evs. evs : yahalom lost ==>                                           \
   1.407 -\     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
   1.408 -\     (EX K: newK``E. EX A B na X.                                        \
   1.409 -\            Says Server A                                                \
   1.410 -\                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}   \
   1.411 -\            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
   1.412 + "!!evs. evs : yahalom lost ==>                                          \
   1.413 +\        (ALL KK. KK <= Compl (range shrK) -->                               \
   1.414 +\             (ALL K: KK. ALL A B na X.                                       \
   1.415 +\                 Says Server A                                              \
   1.416 +\                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   1.417 +\                 ~: set_of_list evs)   -->  \
   1.418 +\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =      \
   1.419 +\             (Nonce NB : analz (sees lost Spy evs)))";
   1.420  by (etac yahalom.induct 1);
   1.421  by analz_Fake_tac;
   1.422 +by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   1.423 +by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
   1.424 +by (rtac ccontr 7);
   1.425 +by (subgoal_tac "ALL A B na X.                                       \
   1.426 +\                 Says Server A                                              \
   1.427 +\                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   1.428 +\                 ~: set_of_list evsa" 7);
   1.429 +by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
   1.430 +by (subgoal_tac "ALL A B na X.                                       \
   1.431 +\                 Says Server A                                              \
   1.432 +\                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
   1.433 +\                 ~: set_of_list evsa" 5);
   1.434  by (ALLGOALS  (*22 seconds*)
   1.435      (asm_simp_tac 
   1.436 -     (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
   1.437 -                          insert_Key_singleton, insert_Key_image]
   1.438 -                         @ pushes)
   1.439 -               setloop split_tac [expand_if])));
   1.440 +     (analz_image_freshK_ss  addsimps
   1.441 +             ([all_conj_distrib, 
   1.442 +               not_parts_not_analz, analz_image_freshK]
   1.443 +              @ pushes @ ball_simps))));
   1.444  (*Base*)
   1.445  by (fast_tac (!claset addss (!simpset)) 1);
   1.446 -(*Fake*) (** LEVEL 4 **)
   1.447 +(*Fake*) (** LEVEL 10 **)
   1.448  by (spy_analz_tac 1);
   1.449 -(*YM1-YM3*) (*24 seconds*)
   1.450 -by (EVERY (map grind_tac [3,2,1]));
   1.451 +(*YM3*)
   1.452 +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.453  (*Oops*)
   1.454 -by (Full_simp_tac 2);
   1.455 -by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
   1.456 -by (grind_tac 2);
   1.457 -by (fast_tac (!claset delrules [bexI] 
   1.458 -                      addDs [unique_session_keys]
   1.459 +(*20 secs*)
   1.460 +by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
   1.461                        addss (!simpset)) 2);
   1.462  (*YM4*)
   1.463 -(** LEVEL 10 **)
   1.464 -by (rtac (impI RS allI) 1);
   1.465 +(** LEVEL 13 **)
   1.466 +by (REPEAT (resolve_tac [impI, allI] 1));
   1.467  by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
   1.468 +by (stac insert_commute 1);
   1.469  by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   1.470 -by (asm_simp_tac (!simpset addsimps [analz_image_newK]
   1.471 -                           setloop split_tac [expand_if]) 1);
   1.472 -(** LEVEL 14 **)
   1.473 -by (grind_tac 1);
   1.474 -by (REPEAT (dtac not_analz_insert 1));
   1.475 +by (asm_simp_tac (analz_image_freshK_ss 
   1.476 +                  addsimps [analz_insertI, analz_image_freshK]) 1);
   1.477 +by (step_tac (!claset addSDs [not_analz_insert]) 1);
   1.478  by (lost_tac "A" 1);
   1.479 +(** LEVEL 20 **)
   1.480  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.481      THEN REPEAT (assume_tac 1));
   1.482 -by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
   1.483 -by (fast_tac (!claset delrules [conjI]
   1.484 -                      addIs [analz_insertI]
   1.485 -                      addss (!simpset)) 1);
   1.486 -val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
   1.487 +by (thin_tac "All ?PP" 1);
   1.488 +by (Fast_tac 1);
   1.489 +qed_spec_mp "Nonce_secrecy";
   1.490  
   1.491  
   1.492  (*Version required below: if NB can be decrypted using a session key then it
   1.493    was distributed with that key.  The more general form above is required
   1.494    for the induction to carry through.*)
   1.495  goal thy 
   1.496 - "!!evs. [| Says Server A                                                   \
   1.497 -\            {|Crypt (shrK A) {|Agent B, Key (newK i), na, Nonce NB'|}, X|} \
   1.498 -\           : set_of_list evs;                                              \
   1.499 -\           Nonce NB : analz (insert (Key (newK i)) (sees lost Spy evs));   \
   1.500 -\           evs : yahalom lost |]                                           \
   1.501 -\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
   1.502 -by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
   1.503 -by (dtac Nonce_secrecy 1 THEN assume_tac 1);
   1.504 -by (fast_tac (!claset addDs [unique_session_keys]
   1.505 -                      addss (!simpset)) 1);
   1.506 -val single_Nonce_secrecy = result();
   1.507 + "!!evs. [| Says Server A                                              \
   1.508 +\            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
   1.509 +\           : set_of_list evs;                                         \
   1.510 +\           Nonce NB : analz (insert (Key KAB) (sees lost Spy evs));   \
   1.511 +\           Nonce NB ~: analz (sees lost Spy evs);                     \
   1.512 +\           KAB ~: range shrK;  evs : yahalom lost |]                  \
   1.513 +\        ==>  NB = NB'";
   1.514 +by (rtac ccontr 1);
   1.515 +by (subgoal_tac "ALL A B na X.                                       \
   1.516 +\                 Says Server A                                              \
   1.517 +\                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
   1.518 +\                 ~: set_of_list evs" 1);
   1.519 +by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   1.520 +by (asm_simp_tac (analz_image_freshK_ss 
   1.521 +                  addsimps ([Nonce_secrecy] @ ball_simps)) 1);
   1.522 +by (auto_tac (!claset addDs [unique_session_keys], (!simpset)));
   1.523 +qed "single_Nonce_secrecy";
   1.524  
   1.525  
   1.526  goal thy 
   1.527 @@ -691,46 +602,41 @@
   1.528  by (ALLGOALS
   1.529      (asm_simp_tac 
   1.530       (!simpset addsimps ([not_parts_not_analz,
   1.531 -                          analz_insert_Key_newK] @ pushes)
   1.532 +                          analz_insert_freshK] @ pushes)
   1.533                 setloop split_tac [expand_if])));
   1.534  by (fast_tac (!claset addSIs [parts_insertI]
   1.535 -                      addSEs partsEs
   1.536 -                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.537 +                      addSEs sees_Spy_partsEs
   1.538                        addss (!simpset)) 2);
   1.539  (*Proof of YM2*) (** LEVEL 4 **)
   1.540 -by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); 
   1.541 -by (fast_tac (!claset addIs [parts_insertI]
   1.542 -                      addSEs partsEs
   1.543 -                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.544 -                      addss (!simpset)) 3);
   1.545 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
   1.546 +by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
   1.547 +                               impOfSubs analz_subset_parts]
   1.548 +                        addSEs partsEs) 3 2);
   1.549  (*Prove YM3 by showing that no NB can also be an NA*)
   1.550  by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
   1.551  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
   1.552  (*Fake*)
   1.553  by (spy_analz_tac 1);
   1.554 -(*YM4*) (** LEVEL 10 **)
   1.555 +(*YM4*) (** LEVEL 8 **)
   1.556  by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   1.557  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.558 +(*43 secs??*)
   1.559  by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
   1.560 -(** LEVEL 13 **)
   1.561  by (lost_tac "Aa" 1);
   1.562  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.563  by (forward_tac [Says_Server_message_form] 3);
   1.564  by (forward_tac [Says_Server_imp_YM2] 4);
   1.565 +(** LEVEL 15 **)
   1.566  by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   1.567 -by (Full_simp_tac 1);
   1.568 -by (REPEAT_FIRST hyp_subst_tac);
   1.569 -(** LEVEL 20 **)
   1.570  by (lost_tac "Ba" 1);
   1.571  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
   1.572  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.573                        addSEs [MPair_parts]) 1);
   1.574  by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
   1.575 +(** LEVEL 20 **)
   1.576  by (dtac Spy_not_see_encrypted_key 1);
   1.577  by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   1.578  by (spy_analz_tac 1);
   1.579 -(*Oops case*) (** LEVEL 27 **)
   1.580 +(*Oops case*) (** LEVEL 23 **)
   1.581  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.582  by (step_tac (!claset delrules [disjE, conjI]) 1);
   1.583  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.584 @@ -738,7 +644,7 @@
   1.585  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   1.586  by (rtac conjI 1);
   1.587  by (no_nonce_tac 1);
   1.588 -(** LEVEL 34 **)
   1.589 +(** LEVEL 30 **)
   1.590  by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   1.591  by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
   1.592  val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
   1.593 @@ -750,16 +656,16 @@
   1.594    ALL POSSIBLE keys instead of our particular K (though at least the
   1.595    nonces are forced to agree with NA and NB). *)
   1.596  goal thy 
   1.597 - "!!evs. [| Says B Server                                        \
   1.598 + "!!evs. [| Says B Server                                               \
   1.599  \            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
   1.600  \           : set_of_list evs;       \
   1.601  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
   1.602  \                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   1.603  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   1.604  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
   1.605 -\         ==> Says Server A                                       \
   1.606 -\                     {|Crypt (shrK A) {|Agent B, Key K,                         \
   1.607 -\                               Nonce NA, Nonce NB|},          \
   1.608 +\         ==> Says Server A                                             \
   1.609 +\                     {|Crypt (shrK A) {|Agent B, Key K,                \
   1.610 +\                               Nonce NA, Nonce NB|},                   \
   1.611  \                       Crypt (shrK B) {|Agent A, Key K|}|}             \
   1.612  \                   : set_of_list evs";
   1.613  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.614 @@ -771,4 +677,3 @@
   1.615  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   1.616  by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   1.617  qed "B_trusts_YM4";
   1.618 -