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