src/HOL/Auth/Yahalom2.ML
author paulson
Fri Nov 01 18:28:19 1996 +0100 (1996-11-01)
changeset 2155 dc85854810eb
parent 2111 81c8d46edfa3
child 2160 ad4382e546fc
permissions -rw-r--r--
New version with simpler disambiguation in YM3,
Oops message, and no encryption in YM2
     1 (*  Title:      HOL/Auth/Yahalom2
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     7 
     8 This version trades encryption of NB for additional explicitness in YM3.
     9 
    10 From page 259 of
    11   Burrows, Abadi and Needham.  A Logic of Authentication.
    12   Proc. Royal Soc. 426 (1989)
    13 *)
    14 
    15 open Yahalom2;
    16 
    17 proof_timing:=true;
    18 HOL_quantifiers := false;
    19 
    20 
    21 (*Weak liveness: there are traces that reach the end*)
    22 
    23 goal thy 
    24  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    25 \        ==> EX X NB K. EX evs: yahalom lost.          \
    26 \               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    27 by (REPEAT (resolve_tac [exI,bexI] 1));
    28 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    29 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    30 by (ALLGOALS Fast_tac);
    31 result();
    32 
    33 
    34 (**** Inductive proofs about yahalom ****)
    35 
    36 (*Monotonicity*)
    37 goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    38 by (rtac subsetI 1);
    39 by (etac yahalom.induct 1);
    40 by (REPEAT_FIRST
    41     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    42                               :: yahalom.intrs))));
    43 qed "yahalom_mono";
    44 
    45 
    46 (*Nobody sends themselves messages*)
    47 goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    48 by (etac yahalom.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 
    55 (** For reasoning about the encrypted portion of messages **)
    56 
    57 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    58 goal thy "!!evs. Says S A {|NB, Crypt Y (shrK A), X|} : set_of_list evs ==> \
    59 \                X : analz (sees lost Spy evs)";
    60 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    61 qed "YM4_analz_sees_Spy";
    62 
    63 bind_thm ("YM4_parts_sees_Spy",
    64           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    65 
    66 (*Relates to both YM4 and Oops*)
    67 goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
    68 \                  : set_of_list evs ==> \
    69 \                K : parts (sees lost Spy evs)";
    70 by (fast_tac (!claset addSEs partsEs
    71                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    72 qed "YM4_Key_parts_sees_Spy";
    73 
    74 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    75   harder: the simplifier does less.*)
    76 val parts_Fake_tac = 
    77     forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
    78     forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
    79 
    80 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    81 fun parts_induct_tac i = SELECT_GOAL
    82     (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
    83 	     (*Fake message*)
    84 	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    85 					   impOfSubs Fake_parts_insert]
    86                                     addss (!simpset)) 2)) THEN
    87      (*Base case*)
    88      fast_tac (!claset addss (!simpset)) 1 THEN
    89      ALLGOALS Asm_simp_tac) i;
    90 
    91 
    92 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    93     sends messages containing X! **)
    94 
    95 (*Spy never sees another agent's shared key! (unless it is leaked at start)*)
    96 goal thy 
    97  "!!evs. [| evs : yahalom lost;  A ~: lost |]    \
    98 \        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    99 by (parts_induct_tac 1);
   100 by (Auto_tac());
   101 qed "Spy_not_see_shrK";
   102 
   103 bind_thm ("Spy_not_analz_shrK",
   104           [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   105 
   106 Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   107 
   108 (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   109   As usual fast_tac cannot be used because it uses the equalities too soon*)
   110 val major::prems = 
   111 goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   112 \             evs : yahalom lost;                               \
   113 \             A:lost ==> R                                  \
   114 \           |] ==> R";
   115 by (rtac ccontr 1);
   116 by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   117 by (swap_res_tac prems 2);
   118 by (ALLGOALS (fast_tac (!claset addIs prems)));
   119 qed "Spy_see_shrK_E";
   120 
   121 bind_thm ("Spy_analz_shrK_E", 
   122           analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   123 
   124 AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   125 
   126 
   127 (*** Future keys can't be seen or used! ***)
   128 
   129 (*Nobody can have SEEN keys that will be generated in the future.
   130   This has to be proved anew for each protocol description,
   131   but should go by similar reasoning every time.  Hardest case is the
   132   standard Fake rule.  
   133       The Union over C is essential for the induction! *)
   134 goal thy "!!evs. evs : yahalom lost ==> \
   135 \                length evs <= length evs' --> \
   136 \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   137 by (parts_induct_tac 1);
   138 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   139                                            impOfSubs parts_insert_subset_Un,
   140                                            Suc_leD]
   141                                     addss (!simpset))));
   142 val lemma = result();
   143 
   144 (*Variant needed for the main theorem below*)
   145 goal thy 
   146  "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   147 \        ==> Key (newK evs') ~: parts (sees lost C evs)";
   148 by (fast_tac (!claset addDs [lemma]) 1);
   149 qed "new_keys_not_seen";
   150 Addsimps [new_keys_not_seen];
   151 
   152 (*Another variant: old messages must contain old keys!*)
   153 goal thy 
   154  "!!evs. [| Says A B X : set_of_list evs;  \
   155 \           Key (newK evt) : parts {X};    \
   156 \           evs : yahalom lost                 \
   157 \        |] ==> length evt < length evs";
   158 by (rtac ccontr 1);
   159 by (dtac leI 1);
   160 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   161                       addIs  [impOfSubs parts_mono]) 1);
   162 qed "Says_imp_old_keys";
   163 
   164 
   165 (*Nobody can have USED keys that will be generated in the future.
   166   ...very like new_keys_not_seen*)
   167 goal thy "!!evs. evs : yahalom lost ==> \
   168 \                length evs <= length evs' --> \
   169 \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   170 by (parts_induct_tac 1);
   171 by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
   172 (*YM1, YM2 and YM3*)
   173 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   174 (*Fake and YM4: these messages send unknown (X) components*)
   175 by (stac insert_commute 2);
   176 by (Simp_tac 2);
   177 (*YM4: the only way K could have been used is if it had been seen,
   178   contradicting new_keys_not_seen*)
   179 by (REPEAT
   180      (best_tac
   181       (!claset addDs [impOfSubs analz_subset_parts,
   182                       impOfSubs (analz_subset_parts RS keysFor_mono),
   183                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   184                       Suc_leD]
   185                addEs [new_keys_not_seen RSN(2,rev_notE)]
   186                addss (!simpset)) 1));
   187 val lemma = result();
   188 
   189 goal thy 
   190  "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   191 \        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   192 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   193 qed "new_keys_not_used";
   194 
   195 bind_thm ("new_keys_not_analzd",
   196           [analz_subset_parts RS keysFor_mono,
   197            new_keys_not_used] MRS contra_subsetD);
   198 
   199 Addsimps [new_keys_not_used, new_keys_not_analzd];
   200 
   201 
   202 (*Describes the form of K when the Server sends this message.  Useful for
   203   Oops as well as main secrecy property.*)
   204 goal thy 
   205  "!!evs. [| Says Server A {|NB', Crypt {|Agent B, K, NA|} (shrK A), X|} \
   206 \            : set_of_list evs;                                         \
   207 \           evs : yahalom lost |]                                       \
   208 \        ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
   209 by (etac rev_mp 1);
   210 by (etac yahalom.induct 1);
   211 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   212 qed "Says_Server_message_form";
   213 
   214 
   215 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   216 val analz_Fake_tac = 
   217     dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   218     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   219     assume_tac 7 THEN Full_simp_tac 7 THEN
   220     REPEAT ((eresolve_tac [bexE,conjE] ORELSE' hyp_subst_tac) 7);
   221 
   222 
   223 (****
   224  The following is to prove theorems of the form
   225 
   226           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   227           Key K : analz (sees lost Spy evs)
   228 
   229  A more general formula must be proved inductively.
   230 
   231 ****)
   232 
   233 (** Session keys are not used to encrypt other session keys **)
   234 
   235 goal thy  
   236  "!!evs. evs : yahalom lost ==> \
   237 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   238 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   239 by (etac yahalom.induct 1);
   240 by analz_Fake_tac;
   241 by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   242 by (ALLGOALS  (*Takes 26 secs*)
   243     (asm_simp_tac 
   244      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   245                          @ pushes)
   246                setloop split_tac [expand_if])));
   247 (*YM4, Fake*) 
   248 by (EVERY (map spy_analz_tac [4, 2]));
   249 (*Oops, YM3, Base*)
   250 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   251 qed_spec_mp "analz_image_newK";
   252 
   253 goal thy
   254  "!!evs. evs : yahalom lost ==>                               \
   255 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   256 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   257 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   258                                    insert_Key_singleton]) 1);
   259 by (Fast_tac 1);
   260 qed "analz_insert_Key_newK";
   261 
   262 
   263 (*** The Key K uniquely identifies the Server's  message. **)
   264 
   265 goal thy 
   266  "!!evs. evs : yahalom lost ==>                                     \
   267 \      EX A' B' NA' NB' X'. ALL A B NA NB X.                        \
   268 \          Says Server A                                            \
   269 \           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
   270 \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   271 by (etac yahalom.induct 1);
   272 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   273 by (Step_tac 1);
   274 (*Remaining case: YM3*)
   275 by (expand_case_tac "K = ?y" 1);
   276 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   277 (*...we assume X is a very new message, and handle this case by contradiction*)
   278 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   279                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   280                       addss (!simpset addsimps [parts_insertI])) 1);
   281 val lemma = result();
   282 
   283 goal thy 
   284 "!!evs. [| Says Server A                                            \
   285 \           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
   286 \           : set_of_list evs;                                      \
   287 \          Says Server A'                                           \
   288 \           {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), X'|}   \
   289 \           : set_of_list evs;                                      \
   290 \          evs : yahalom lost |]                                    \
   291 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   292 by (dtac lemma 1);
   293 by (REPEAT (etac exE 1));
   294 (*Duplicate the assumption*)
   295 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   296 by (fast_tac (!claset addSDs [spec]) 1);
   297 qed "unique_session_keys";
   298 
   299 
   300 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   301 
   302 goal thy 
   303  "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
   304 \           evs : yahalom lost |]            \
   305 \        ==> Says Server A                                           \
   306 \              {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),           \
   307 \                    Crypt {|NB, Key K, Agent A|} (shrK B)|}          \
   308 \             : set_of_list evs -->                               \
   309 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
   310 \            Key K ~: analz (sees lost Spy evs)";
   311 by (etac yahalom.induct 1);
   312 by analz_Fake_tac;
   313 by (ALLGOALS
   314     (asm_simp_tac 
   315      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   316                           analz_insert_Key_newK] @ pushes)
   317                setloop split_tac [expand_if])));
   318 (*YM3*)
   319 by (fast_tac (!claset addIs [parts_insertI]
   320                       addEs [Says_imp_old_keys RS less_irrefl]
   321                       addss (!simpset)) 2);
   322 (*OR4, Fake*) 
   323 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   324 (*Oops*)
   325 by (fast_tac (!claset delrules [disjE] 
   326 		      addDs [unique_session_keys]
   327 	              addss (!simpset)) 1);
   328 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   329 
   330 
   331 (*Final version: Server's message in the most abstract form*)
   332 goal thy 
   333  "!!evs. [| Says Server A                                         \
   334 \              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   335 \                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
   336 \           : set_of_list evs;                                    \
   337 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
   338 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   339 \        ==> K ~: analz (sees lost Spy evs)";
   340 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   341 by (fast_tac (!claset addSEs [lemma]) 1);
   342 qed "Spy_not_see_encrypted_key";
   343 
   344 
   345 goal thy 
   346  "!!evs. [| C ~: {A,B,Server};                                    \
   347 \           Says Server A                                         \
   348 \              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   349 \                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
   350 \           : set_of_list evs;                                    \
   351 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
   352 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   353 \        ==> K ~: analz (sees lost C evs)";
   354 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   355 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   356 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   357 by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
   358 qed "Agent_not_see_encrypted_key";
   359 
   360 
   361 (*** Security Guarantees for A and B ***)
   362 
   363 (*If the encrypted message appears then it originated with the Server.*)
   364 goal thy
   365  "!!evs. [| Crypt {|Agent B, Key K, NA|} (shrK A)                \
   366 \            : parts (sees lost Spy evs);                              \
   367 \           A ~: lost;  evs : yahalom lost |]                          \
   368 \         ==> EX NB. Says Server A                                     \
   369 \                      {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),    \
   370 \                            Crypt {|NB, Key K, Agent A|} (shrK B)|}   \
   371 \                    : set_of_list evs";
   372 by (etac rev_mp 1);
   373 by (parts_induct_tac 1);
   374 (*The nested conjunctions are entirely useless*)
   375 by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI])));
   376 qed "A_trust_YM3";
   377 
   378 
   379 (*B knows, by the first part of A's message, that the Server distributed 
   380   the key for A and B. *)
   381 goal thy 
   382  "!!evs. [| Crypt {|Nonce NB, Key K, Agent A|} (shrK B)              \
   383 \            : parts (sees lost Spy evs);                            \
   384 \           B ~: lost;  evs : yahalom lost |]                        \
   385 \        ==> EX NA. Says Server A                                    \
   386 \                    {|Nonce NB,                                     \
   387 \                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),  \
   388 \                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
   389 \                       : set_of_list evs";
   390 by (etac rev_mp 1);
   391 by (parts_induct_tac 1);
   392 (*YM3*)
   393 by (Fast_tac 1);
   394 qed "B_trusts_YM4_shrK";
   395 
   396 (*With this variant we don't bother to use the 2nd part of YM4 at all, since
   397   Nonce NB is available in the first part.  However the 2nd part does assure B
   398   of A's existence.*)
   399 
   400 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   401   because we do not have to show that NB is secret. *)
   402 goal thy 
   403  "!!evs. [| Says A' B {|Crypt {|Nonce NB, Key K, Agent A|} (shrK B),    \
   404 \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   405 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   406 \        ==> EX NA. Says Server A                                       \
   407 \                    {|Nonce NB,                                        \
   408 \                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),     \
   409 \                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|}    \
   410 \                   : set_of_list evs";
   411 be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
   412 by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
   413 qed "B_trust_YM4";