src/HOL/Auth/Yahalom.ML
changeset 1995 c80e58e78d9c
parent 1985 84cf16192e03
child 2001 974167c1d2c4
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Sep 13 13:15:48 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Sep 13 13:16:57 1996 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Auth/OtwayRees
     1.5 +(*  Title:      HOL/Auth/Yahalom
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1996  University of Cambridge
     1.9 @@ -10,11 +10,25 @@
    1.10    Proc. Royal Soc. 426 (1989)
    1.11  *)
    1.12  
    1.13 -open OtwayRees;
    1.14 +open Yahalom;
    1.15  
    1.16  proof_timing:=true;
    1.17  HOL_quantifiers := false;
    1.18  
    1.19 +
    1.20 +(** Weak liveness: there are traces that reach the end **)
    1.21 +
    1.22 +goal thy 
    1.23 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.24 +\        ==> EX X NB K. EX evs: yahalom.          \
    1.25 +\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    1.26 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.27 +br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
    1.28 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.29 +by (ALLGOALS Fast_tac);
    1.30 +qed "weak_liveness";
    1.31 +
    1.32 +
    1.33  (**** Inductive proofs about yahalom ****)
    1.34  
    1.35  (*The Enemy can see more than anybody else, except for their initial state*)
    1.36 @@ -45,30 +59,19 @@
    1.37  
    1.38  (** For reasoning about the encrypted portion of messages **)
    1.39  
    1.40 -goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
    1.41 -\                X : analz (sees Enemy evs)";
    1.42 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.43 -qed "YM2_analz_sees_Enemy";
    1.44 -
    1.45 -goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
    1.46 +(*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.47 +goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
    1.48  \                X : analz (sees Enemy evs)";
    1.49  by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.50  qed "YM4_analz_sees_Enemy";
    1.51  
    1.52 -goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
    1.53 +goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
    1.54 +\                  : set_of_list evs ==> \
    1.55  \                K : parts (sees Enemy evs)";
    1.56  by (fast_tac (!claset addSEs partsEs
    1.57  	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.58 -qed "YM5_parts_sees_Enemy";
    1.59 +qed "YM4_parts_sees_Enemy";
    1.60  
    1.61 -(*YM2_analz... and YM4_analz... let us treat those cases using the same 
    1.62 -  argument as for the Fake case.  This is possible for most, but not all,
    1.63 -  proofs: Fake does not invent new nonces (as in YM2), and of course Fake
    1.64 -  messages originate from the Enemy. *)
    1.65 -
    1.66 -val YM2_YM4_tac = 
    1.67 -    dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    1.68 -    dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    1.69  
    1.70  
    1.71  (*** Shared keys are not betrayed ***)
    1.72 @@ -78,11 +81,13 @@
    1.73   "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
    1.74  \        Key (shrK A) ~: parts (sees Enemy evs)";
    1.75  be yahalom.induct 1;
    1.76 -by YM2_YM4_tac;
    1.77 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
    1.78 +by (ALLGOALS Asm_simp_tac);
    1.79 +by (stac insert_commute 3);
    1.80  by (Auto_tac());
    1.81 -(*Deals with Fake message*)
    1.82 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.83 -			     impOfSubs Fake_parts_insert]) 1);
    1.84 +(*Fake and YM4 are similar*)
    1.85 +by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
    1.86 +					impOfSubs Fake_parts_insert])));
    1.87  qed "Enemy_not_see_shrK";
    1.88  
    1.89  bind_thm ("Enemy_not_analz_shrK",
    1.90 @@ -94,7 +99,7 @@
    1.91    As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.92  val major::prems = 
    1.93  goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
    1.94 -\             evs : yahalom;                                 \
    1.95 +\             evs : yahalom;                               \
    1.96  \             A:bad ==> R                                  \
    1.97  \           |] ==> R";
    1.98  br ccontr 1;
    1.99 @@ -121,13 +126,11 @@
   1.100  \                length evs <= length evs' --> \
   1.101  \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.102  be yahalom.induct 1;
   1.103 -by YM2_YM4_tac;
   1.104 -(*auto_tac does not work here, as it performs safe_tac first*)
   1.105 -by (ALLGOALS Asm_simp_tac);
   1.106 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.107  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.108 -				       impOfSubs parts_insert_subset_Un,
   1.109 -				       Suc_leD]
   1.110 -			        addss (!simpset))));
   1.111 +					   impOfSubs parts_insert_subset_Un,
   1.112 +					   Suc_leD]
   1.113 +			            addss (!simpset))));
   1.114  val lemma = result();
   1.115  
   1.116  (*Variant needed for the main theorem below*)
   1.117 @@ -156,27 +159,24 @@
   1.118  \                length evs <= length evs' --> \
   1.119  \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.120  be yahalom.induct 1;
   1.121 -by YM2_YM4_tac;
   1.122 -bd YM5_parts_sees_Enemy 7;
   1.123 -by (ALLGOALS Asm_simp_tac);
   1.124 -(*YM1 and YM3*)
   1.125 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   1.126 -(*Fake, YM2, YM4: these messages send unknown (X) components*)
   1.127 -by (EVERY 
   1.128 -    (map
   1.129 +by (forward_tac [YM4_parts_sees_Enemy] 6);
   1.130 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.131 +by (ALLGOALS Asm_full_simp_tac);
   1.132 +(*YM1, YM2 and YM3*)
   1.133 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   1.134 +(*Fake and YM4: these messages send unknown (X) components*)
   1.135 +by (stac insert_commute 2);
   1.136 +by (Simp_tac 2);
   1.137 +(*YM4: the only way K could have been used is if it had been seen,
   1.138 +  contradicting new_keys_not_seen*)
   1.139 +by (ALLGOALS
   1.140       (best_tac
   1.141 -      (!claset addSDs [newK_invKey]
   1.142 -	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.143 +      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.144  		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.145  		      Suc_leD]
   1.146 -	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.147 -	       addss (!simpset)))
   1.148 -     [3,2,1]));
   1.149 -(*YM5: dummy message*)
   1.150 -by (best_tac (!claset addSDs [newK_invKey]
   1.151 -		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
   1.152 -			addIs  [less_SucI, impOfSubs keysFor_mono]
   1.153 -			addss (!simpset addsimps [le_def])) 1);
   1.154 +	       addDs [impOfSubs analz_subset_parts]
   1.155 +	       addEs [new_keys_not_seen RSN(2,rev_notE)]
   1.156 +	       addss (!simpset))));
   1.157  val lemma = result();
   1.158  
   1.159  goal thy 
   1.160 @@ -214,14 +214,16 @@
   1.161  \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.162  \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.163  be yahalom.induct 1;
   1.164 -by YM2_YM4_tac;
   1.165 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.166  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.167  (*Deals with Faked messages*)
   1.168 -by (best_tac (!claset addSEs partsEs
   1.169 -		      addDs [impOfSubs analz_subset_parts,
   1.170 -                             impOfSubs parts_insert_subset_Un]
   1.171 -                      addss (!simpset)) 2);
   1.172 -(*Base case and YM5*)
   1.173 +by (EVERY 
   1.174 +    (map (best_tac (!claset addSEs partsEs
   1.175 +			    addDs [impOfSubs analz_subset_parts,
   1.176 +				   impOfSubs parts_insert_subset_Un]
   1.177 +			    addss (!simpset)))
   1.178 +     [3,2]));
   1.179 +(*Base case*)
   1.180  by (Auto_tac());
   1.181  result();
   1.182  
   1.183 @@ -259,19 +261,6 @@
   1.184  
   1.185  (** Session keys are not used to encrypt other session keys **)
   1.186  
   1.187 -(*Could generalize this so that the X component doesn't have to be first
   1.188 -  in the message?*)
   1.189 -val enemy_analz_tac =
   1.190 -  SELECT_GOAL 
   1.191 -   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
   1.192 -	   dtac (impOfSubs Fake_analz_insert) 1,
   1.193 -	   eresolve_tac [asm_rl, synth.Inj] 1,
   1.194 -	   Fast_tac 1,
   1.195 -	   Asm_full_simp_tac 1,
   1.196 -	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
   1.197 -	   ]);
   1.198 -
   1.199 -
   1.200  (*Lemma for the trivial direction of the if-and-only-if*)
   1.201  goal thy  
   1.202   "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   1.203 @@ -286,34 +275,23 @@
   1.204  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.205  \           (K : newK``E | Key K : analz (sees Enemy evs))";
   1.206  be yahalom.induct 1;
   1.207 -bd YM2_analz_sees_Enemy 4;
   1.208  bd YM4_analz_sees_Enemy 6;
   1.209  by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   1.210 -by (ALLGOALS (*Takes 35 secs*)
   1.211 +by (ALLGOALS 
   1.212      (asm_simp_tac 
   1.213       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.214  			 @ pushes)
   1.215                 setloop split_tac [expand_if])));
   1.216  (*YM4*) 
   1.217 -by (enemy_analz_tac 5);
   1.218 +by (enemy_analz_tac 4);
   1.219  (*YM3*)
   1.220 -by (Fast_tac 4);
   1.221 -(*YM2*) (** LEVEL 7 **)
   1.222 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   1.223 -    (insert_commute RS ssubst) 3);
   1.224 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.225 -    (insert_commute RS ssubst) 3);
   1.226 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   1.227 -by (enemy_analz_tac 3);
   1.228 -(*Fake case*) (** LEVEL 11 **)
   1.229 -by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   1.230 -    (insert_commute RS ssubst) 2);
   1.231 +by (Fast_tac 3);
   1.232 +(*Fake case*)
   1.233  by (enemy_analz_tac 2);
   1.234  (*Base case*)
   1.235  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.236  qed_spec_mp "analz_image_newK";
   1.237  
   1.238 -
   1.239  goal thy
   1.240   "!!evs. evs : yahalom ==>                               \
   1.241  \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   1.242 @@ -326,29 +304,28 @@
   1.243  
   1.244  (*Describes the form *and age* of K when the following message is sent*)
   1.245  goal thy 
   1.246 - "!!evs. [| Says Server B \
   1.247 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.248 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.249 + "!!evs. [| Says Server A                                           \
   1.250 +\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
   1.251 +\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
   1.252  \           evs : yahalom |]                                        \
   1.253 -\        ==> (EX evt:yahalom. K = Key(newK evt) & \
   1.254 -\                           length evt < length evs) &            \
   1.255 -\            (EX i. NA = Nonce i)";
   1.256 +\        ==> (EX evt:yahalom. K = Key(newK evt) &                   \
   1.257 +\                           length evt < length evs)";
   1.258  be rev_mp 1;
   1.259  be yahalom.induct 1;
   1.260  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.261  qed "Says_Server_message_form";
   1.262  
   1.263  
   1.264 -(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
   1.265 +(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3
   1.266 +  As with Otway-Rees, proof does not need uniqueness of session keys.*)
   1.267  goal thy 
   1.268   "!!evs. [| Says Server A \
   1.269 -\            {|NA, Crypt {|NA, K|} (shrK B),                      \
   1.270 -\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
   1.271 -\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
   1.272 +\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   1.273 +\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   1.274 +\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
   1.275  \     K ~: analz (sees Enemy evs)";
   1.276  be rev_mp 1;
   1.277  be yahalom.induct 1;
   1.278 -bd YM2_analz_sees_Enemy 4;
   1.279  bd YM4_analz_sees_Enemy 6;
   1.280  by (ALLGOALS Asm_simp_tac);
   1.281  (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.282 @@ -360,87 +337,10 @@
   1.283       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.284  			  analz_insert_Key_newK] @ pushes)
   1.285                 setloop split_tac [expand_if])));
   1.286 +(*YM4*)
   1.287 +by (enemy_analz_tac 3);
   1.288  (*YM3*)
   1.289 -by (fast_tac (!claset addSEs [less_irrefl]) 3);
   1.290 +by (fast_tac (!claset addSEs [less_irrefl]) 2);
   1.291  (*Fake*) (** LEVEL 10 **)
   1.292 -by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   1.293 -by (enemy_analz_tac 1);
   1.294 -(*YM4*)
   1.295 -by (mp_tac 2);
   1.296 -by (enemy_analz_tac 2);
   1.297 -(*YM2*)
   1.298 -by (mp_tac 1);
   1.299 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.300 -    (insert_commute RS ssubst) 1);
   1.301 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.302  by (enemy_analz_tac 1);
   1.303  qed "Enemy_not_see_encrypted_key";
   1.304 -
   1.305 -
   1.306 -
   1.307 -(*** Session keys are issued at most once, and identify the principals ***)
   1.308 -
   1.309 -(** First, two lemmas for the Fake, YM2 and YM4 cases **)
   1.310 -
   1.311 -goal thy 
   1.312 - "!!evs. [| X : synth (analz (sees Enemy evs));                \
   1.313 -\           Crypt X' (shrK C) : parts{X};                      \
   1.314 -\           C ~: bad;  evs : yahalom |]  \
   1.315 -\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   1.316 -by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.317 -	              addDs [impOfSubs parts_insert_subset_Un]
   1.318 -                      addss (!simpset)) 1);
   1.319 -qed "Crypt_Fake_parts";
   1.320 -
   1.321 -goal thy 
   1.322 - "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
   1.323 -\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   1.324 -\            Crypt X' K : parts {Y}";
   1.325 -bd parts_singleton 1;
   1.326 -by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.327 -qed "Crypt_parts_singleton";
   1.328 -
   1.329 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.330 -
   1.331 -(*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.332 -  C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.333 -goal thy 
   1.334 - "!!evs. evs : yahalom ==>                                     \
   1.335 -\      EX A B. ALL C.                                        \
   1.336 -\         C ~: bad -->                                       \
   1.337 -\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   1.338 -\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   1.339 -by (Simp_tac 1);
   1.340 -be yahalom.induct 1;
   1.341 -bd YM2_analz_sees_Enemy 4;
   1.342 -bd YM4_analz_sees_Enemy 6;
   1.343 -by (ALLGOALS 
   1.344 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.345 -by (REPEAT_FIRST (etac exE));
   1.346 -(*YM4*)
   1.347 -by (ex_strip_tac 4);
   1.348 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.349 -			      Crypt_parts_singleton]) 4);
   1.350 -(*YM3: Case split propagates some context to other subgoal...*)
   1.351 -	(** LEVEL 8 **)
   1.352 -by (excluded_middle_tac "K = newK evsa" 3);
   1.353 -by (Asm_simp_tac 3);
   1.354 -by (REPEAT (ares_tac [exI] 3));
   1.355 -(*...we prove this case by contradiction: the key is too new!*)
   1.356 -by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.357 -		      addSEs partsEs
   1.358 -		      addEs [Says_imp_old_keys RS less_irrefl]
   1.359 -	              addss (!simpset)) 3);
   1.360 -(*YM2*) (** LEVEL 12 **)
   1.361 -by (ex_strip_tac 2);
   1.362 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.363 -    (insert_commute RS ssubst) 2);
   1.364 -by (Simp_tac 2);
   1.365 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.366 -			      Crypt_parts_singleton]) 2);
   1.367 -(*Fake*) (** LEVEL 16 **)
   1.368 -by (ex_strip_tac 1);
   1.369 -by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.370 -qed "unique_session_keys";
   1.371 -
   1.372 -(*It seems strange but this theorem is NOT needed to prove the main result!*)