src/HOL/Auth/Yahalom.ML
author paulson
Fri Sep 13 18:49:43 1996 +0200 (1996-09-13)
changeset 2001 974167c1d2c4
parent 1995 c80e58e78d9c
child 2013 4b7a432fb3ed
permissions -rw-r--r--
Reformatting; proved B_gets_secure_key
     1 (*  Title:      HOL/Auth/Yahalom
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "otway" for the Yahalom protocol.
     7 
     8 From page 257 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 open Yahalom;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 
    18 
    19 (** Weak liveness: there are traces that reach the end **)
    20 
    21 goal thy 
    22  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    23 \        ==> EX X NB K. EX evs: yahalom.          \
    24 \               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    25 by (REPEAT (resolve_tac [exI,bexI] 1));
    26 br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
    27 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    28 by (ALLGOALS Fast_tac);
    29 qed "weak_liveness";
    30 
    31 
    32 (**** Inductive proofs about yahalom ****)
    33 
    34 (*The Enemy can see more than anybody else, except for their initial state*)
    35 goal thy 
    36  "!!evs. evs : yahalom ==> \
    37 \     sees A evs <= initState A Un sees Enemy evs";
    38 be yahalom.induct 1;
    39 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    40 			        addss (!simpset))));
    41 qed "sees_agent_subset_sees_Enemy";
    42 
    43 
    44 (*Nobody sends themselves messages*)
    45 goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
    46 be yahalom.induct 1;
    47 by (Auto_tac());
    48 qed_spec_mp "not_Says_to_self";
    49 Addsimps [not_Says_to_self];
    50 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    51 
    52 goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs";
    53 be yahalom.induct 1;
    54 by (Auto_tac());
    55 qed "not_Notes";
    56 Addsimps [not_Notes];
    57 AddSEs   [not_Notes RSN (2, rev_notE)];
    58 
    59 
    60 (** For reasoning about the encrypted portion of messages **)
    61 
    62 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    63 goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
    64 \                X : analz (sees Enemy evs)";
    65 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    66 qed "YM4_analz_sees_Enemy";
    67 
    68 goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
    69 \                  : set_of_list evs ==> \
    70 \                K : parts (sees Enemy evs)";
    71 by (fast_tac (!claset addSEs partsEs
    72 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    73 qed "YM4_parts_sees_Enemy";
    74 
    75 
    76 
    77 (*** Shared keys are not betrayed ***)
    78 
    79 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    80 goal thy 
    81  "!!evs. [| evs : yahalom;  A ~: bad |]    \
    82 \        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    83 be yahalom.induct 1;
    84 bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
    85 by (ALLGOALS Asm_simp_tac);
    86 by (stac insert_commute 3);
    87 by (Auto_tac());
    88 (*Fake and YM4 are similar*)
    89 by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
    90 					impOfSubs Fake_parts_insert])));
    91 qed "Enemy_not_see_shrK";
    92 
    93 bind_thm ("Enemy_not_analz_shrK",
    94 	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    95 
    96 Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
    97 
    98 (*We go to some trouble to preserve R in the 3rd and 4th subgoals
    99   As usual fast_tac cannot be used because it uses the equalities too soon*)
   100 val major::prems = 
   101 goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   102 \             evs : yahalom;                               \
   103 \             A:bad ==> R                                  \
   104 \           |] ==> R";
   105 br ccontr 1;
   106 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   107 by (swap_res_tac prems 2);
   108 by (ALLGOALS (fast_tac (!claset addIs prems)));
   109 qed "Enemy_see_shrK_E";
   110 
   111 bind_thm ("Enemy_analz_shrK_E", 
   112 	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   113 
   114 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   115 
   116 
   117 (*** Future keys can't be seen or used! ***)
   118 
   119 (*Nobody can have SEEN keys that will be generated in the future.
   120   This has to be proved anew for each protocol description,
   121   but should go by similar reasoning every time.  Hardest case is the
   122   standard Fake rule.  
   123       The length comparison, and Union over C, are essential for the 
   124   induction! *)
   125 goal thy "!!evs. evs : yahalom ==> \
   126 \                length evs <= length evs' --> \
   127 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   128 be yahalom.induct 1;
   129 bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   130 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   131 					   impOfSubs parts_insert_subset_Un,
   132 					   Suc_leD]
   133 			            addss (!simpset))));
   134 val lemma = result();
   135 
   136 (*Variant needed for the main theorem below*)
   137 goal thy 
   138  "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
   139 \        ==> Key (newK evs') ~: parts (sees C evs)";
   140 by (fast_tac (!claset addDs [lemma]) 1);
   141 qed "new_keys_not_seen";
   142 Addsimps [new_keys_not_seen];
   143 
   144 (*Another variant: old messages must contain old keys!*)
   145 goal thy 
   146  "!!evs. [| Says A B X : set_of_list evs;  \
   147 \           Key (newK evt) : parts {X};    \
   148 \           evs : yahalom                 \
   149 \        |] ==> length evt < length evs";
   150 br ccontr 1;
   151 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   152 	              addIs [impOfSubs parts_mono, leI]) 1);
   153 qed "Says_imp_old_keys";
   154 
   155 
   156 (*Nobody can have USED keys that will be generated in the future.
   157   ...very like new_keys_not_seen*)
   158 goal thy "!!evs. evs : yahalom ==> \
   159 \                length evs <= length evs' --> \
   160 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   161 be yahalom.induct 1;
   162 by (forward_tac [YM4_parts_sees_Enemy] 6);
   163 bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   164 by (ALLGOALS Asm_full_simp_tac);
   165 (*YM1, YM2 and YM3*)
   166 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   167 (*Fake and YM4: these messages send unknown (X) components*)
   168 by (stac insert_commute 2);
   169 by (Simp_tac 2);
   170 (*YM4: the only way K could have been used is if it had been seen,
   171   contradicting new_keys_not_seen*)
   172 by (ALLGOALS
   173      (best_tac
   174       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   175 		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   176 		      Suc_leD]
   177 	       addDs [impOfSubs analz_subset_parts]
   178 	       addEs [new_keys_not_seen RSN(2,rev_notE)]
   179 	       addss (!simpset))));
   180 val lemma = result();
   181 
   182 goal thy 
   183  "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
   184 \        ==> newK evs' ~: keysFor (parts (sees C evs))";
   185 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   186 qed "new_keys_not_used";
   187 
   188 bind_thm ("new_keys_not_analzd",
   189 	  [analz_subset_parts RS keysFor_mono,
   190 	   new_keys_not_used] MRS contra_subsetD);
   191 
   192 Addsimps [new_keys_not_used, new_keys_not_analzd];
   193 
   194 
   195 (** Lemmas concerning the form of items passed in messages **)
   196 
   197 
   198 (****
   199  The following is to prove theorems of the form
   200 
   201           Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   202           Key K : analz (sees Enemy evs)
   203 
   204  A more general formula must be proved inductively.
   205 
   206 ****)
   207 
   208 
   209 (*NOT useful in this form, but it says that session keys are not used
   210   to encrypt messages containing other keys, in the actual protocol.
   211   We require that agents should behave like this subsequently also.*)
   212 goal thy 
   213  "!!evs. evs : yahalom ==> \
   214 \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   215 \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   216 be yahalom.induct 1;
   217 bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   218 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   219 (*Deals with Faked messages*)
   220 by (EVERY 
   221     (map (best_tac (!claset addSEs partsEs
   222 			    addDs [impOfSubs analz_subset_parts,
   223 				   impOfSubs parts_insert_subset_Un]
   224 			    addss (!simpset)))
   225      [3,2]));
   226 (*Base case*)
   227 by (Auto_tac());
   228 result();
   229 
   230 
   231 (** Specialized rewriting for this proof **)
   232 
   233 Delsimps [image_insert];
   234 Addsimps [image_insert RS sym];
   235 
   236 Delsimps [image_Un];
   237 Addsimps [image_Un RS sym];
   238 
   239 goal thy "insert (Key (newK x)) (sees A evs) = \
   240 \         Key `` (newK``{x}) Un (sees A evs)";
   241 by (Fast_tac 1);
   242 val insert_Key_singleton = result();
   243 
   244 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   245 \         Key `` (f `` (insert x E)) Un C";
   246 by (Fast_tac 1);
   247 val insert_Key_image = result();
   248 
   249 
   250 (*This lets us avoid analyzing the new message -- unless we have to!*)
   251 (*NEEDED??*)
   252 goal thy "synth (analz (sees Enemy evs)) <=   \
   253 \         synth (analz (sees Enemy (Says A B X # evs)))";
   254 by (Simp_tac 1);
   255 br (subset_insertI RS analz_mono RS synth_mono) 1;
   256 qed "synth_analz_thin";
   257 
   258 AddIs [impOfSubs synth_analz_thin];
   259 
   260 
   261 
   262 (** Session keys are not used to encrypt other session keys **)
   263 
   264 (*Lemma for the trivial direction of the if-and-only-if*)
   265 goal thy  
   266  "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   267 \         (K : nE | Key K : analz sEe)  ==>     \
   268 \        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   269 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   270 val lemma = result();
   271 
   272 
   273 goal thy  
   274  "!!evs. evs : yahalom ==> \
   275 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   276 \           (K : newK``E | Key K : analz (sees Enemy evs))";
   277 be yahalom.induct 1;
   278 bd YM4_analz_sees_Enemy 6;
   279 by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   280 by (ALLGOALS 
   281     (asm_simp_tac 
   282      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   283 			 @ pushes)
   284                setloop split_tac [expand_if])));
   285 (*YM4*) 
   286 by (enemy_analz_tac 4);
   287 (*YM3*)
   288 by (Fast_tac 3);
   289 (*Fake case*)
   290 by (enemy_analz_tac 2);
   291 (*Base case*)
   292 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   293 qed_spec_mp "analz_image_newK";
   294 
   295 goal thy
   296  "!!evs. evs : yahalom ==>                               \
   297 \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   298 \        (K = newK evt | Key K : analz (sees Enemy evs))";
   299 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   300 				   insert_Key_singleton]) 1);
   301 by (Fast_tac 1);
   302 qed "analz_insert_Key_newK";
   303 
   304 
   305 (*Describes the form *and age* of K when the following message is sent*)
   306 goal thy 
   307  "!!evs. [| Says Server A                                           \
   308 \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
   309 \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
   310 \           evs : yahalom |]                                        \
   311 \        ==> (EX evt:yahalom. K = Key(newK evt) &                   \
   312 \                           length evt < length evs)";
   313 be rev_mp 1;
   314 be yahalom.induct 1;
   315 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   316 qed "Says_Server_message_form";
   317 
   318 
   319 (*Crucial secrecy property: Enemy does not see the keys sent in msg YM3
   320   As with Otway-Rees, proof does not need uniqueness of session keys.*)
   321 goal thy 
   322  "!!evs. [| Says Server A \
   323 \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   324 \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   325 \           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
   326 \     K ~: analz (sees Enemy evs)";
   327 be rev_mp 1;
   328 be yahalom.induct 1;
   329 bd YM4_analz_sees_Enemy 6;
   330 by (ALLGOALS Asm_simp_tac);
   331 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   332 by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   333 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   334 by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   335 by (ALLGOALS
   336     (asm_full_simp_tac 
   337      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   338 			  analz_insert_Key_newK] @ pushes)
   339                setloop split_tac [expand_if])));
   340 (*YM4*)
   341 by (enemy_analz_tac 3);
   342 (*YM3*)
   343 by (fast_tac (!claset addSEs [less_irrefl]) 2);
   344 (*Fake*) (** LEVEL 10 **)
   345 by (enemy_analz_tac 1);
   346 qed "Enemy_not_see_encrypted_key";
   347 
   348 
   349 goal thy 
   350  "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : analz (sees Enemy evs); \
   351 \           B ~: bad;  evs : yahalom |]                                 \
   352 \        ==> EX NA NB. Says Server A                                    \
   353 \                     {|Crypt {|Agent B, Key K,                         \
   354 \                               Nonce NA, Nonce NB|} (shrK A),          \
   355 \                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   356 \                   : set_of_list evs";
   357 be rev_mp 1;
   358 be yahalom.induct 1;
   359 by (forward_tac [YM4_analz_sees_Enemy] 6);
   360 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   361 (*YM4*)
   362 by (enemy_analz_tac 4);
   363 (*YM3*)
   364 by (Fast_tac 3);
   365 (*Fake*)
   366 by (enemy_analz_tac 2);
   367 (*Base case*)
   368 by (fast_tac (!claset addss (!simpset)) 1);
   369 qed "Enemy_analz_Server_msg";
   370 
   371 
   372 (*What can B deduce from receipt of YM4?  
   373   NOT THAT THE NONCES AGREE (in this version).  But what does the Nonce
   374 	give us??*)
   375 goal thy 
   376  "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   377 \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   378 \           B ~: bad;  evs : yahalom |]                                 \
   379 \        ==> EX NA NB. Says Server A                                    \
   380 \                     {|Crypt {|Agent B, Key K,                         \
   381 \                               Nonce NA, Nonce NB|} (shrK A),          \
   382 \                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   383 \                   : set_of_list evs";
   384 be rev_mp 1;
   385 be yahalom.induct 1;
   386 by (forward_tac [YM4_analz_sees_Enemy] 6);
   387 by (ALLGOALS Asm_simp_tac);
   388 (*YM4*)
   389 by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 3);
   390 (*YM3*)
   391 by (Fast_tac 2);
   392 (*Fake*)
   393 by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 1);
   394 qed "YM4_imp_Says_Server_A";
   395 
   396 
   397 
   398 goal thy 
   399  "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   400 \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   401 \           A ~: bad;  B ~: bad;  evs : yahalom |]                      \
   402 \        ==> Key K ~: analz (sees Enemy evs)";
   403 by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A,
   404 			      Enemy_not_see_encrypted_key]) 1);
   405 qed "B_gets_secure_key";