src/HOL/Auth/Yahalom.ML
author paulson
Thu Sep 12 10:40:05 1996 +0200 (1996-09-12)
changeset 1985 84cf16192e03
child 1995 c80e58e78d9c
permissions -rw-r--r--
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.
     1 (*  Title:      HOL/Auth/OtwayRees
     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 OtwayRees;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 
    18 (**** Inductive proofs about yahalom ****)
    19 
    20 (*The Enemy can see more than anybody else, except for their initial state*)
    21 goal thy 
    22  "!!evs. evs : yahalom ==> \
    23 \     sees A evs <= initState A Un sees Enemy evs";
    24 be yahalom.induct 1;
    25 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    26 			        addss (!simpset))));
    27 qed "sees_agent_subset_sees_Enemy";
    28 
    29 
    30 (*Nobody sends themselves messages*)
    31 goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
    32 be yahalom.induct 1;
    33 by (Auto_tac());
    34 qed_spec_mp "not_Says_to_self";
    35 Addsimps [not_Says_to_self];
    36 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    37 
    38 goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs";
    39 be yahalom.induct 1;
    40 by (Auto_tac());
    41 qed "not_Notes";
    42 Addsimps [not_Notes];
    43 AddSEs   [not_Notes RSN (2, rev_notE)];
    44 
    45 
    46 (** For reasoning about the encrypted portion of messages **)
    47 
    48 goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
    49 \                X : analz (sees Enemy evs)";
    50 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    51 qed "YM2_analz_sees_Enemy";
    52 
    53 goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
    54 \                X : analz (sees Enemy evs)";
    55 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    56 qed "YM4_analz_sees_Enemy";
    57 
    58 goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
    59 \                K : parts (sees Enemy evs)";
    60 by (fast_tac (!claset addSEs partsEs
    61 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    62 qed "YM5_parts_sees_Enemy";
    63 
    64 (*YM2_analz... and YM4_analz... let us treat those cases using the same 
    65   argument as for the Fake case.  This is possible for most, but not all,
    66   proofs: Fake does not invent new nonces (as in YM2), and of course Fake
    67   messages originate from the Enemy. *)
    68 
    69 val YM2_YM4_tac = 
    70     dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    71     dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    72 
    73 
    74 (*** Shared keys are not betrayed ***)
    75 
    76 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    77 goal thy 
    78  "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
    79 \        Key (shrK A) ~: parts (sees Enemy evs)";
    80 be yahalom.induct 1;
    81 by YM2_YM4_tac;
    82 by (Auto_tac());
    83 (*Deals with Fake message*)
    84 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    85 			     impOfSubs Fake_parts_insert]) 1);
    86 qed "Enemy_not_see_shrK";
    87 
    88 bind_thm ("Enemy_not_analz_shrK",
    89 	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    90 
    91 Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
    92 
    93 (*We go to some trouble to preserve R in the 3rd and 4th subgoals
    94   As usual fast_tac cannot be used because it uses the equalities too soon*)
    95 val major::prems = 
    96 goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
    97 \             evs : yahalom;                                 \
    98 \             A:bad ==> R                                  \
    99 \           |] ==> R";
   100 br ccontr 1;
   101 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   102 by (swap_res_tac prems 2);
   103 by (ALLGOALS (fast_tac (!claset addIs prems)));
   104 qed "Enemy_see_shrK_E";
   105 
   106 bind_thm ("Enemy_analz_shrK_E", 
   107 	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   108 
   109 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   110 
   111 
   112 (*** Future keys can't be seen or used! ***)
   113 
   114 (*Nobody can have SEEN keys that will be generated in the future.
   115   This has to be proved anew for each protocol description,
   116   but should go by similar reasoning every time.  Hardest case is the
   117   standard Fake rule.  
   118       The length comparison, and Union over C, are essential for the 
   119   induction! *)
   120 goal thy "!!evs. evs : yahalom ==> \
   121 \                length evs <= length evs' --> \
   122 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   123 be yahalom.induct 1;
   124 by YM2_YM4_tac;
   125 (*auto_tac does not work here, as it performs safe_tac first*)
   126 by (ALLGOALS Asm_simp_tac);
   127 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   128 				       impOfSubs parts_insert_subset_Un,
   129 				       Suc_leD]
   130 			        addss (!simpset))));
   131 val lemma = result();
   132 
   133 (*Variant needed for the main theorem below*)
   134 goal thy 
   135  "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
   136 \        Key (newK evs') ~: parts (sees C evs)";
   137 by (fast_tac (!claset addDs [lemma]) 1);
   138 qed "new_keys_not_seen";
   139 Addsimps [new_keys_not_seen];
   140 
   141 (*Another variant: old messages must contain old keys!*)
   142 goal thy 
   143  "!!evs. [| Says A B X : set_of_list evs;  \
   144 \           Key (newK evt) : parts {X};    \
   145 \           evs : yahalom                 \
   146 \        |] ==> length evt < length evs";
   147 br ccontr 1;
   148 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   149 	              addIs [impOfSubs parts_mono, leI]) 1);
   150 qed "Says_imp_old_keys";
   151 
   152 
   153 (*Nobody can have USED keys that will be generated in the future.
   154   ...very like new_keys_not_seen*)
   155 goal thy "!!evs. evs : yahalom ==> \
   156 \                length evs <= length evs' --> \
   157 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   158 be yahalom.induct 1;
   159 by YM2_YM4_tac;
   160 bd YM5_parts_sees_Enemy 7;
   161 by (ALLGOALS Asm_simp_tac);
   162 (*YM1 and YM3*)
   163 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   164 (*Fake, YM2, YM4: these messages send unknown (X) components*)
   165 by (EVERY 
   166     (map
   167      (best_tac
   168       (!claset addSDs [newK_invKey]
   169 	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   170 		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   171 		      Suc_leD]
   172 	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   173 	       addss (!simpset)))
   174      [3,2,1]));
   175 (*YM5: dummy message*)
   176 by (best_tac (!claset addSDs [newK_invKey]
   177 		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
   178 			addIs  [less_SucI, impOfSubs keysFor_mono]
   179 			addss (!simpset addsimps [le_def])) 1);
   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 by YM2_YM4_tac;
   218 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   219 (*Deals with Faked messages*)
   220 by (best_tac (!claset addSEs partsEs
   221 		      addDs [impOfSubs analz_subset_parts,
   222                              impOfSubs parts_insert_subset_Un]
   223                       addss (!simpset)) 2);
   224 (*Base case and YM5*)
   225 by (Auto_tac());
   226 result();
   227 
   228 
   229 (** Specialized rewriting for this proof **)
   230 
   231 Delsimps [image_insert];
   232 Addsimps [image_insert RS sym];
   233 
   234 Delsimps [image_Un];
   235 Addsimps [image_Un RS sym];
   236 
   237 goal thy "insert (Key (newK x)) (sees A evs) = \
   238 \         Key `` (newK``{x}) Un (sees A evs)";
   239 by (Fast_tac 1);
   240 val insert_Key_singleton = result();
   241 
   242 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   243 \         Key `` (f `` (insert x E)) Un C";
   244 by (Fast_tac 1);
   245 val insert_Key_image = result();
   246 
   247 
   248 (*This lets us avoid analyzing the new message -- unless we have to!*)
   249 (*NEEDED??*)
   250 goal thy "synth (analz (sees Enemy evs)) <=   \
   251 \         synth (analz (sees Enemy (Says A B X # evs)))";
   252 by (Simp_tac 1);
   253 br (subset_insertI RS analz_mono RS synth_mono) 1;
   254 qed "synth_analz_thin";
   255 
   256 AddIs [impOfSubs synth_analz_thin];
   257 
   258 
   259 
   260 (** Session keys are not used to encrypt other session keys **)
   261 
   262 (*Could generalize this so that the X component doesn't have to be first
   263   in the message?*)
   264 val enemy_analz_tac =
   265   SELECT_GOAL 
   266    (EVERY [REPEAT (resolve_tac [impI,notI] 1),
   267 	   dtac (impOfSubs Fake_analz_insert) 1,
   268 	   eresolve_tac [asm_rl, synth.Inj] 1,
   269 	   Fast_tac 1,
   270 	   Asm_full_simp_tac 1,
   271 	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
   272 	   ]);
   273 
   274 
   275 (*Lemma for the trivial direction of the if-and-only-if*)
   276 goal thy  
   277  "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   278 \         (K : nE | Key K : analz sEe)  ==>     \
   279 \        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   280 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   281 val lemma = result();
   282 
   283 
   284 goal thy  
   285  "!!evs. evs : yahalom ==> \
   286 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   287 \           (K : newK``E | Key K : analz (sees Enemy evs))";
   288 be yahalom.induct 1;
   289 bd YM2_analz_sees_Enemy 4;
   290 bd YM4_analz_sees_Enemy 6;
   291 by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   292 by (ALLGOALS (*Takes 35 secs*)
   293     (asm_simp_tac 
   294      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   295 			 @ pushes)
   296                setloop split_tac [expand_if])));
   297 (*YM4*) 
   298 by (enemy_analz_tac 5);
   299 (*YM3*)
   300 by (Fast_tac 4);
   301 (*YM2*) (** LEVEL 7 **)
   302 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   303     (insert_commute RS ssubst) 3);
   304 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   305     (insert_commute RS ssubst) 3);
   306 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   307 by (enemy_analz_tac 3);
   308 (*Fake case*) (** LEVEL 11 **)
   309 by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   310     (insert_commute RS ssubst) 2);
   311 by (enemy_analz_tac 2);
   312 (*Base case*)
   313 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   314 qed_spec_mp "analz_image_newK";
   315 
   316 
   317 goal thy
   318  "!!evs. evs : yahalom ==>                               \
   319 \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   320 \        (K = newK evt | Key K : analz (sees Enemy evs))";
   321 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   322 				   insert_Key_singleton]) 1);
   323 by (Fast_tac 1);
   324 qed "analz_insert_Key_newK";
   325 
   326 
   327 (*Describes the form *and age* of K when the following message is sent*)
   328 goal thy 
   329  "!!evs. [| Says Server B \
   330 \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   331 \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   332 \           evs : yahalom |]                                        \
   333 \        ==> (EX evt:yahalom. K = Key(newK evt) & \
   334 \                           length evt < length evs) &            \
   335 \            (EX i. NA = Nonce i)";
   336 be rev_mp 1;
   337 be yahalom.induct 1;
   338 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   339 qed "Says_Server_message_form";
   340 
   341 
   342 (*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
   343 goal thy 
   344  "!!evs. [| Says Server A \
   345 \            {|NA, Crypt {|NA, K|} (shrK B),                      \
   346 \                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
   347 \           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
   348 \     K ~: analz (sees Enemy evs)";
   349 be rev_mp 1;
   350 be yahalom.induct 1;
   351 bd YM2_analz_sees_Enemy 4;
   352 bd YM4_analz_sees_Enemy 6;
   353 by (ALLGOALS Asm_simp_tac);
   354 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   355 by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   356 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   357 by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   358 by (ALLGOALS
   359     (asm_full_simp_tac 
   360      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   361 			  analz_insert_Key_newK] @ pushes)
   362                setloop split_tac [expand_if])));
   363 (*YM3*)
   364 by (fast_tac (!claset addSEs [less_irrefl]) 3);
   365 (*Fake*) (** LEVEL 10 **)
   366 by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   367 by (enemy_analz_tac 1);
   368 (*YM4*)
   369 by (mp_tac 2);
   370 by (enemy_analz_tac 2);
   371 (*YM2*)
   372 by (mp_tac 1);
   373 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   374     (insert_commute RS ssubst) 1);
   375 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   376 by (enemy_analz_tac 1);
   377 qed "Enemy_not_see_encrypted_key";
   378 
   379 
   380 
   381 (*** Session keys are issued at most once, and identify the principals ***)
   382 
   383 (** First, two lemmas for the Fake, YM2 and YM4 cases **)
   384 
   385 goal thy 
   386  "!!evs. [| X : synth (analz (sees Enemy evs));                \
   387 \           Crypt X' (shrK C) : parts{X};                      \
   388 \           C ~: bad;  evs : yahalom |]  \
   389 \        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   390 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   391 	              addDs [impOfSubs parts_insert_subset_Un]
   392                       addss (!simpset)) 1);
   393 qed "Crypt_Fake_parts";
   394 
   395 goal thy 
   396  "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
   397 \        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   398 \            Crypt X' K : parts {Y}";
   399 bd parts_singleton 1;
   400 by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   401 qed "Crypt_parts_singleton";
   402 
   403 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   404 
   405 (*The Key K uniquely identifies a pair of senders in the message encrypted by
   406   C, but if C=Enemy then he could send all sorts of nonsense.*)
   407 goal thy 
   408  "!!evs. evs : yahalom ==>                                     \
   409 \      EX A B. ALL C.                                        \
   410 \         C ~: bad -->                                       \
   411 \         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   412 \           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   413 by (Simp_tac 1);
   414 be yahalom.induct 1;
   415 bd YM2_analz_sees_Enemy 4;
   416 bd YM4_analz_sees_Enemy 6;
   417 by (ALLGOALS 
   418     (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   419 by (REPEAT_FIRST (etac exE));
   420 (*YM4*)
   421 by (ex_strip_tac 4);
   422 by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   423 			      Crypt_parts_singleton]) 4);
   424 (*YM3: Case split propagates some context to other subgoal...*)
   425 	(** LEVEL 8 **)
   426 by (excluded_middle_tac "K = newK evsa" 3);
   427 by (Asm_simp_tac 3);
   428 by (REPEAT (ares_tac [exI] 3));
   429 (*...we prove this case by contradiction: the key is too new!*)
   430 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   431 		      addSEs partsEs
   432 		      addEs [Says_imp_old_keys RS less_irrefl]
   433 	              addss (!simpset)) 3);
   434 (*YM2*) (** LEVEL 12 **)
   435 by (ex_strip_tac 2);
   436 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   437     (insert_commute RS ssubst) 2);
   438 by (Simp_tac 2);
   439 by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   440 			      Crypt_parts_singleton]) 2);
   441 (*Fake*) (** LEVEL 16 **)
   442 by (ex_strip_tac 1);
   443 by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   444 qed "unique_session_keys";
   445 
   446 (*It seems strange but this theorem is NOT needed to prove the main result!*)