src/HOL/Auth/OtwayRees_AN.ML
author paulson
Fri Dec 13 10:20:55 1996 +0100 (1996-12-13)
changeset 2375 14539397fc04
parent 2331 d6a56ff0d94e
child 2417 95f275c8476e
permissions -rw-r--r--
Streamlined some proofs
     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 (*Fake, OR4: these messages send unknown (X) components*)
   155 by (EVERY
   156     (map 
   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))) [5,1]));
   163 (*Remaining subgoals*)
   164 by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
   165 qed_spec_mp "new_keys_not_used";
   166 
   167 bind_thm ("new_keys_not_analzd",
   168           [analz_subset_parts RS keysFor_mono,
   169            new_keys_not_used] MRS contra_subsetD);
   170 
   171 Addsimps [new_keys_not_used, new_keys_not_analzd];
   172 
   173 
   174 
   175 (*** Proofs involving analz ***)
   176 
   177 (*Describes the form of K and NA when the Server sends this message.*)
   178 goal thy 
   179  "!!evs. [| Says Server B \
   180 \           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
   181 \             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
   182 \           evs : otway lost |]                                               \
   183 \        ==> (EX evt: otway lost. K = Key(newK evt)) & \
   184 \            (EX i. NA = Nonce i) &                    \
   185 \            (EX j. NB = Nonce j)";
   186 by (etac rev_mp 1);
   187 by (etac otway.induct 1);
   188 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   189 qed "Says_Server_message_form";
   190 
   191 
   192 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   193 val analz_Fake_tac = 
   194     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   195     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   196     assume_tac 7 THEN Full_simp_tac 7 THEN
   197     REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   198 
   199 
   200 (****
   201  The following is to prove theorems of the form
   202 
   203           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   204           Key K : analz (sees lost Spy evs)
   205 
   206  A more general formula must be proved inductively.
   207 
   208 ****)
   209 
   210 
   211 (** Session keys are not used to encrypt other session keys **)
   212 
   213 (*The equality makes the induction hypothesis easier to apply*)
   214 goal thy  
   215  "!!evs. evs : otway lost ==>                                         \
   216 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   217 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   218 by (etac otway.induct 1);
   219 by analz_Fake_tac;
   220 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   221 by (ALLGOALS (*Takes 28 secs*)
   222     (asm_simp_tac 
   223      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   224                          @ pushes)
   225                setloop split_tac [expand_if])));
   226 (** LEVEL 5 **)
   227 (*OR4, Fake*) 
   228 by (EVERY (map spy_analz_tac [4,2]));
   229 (*Oops, OR3, Base*)
   230 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   231 qed_spec_mp "analz_image_newK";
   232 
   233 
   234 goal thy
   235  "!!evs. evs : otway lost ==>                                          \
   236 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   237 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   238 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   239                                    insert_Key_singleton]) 1);
   240 by (Fast_tac 1);
   241 qed "analz_insert_Key_newK";
   242 
   243 
   244 (*** The Key K uniquely identifies the Server's  message. **)
   245 
   246 goal thy 
   247  "!!evs. evs : otway lost ==>                              \
   248 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   249 \       Says Server B \
   250 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
   251 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
   252 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   253 by (etac otway.induct 1);
   254 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   255 by (Step_tac 1);
   256 (*Remaining cases: OR3 and OR4*)
   257 by (ex_strip_tac 2);
   258 by (Fast_tac 2);
   259 by (expand_case_tac "K = ?y" 1);
   260 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   261 (*...we assume X is a very new message, and handle this case by contradiction*)
   262 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   263                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   264                       addss (!simpset addsimps [parts_insertI])) 1);
   265 val lemma = result();
   266 
   267 
   268 goal thy 
   269 "!!evs. [| Says Server B                                           \
   270 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
   271 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
   272 \           : set_of_list evs;                                     \
   273 \          Says Server B'                                          \
   274 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
   275 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
   276 \           : set_of_list evs;                                     \
   277 \          evs : otway lost |]                                     \
   278 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   279 by (dtac lemma 1);
   280 by (REPEAT (etac exE 1));
   281 (*Duplicate the assumption*)
   282 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   283 by (fast_tac (!claset addSDs [spec]) 1);
   284 qed "unique_session_keys";
   285 
   286 
   287 
   288 (**** Authenticity properties relating to NA ****)
   289 
   290 (*If the encrypted message appears then it originated with the Server!*)
   291 goal thy 
   292  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   293 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   294 \      : parts (sees lost Spy evs)                          \
   295 \     --> (EX NB. Says Server B                                          \
   296 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   297 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   298 \                  : set_of_list evs)";
   299 by (parts_induct_tac 1);
   300 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   301 (*OR3*)
   302 by (Fast_tac 1);
   303 qed_spec_mp "NA_Crypt_imp_Server_msg";
   304 
   305 
   306 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   307   then the key really did come from the Server!  CANNOT prove this of the
   308   bad form of this protocol, even though we can prove
   309   Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
   310   the Server's message from its nonce NA.)*)
   311 goal thy 
   312  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   313 \            : set_of_list evs;                                         \
   314 \           A ~: lost;  evs : otway lost |]                             \
   315 \        ==> EX NB. Says Server B                                       \
   316 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   317 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   318 \                   : set_of_list evs";
   319 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   320                       addEs  partsEs
   321                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   322 qed "A_trusts_OR4";
   323 
   324 
   325 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   326     Does not in itself guarantee security: an attack could violate 
   327     the premises, e.g. by having A=Spy **)
   328 
   329 goal thy 
   330  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   331 \        ==> Says Server B                                                 \
   332 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   333 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   334 \            : set_of_list evs -->                                         \
   335 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   336 \            Key K ~: analz (sees lost Spy evs)";
   337 by (etac otway.induct 1);
   338 by analz_Fake_tac;
   339 by (ALLGOALS
   340     (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
   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 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";