src/HOL/Auth/OtwayRees.ML
author paulson
Tue Sep 03 16:43:31 1996 +0200 (1996-09-03)
changeset 1941 f97a6e5b6375
child 1945 20ca9cf90e69
permissions -rw-r--r--
Initial working proof of Otway-Rees protocol
     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 Otway-Rees protocol.
     7 
     8 From page 244 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 otway ****)
    19 
    20 (*The Enemy can see more than anybody else, except for their initial state*)
    21 goal thy 
    22  "!!evs. evs : otway ==> \
    23 \     sees A evs <= initState A Un sees Enemy evs";
    24 be otway.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 : otway ==> ALL A X. Says A A X ~: set_of_list evs";
    32 be otway.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 : otway ==> Notes A X ~: set_of_list evs";
    39 be otway.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 "OR2_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 "OR4_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 "OR5_parts_sees_Enemy";
    63 
    64 (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    65   argument as for the Fake case.*)
    66 val OR2_OR4_tac = 
    67     dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    68     dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    69 
    70 
    71 (*** Shared keys are not betrayed ***)
    72 
    73 (*Enemy never sees another agent's shared key!*)
    74 goal thy 
    75  "!!evs. [| evs : otway; A ~= Enemy |] ==> \
    76 \        Key (shrK A) ~: parts (sees Enemy evs)";
    77 be otway.induct 1;
    78 by OR2_OR4_tac;
    79 by (Auto_tac());
    80 (*Deals with Fake message*)
    81 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    82 			     impOfSubs Fake_parts_insert]) 1);
    83 qed "Enemy_not_see_shrK";
    84 
    85 bind_thm ("Enemy_not_analz_shrK",
    86 	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    87 
    88 Addsimps [Enemy_not_see_shrK, 
    89 	  not_sym RSN (2, Enemy_not_see_shrK), 
    90 	  Enemy_not_analz_shrK, 
    91 	  not_sym RSN (2, Enemy_not_analz_shrK)];
    92 
    93 (*We go to some trouble to preserve R in the 3rd subgoal*)
    94 val major::prems = 
    95 goal thy  "[| Key (shrK A) : parts (sees Enemy evs);    \
    96 \             evs : otway;                                  \
    97 \             A=Enemy ==> R                                  \
    98 \           |] ==> R";
    99 br ccontr 1;
   100 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   101 by (swap_res_tac prems 2);
   102 by (ALLGOALS (fast_tac (!claset addIs prems)));
   103 qed "Enemy_see_shrK_E";
   104 
   105 bind_thm ("Enemy_analz_shrK_E", 
   106 	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   107 
   108 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
   109 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   110 
   111 
   112 (*No Friend will ever see another agent's shared key 
   113   (excluding the Enemy, who might transmit his).
   114   The Server, of course, knows all shared keys.*)
   115 goal thy 
   116  "!!evs. [| evs : otway; A ~= Enemy;  A ~= Friend j |] ==> \
   117 \        Key (shrK A) ~: parts (sees (Friend j) evs)";
   118 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   119 by (ALLGOALS Asm_simp_tac);
   120 qed "Friend_not_see_shrK";
   121 
   122 
   123 (*Not for Addsimps -- it can cause goals to blow up!*)
   124 goal thy  
   125  "!!evs. evs : otway ==>                                  \
   126 \        (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) =  \
   127 \        (A=B | A=Enemy)";
   128 by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   129 		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   130 	              addss (!simpset)) 1);
   131 qed "shrK_mem_analz";
   132 
   133 
   134 (*** Future keys can't be seen or used! ***)
   135 
   136 (*Nobody can have SEEN keys that will be generated in the future.
   137   This has to be proved anew for each protocol description,
   138   but should go by similar reasoning every time.  Hardest case is the
   139   standard Fake rule.  
   140       The length comparison, and Union over C, are essential for the 
   141   induction! *)
   142 goal thy "!!evs. evs : otway ==> \
   143 \                length evs <= length evs' --> \
   144 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   145 be otway.induct 1;
   146 by OR2_OR4_tac;
   147 (*auto_tac does not work here, as it performs safe_tac first*)
   148 by (ALLGOALS Asm_simp_tac);
   149 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   150 				       impOfSubs parts_insert_subset_Un,
   151 				       Suc_leD]
   152 			        addss (!simpset))));
   153 val lemma = result();
   154 
   155 (*Variant needed for the main theorem below*)
   156 goal thy 
   157  "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
   158 \        Key (newK evs') ~: parts (sees C evs)";
   159 by (fast_tac (!claset addDs [lemma]) 1);
   160 qed "new_keys_not_seen";
   161 Addsimps [new_keys_not_seen];
   162 
   163 (*Another variant: old messages must contain old keys!*)
   164 goal thy 
   165  "!!evs. [| Says A B X : set_of_list evs;  \
   166 \           Key (newK evt) : parts {X};    \
   167 \           evs : otway                 \
   168 \        |] ==> length evt < length evs";
   169 br ccontr 1;
   170 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   171 	              addIs [impOfSubs parts_mono, leI]) 1);
   172 qed "Says_imp_old_keys";
   173 
   174 
   175 (*Nobody can have USED keys that will be generated in the future.
   176   ...very like new_keys_not_seen*)
   177 goal thy "!!evs. evs : otway ==> \
   178 \                length evs <= length evs' --> \
   179 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   180 be otway.induct 1;
   181 by OR2_OR4_tac;
   182 bd OR5_parts_sees_Enemy 7;
   183 by (ALLGOALS Asm_simp_tac);
   184 (*OR1 and OR3*)
   185 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   186 (*Fake, OR2, OR4: these messages send unknown (X) components*)
   187 by (EVERY 
   188     (map
   189      (best_tac
   190       (!claset addSDs [newK_invKey]
   191 	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   192 		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   193 		      Suc_leD]
   194 	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   195 	       addss (!simpset)))
   196      [3,2,1]));
   197 (*OR5: dummy message*)
   198 by (best_tac (!claset addSDs [newK_invKey]
   199 		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
   200 			addIs  [less_SucI, impOfSubs keysFor_mono]
   201 			addss (!simpset addsimps [le_def])) 1);
   202 val lemma = result();
   203 
   204 goal thy 
   205  "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
   206 \        newK evs' ~: keysFor (parts (sees C evs))";
   207 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   208 qed "new_keys_not_used";
   209 
   210 bind_thm ("new_keys_not_analzd",
   211 	  [analz_subset_parts RS keysFor_mono,
   212 	   new_keys_not_used] MRS contra_subsetD);
   213 
   214 Addsimps [new_keys_not_used, new_keys_not_analzd];
   215 
   216 
   217 (** Lemmas concerning the form of items passed in messages **)
   218 
   219 
   220 (****
   221  The following is to prove theorems of the form
   222 
   223           Key K : analz (insert (Key (newK evt)) 
   224 	                   (insert (Key (shrK C)) (sees Enemy evs))) ==>
   225           Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
   226 
   227  A more general formula must be proved inductively.
   228 
   229 ****)
   230 
   231 
   232 (*NOT useful in this form, but it says that session keys are not used
   233   to encrypt messages containing other keys, in the actual protocol.
   234   We require that agents should behave like this subsequently also.*)
   235 goal thy 
   236  "!!evs. evs : otway ==> \
   237 \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   238 \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   239 be otway.induct 1;
   240 by OR2_OR4_tac;
   241 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   242 (*Deals with Faked messages*)
   243 by (best_tac (!claset addSEs partsEs
   244 		      addDs [impOfSubs analz_subset_parts,
   245                              impOfSubs parts_insert_subset_Un]
   246                       addss (!simpset)) 1);
   247 (*OR5*)
   248 by (fast_tac (!claset addss (!simpset)) 1);
   249 result();
   250 
   251 
   252 (** Specialized rewriting for this proof **)
   253 
   254 Delsimps [image_insert];
   255 Addsimps [image_insert RS sym];
   256 
   257 goal thy "insert (Key (newK x)) (sees A evs) = \
   258 \         Key `` (newK``{x}) Un (sees A evs)";
   259 by (Fast_tac 1);
   260 val insert_Key_singleton = result();
   261 
   262 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   263 \         Key `` (f `` (insert x E)) Un C";
   264 by (Fast_tac 1);
   265 val insert_Key_image = result();
   266 
   267 
   268 (*This lets us avoid analyzing the new message -- unless we have to!*)
   269 (*NEEDED??*)
   270 goal thy "synth (analz (sees Enemy evs)) <=   \
   271 \         synth (analz (sees Enemy (Says A B X # evs)))";
   272 by (Simp_tac 1);
   273 br (subset_insertI RS analz_mono RS synth_mono) 1;
   274 qed "synth_analz_thin";
   275 
   276 AddIs [impOfSubs synth_analz_thin];
   277 
   278 
   279 
   280 (** Session keys are not used to encrypt other session keys **)
   281 
   282 (*Could generalize this so that the X component doesn't have to be first
   283   in the message?*)
   284 val enemy_analz_tac =
   285   SELECT_GOAL 
   286    (EVERY [REPEAT (resolve_tac [impI,notI] 1),
   287 	   dtac (impOfSubs Fake_analz_insert) 1,
   288 	   eresolve_tac [asm_rl, synth.Inj] 1,
   289 	   Fast_tac 1,
   290 	   Asm_full_simp_tac 1,
   291 	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
   292 	   ]);
   293 
   294 
   295 (*Lemma for the trivial direction of the if-and-only-if*)
   296 goal thy  
   297  "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \
   298 \          (K : nE | Key K : analz (insert KsC sEe))  ==>     \
   299 \        (Key K : analz (insert KsC (Key``nE Un sEe))) = \
   300 \          (K : nE | Key K : analz (insert KsC sEe))";
   301 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   302 val lemma = result();
   303 
   304 goal thy  
   305  "!!evs. evs : otway ==> \
   306 \  ALL K E. (Key K : analz (insert (Key (shrK C)) \
   307 \                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   308 \           (K : newK``E |  \
   309 \            Key K : analz (insert (Key (shrK C)) \
   310 \                             (sees Enemy evs)))";
   311 be otway.induct 1;
   312 bd OR2_analz_sees_Enemy 4;
   313 bd OR4_analz_sees_Enemy 6;
   314 by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   315 by (ALLGOALS (*Takes 40 secs*)
   316     (asm_simp_tac 
   317      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   318 			 @ pushes)
   319                setloop split_tac [expand_if])));
   320 (*OR4*) 
   321 by (enemy_analz_tac 5);
   322 (*OR3*)
   323 by (Fast_tac 4);
   324 (*OR2*) (** LEVEL 11 **)
   325 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   326     (insert_commute RS ssubst) 3);
   327 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   328     (insert_commute RS ssubst) 3);
   329 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   330 by (enemy_analz_tac 3);
   331 (*Fake case*) (** LEVEL 6 **)
   332 by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   333     (insert_commute RS ssubst) 2);
   334 by (enemy_analz_tac 2);
   335 (*Base case*)
   336 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   337 qed_spec_mp "analz_image_newK";
   338 
   339 
   340 goal thy
   341  "!!evs. evs : otway ==>                               \
   342 \        Key K : analz (insert (Key (newK evt))            \
   343 \                         (insert (Key (shrK C))      \
   344 \                          (sees Enemy evs))) =            \
   345 \             (K = newK evt |                              \
   346 \              Key K : analz (insert (Key (shrK C))   \
   347 \                               (sees Enemy evs)))";
   348 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   349 				   insert_Key_singleton]) 1);
   350 by (Fast_tac 1);
   351 qed "analz_insert_Key_newK";
   352 
   353 
   354 (*** Session keys are issued at most once, and identify the principals ***)
   355 
   356 (*NOW WE HAVE... 
   357           Says S B
   358            {|Nonce NA, Crypt {|Nonce NA, Key (newK evta)|} (shrK A),
   359             Crypt {|Nonce NB, Key (newK evta)|} (shrK B)|} 
   360 AND
   361           Says Server (Friend j)
   362            {|Ni, Crypt {|Ni, Key (newK evta)|} (shrK (Friend i)),
   363             Crypt {|Nj, Key (newK evta)|} (shrK (Friend j))|} 
   364 THUS
   365           A = Friend i | A = Friend j
   366 AND THIS LETS US PROVE IT!!
   367 *)
   368 
   369 goal thy 
   370  "!!evs. [| X : synth (analz (sees Enemy evs));       \
   371 \           Crypt X' (shrK C) : parts{X};             \
   372 \           C ~= Enemy;   evs : otway |]              \
   373 \        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   374 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   375 	              addDs [impOfSubs parts_insert_subset_Un]
   376                       addss (!simpset)) 1);
   377 qed "Crypt_Fake_parts";
   378 
   379 goal thy 
   380  "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
   381 \        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   382 \            Crypt X' K : parts {Y}";
   383 bd parts_singleton 1;
   384 by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   385 qed "Crypt_parts_singleton";
   386 
   387 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   388 
   389 (*The Key K uniquely identifies a pair of senders in the message encrypted by
   390   C, but if C=Enemy then he could send all sorts of nonsense.*)
   391 goal thy 
   392  "!!evs. evs : otway ==>                        \
   393 \      EX A B. ALL C S S' X NA.                    \
   394 \         C ~= Enemy -->                        \
   395 \         Says S S' X : set_of_list evs -->     \
   396 \           (Crypt {|NA, Key K|} (shrK C) : parts{X} --> C=A | C=B)";
   397 be otway.induct 1;
   398 bd OR2_analz_sees_Enemy 4;
   399 bd OR4_analz_sees_Enemy 6;
   400 by (ALLGOALS 
   401     (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   402 by (REPEAT_FIRST (etac exE));
   403 (*OR4*)
   404 by (ex_strip_tac 4);
   405 by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   406 			      Crypt_parts_singleton]) 4);
   407 (*OR3: Case split propagates some context to other subgoal...*)
   408 	(** LEVEL 8 **)
   409 by (excluded_middle_tac "K = newK evsa" 3);
   410 by (Asm_simp_tac 3);
   411 by (REPEAT (ares_tac [exI] 3));
   412 (*...we prove this case by contradiction: the key is too new!*)
   413 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   414 		      addSEs partsEs
   415 		      addEs [Says_imp_old_keys RS less_irrefl]
   416 	              addss (!simpset)) 3);
   417 (*OR2*) (** LEVEL 12 **)
   418 by (ex_strip_tac 2);
   419 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   420     (insert_commute RS ssubst) 2);
   421 by (Simp_tac 2);
   422 by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   423 			      Crypt_parts_singleton]) 2);
   424 (*Fake*) (** LEVEL 16 **)
   425 by (ex_strip_tac 1);
   426 by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   427 qed "unique_session_keys";
   428 
   429 
   430 (*Describes the form *and age* of K when the following message is sent*)
   431 goal thy 
   432  "!!evs. [| Says Server B \
   433 \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   434 \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   435 \           evs : otway |]                                        \
   436 \        ==> (EX evt:otway. K = Key(newK evt) & \
   437 \                           length evt < length evs) &            \
   438 \            (EX i. NA = Nonce i)";
   439 be rev_mp 1;
   440 be otway.induct 1;
   441 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   442 qed "Says_Server_message_form";
   443 
   444 
   445 (*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*)
   446 goal thy 
   447  "!!evs. [| Says Server (Friend j) \
   448 \            {|Ni, Crypt {|Ni, K|} (shrK (Friend i)),                      \
   449 \                  Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs;  \
   450 \           evs : otway;  Friend i ~= C;  Friend j ~= C              \
   451 \        |] ==>                                                       \
   452 \     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
   453 be rev_mp 1;
   454 be otway.induct 1;
   455 bd OR2_analz_sees_Enemy 4;
   456 bd OR4_analz_sees_Enemy 6;
   457 by (ALLGOALS Asm_simp_tac);
   458 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   459 by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   460 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   461 by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   462 by (ALLGOALS 
   463     (asm_full_simp_tac 
   464      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   465 			  analz_insert_Key_newK] @ pushes)
   466                setloop split_tac [expand_if])));
   467 (*OR3*)
   468 by (fast_tac (!claset addSEs [less_irrefl]) 3);
   469 (*Fake*) (** LEVEL 8 **)
   470 by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   471 by (enemy_analz_tac 1);
   472 (*OR4*)
   473 by (mp_tac 2);
   474 by (enemy_analz_tac 2);
   475 (*OR2*)
   476 by (mp_tac 1);
   477 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   478     (insert_commute RS ssubst) 1);
   479 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   480 by (enemy_analz_tac 1);
   481 qed "Enemy_not_see_encrypted_key";