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