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