src/HOL/Auth/OtwayRees_AN.ML
author paulson
Thu Nov 07 10:19:15 1996 +0100 (1996-11-07)
changeset 2166 d276a806cc10
parent 2160 ad4382e546fc
child 2264 f298678bd54a
permissions -rw-r--r--
Tidying up: removing redundant assumptions, etc.
     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 Simplified version with minimal encryption but explicit messages
     9 
    10 From page 11 of
    11   Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    12   IEEE Trans. SE 22 (1), 1996
    13 *)
    14 
    15 open OtwayRees_AN;
    16 
    17 proof_timing:=true;
    18 HOL_quantifiers := false;
    19 
    20 
    21 (*Weak liveness: there are traces that reach the end*)
    22 goal thy 
    23  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    24 \        ==> EX K. EX NA. EX evs: otway lost.          \
    25 \             Says B A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) \
    26 \             : set_of_list evs";
    27 by (REPEAT (resolve_tac [exI,bexI] 1));
    28 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    29 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    30 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    31 by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    32 result();
    33 
    34 
    35 (**** Inductive proofs about otway ****)
    36 
    37 (*Monotonicity*)
    38 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    39 by (rtac subsetI 1);
    40 by (etac otway.induct 1);
    41 by (REPEAT_FIRST
    42     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    43                               :: otway.intrs))));
    44 qed "otway_mono";
    45 
    46 (*Nobody sends themselves messages*)
    47 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    48 by (etac 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 
    55 (** For reasoning about the encrypted portion of messages **)
    56 
    57 goal thy "!!evs. Says S B {|X, X'|} : set_of_list evs ==> \
    58 \                X : analz (sees lost Spy evs)";
    59 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    60 qed "OR4_analz_sees_Spy";
    61 
    62 goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
    63 \                  : set_of_list evs ==> 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 "Oops_parts_sees_Spy";
    67 
    68 (*OR4_analz_sees_Spy lets us treat those cases using the same 
    69   argument as for the Fake case.  This is possible for most, but not all,
    70   proofs, since Fake messages originate from the Spy. *)
    71 
    72 bind_thm ("OR4_parts_sees_Spy",
    73           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    74 
    75 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    76   harder to complete, since simplification does less for us.*)
    77 val parts_Fake_tac = 
    78     forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
    79     forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
    80 
    81 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    82 fun parts_induct_tac i = SELECT_GOAL
    83     (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    84 	     (*Fake message*)
    85 	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    86 					   impOfSubs Fake_parts_insert]
    87                                     addss (!simpset)) 2)) THEN
    88      (*Base case*)
    89      fast_tac (!claset addss (!simpset)) 1 THEN
    90      ALLGOALS Asm_simp_tac) i;
    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's lost at start)*)
    96 goal thy 
    97  "!!evs. evs : otway lost \
    98 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    99 by (parts_induct_tac 1);
   100 by (Auto_tac());
   101 qed "Spy_see_shrK";
   102 Addsimps [Spy_see_shrK];
   103 
   104 goal thy 
   105  "!!evs. evs : otway lost \
   106 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   107 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   108 qed "Spy_analz_shrK";
   109 Addsimps [Spy_analz_shrK];
   110 
   111 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   112 \                  evs : otway lost |] ==> A:lost";
   113 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   114 qed "Spy_see_shrK_D";
   115 
   116 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   117 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   118 
   119 
   120 (*** Future keys can't be seen or used! ***)
   121 
   122 (*Nobody can have SEEN keys that will be generated in the future. *)
   123 goal thy "!!evs. evs : otway lost ==> \
   124 \                length evs <= length evs' --> \
   125 \                Key (newK evs') ~: parts (sees lost Spy evs)";
   126 by (parts_induct_tac 1);
   127 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   128                                            impOfSubs parts_insert_subset_Un,
   129                                            Suc_leD]
   130                                     addss (!simpset))));
   131 qed_spec_mp "new_keys_not_seen";
   132 Addsimps [new_keys_not_seen];
   133 
   134 (*Variant: old messages must contain old keys!*)
   135 goal thy 
   136  "!!evs. [| Says A B X : set_of_list evs;  \
   137 \           Key (newK evt) : parts {X};    \
   138 \           evs : otway lost                 \
   139 \        |] ==> length evt < length evs";
   140 by (rtac ccontr 1);
   141 by (dtac leI 1);
   142 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   143                       addIs  [impOfSubs parts_mono]) 1);
   144 qed "Says_imp_old_keys";
   145 
   146 
   147 (*Nobody can have USED keys that will be generated in the future.
   148   ...very like new_keys_not_seen*)
   149 goal thy "!!evs. evs : otway lost ==> \
   150 \                length evs <= length evs' --> \
   151 \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   152 by (parts_induct_tac 1);
   153 (*OR1 and OR3*)
   154 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   155 (*Fake, OR2, OR4: these messages send unknown (X) components*)
   156 by (REPEAT
   157     (best_tac
   158       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   159                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   160                       Suc_leD]
   161                addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   162                addss (!simpset)) 1));
   163 qed_spec_mp "new_keys_not_used";
   164 
   165 bind_thm ("new_keys_not_analzd",
   166           [analz_subset_parts RS keysFor_mono,
   167            new_keys_not_used] MRS contra_subsetD);
   168 
   169 Addsimps [new_keys_not_used, new_keys_not_analzd];
   170 
   171 
   172 
   173 (*** Proofs involving analz ***)
   174 
   175 (*Describes the form of K and NA when the Server sends this message.*)
   176 goal thy 
   177  "!!evs. [| Says Server B \
   178 \           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   179 \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   180 \           evs : otway lost |]                                        \
   181 \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   182 \            (EX i. NA = Nonce i) &                  \
   183 \            (EX j. NB = Nonce j)";
   184 by (etac rev_mp 1);
   185 by (etac otway.induct 1);
   186 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   187 qed "Says_Server_message_form";
   188 
   189 
   190 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   191 val analz_Fake_tac = 
   192     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   193     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   194     assume_tac 7 THEN Full_simp_tac 7 THEN
   195     REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   196 
   197 
   198 (****
   199  The following is to prove theorems of the form
   200 
   201           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   202           Key K : analz (sees lost Spy evs)
   203 
   204  A more general formula must be proved inductively.
   205 
   206 ****)
   207 
   208 
   209 (** Session keys are not used to encrypt other session keys **)
   210 
   211 (*The equality makes the induction hypothesis easier to apply*)
   212 goal thy  
   213  "!!evs. evs : otway lost ==> \
   214 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   215 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   216 by (etac otway.induct 1);
   217 by analz_Fake_tac;
   218 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   219 by (ALLGOALS (*Takes 28 secs*)
   220     (asm_simp_tac 
   221      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   222                          @ pushes)
   223                setloop split_tac [expand_if])));
   224 (** LEVEL 5 **)
   225 (*OR4, Fake*) 
   226 by (EVERY (map spy_analz_tac [4,2]));
   227 (*Oops, OR3, Base*)
   228 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   229 qed_spec_mp "analz_image_newK";
   230 
   231 
   232 goal thy
   233  "!!evs. evs : otway lost ==>                               \
   234 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   235 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   236 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   237                                    insert_Key_singleton]) 1);
   238 by (Fast_tac 1);
   239 qed "analz_insert_Key_newK";
   240 
   241 
   242 (*** The Key K uniquely identifies the Server's  message. **)
   243 
   244 goal thy 
   245  "!!evs. evs : otway lost ==>                      \
   246 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   247 \       Says Server B \
   248 \         {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   249 \           Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs  \
   250 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   251 by (etac otway.induct 1);
   252 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   253 by (Step_tac 1);
   254 (*Remaining cases: OR3 and OR4*)
   255 by (ex_strip_tac 2);
   256 by (Fast_tac 2);
   257 by (expand_case_tac "K = ?y" 1);
   258 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   259 (*...we assume X is a very new message, and handle this case by contradiction*)
   260 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   261                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   262                       addss (!simpset addsimps [parts_insertI])) 1);
   263 val lemma = result();
   264 
   265 
   266 goal thy 
   267 "!!evs. [| Says Server B                                           \
   268 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),         \
   269 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|}        \
   270 \           : set_of_list evs;                                     \
   271 \          Says Server B'                                          \
   272 \            {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'),     \
   273 \              Crypt {|NB', Agent A', Agent B', K|} (shrK B')|}    \
   274 \           : set_of_list evs;                                     \
   275 \          evs : otway lost |]                                     \
   276 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   277 by (dtac lemma 1);
   278 by (REPEAT (etac exE 1));
   279 (*Duplicate the assumption*)
   280 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   281 by (fast_tac (!claset addSDs [spec]) 1);
   282 qed "unique_session_keys";
   283 
   284 
   285 
   286 (**** Authenticity properties relating to NA ****)
   287 
   288 (*If the encrypted message appears then it originated with the Server!*)
   289 goal thy 
   290  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   291 \ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)        \
   292 \      : parts (sees lost Spy evs)                          \
   293 \     --> (EX NB. Says Server B                                     \
   294 \                  {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   295 \                    Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   296 \                  : set_of_list evs)";
   297 by (parts_induct_tac 1);
   298 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   299 (*OR3*)
   300 by (Fast_tac 1);
   301 qed_spec_mp "NA_Crypt_imp_Server_msg";
   302 
   303 
   304 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   305   then the key really did come from the Server!  CANNOT prove this of the
   306   bad form of this protocol, even though we can prove
   307   Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
   308   the Server's message from its nonce NA.)*)
   309 goal thy 
   310  "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
   311 \            : set_of_list evs;                                         \
   312 \           A ~: lost;  evs : otway lost |]                             \
   313 \        ==> EX NB. Says Server B                                       \
   314 \                    {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),  \
   315 \                      Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
   316 \                   : set_of_list evs";
   317 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   318                       addEs  partsEs
   319                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   320 qed "A_trust_OR4";
   321 
   322 
   323 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   324     Does not in itself guarantee security: an attack could violate 
   325     the premises, e.g. by having A=Spy **)
   326 
   327 goal thy 
   328  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   329 \        ==> Says Server B                                                 \
   330 \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
   331 \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
   332 \            : set_of_list evs -->                                         \
   333 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   334 \            Key K ~: analz (sees lost Spy evs)";
   335 by (etac otway.induct 1);
   336 by analz_Fake_tac;
   337 by (ALLGOALS
   338     (asm_full_simp_tac 
   339      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   340                           analz_insert_Key_newK] @ pushes)
   341                setloop split_tac [expand_if])));
   342 (*OR3*)
   343 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   344                       addss (!simpset addsimps [parts_insert2])) 2);
   345 (*OR4, Fake*) 
   346 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   347 (*Oops*) 
   348 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   349 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   350 
   351 goal thy 
   352  "!!evs. [| Says Server B                                                     \
   353 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   354 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   355 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   356 \           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   357 \        ==> K ~: analz (sees lost Spy evs)";
   358 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   359 by (fast_tac (!claset addSEs [lemma]) 1);
   360 qed "Spy_not_see_encrypted_key";
   361 
   362 
   363 goal thy 
   364  "!!evs. [| C ~: {A,B,Server};                                                \
   365 \           Says Server B                                                     \
   366 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   367 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   368 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   369 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   370 \        ==> K ~: analz (sees lost C evs)";
   371 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   372 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   373 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   374 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   375 qed "Agent_not_see_encrypted_key";
   376 
   377 
   378 (**** Authenticity properties relating to NB ****)
   379 
   380 (*If the encrypted message appears then it originated with the Server!*)
   381 goal thy 
   382  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   383 \    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)                     \
   384 \         : parts (sees lost Spy evs)                                       \
   385 \        --> (EX NA. Says Server B                                          \
   386 \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   387 \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   388 \                     : set_of_list evs)";
   389 by (parts_induct_tac 1);
   390 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   391 (*OR3*)
   392 by (Fast_tac 1);
   393 qed_spec_mp "NB_Crypt_imp_Server_msg";
   394 
   395 
   396 (*Guarantee for B: if it gets a message with matching NB then the Server
   397   has sent the correct message.*)
   398 goal thy 
   399  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   400 \           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}  \
   401 \            : set_of_list evs |]                                           \
   402 \        ==> EX NA. Says Server B                                           \
   403 \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   404 \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   405 \                     : set_of_list evs";
   406 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   407                       addEs  partsEs
   408                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   409 qed "B_trust_OR3";