src/HOL/Auth/OtwayRees.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24)
changeset 4477 b3e5857d8d99
parent 4470 af3239def3d4
child 4509 828148415197
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     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 Version that encrypts Nonce NB
     9 
    10 From page 244 of
    11   Burrows, Abadi and Needham.  A Logic of Authentication.
    12   Proc. Royal Soc. 426 (1989)
    13 *)
    14 
    15 open OtwayRees;
    16 
    17 set proof_timing;
    18 HOL_quantifiers := false;
    19 
    20 AddEs spies_partsEs;
    21 AddDs [impOfSubs analz_subset_parts];
    22 AddDs [impOfSubs Fake_parts_insert];
    23 
    24 
    25 (*A "possibility property": there are traces that reach the end*)
    26 goal thy 
    27  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    28 \        ==> EX K. EX NA. EX evs: otway.          \
    29 \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    30 \                 : set evs";
    31 by (REPEAT (resolve_tac [exI,bexI] 1));
    32 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    33 by possibility_tac;
    34 result();
    35 
    36 
    37 (**** Inductive proofs about otway ****)
    38 
    39 (*Nobody sends themselves messages*)
    40 goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    41 by (etac otway.induct 1);
    42 by Auto_tac;
    43 qed_spec_mp "not_Says_to_self";
    44 Addsimps [not_Says_to_self];
    45 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    46 
    47 
    48 (** For reasoning about the encrypted portion of messages **)
    49 
    50 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    51 \                ==> X : analz (spies evs)";
    52 by (dtac (Says_imp_spies RS analz.Inj) 1);
    53 by (Blast_tac 1);
    54 qed "OR2_analz_spies";
    55 
    56 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    57 \                ==> X : analz (spies evs)";
    58 by (dtac (Says_imp_spies RS analz.Inj) 1);
    59 by (Blast_tac 1);
    60 qed "OR4_analz_spies";
    61 
    62 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    63 \                 ==> K : parts (spies evs)";
    64 by (Blast_tac 1);
    65 qed "Oops_parts_spies";
    66 
    67 (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    68   argument as for the Fake case.  This is possible for most, but not all,
    69   proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    70   messages originate from the Spy. *)
    71 
    72 bind_thm ("OR2_parts_spies",
    73           OR2_analz_spies RS (impOfSubs analz_subset_parts));
    74 bind_thm ("OR4_parts_spies",
    75           OR4_analz_spies RS (impOfSubs analz_subset_parts));
    76 
    77 (*For proving the easier theorems about X ~: parts (spies evs).*)
    78 fun parts_induct_tac i = 
    79     etac otway.induct i			THEN 
    80     forward_tac [Oops_parts_spies] (i+6) THEN
    81     forward_tac [OR4_parts_spies]  (i+5) THEN
    82     forward_tac [OR2_parts_spies]  (i+3) THEN 
    83     prove_simple_subgoals_tac  i;
    84 
    85 
    86 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    87     sends messages containing X! **)
    88 
    89 
    90 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    91 goal thy 
    92  "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    93 by (parts_induct_tac 1);
    94 by (ALLGOALS Blast_tac);
    95 qed "Spy_see_shrK";
    96 Addsimps [Spy_see_shrK];
    97 
    98 goal thy 
    99  "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   100 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   101 qed "Spy_analz_shrK";
   102 Addsimps [Spy_analz_shrK];
   103 
   104 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
   105 	Spy_analz_shrK RSN (2, rev_iffD1)];
   106 
   107 
   108 (*Nobody can have used non-existent keys!*)
   109 goal thy "!!evs. evs : otway ==>          \
   110 \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   111 by (parts_induct_tac 1);
   112 (*Fake*)
   113 by (best_tac
   114       (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   115 		addIs  [impOfSubs analz_subset_parts]
   116 		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
   117 		addss  (simpset())) 1);
   118 by (ALLGOALS Blast_tac);
   119 qed_spec_mp "new_keys_not_used";
   120 
   121 bind_thm ("new_keys_not_analzd",
   122           [analz_subset_parts RS keysFor_mono,
   123            new_keys_not_used] MRS contra_subsetD);
   124 
   125 Addsimps [new_keys_not_used, new_keys_not_analzd];
   126 
   127 
   128 
   129 (*** Proofs involving analz ***)
   130 
   131 (*Describes the form of K and NA when the Server sends this message.  Also
   132   for Oops case.*)
   133 goal thy 
   134  "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
   135 \           evs : otway |]                                           \
   136 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   137 by (etac rev_mp 1);
   138 by (etac otway.induct 1);
   139 by (ALLGOALS Simp_tac);
   140 by (ALLGOALS Blast_tac);
   141 qed "Says_Server_message_form";
   142 
   143 
   144 (*For proofs involving analz.*)
   145 val analz_spies_tac = 
   146     dtac OR2_analz_spies 4 THEN 
   147     dtac OR4_analz_spies 6 THEN
   148     forward_tac [Says_Server_message_form] 7 THEN
   149     assume_tac 7 THEN
   150     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   151 
   152 
   153 (****
   154  The following is to prove theorems of the form
   155 
   156   Key K : analz (insert (Key KAB) (spies evs)) ==>
   157   Key K : analz (spies evs)
   158 
   159  A more general formula must be proved inductively.
   160 ****)
   161 
   162 
   163 (** Session keys are not used to encrypt other session keys **)
   164 
   165 (*The equality makes the induction hypothesis easier to apply*)
   166 goal thy  
   167  "!!evs. evs : otway ==>                                    \
   168 \  ALL K KK. KK <= Compl (range shrK) -->                   \
   169 \            (Key K : analz (Key``KK Un (spies evs))) =  \
   170 \            (K : KK | Key K : analz (spies evs))";
   171 by (etac otway.induct 1);
   172 by analz_spies_tac;
   173 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   174 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   175 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   176 (*Fake*) 
   177 by (spy_analz_tac 1);
   178 qed_spec_mp "analz_image_freshK";
   179 
   180 
   181 goal thy
   182  "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
   183 \        Key K : analz (insert (Key KAB) (spies evs)) =  \
   184 \        (K = KAB | Key K : analz (spies evs))";
   185 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   186 qed "analz_insert_freshK";
   187 
   188 
   189 (*** The Key K uniquely identifies the Server's  message. **)
   190 
   191 goal thy 
   192  "!!evs. evs : otway ==>                                                  \
   193 \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
   194 \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
   195 \     B=B' & NA=NA' & NB=NB' & X=X'";
   196 by (etac otway.induct 1);
   197 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   198 by (ALLGOALS Clarify_tac);
   199 (*Remaining cases: OR3 and OR4*)
   200 by (ex_strip_tac 2);
   201 by (Best_tac 2);
   202 by (expand_case_tac "K = ?y" 1);
   203 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   204 (*...we assume X is a recent message, and handle this case by contradiction*)
   205 by (Blast_tac 1);
   206 val lemma = result();
   207 
   208 goal thy 
   209  "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
   210 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
   211 \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   212 by (prove_unique_tac lemma 1);
   213 qed "unique_session_keys";
   214 
   215 
   216 
   217 (**** Authenticity properties relating to NA ****)
   218 
   219 (*Only OR1 can have caused such a part of a message to appear.*)
   220 goal thy 
   221  "!!evs. [| A ~: bad;  evs : otway |]                             \
   222 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   223 \            Says A B {|NA, Agent A, Agent B,                      \
   224 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   225 \             : set evs";
   226 by (parts_induct_tac 1);
   227 by (Blast_tac 1);
   228 qed_spec_mp "Crypt_imp_OR1";
   229 
   230 
   231 (** The Nonce NA uniquely identifies A's message. **)
   232 
   233 goal thy 
   234  "!!evs. [| evs : otway; A ~: bad |]               \
   235 \ ==> EX B'. ALL B.                                 \
   236 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   237 \        --> B = B'";
   238 by (parts_induct_tac 1);
   239 by (Blast_tac 1);
   240 by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   241 (*OR1: creation of new Nonce.  Move assertion into global context*)
   242 by (expand_case_tac "NA = ?y" 1);
   243 by (Blast_tac 1);
   244 val lemma = result();
   245 
   246 goal thy 
   247  "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   248 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   249 \          evs : otway;  A ~: bad |]                                   \
   250 \        ==> B = C";
   251 by (prove_unique_tac lemma 1);
   252 qed "unique_NA";
   253 
   254 
   255 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   256   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   257   over-simplified version of this protocol: see OtwayRees_Bad.*)
   258 goal thy 
   259  "!!evs. [| A ~: bad;  evs : otway |]                      \
   260 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   261 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   262 \             ~: parts (spies evs)";
   263 by (parts_induct_tac 1);
   264 by (ALLGOALS Blast_tac);
   265 qed_spec_mp"no_nonce_OR1_OR2";
   266 
   267 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE);
   268 
   269 (*Crucial property: If the encrypted message appears, and A has used NA
   270   to start a run, then it originated with the Server!*)
   271 goal thy 
   272  "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                      \
   273 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   274 \        --> Says A B {|NA, Agent A, Agent B,                          \
   275 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   276 \             : set evs -->                                            \
   277 \            (EX NB. Says Server B                                     \
   278 \                 {|NA,                                                \
   279 \                   Crypt (shrK A) {|NA, Key K|},                      \
   280 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   281 \                   : set evs)";
   282 by (parts_induct_tac 1);
   283 by (Blast_tac 1);
   284 (*OR1: it cannot be a new Nonce, contradiction.*)
   285 by (Blast_tac 1);
   286 (*OR3 and OR4*)
   287 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   288 by (rtac conjI 1);
   289 by (ALLGOALS Clarify_tac);
   290 (*OR4*)
   291 by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3);
   292 (*OR3, two cases*)  (** LEVEL 7 **)
   293 by (blast_tac (claset() addSEs  [nonce_OR1_OR2_E]
   294                         delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   295 by (blast_tac (claset() addIs  [unique_NA]) 1);
   296 qed_spec_mp "NA_Crypt_imp_Server_msg";
   297 
   298 
   299 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   300   then the key really did come from the Server!  CANNOT prove this of the
   301   bad form of this protocol, even though we can prove
   302   Spy_not_see_encrypted_key*)
   303 goal thy 
   304  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   305 \           Says A  B {|NA, Agent A, Agent B,                       \
   306 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   307 \           A ~: bad;  A ~= Spy;  evs : otway |]                  \
   308 \        ==> EX NB. Says Server B                                  \
   309 \                     {|NA,                                        \
   310 \                       Crypt (shrK A) {|NA, Key K|},              \
   311 \                       Crypt (shrK B) {|NB, Key K|}|}             \
   312 \                       : set evs";
   313 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
   314 qed "A_trusts_OR4";
   315 
   316 
   317 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   318     Does not in itself guarantee security: an attack could violate 
   319     the premises, e.g. by having A=Spy **)
   320 
   321 goal thy 
   322  "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
   323 \        ==> Says Server B                                            \
   324 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   325 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   326 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   327 \            Key K ~: analz (spies evs)";
   328 by (etac otway.induct 1);
   329 by analz_spies_tac;
   330 by (ALLGOALS
   331     (asm_simp_tac (simpset() addcongs [conj_cong] 
   332                             addsimps [analz_insert_eq, analz_insert_freshK]
   333                             addsimps (pushes@expand_ifs))));
   334 (*Oops*)
   335 by (blast_tac (claset() addSDs [unique_session_keys]) 4);
   336 (*OR4*) 
   337 by (Blast_tac 3);
   338 (*OR3*)
   339 by (Blast_tac 2);
   340 (*Fake*) 
   341 by (spy_analz_tac 1);
   342 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   343 
   344 goal thy 
   345  "!!evs. [| Says Server B                                           \
   346 \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   347 \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   348 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   349 \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   350 \        ==> Key K ~: analz (spies evs)";
   351 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   352 by (blast_tac (claset() addSEs [lemma]) 1);
   353 qed "Spy_not_see_encrypted_key";
   354 
   355 
   356 (**** Authenticity properties relating to NB ****)
   357 
   358 (*Only OR2 can have caused such a part of a message to appear.  We do not
   359   know anything about X: it does NOT have to have the right form.*)
   360 goal thy 
   361  "!!evs. [| B ~: bad;  evs : otway |]                         \
   362 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   363 \             : parts (spies evs) -->                       \
   364 \            (EX X. Says B Server                              \
   365 \             {|NA, Agent A, Agent B, X,                       \
   366 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   367 \             : set evs)";
   368 by (parts_induct_tac 1);
   369 by (ALLGOALS Blast_tac);
   370 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   371 
   372 
   373 (** The Nonce NB uniquely identifies B's  message. **)
   374 
   375 goal thy 
   376  "!!evs. [| evs : otway; B ~: bad |]                    \
   377 \ ==> EX NA' A'. ALL NA A.                               \
   378 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
   379 \      --> NA = NA' & A = A'";
   380 by (parts_induct_tac 1);
   381 by (Blast_tac 1);
   382 by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
   383 (*OR2: creation of new Nonce.  Move assertion into global context*)
   384 by (expand_case_tac "NB = ?y" 1);
   385 by (Blast_tac 1);
   386 val lemma = result();
   387 
   388 goal thy 
   389  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   390 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   391 \          evs : otway;  B ~: bad |]             \
   392 \        ==> NC = NA & C = A";
   393 by (prove_unique_tac lemma 1);
   394 qed "unique_NB";
   395 
   396 
   397 (*If the encrypted message appears, and B has used Nonce NB,
   398   then it originated with the Server!*)
   399 goal thy 
   400  "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway |]                        \
   401 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)             \
   402 \        --> (ALL X'. Says B Server                                      \
   403 \                       {|NA, Agent A, Agent B, X',                      \
   404 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   405 \             : set evs                                                  \
   406 \             --> Says Server B                                          \
   407 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   408 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   409 \                   : set evs)";
   410 by (parts_induct_tac 1);
   411 by (Blast_tac 1);
   412 (*OR1: it cannot be a new Nonce, contradiction.*)
   413 by (Blast_tac 1);
   414 (*OR4*)
   415 by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 2);
   416 (*OR3*)
   417 (*Provable in 38s by the single command
   418     by (blast_tac (claset() addDs  [unique_NB] addEs[nonce_OR1_OR2_E]) 1);
   419 *)
   420 by (safe_tac (claset() delrules [disjCI, impCE]));
   421 by (Blast_tac 3); 
   422 by (blast_tac (claset() addDs  [unique_NB]) 2);
   423 by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
   424                         delrules [conjI] (*stop split-up*)) 1);
   425 qed_spec_mp "NB_Crypt_imp_Server_msg";
   426 
   427 
   428 (*Guarantee for B: if it gets a message with matching NB then the Server
   429   has sent the correct message.*)
   430 goal thy 
   431  "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway;                    \
   432 \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
   433 \           Says B Server {|NA, Agent A, Agent B, X',              \
   434 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   435 \            : set evs |]                                          \
   436 \        ==> Says Server B                                         \
   437 \                 {|NA,                                            \
   438 \                   Crypt (shrK A) {|NA, Key K|},                  \
   439 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   440 \                   : set evs";
   441 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
   442 qed "B_trusts_OR3";
   443 
   444 
   445 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   446 
   447 
   448 goal thy 
   449  "!!evs. [| B ~: bad;  evs : otway |]                           \
   450 \        ==> Says Server B                                       \
   451 \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   452 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
   453 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,     \
   454 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   455 \            : set evs)";
   456 by (etac otway.induct 1);
   457 by (ALLGOALS Asm_simp_tac);
   458 by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 3);
   459 by (ALLGOALS Blast_tac);
   460 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   461 
   462 
   463 (*After getting and checking OR4, agent A can trust that B has been active.
   464   We could probably prove that X has the expected form, but that is not
   465   strictly necessary for authentication.*)
   466 goal thy 
   467  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   468 \           Says A B {|NA, Agent A, Agent B,                                \
   469 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   470 \           A ~: bad;  A ~= Spy;  B ~: bad;  evs : otway |]               \
   471 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   472 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   473 \            : set evs";
   474 by (blast_tac (claset() addSDs [A_trusts_OR4]
   475                         addSEs [OR3_imp_OR2]) 1);
   476 qed "A_auths_B";