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