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