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