src/HOL/Auth/Yahalom.ML
changeset 2133 f00a688760b9
parent 2110 d01151e66cd4
child 2156 9c361df93bd5
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Oct 28 13:01:25 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Oct 28 13:02:37 1996 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 +Pretty.setdepth 20;
     1.8  
     1.9  
    1.10  (*Weak liveness: there are traces that reach the end*)
    1.11 @@ -61,7 +62,7 @@
    1.12  bind_thm ("YM4_parts_sees_Spy",
    1.13            YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.14  
    1.15 -(*Relates to both YM4 and Revl*)
    1.16 +(*Relates to both YM4 and Oops*)
    1.17  goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
    1.18  \                  : set_of_list evs ==> \
    1.19  \                K : parts (sees lost Spy evs)";
    1.20 @@ -90,36 +91,29 @@
    1.21  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.22      sends messages containing X! **)
    1.23  
    1.24 -(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
    1.25 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.26  goal thy 
    1.27 - "!!evs. [| evs : yahalom lost;  A ~: lost |]    \
    1.28 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.29 + "!!evs. evs : yahalom lost \
    1.30 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.31  by (parts_induct_tac 1);
    1.32  by (Auto_tac());
    1.33 -qed "Spy_not_see_shrK";
    1.34 -
    1.35 -bind_thm ("Spy_not_analz_shrK",
    1.36 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    1.37 -
    1.38 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    1.39 +qed "Spy_see_shrK";
    1.40 +Addsimps [Spy_see_shrK];
    1.41  
    1.42 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    1.43 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.44 -val major::prems = 
    1.45 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
    1.46 -\             evs : yahalom lost;                               \
    1.47 -\             A:lost ==> R                                  \
    1.48 -\           |] ==> R";
    1.49 -by (rtac ccontr 1);
    1.50 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
    1.51 -by (swap_res_tac prems 2);
    1.52 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    1.53 -qed "Spy_see_shrK_E";
    1.54 +goal thy 
    1.55 + "!!evs. evs : yahalom lost \
    1.56 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.57 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.58 +qed "Spy_analz_shrK";
    1.59 +Addsimps [Spy_analz_shrK];
    1.60  
    1.61 -bind_thm ("Spy_analz_shrK_E", 
    1.62 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
    1.63 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.64 +\                  evs : yahalom lost |] ==> A:lost";
    1.65 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.66 +qed "Spy_see_shrK_D";
    1.67  
    1.68 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
    1.69 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.70 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.71  
    1.72  
    1.73  (*** Future keys can't be seen or used! ***)
    1.74 @@ -160,6 +154,16 @@
    1.75  qed "Says_imp_old_keys";
    1.76  
    1.77  
    1.78 +(*Ready-made for the classical reasoner*)
    1.79 +goal thy "!!evs. [| Says A B {|Crypt {|b, Key (newK evs), na, nb|} K, X|}  \
    1.80 +\                   : set_of_list evs;  evs : yahalom lost |]              \
    1.81 +\                ==> R";
    1.82 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.83 +                      addss (!simpset addsimps [parts_insertI])) 1);
    1.84 +qed "Says_too_new_key";
    1.85 +AddSEs [Says_too_new_key];
    1.86 +
    1.87 +
    1.88  (*Nobody can have USED keys that will be generated in the future.
    1.89    ...very like new_keys_not_seen*)
    1.90  goal thy "!!evs. evs : yahalom lost ==> \
    1.91 @@ -167,7 +171,6 @@
    1.92  \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    1.93  by (parts_induct_tac 1);
    1.94  by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
    1.95 -
    1.96  (*YM1, YM2 and YM3*)
    1.97  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    1.98  (*Fake and YM4: these messages send unknown (X) components*)
    1.99 @@ -198,40 +201,25 @@
   1.100  Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.101  
   1.102  
   1.103 -(*Describes the form of Key K when the following message is sent.  The use of
   1.104 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.105 -  assumption A ~: lost prevents its being a Faked message.  (Based
   1.106 -  on NS_Shared/Says_S_message_form) *)
   1.107 -goal thy
   1.108 - "!!evs. evs: yahalom lost ==>                                           \
   1.109 -\        Crypt {|B, Key K, NA, NB|} (shrK A) : parts (sees lost Spy evs)  \
   1.110 -\        --> A ~: lost --> (EX evt: yahalom lost. K = newK evt)";
   1.111 -by (parts_induct_tac 1);
   1.112 -by (Auto_tac());
   1.113 -qed_spec_mp "Reveal_message_lemma";
   1.114 -
   1.115 -(*EITHER describes the form of Key K when the following message is sent, 
   1.116 -  OR     reduces it to the Fake case.*)
   1.117 -
   1.118 +(*Describes the form of K when the Server sends this message.  Useful for
   1.119 +  Oops as well as main secrecy property.*)
   1.120  goal thy 
   1.121 - "!!evs. [| Says S A {|Crypt {|B, Key K, NA, NB|} (shrK A), X|} \
   1.122 -\           : set_of_list evs;                                    \
   1.123 -\           evs : yahalom lost |]                                 \
   1.124 -\        ==> (EX evt: yahalom lost. K = newK evt)                 \
   1.125 -\          | Key K : analz (sees lost Spy evs)";
   1.126 -br (Reveal_message_lemma RS disjCI) 1;
   1.127 -ba 1;
   1.128 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.129 -                      addDs [impOfSubs analz_subset_parts]) 1);
   1.130 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.131 -                      addss (!simpset)) 1);
   1.132 -qed "Reveal_message_form";
   1.133 + "!!evs. [| Says Server A                                           \
   1.134 +\            {|Crypt {|Agent B, K, NA, NB|} (shrK A), X|} : set_of_list evs; \
   1.135 +\           evs : yahalom lost |]                                   \
   1.136 +\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   1.137 +by (etac rev_mp 1);
   1.138 +by (etac yahalom.induct 1);
   1.139 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.140 +qed "Says_Server_message_form";
   1.141  
   1.142  
   1.143  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.144  val analz_Fake_tac = 
   1.145 -    dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   1.146 -    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   1.147 +    forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   1.148 +    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.149 +    assume_tac 7 THEN Full_simp_tac 7 THEN
   1.150 +    REPEAT ((etac bexE ORELSE' hyp_subst_tac) 7);
   1.151  
   1.152  
   1.153  (****
   1.154 @@ -273,16 +261,15 @@
   1.155  by (etac yahalom.induct 1);
   1.156  by analz_Fake_tac;
   1.157  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   1.158 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 8));
   1.159  by (ALLGOALS  (*Takes 26 secs*)
   1.160      (asm_simp_tac 
   1.161       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.162                           @ pushes)
   1.163                 setloop split_tac [expand_if])));
   1.164  (** LEVEL 5 **)
   1.165 -(*Reveal case 2, YM4, Fake*) 
   1.166 -by (EVERY (map spy_analz_tac [6, 4, 2]));
   1.167 -(*Reveal case 1, YM3, Base*)
   1.168 +(*YM4, Fake*) 
   1.169 +by (EVERY (map spy_analz_tac [4, 2]));
   1.170 +(*Oops, YM3, Base*)
   1.171  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.172  qed_spec_mp "analz_image_newK";
   1.173  
   1.174 @@ -290,7 +277,7 @@
   1.175   "!!evs. evs : yahalom lost ==>                               \
   1.176  \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   1.177  \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   1.178 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.179 +by (asm_simp_tac (HOL_ss addsimps [analz_image_newK, 
   1.180                                     insert_Key_singleton]) 1);
   1.181  by (Fast_tac 1);
   1.182  qed "analz_insert_Key_newK";
   1.183 @@ -300,31 +287,28 @@
   1.184  
   1.185  goal thy 
   1.186   "!!evs. evs : yahalom lost ==>                                     \
   1.187 -\      EX A' B' NA' NB'. ALL A B NA NB.                             \
   1.188 +\      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
   1.189  \          Says Server A                                            \
   1.190 -\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),            \
   1.191 -\             Crypt {|Agent A, Key K|} (shrK B)|}                   \
   1.192 -\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB'";
   1.193 +\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
   1.194 +\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   1.195  by (etac yahalom.induct 1);
   1.196  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.197  by (Step_tac 1);
   1.198 +by (ex_strip_tac 2);
   1.199 +by (Fast_tac 2);
   1.200  (*Remaining case: YM3*)
   1.201  by (expand_case_tac "K = ?y" 1);
   1.202  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.203  (*...we assume X is a very new message, and handle this case by contradiction*)
   1.204 -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.205 -                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.206 -                      addss (!simpset addsimps [parts_insertI])) 1);
   1.207 +by (Fast_tac 1);  (*uses Says_too_new_key*)
   1.208  val lemma = result();
   1.209  
   1.210  goal thy 
   1.211  "!!evs. [| Says Server A                                            \
   1.212 -\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),            \
   1.213 -\             Crypt {|Agent A, Key K|} (shrK B)|}                   \
   1.214 +\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
   1.215  \           : set_of_list evs;                                      \
   1.216  \          Says Server A'                                           \
   1.217 -\           {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'),        \
   1.218 -\             Crypt {|Agent A', Key K|} (shrK B')|}                 \
   1.219 +\           {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), X'|}   \
   1.220  \           : set_of_list evs;                                      \
   1.221  \          evs : yahalom lost |]                                    \
   1.222  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.223 @@ -350,24 +334,10 @@
   1.224  qed "A_trust_YM3";
   1.225  
   1.226  
   1.227 -(*Describes the form of K when the Server sends this message.*)
   1.228 -goal thy 
   1.229 - "!!evs. [| Says Server A                                           \
   1.230 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
   1.231 -\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
   1.232 -\           evs : yahalom lost |]                                   \
   1.233 -\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   1.234 -by (etac rev_mp 1);
   1.235 -by (etac yahalom.induct 1);
   1.236 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.237 -qed "Says_Server_message_form";
   1.238 -
   1.239 -
   1.240  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   1.241  
   1.242  goal thy 
   1.243 - "!!evs. [| A ~: lost;  B ~: lost;                                \
   1.244 -\           evs : yahalom lost;  evt : yahalom lost |]            \
   1.245 + "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.246  \        ==> Says Server A                                        \
   1.247  \              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),       \
   1.248  \                Crypt {|Agent A, Key K|} (shrK B)|}              \
   1.249 @@ -376,28 +346,18 @@
   1.250  \            Key K ~: analz (sees lost Spy evs)";
   1.251  by (etac yahalom.induct 1);
   1.252  by analz_Fake_tac;
   1.253 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.254  by (ALLGOALS
   1.255      (asm_simp_tac 
   1.256       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.257                            analz_insert_Key_newK] @ pushes)
   1.258                 setloop split_tac [expand_if])));
   1.259  (*YM3*)
   1.260 -by (fast_tac (!claset addIs [parts_insertI]
   1.261 -                      addEs [Says_imp_old_keys RS less_irrefl]
   1.262 -                      addss (!simpset)) 2);
   1.263 -(*Reveal case 2, OR4, Fake*) 
   1.264 +by (Fast_tac 2);  (*uses Says_too_new_key*)
   1.265 +(*OR4, Fake*) 
   1.266  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.267 -(*Reveal case 1*) (** LEVEL 6 **)
   1.268 -by (case_tac "Aa : lost" 1);
   1.269 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.270 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.271 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.272 -(*So now we have  Aa ~: lost *)
   1.273 -bd (Says_imp_sees_Spy RS parts.Inj) 1;
   1.274 +(*Oops*) (** LEVEL 6 **)
   1.275  by (fast_tac (!claset delrules [disjE] 
   1.276 -	              addSEs [MPair_parts]
   1.277 -		      addDs [A_trust_YM3, unique_session_keys]
   1.278 +		      addDs [unique_session_keys]
   1.279  	              addss (!simpset)) 1);
   1.280  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.281  
   1.282 @@ -448,12 +408,175 @@
   1.283  by (Fast_tac 1);
   1.284  qed "B_trusts_YM4_shrK";
   1.285  
   1.286 -(*B knows, by the second part of A's message, that the Server distributed 
   1.287 -  the key quoting nonce NB.  This part says nothing about agent names.*)
   1.288 +
   1.289 +(*** General properties of nonces ***)
   1.290 +
   1.291 +goal thy "!!evs. evs : yahalom lost ==> \
   1.292 +\                length evs <= length evt --> \
   1.293 +\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
   1.294 +by (etac yahalom.induct 1);
   1.295 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.296 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
   1.297 +                                     addcongs [disj_cong])));
   1.298 +by (REPEAT_FIRST
   1.299 +    (fast_tac (!claset addSEs partsEs
   1.300 +	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
   1.301 +		       addDs  [impOfSubs analz_subset_parts,
   1.302 +			       impOfSubs parts_insert_subset_Un, Suc_leD]
   1.303 +		       addss (!simpset))));
   1.304 +val lemma = result();
   1.305 +
   1.306 +(*Variant needed for the main theorem below*)
   1.307 +goal thy 
   1.308 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   1.309 +\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
   1.310 +by (fast_tac (!claset addDs [lemma]) 1);
   1.311 +qed "new_nonces_not_seen";
   1.312 +Addsimps [new_nonces_not_seen];
   1.313 +
   1.314 +(*Another variant: old messages must contain old nonces!*)
   1.315 +goal thy 
   1.316 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.317 +\           Nonce (newN evt) : parts {X};    \
   1.318 +\           evs : yahalom lost                 \
   1.319 +\        |] ==> length evt < length evs";
   1.320 +by (rtac ccontr 1);
   1.321 +by (dtac leI 1);
   1.322 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   1.323 +                      addIs  [impOfSubs parts_mono]) 1);
   1.324 +qed "Says_imp_old_nonces";
   1.325 +
   1.326 +
   1.327 +(** The Nonce NB uniquely identifies B's message. **)
   1.328 +
   1.329 +val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   1.330 +
   1.331 +goal thy 
   1.332 + "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
   1.333 +\      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
   1.334 +\      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   1.335 +by (parts_induct_tac 1);  (*TWO MINUTES*)
   1.336 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.337 +(*YM2: creation of new Nonce.  Move assertion into global context*)
   1.338 +by (expand_case_tac "NB = ?y" 1);
   1.339 +by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   1.340 +val lemma = result();
   1.341 +
   1.342  goal thy 
   1.343 - "!!evs. evs : yahalom lost                                     \
   1.344 -\        ==> Key K ~: analz (sees lost Spy evs) -->             \
   1.345 -\            Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
   1.346 + "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
   1.347 +\                  : parts (sees lost Spy evs);         \
   1.348 +\          Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
   1.349 +\                  : parts (sees lost Spy evs);         \
   1.350 +\          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   1.351 +\        ==> NA' = NA & A' = A & B' = B";
   1.352 +by (dtac lemma 1);
   1.353 +by (REPEAT (etac exE 1));
   1.354 +(*Duplicate the assumption*)
   1.355 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.356 +by (fast_tac (!claset addSDs [spec]) 1);
   1.357 +qed "unique_NB";
   1.358 +
   1.359 +fun lost_tac s =
   1.360 +    case_tac ("(" ^ s ^ ") : lost") THEN'
   1.361 +    SELECT_GOAL 
   1.362 +      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   1.363 +       REPEAT_DETERM (etac MPair_analz 1) THEN
   1.364 +       dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
   1.365 +       assume_tac 1 THEN Fast_tac 1);
   1.366 +
   1.367 +fun lost_tac s =
   1.368 +    case_tac ("(" ^ s ^ ") : lost") THEN'
   1.369 +    SELECT_GOAL 
   1.370 +      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   1.371 +       REPEAT_DETERM (etac MPair_analz 1) THEN
   1.372 +       THEN_BEST_FIRST 
   1.373 +         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   1.374 + 	 (has_fewer_prems 1, size_of_thm)
   1.375 +	 (Step_tac 1));
   1.376 +
   1.377 +
   1.378 +(*Variant useful for proving secrecy of NB*)
   1.379 +goal thy 
   1.380 + "!!evs.[| Says C D   {|X,  Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
   1.381 +\          : set_of_list evs;  B ~: lost;         \
   1.382 +\          Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
   1.383 +\          : set_of_list evs;                           \
   1.384 +\          NB ~: analz (sees lost Spy evs);             \
   1.385 +\          evs : yahalom lost |]  \
   1.386 +\        ==> NA' = NA & A' = A & B' = B";
   1.387 +by (lost_tac "B'" 1);
   1.388 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.389 +                      addSEs [MPair_parts]
   1.390 +                      addDs  [unique_NB]) 1);
   1.391 +qed "Says_unique_NB";
   1.392 +
   1.393 +goal thy 
   1.394 + "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
   1.395 +\ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
   1.396 +\      Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
   1.397 +\ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
   1.398 +by (etac yahalom.induct 1);
   1.399 +by parts_Fake_tac;
   1.400 +by (REPEAT_FIRST 
   1.401 +    (rtac impI THEN' 
   1.402 +     dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   1.403 +     mp_tac));
   1.404 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.405 +			     impOfSubs Fake_parts_insert]
   1.406 +	              addss (!simpset)) 2);
   1.407 +by (ALLGOALS Asm_simp_tac);
   1.408 +by (fast_tac (!claset addss (!simpset)) 1);
   1.409 +by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   1.410 +	              addSIs [parts_insertI]
   1.411 +                      addSEs partsEs
   1.412 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.413 +                      addss (!simpset)) 1);
   1.414 +val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
   1.415 +
   1.416 +
   1.417 +
   1.418 +(**** Towards proving secrecy of Nonce NB ****)
   1.419 +
   1.420 +(*B knows, by the second part of A's message, that the Server distributed 
   1.421 +  the key quoting nonce NB.  This part says nothing about agent names. 
   1.422 +  Secrecy of NB is crucial.*)
   1.423 +goal thy 
   1.424 + "!!evs. evs : yahalom lost                                             \
   1.425 +\        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   1.426 +\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
   1.427 +\            (EX A B NA. Says Server A                                  \
   1.428 +\                        {|Crypt {|Agent B, Key K,                      \
   1.429 +\                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.430 +\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   1.431 +\                       : set_of_list evs)";
   1.432 +by (etac yahalom.induct 1);
   1.433 +by parts_Fake_tac;
   1.434 +by (fast_tac (!claset addss (!simpset)) 1);
   1.435 +by (REPEAT_FIRST
   1.436 +    (rtac impI THEN'
   1.437 +     dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   1.438 +by (ALLGOALS Asm_simp_tac);
   1.439 +(*Fake, YM3, YM4*)
   1.440 +by (Fast_tac 2);
   1.441 +by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   1.442 +                      addDs [impOfSubs analz_subset_parts]
   1.443 +                      addss (!simpset)) 1);
   1.444 +(*YM4*)
   1.445 +by (Step_tac 1);
   1.446 +by (lost_tac "A" 1);
   1.447 +by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   1.448 +			     A_trust_YM3]) 1);
   1.449 +val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
   1.450 +
   1.451 +
   1.452 +(*This is the original version of the result above.  But it is of little
   1.453 +  value because it assumes secrecy of K, which we cannot be assured of
   1.454 +  until we know that K is fresh -- which we do not know at the point this
   1.455 +  result is applied.*)
   1.456 +goal thy 
   1.457 + "!!evs. evs : yahalom lost                                             \
   1.458 +\        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   1.459 +\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
   1.460  \            (EX A B NA. Says Server A                                  \
   1.461  \                        {|Crypt {|Agent B, Key K,                      \
   1.462  \                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.463 @@ -468,37 +591,216 @@
   1.464  by (ALLGOALS Asm_simp_tac);
   1.465  (*Fake, YM3, YM4*)
   1.466  by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   1.467 -                      addDs [impOfSubs analz_subset_parts]) 1);
   1.468 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   1.469  by (Fast_tac 1);
   1.470  (*YM4*)
   1.471  by (Step_tac 1);
   1.472 -by (case_tac "A : lost" 1);
   1.473 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.474 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.475 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.476 +by (lost_tac "A" 1);
   1.477  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   1.478  			     A_trust_YM3]) 1);
   1.479 -val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
   1.480 +result() RS mp RSN (2, rev_mp);
   1.481 +
   1.482 +
   1.483 +(*YM3 can only be triggered by YM2*)
   1.484 +goal thy 
   1.485 + "!!evs. [| Says Server A                                           \
   1.486 +\            {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
   1.487 +\           evs : yahalom lost |]                                        \
   1.488 +\        ==> EX B'. Says B' Server                                       \
   1.489 +\                      {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
   1.490 +\                   : set_of_list evs";
   1.491 +by (etac rev_mp 1);
   1.492 +by (etac yahalom.induct 1);
   1.493 +by (ALLGOALS Asm_simp_tac);
   1.494 +by (ALLGOALS Fast_tac);
   1.495 +qed "Says_Server_imp_YM2";
   1.496 +
   1.497 +
   1.498 +(** Dedicated tactics for the nonce secrecy proofs **)
   1.499 +
   1.500 +val no_nonce_tac = SELECT_GOAL
   1.501 +   (REPEAT (resolve_tac [impI, notI] 1) THEN
   1.502 +    REPEAT (hyp_subst_tac 1) THEN
   1.503 +    etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
   1.504 +    THEN
   1.505 +    etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
   1.506 +    THEN 
   1.507 +    REPEAT_FIRST assume_tac);
   1.508 +
   1.509 +val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
   1.510 +
   1.511 +fun grind_tac i = 
   1.512 + SELECT_GOAL
   1.513 +  (REPEAT_FIRST 
   1.514 +   (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
   1.515 +    assume_tac ORELSE'
   1.516 +    depth_tac (!claset delrules [conjI]
   1.517 +		       addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
   1.518 +			       impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
   1.519 +
   1.520 +(*The only nonces that can be found with the help of session keys are
   1.521 +  those distributed as nonce NB by the Server.  The form of the theorem
   1.522 +  recalls analz_image_newK, but it is much more complicated.*)
   1.523 +goal thy 
   1.524 + "!!evs. evs : yahalom lost ==>                                           \
   1.525 +\     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
   1.526 +\     (EX K: newK``E. EX A B na X.                                        \
   1.527 +\            Says Server A                                                \
   1.528 +\                {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|}   \
   1.529 +\            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
   1.530 +by (etac yahalom.induct 1);
   1.531 +by analz_Fake_tac;
   1.532 +by (ALLGOALS  (*45 SECONDS*)
   1.533 +    (asm_simp_tac 
   1.534 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.535 +                          analz_image_newK,
   1.536 +			  insert_Key_singleton, insert_Key_image]
   1.537 +			 @ pushes)
   1.538 +               setloop split_tac [expand_if])));
   1.539 +(*Base*)
   1.540 +by (fast_tac (!claset addss (!simpset)) 1);
   1.541 +(*Fake*) (** LEVEL 4 **)
   1.542 +by (spy_analz_tac 1);
   1.543 +(*YM1-YM3*)
   1.544 +by (EVERY (map grind_tac [3,2,1]));
   1.545 +(*Oops*)
   1.546 +by (Full_simp_tac 2);
   1.547 +by (REPEAT ((eresolve_tac [bexE] ORELSE' hyp_subst_tac) 2));
   1.548 +by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
   1.549 +by (grind_tac 2);
   1.550 +by (fast_tac (!claset delrules [bexI] 
   1.551 +		      addDs [unique_session_keys]
   1.552 +	              addss (!simpset)) 2);
   1.553 +(*YM4*)
   1.554 +(** LEVEL 11 **)
   1.555 +br (impI RS allI) 1;
   1.556 +by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN 
   1.557 +    Fast_tac 1);
   1.558 +by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   1.559 +by (asm_simp_tac (!simpset addsimps [analz_image_newK]
   1.560 +	                   setloop split_tac [expand_if]) 1);
   1.561 +(** LEVEL 15 **)
   1.562 +by (grind_tac 1);
   1.563 +by (REPEAT (dtac not_analz_insert 1));
   1.564 +by (lost_tac "A" 1);
   1.565 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1
   1.566 +    THEN REPEAT (assume_tac 1));
   1.567 +by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
   1.568 +by (fast_tac (!claset delrules [conjI]
   1.569 +	              addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.570 +		      addss (!simpset)) 1);
   1.571 +val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
   1.572 +
   1.573 +
   1.574 +(*Version required below: if NB can be decrypted using a session key then it
   1.575 +  was distributed with that key.  The more general form above is required
   1.576 +  for the induction to carry through.*)
   1.577 +goal thy 
   1.578 + "!!evs. [| Says Server A                                                     \
   1.579 +\            {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
   1.580 +\           : set_of_list evs;                                                \
   1.581 +\           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
   1.582 +\           evs : yahalom lost |]                                             \
   1.583 +\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
   1.584 +by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
   1.585 +by (dtac Nonce_secrecy 1 THEN assume_tac 1);
   1.586 +by (fast_tac (!claset addDs [unique_session_keys]
   1.587 +	              addss (!simpset)) 1);
   1.588 +val single_Nonce_secrecy = result();
   1.589 +
   1.590 +
   1.591 +goal thy 
   1.592 + "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   1.593 +\ ==> Says B Server                                                    \
   1.594 +\          {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
   1.595 +\     : set_of_list evs -->                               \
   1.596 +\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   1.597 +\     Nonce NB ~: analz (sees lost Spy evs)";
   1.598 +by (etac yahalom.induct 1);
   1.599 +by analz_Fake_tac;
   1.600 +by (ALLGOALS
   1.601 +    (asm_simp_tac 
   1.602 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.603 +                          analz_insert_Key_newK] @ pushes)
   1.604 +               setloop split_tac [expand_if])));
   1.605 +by (fast_tac (!claset addSIs [parts_insertI]
   1.606 +                      addSEs partsEs
   1.607 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.608 +                      addss (!simpset)) 2);
   1.609 +(*Proof of YM2*) (** LEVEL 5 **)
   1.610 +by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); 
   1.611 +by (fast_tac (!claset addIs [parts_insertI]
   1.612 +                      addSEs partsEs
   1.613 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.614 +                      addss (!simpset)) 3);
   1.615 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
   1.616 +(*Prove YM3 by showing that no NB can also be an NA*)
   1.617 +by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
   1.618 +by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
   1.619 +(*Fake*) (** LEVEL 10 **)
   1.620 +by (SELECT_GOAL (REPEAT (Safe_step_tac 1 ORELSE spy_analz_tac 1)) 1);
   1.621 +(*YM4*)
   1.622 +by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   1.623 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.624 +by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
   1.625 +(** LEVEL 14 **)
   1.626 +by (lost_tac "Aa" 1);
   1.627 +bd (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1;
   1.628 +by (forward_tac [Says_Server_message_form] 3);
   1.629 +by (forward_tac [Says_Server_imp_YM2] 4);
   1.630 +by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   1.631 +by (Full_simp_tac 1);
   1.632 +(** LEVEL 20 **)
   1.633 +by (REPEAT_FIRST hyp_subst_tac);
   1.634 +by (lost_tac "Ba" 1);
   1.635 +bd (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1;
   1.636 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.637 +                      addSEs [MPair_parts]) 1);
   1.638 +by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
   1.639 +bd Spy_not_see_encrypted_key 1;
   1.640 +by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   1.641 +by (spy_analz_tac 1);
   1.642 +(*Oops case*) (** LEVEL 28 **)
   1.643 +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.644 +by (step_tac (!claset delrules [disjE, conjI]) 1);
   1.645 +by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.646 +by (expand_case_tac "NB = NBa" 1);
   1.647 +by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   1.648 +br conjI 1;
   1.649 +by (no_nonce_tac 1);
   1.650 +(** LEVEL 35 **)
   1.651 +by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   1.652 +by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
   1.653 +val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
   1.654 +
   1.655  
   1.656  (*What can B deduce from receipt of YM4?  Note how the two components of
   1.657    the message contribute to a single conclusion about the Server's message.
   1.658    It's annoying that the "Says A Spy" assumption must quantify over 
   1.659 -  ALL POSSIBLE nonces instead of our particular NB.  Perhaps a different
   1.660 -  proof of B_trusts_YM4_newK could eliminate this problem.*)
   1.661 +  ALL POSSIBLE keys instead of our particular K (though at least the
   1.662 +  nonces are forced to agree with NA and NB). *)
   1.663  goal thy 
   1.664 - "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   1.665 + "!!evs. [| Says B Server                                        \
   1.666 +\            {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}  \
   1.667 +\           : set_of_list evs;       \
   1.668 +\           Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   1.669  \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   1.670 -\           ALL N N'. Says A Spy {|N,N', Key K|} ~: set_of_list evs;    \
   1.671 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   1.672 -\        ==> EX NA. Says Server A                                       \
   1.673 +\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   1.674 +\           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
   1.675 +\         ==> Says Server A                                       \
   1.676  \                     {|Crypt {|Agent B, Key K,                         \
   1.677  \                               Nonce NA, Nonce NB|} (shrK A),          \
   1.678  \                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   1.679  \                   : set_of_list evs";
   1.680 -be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
   1.681 -bd B_trusts_YM4_shrK 1;
   1.682 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.683 +by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   1.684 +    dtac B_trusts_YM4_shrK 1);
   1.685  bd B_trusts_YM4_newK 3;
   1.686  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.687 -by (fast_tac (!claset addDs [unique_session_keys]) 2);
   1.688 -by (fast_tac (!claset addDs [Spy_not_see_encrypted_key]) 1);
   1.689 +by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.690 +by (dresolve_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
   1.691 +by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   1.692  qed "B_trust_YM4";
   1.693 +
   1.694 +
   1.695 +