src/HOL/Auth/OtwayRees_AN.ML
author paulson
Tue Nov 05 11:20:52 1996 +0100 (1996-11-05)
changeset 2160 ad4382e546fc
parent 2131 3106a99d30a5
child 2166 d276a806cc10
permissions -rw-r--r--
Simplified new_keys_not_seen, etc.: replaced the
union over all
agents by the Spy alone. Proofs run faster and they do not have to be
set up in terms of a previous lemma.
     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 (*** Future nonces can't be seen or used! ***)
   148 
   149 goal thy "!!evs. evs : otway lost ==> \
   150 \                length evs <= length evt --> \
   151 \                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   152 by (parts_induct_tac 1);
   153 by (REPEAT_FIRST (fast_tac (!claset 
   154                               addSEs partsEs
   155                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
   156                               addDs  [impOfSubs analz_subset_parts,
   157                                       impOfSubs parts_insert_subset_Un,
   158                                       Suc_leD]
   159                               addss (!simpset))));
   160 qed_spec_mp "new_nonces_not_seen";
   161 Addsimps [new_nonces_not_seen];
   162 
   163 
   164 (*Nobody can have USED keys that will be generated in the future.
   165   ...very like new_keys_not_seen*)
   166 goal thy "!!evs. evs : otway lost ==> \
   167 \                length evs <= length evs' --> \
   168 \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   169 by (parts_induct_tac 1);
   170 (*OR1 and OR3*)
   171 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   172 (*Fake, OR2, OR4: these messages send unknown (X) components*)
   173 by (REPEAT
   174     (best_tac
   175       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   176                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   177                       Suc_leD]
   178                addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   179                addss (!simpset)) 1));
   180 qed_spec_mp "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 
   190 (*** Proofs involving analz ***)
   191 
   192 (*Describes the form of K and NA when the Server sends this message.*)
   193 goal thy 
   194  "!!evs. [| Says Server B \
   195 \           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   196 \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   197 \           evs : otway lost |]                                        \
   198 \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   199 \            (EX i. NA = Nonce i) &                  \
   200 \            (EX j. NB = Nonce j)";
   201 by (etac rev_mp 1);
   202 by (etac otway.induct 1);
   203 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   204 qed "Says_Server_message_form";
   205 
   206 
   207 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   208 val analz_Fake_tac = 
   209     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   210     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   211     assume_tac 7 THEN Full_simp_tac 7 THEN
   212     REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   213 
   214 
   215 (****
   216  The following is to prove theorems of the form
   217 
   218           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   219           Key K : analz (sees lost Spy evs)
   220 
   221  A more general formula must be proved inductively.
   222 
   223 ****)
   224 
   225 
   226 (** Session keys are not used to encrypt other session keys **)
   227 
   228 (*The equality makes the induction hypothesis easier to apply*)
   229 goal thy  
   230  "!!evs. evs : otway lost ==> \
   231 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   232 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   233 by (etac otway.induct 1);
   234 by analz_Fake_tac;
   235 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   236 by (ALLGOALS (*Takes 28 secs*)
   237     (asm_simp_tac 
   238      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   239                          @ pushes)
   240                setloop split_tac [expand_if])));
   241 (** LEVEL 5 **)
   242 (*OR4, Fake*) 
   243 by (EVERY (map spy_analz_tac [4,2]));
   244 (*Oops, OR3, Base*)
   245 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   246 qed_spec_mp "analz_image_newK";
   247 
   248 
   249 goal thy
   250  "!!evs. evs : otway lost ==>                               \
   251 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   252 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   253 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   254                                    insert_Key_singleton]) 1);
   255 by (Fast_tac 1);
   256 qed "analz_insert_Key_newK";
   257 
   258 
   259 (*** The Key K uniquely identifies the Server's  message. **)
   260 
   261 goal thy 
   262  "!!evs. evs : otway lost ==>                      \
   263 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   264 \       Says Server B \
   265 \         {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   266 \           Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs  \
   267 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   268 by (etac otway.induct 1);
   269 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   270 by (Step_tac 1);
   271 (*Remaining cases: OR3 and OR4*)
   272 by (ex_strip_tac 2);
   273 by (Fast_tac 2);
   274 by (expand_case_tac "K = ?y" 1);
   275 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   276 (*...we assume X is a very new message, and handle this case by contradiction*)
   277 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   278                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   279                       addss (!simpset addsimps [parts_insertI])) 1);
   280 val lemma = result();
   281 
   282 
   283 goal thy 
   284 "!!evs. [| Says Server B                                           \
   285 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),         \
   286 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|}        \
   287 \           : set_of_list evs;                                     \
   288 \          Says Server B'                                          \
   289 \            {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'),     \
   290 \              Crypt {|NB', Agent A', Agent B', K|} (shrK B')|}    \
   291 \           : set_of_list evs;                                     \
   292 \          evs : otway lost |]                                     \
   293 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   294 by (dtac lemma 1);
   295 by (REPEAT (etac exE 1));
   296 (*Duplicate the assumption*)
   297 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   298 by (fast_tac (!claset addSDs [spec]) 1);
   299 qed "unique_session_keys";
   300 
   301 
   302 
   303 (**** Authenticity properties relating to NA ****)
   304 
   305 (*If the encrypted message appears then it originated with the Server!*)
   306 goal thy 
   307  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   308 \ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)        \
   309 \      : parts (sees lost Spy evs)                          \
   310 \     --> (EX NB. Says Server B                                     \
   311 \                  {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   312 \                    Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   313 \                  : set_of_list evs)";
   314 by (parts_induct_tac 1);
   315 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   316 (*OR3*)
   317 by (Fast_tac 1);
   318 qed_spec_mp "NA_Crypt_imp_Server_msg";
   319 
   320 
   321 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   322   then the key really did come from the Server!  CANNOT prove this of the
   323   bad form of this protocol, even though we can prove
   324   Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
   325   the Server's message from its nonce NA.)*)
   326 goal thy 
   327  "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
   328 \            : set_of_list evs;                                         \
   329 \           A ~: lost;  evs : otway lost |]                             \
   330 \        ==> EX NB. Says Server B                                       \
   331 \                    {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),  \
   332 \                      Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
   333 \                   : set_of_list evs";
   334 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   335                       addEs  partsEs
   336                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   337 qed "A_trust_OR4";
   338 
   339 
   340 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   341     Does not in itself guarantee security: an attack could violate 
   342     the premises, e.g. by having A=Spy **)
   343 
   344 goal thy 
   345  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
   346 \        ==> Says Server B                                                 \
   347 \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
   348 \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
   349 \            : set_of_list evs -->                                         \
   350 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   351 \            Key K ~: analz (sees lost Spy evs)";
   352 by (etac otway.induct 1);
   353 by analz_Fake_tac;
   354 by (ALLGOALS
   355     (asm_full_simp_tac 
   356      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   357                           analz_insert_Key_newK] @ pushes)
   358                setloop split_tac [expand_if])));
   359 (*OR3*)
   360 by (fast_tac (!claset addSIs [parts_insertI]
   361                       addEs [Says_imp_old_keys RS less_irrefl]
   362                       addss (!simpset addsimps [parts_insert2])) 2);
   363 (*OR4, Fake*) 
   364 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   365 (*Oops*) 
   366 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   367 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   368 
   369 goal thy 
   370  "!!evs. [| Says Server B                                                     \
   371 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   372 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   373 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   374 \           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   375 \        ==> K ~: analz (sees lost Spy evs)";
   376 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   377 by (fast_tac (!claset addSEs [lemma]) 1);
   378 qed "Spy_not_see_encrypted_key";
   379 
   380 
   381 goal thy 
   382  "!!evs. [| C ~: {A,B,Server};                                                \
   383 \           Says Server B                                                     \
   384 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   385 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   386 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   387 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   388 \        ==> K ~: analz (sees lost C evs)";
   389 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   390 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   391 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   392 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   393 qed "Agent_not_see_encrypted_key";
   394 
   395 
   396 (**** Authenticity properties relating to NB ****)
   397 
   398 (*If the encrypted message appears then it originated with the Server!*)
   399 goal thy 
   400  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   401 \    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)                     \
   402 \         : parts (sees lost Spy evs)                                       \
   403 \        --> (EX NA. Says Server B                                          \
   404 \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   405 \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   406 \                     : set_of_list evs)";
   407 by (parts_induct_tac 1);
   408 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   409 (*OR3*)
   410 by (Fast_tac 1);
   411 qed_spec_mp "NB_Crypt_imp_Server_msg";
   412 
   413 
   414 (*Guarantee for B: if it gets a message with matching NB then the Server
   415   has sent the correct message.*)
   416 goal thy 
   417  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   418 \           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}  \
   419 \            : set_of_list evs |]                                           \
   420 \        ==> EX NA. Says Server B                                           \
   421 \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   422 \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   423 \                     : set_of_list evs";
   424 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   425                       addEs  partsEs
   426                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   427 qed "B_trust_OR3";