src/HOL/Auth/OtwayRees_AN.ML
author paulson
Fri Dec 20 10:23:48 1996 +0100 (1996-12-20)
changeset 2454 92f43ed48935
parent 2451 ce85a2aafc7a
child 2516 4d68fbe6378b
permissions -rw-r--r--
Corrected comments
     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 "!!i. evs : otway lost ==>             \
   124 \              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   125 by (parts_induct_tac 1);
   126 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   127 				    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 i) : parts {X};              \
   138 \           evs : otway lost                       \
   139 \        |] ==> i < 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 "!!i. evs : otway lost ==>          \
   150 \           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
   151 by (parts_induct_tac 1);
   152 (*Fake, OR4: these messages send unknown (X) components*)
   153 by (EVERY
   154     (map 
   155      (best_tac
   156       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   157                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   158                       Suc_leD]
   159                addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   160                addss (!simpset))) [5,1]));
   161 (*Remaining subgoals*)
   162 by (REPEAT (fast_tac (!claset addDs [Suc_leD] 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 (shrK A) {|NA, Agent A, Agent B, K|},                     \
   179 \             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
   180 \           evs : otway lost |]                                               \
   181 \        ==> (EX n. K = Key(newK n)) &                                        \
   182 \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   183 by (etac rev_mp 1);
   184 by (etac otway.induct 1);
   185 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   186 qed "Says_Server_message_form";
   187 
   188 
   189 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   190 val analz_Fake_tac = 
   191     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   192     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   193     assume_tac 7 THEN Full_simp_tac 7 THEN
   194     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   195 
   196 
   197 (****
   198  The following is to prove theorems of the form
   199 
   200   Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   201   Key K : analz (sees lost Spy evs)
   202 
   203  A more general formula must be proved inductively.
   204 
   205 ****)
   206 
   207 
   208 (** Session keys are not used to encrypt other session keys **)
   209 
   210 (*The equality makes the induction hypothesis easier to apply*)
   211 goal thy  
   212  "!!evs. evs : otway lost ==>                                         \
   213 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   214 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   215 by (etac otway.induct 1);
   216 by analz_Fake_tac;
   217 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   218 by (ALLGOALS (*Takes 18 secs*)
   219     (asm_simp_tac 
   220      (!simpset addsimps [Un_assoc RS sym, 
   221 			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   222                setloop split_tac [expand_if])));
   223 (*OR4, Fake*) 
   224 by (EVERY (map spy_analz_tac [4,2]));
   225 (*Oops, OR3, Base*)
   226 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   227 qed_spec_mp "analz_image_newK";
   228 
   229 
   230 goal thy
   231  "!!evs. evs : otway lost ==>                                          \
   232 \        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   233 \        (K = newK i | Key K : analz (sees lost Spy evs))";
   234 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   235                                    insert_Key_singleton]) 1);
   236 by (Fast_tac 1);
   237 qed "analz_insert_Key_newK";
   238 
   239 
   240 (*** The Key K uniquely identifies the Server's  message. **)
   241 
   242 goal thy 
   243  "!!evs. evs : otway lost ==>                              \
   244 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   245 \       Says Server B \
   246 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
   247 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
   248 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   249 by (etac otway.induct 1);
   250 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   251 by (Step_tac 1);
   252 (*Remaining cases: OR3 and OR4*)
   253 by (ex_strip_tac 2);
   254 by (Fast_tac 2);
   255 by (expand_case_tac "K = ?y" 1);
   256 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   257 (*...we assume X is a very new message, and handle this case by contradiction*)
   258 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   259                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   260                       addss (!simpset addsimps [parts_insertI])) 1);
   261 val lemma = result();
   262 
   263 
   264 goal thy 
   265 "!!evs. [| Says Server B                                           \
   266 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
   267 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
   268 \           : set_of_list evs;                                     \
   269 \          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 \          evs : otway lost |]                                     \
   274 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   275 by (prove_unique_tac lemma 1);
   276 qed "unique_session_keys";
   277 
   278 
   279 
   280 (**** Authenticity properties relating to NA ****)
   281 
   282 (*If the encrypted message appears then it originated with the Server!*)
   283 goal thy 
   284  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   285 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   286 \      : parts (sees lost Spy evs)                          \
   287 \     --> (EX NB. Says Server B                                          \
   288 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   289 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   290 \                  : set_of_list evs)";
   291 by (parts_induct_tac 1);
   292 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   293 (*OR3*)
   294 by (Fast_tac 1);
   295 qed_spec_mp "NA_Crypt_imp_Server_msg";
   296 
   297 
   298 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   299   Freshness may be inferred from nonce NA.*)
   300 goal thy 
   301  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   302 \            : set_of_list evs;                                         \
   303 \           A ~: lost;  evs : otway lost |]                             \
   304 \        ==> EX NB. Says Server B                                       \
   305 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   306 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   307 \                   : set_of_list evs";
   308 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   309                       addEs  partsEs
   310                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   311 qed "A_trusts_OR4";
   312 
   313 
   314 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   315     Does not in itself guarantee security: an attack could violate 
   316     the premises, e.g. by having A=Spy **)
   317 
   318 goal thy 
   319  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   320 \        ==> Says Server B                                                 \
   321 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   322 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   323 \            : set_of_list evs -->                                         \
   324 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   325 \            Key K ~: analz (sees lost Spy evs)";
   326 by (etac otway.induct 1);
   327 by analz_Fake_tac;
   328 by (ALLGOALS
   329     (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
   330 				      analz_insert_Key_newK]
   331 		            setloop split_tac [expand_if])));
   332 (*OR3*)
   333 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   334                       addss (!simpset addsimps [parts_insert2])) 2);
   335 (*OR4, Fake*) 
   336 by (REPEAT_FIRST spy_analz_tac);
   337 (*Oops*) 
   338 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   339 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   340 
   341 goal thy 
   342  "!!evs. [| Says Server B                                                     \
   343 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   344 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   345 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   346 \           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   347 \        ==> K ~: analz (sees lost Spy evs)";
   348 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   349 by (fast_tac (!claset addSEs [lemma]) 1);
   350 qed "Spy_not_see_encrypted_key";
   351 
   352 
   353 goal thy 
   354  "!!evs. [| C ~: {A,B,Server};                                                \
   355 \           Says Server B                                                     \
   356 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   357 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   358 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   359 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   360 \        ==> K ~: analz (sees lost C evs)";
   361 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   362 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   363 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   364 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   365 qed "Agent_not_see_encrypted_key";
   366 
   367 
   368 (**** Authenticity properties relating to NB ****)
   369 
   370 (*If the encrypted message appears then it originated with the Server!*)
   371 goal thy 
   372  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   373 \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   374 \         : parts (sees lost Spy evs)                                       \
   375 \        --> (EX NA. Says Server B                                          \
   376 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   377 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   378 \                     : set_of_list evs)";
   379 by (parts_induct_tac 1);
   380 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   381 (*OR3*)
   382 by (Fast_tac 1);
   383 qed_spec_mp "NB_Crypt_imp_Server_msg";
   384 
   385 
   386 (*Guarantee for B: if it gets a well-formed certificate then the Server
   387   has sent the correct message in round 3.*)
   388 goal thy 
   389  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   390 \           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
   391 \            : set_of_list evs |]                                           \
   392 \        ==> EX NA. Says Server B                                           \
   393 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   394 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   395 \                     : set_of_list evs";
   396 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   397                       addEs  partsEs
   398                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   399 qed "B_trusts_OR3";