src/HOL/Auth/TLS.ML
author paulson
Wed Oct 01 13:42:18 1997 +0200 (1997-10-01)
changeset 3760 77f71f650433
parent 3758 188a4fbfaf55
child 3772 6ee707a73248
permissions -rw-r--r--
Strengthened the possibility property for resumption so that it could have
detected the problem with ServerResume
     1 (*  Title:      HOL/Auth/TLS
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Protocol goals: 
     7 * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
     8      parties (though A is not necessarily authenticated).
     9 
    10 * B upon receiving CertVerify knows that A is present (But this
    11     message is optional!)
    12 
    13 * A upon receiving ServerFinished knows that B is present
    14 
    15 * Each party who has received a FINISHED message can trust that the other
    16   party agrees on all message components, including PA and PB (thus foiling
    17   rollback attacks).
    18 *)
    19 
    20 
    21 open TLS;
    22 
    23 proof_timing:=true;
    24 HOL_quantifiers := false;
    25 
    26 (** We mostly DO NOT unfold the definition of "certificate".  The attached
    27     lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
    28     contexts.
    29 **)
    30 
    31 goalw thy [certificate_def] 
    32     "parts (insert (certificate B KB) H) =  \
    33 \    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
    34 by (rtac refl 1);
    35 qed "parts_insert_certificate";
    36 
    37 goalw thy [certificate_def] 
    38     "analz (insert (certificate B KB) H) =  \
    39 \    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
    40 by (rtac refl 1);
    41 qed "analz_insert_certificate";
    42 Addsimps [parts_insert_certificate, analz_insert_certificate];
    43 
    44 goalw thy [certificate_def] 
    45     "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
    46 by (Blast_tac 1);
    47 qed "eq_certificate_iff";
    48 AddIffs [eq_certificate_iff];
    49 
    50 
    51 (*Injectiveness of key-generating functions*)
    52 AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
    53 
    54 (* invKey(sessionK x) = sessionK x*)
    55 Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
    56 
    57 
    58 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    59 
    60 goal thy "pubK A ~= sessionK arg";
    61 br notI 1;
    62 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    63 by (Full_simp_tac 1);
    64 qed "pubK_neq_sessionK";
    65 
    66 goal thy "priK A ~= sessionK arg";
    67 br notI 1;
    68 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    69 by (Full_simp_tac 1);
    70 qed "priK_neq_sessionK";
    71 
    72 val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
    73 AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    74 
    75 
    76 (**** Protocol Proofs ****)
    77 
    78 (*A "possibility property": there are traces that reach the end.
    79   This protocol has three end points and six messages to consider.*)
    80 
    81 
    82 (** These proofs make the further assumption that the Nonce_supply nonces 
    83 	(which have the form  @ N. Nonce N ~: used evs)
    84     lie outside the range of PRF.  This assumption seems reasonable, but
    85     as it is needed only for the possibility theorems, it is not taken
    86     as an axiom.
    87 **)
    88 
    89 
    90 (*Possibility property ending with ClientAccepts.*)
    91 goal thy 
    92  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    93 \           A ~= B |]            \
    94 \  ==> EX SID M. EX evs: tls.    \
    95 \        Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    96 by (REPEAT (resolve_tac [exI,bexI] 1));
    97 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    98 	  tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
    99 	  tls.ClientAccepts) 2);
   100 by possibility_tac;
   101 by (REPEAT (Blast_tac 1));
   102 result();
   103 
   104 (*And one for ServerAccepts.  Either FINISHED message may come first.*)
   105 goal thy 
   106  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   107 \           A ~= B |]                        \
   108 \  ==> EX SID NA PA NB PB M. EX evs: tls.    \
   109 \        Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
   110 by (REPEAT (resolve_tac [exI,bexI] 1));
   111 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
   112 	  tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
   113 	  tls.ServerAccepts) 2);
   114 by possibility_tac;
   115 by (REPEAT (Blast_tac 1));
   116 result();
   117 
   118 (*Another one, for CertVerify (which is optional)*)
   119 goal thy 
   120  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   121 \           A ~= B |]                       \
   122 \  ==> EX NB PMS. EX evs: tls.   \
   123 \  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
   124 by (REPEAT (resolve_tac [exI,bexI] 1));
   125 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
   126 	  tls.ClientKeyExch RS tls.CertVerify) 2);
   127 by possibility_tac;
   128 by (REPEAT (Blast_tac 1));
   129 result();
   130 
   131 (*Another one, for session resumption (both ServerResume and ClientResume) *)
   132 goal thy 
   133  "!!A B. [| evs0 : tls;     \
   134 \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
   135 \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
   136 \           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   137 \           A ~= B |] ==> EX NA PA NB PB X. EX evs: tls.    \
   138 \      X = Hash{|Number SID, Nonce M,             \
   139 \                       Nonce NA, Number PA, Agent A,      \
   140 \                       Nonce NB, Number PB, Agent B|}  &  \
   141 \      Says A B (Crypt (clientK(NA,NB,M)) X) : set evs  &  \
   142 \      Says B A (Crypt (serverK(NA,NB,M)) X) : set evs";
   143 by (REPEAT (resolve_tac [exI,bexI] 1));
   144 by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
   145 	  tls.ClientResume) 2);
   146 by possibility_tac;
   147 by (REPEAT (Blast_tac 1));
   148 result();
   149 
   150 
   151 
   152 (**** Inductive proofs about tls ****)
   153 
   154 (*Nobody sends themselves messages*)
   155 goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   156 by (etac tls.induct 1);
   157 by (Auto_tac());
   158 qed_spec_mp "not_Says_to_self";
   159 Addsimps [not_Says_to_self];
   160 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   161 
   162 
   163 (*Induction for regularity theorems.  If induction formula has the form
   164    X ~: analz (spies evs) --> ... then it shortens the proof by discarding
   165    needless information about analz (insert X (spies evs))  *)
   166 fun parts_induct_tac i = 
   167     etac tls.induct i
   168     THEN 
   169     REPEAT (FIRSTGOAL analz_mono_contra_tac)
   170     THEN 
   171     fast_tac (!claset addss (!simpset)) i THEN
   172     ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
   173 
   174 
   175 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   176     sends messages containing X! **)
   177 
   178 (*Spy never sees another agent's private key! (unless it's bad at start)*)
   179 goal thy 
   180  "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
   181 by (parts_induct_tac 1);
   182 by (Fake_parts_insert_tac 1);
   183 qed "Spy_see_priK";
   184 Addsimps [Spy_see_priK];
   185 
   186 goal thy 
   187  "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
   188 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   189 qed "Spy_analz_priK";
   190 Addsimps [Spy_analz_priK];
   191 
   192 goal thy  "!!A. [| Key (priK A) : parts (spies evs);  evs : tls |] ==> A:bad";
   193 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
   194 qed "Spy_see_priK_D";
   195 
   196 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
   197 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
   198 
   199 
   200 (*This lemma says that no false certificates exist.  One might extend the
   201   model to include bogus certificates for the agents, but there seems
   202   little point in doing so: the loss of their private keys is a worse
   203   breach of security.*)
   204 goalw thy [certificate_def]
   205  "!!evs. evs : tls ==> certificate B KB : parts (spies evs) --> KB = pubK B";
   206 by (parts_induct_tac 1);
   207 by (Fake_parts_insert_tac 1);
   208 bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   209 
   210 
   211 (*Replace key KB in ClientKeyExch by (pubK B) *)
   212 val ClientKeyExch_tac = 
   213     forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
   214     THEN' assume_tac
   215     THEN' hyp_subst_tac;
   216 
   217 fun analz_induct_tac i = 
   218     etac tls.induct i   THEN
   219     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
   220     ALLGOALS (asm_simp_tac 
   221               (!simpset addcongs [if_weak_cong]
   222                         setloop split_tac [expand_if]))  THEN
   223     (*Remove instances of pubK B:  the Spy already knows all public keys.
   224       Combining the two simplifier calls makes them run extremely slowly.*)
   225     ALLGOALS (asm_simp_tac 
   226               (!simpset addcongs [if_weak_cong]
   227 			addsimps [insert_absorb]
   228                         setloop split_tac [expand_if]));
   229 
   230 
   231 (*** Properties of items found in Notes ***)
   232 
   233 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   234 \                ==> Crypt (pubK B) X : parts (spies evs)";
   235 by (etac rev_mp 1);
   236 by (analz_induct_tac 1);
   237 by (blast_tac (!claset addIs [parts_insertI]) 1);
   238 qed "Notes_Crypt_parts_spies";
   239 
   240 (*C may be either A or B*)
   241 goal thy
   242  "!!evs. [| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \
   243 \           evs : tls     \
   244 \        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
   245 by (etac rev_mp 1);
   246 by (parts_induct_tac 1);
   247 by (ALLGOALS Clarify_tac);
   248 (*Fake*)
   249 by (blast_tac (!claset addIs [parts_insertI]) 1);
   250 (*Client, Server Accept*)
   251 by (REPEAT (blast_tac (!claset addSEs spies_partsEs
   252                                addSDs [Notes_Crypt_parts_spies]) 1));
   253 qed "Notes_master_imp_Crypt_PMS";
   254 
   255 (*Compared with the theorem above, both premise and conclusion are stronger*)
   256 goal thy
   257  "!!evs. [| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\
   258 \           evs : tls     \
   259 \        |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   260 by (etac rev_mp 1);
   261 by (parts_induct_tac 1);
   262 (*ServerAccepts*)
   263 by (Fast_tac 1);	(*Blast_tac's very slow here*)
   264 qed "Notes_master_imp_Notes_PMS";
   265 
   266 
   267 (*** Protocol goal: if B receives CertVerify, then A sent it ***)
   268 
   269 (*B can check A's signature if he has received A's certificate.*)
   270 goal thy
   271  "!!evs. [| X : parts (spies evs);          \
   272 \           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});      \
   273 \           evs : tls;  A ~: bad |]                       \
   274 \    ==> Says A B X : set evs";
   275 by (etac rev_mp 1);
   276 by (hyp_subst_tac 1);
   277 by (parts_induct_tac 1);
   278 by (Fake_parts_insert_tac 1);
   279 val lemma = result();
   280 
   281 (*Final version: B checks X using the distributed KA instead of priK A*)
   282 goal thy
   283  "!!evs. [| X : parts (spies evs);          \
   284 \           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});      \
   285 \           certificate A KA : parts (spies evs);       \
   286 \           evs : tls;  A ~: bad |]                       \
   287 \    ==> Says A B X : set evs";
   288 by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
   289 qed "TrustCertVerify";
   290 
   291 
   292 (*If CertVerify is present then A has chosen PMS.*)
   293 goal thy
   294  "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|})  \
   295 \             : parts (spies evs);                                \
   296 \           evs : tls;  A ~: bad |]                                      \
   297 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   298 be rev_mp 1;
   299 by (parts_induct_tac 1);
   300 by (Fake_parts_insert_tac 1);
   301 val lemma = result();
   302 
   303 (*Final version using the distributed KA instead of priK A*)
   304 goal thy
   305  "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})  \
   306 \             : parts (spies evs);                                \
   307 \           certificate A KA : parts (spies evs);       \
   308 \           evs : tls;  A ~: bad |]                                      \
   309 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   310 by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
   311 qed "UseCertVerify";
   312 
   313 
   314 (*Key compromise lemma needed to prove analz_image_keys.
   315   No collection of keys can help the spy get new private keys.*)
   316 goal thy  
   317  "!!evs. evs : tls ==>                                    \
   318 \  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
   319 \          (priK B : KK | B : bad)";
   320 by (etac tls.induct 1);
   321 by (ALLGOALS
   322     (asm_simp_tac (analz_image_keys_ss
   323 		   addsimps (analz_insert_certificate::keys_distinct))));
   324 (*Fake*) 
   325 by (spy_analz_tac 2);
   326 (*Base*)
   327 by (Blast_tac 1);
   328 qed_spec_mp "analz_image_priK";
   329 
   330 
   331 (*slightly speeds up the big simplification below*)
   332 goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   333 by (Blast_tac 1);
   334 val range_sessionkeys_not_priK = result();
   335 
   336 (*Lemma for the trivial direction of the if-and-only-if*)
   337 goal thy  
   338  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   339 \        (X : analz (G Un H))  =  (X : analz H)";
   340 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   341 val lemma = result();
   342 
   343 (** It is a mystery to me why the following formulation is actually slower
   344     in simplification:
   345 
   346 \    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   347 \           (Nonce N : analz (spies evs))";
   348 
   349 More so as it can take advantage of unconditional rewrites such as 
   350      priK B ~: sessionK``Z
   351 **)
   352 
   353 goal thy  
   354  "!!evs. evs : tls ==>                                 \
   355 \    ALL KK. KK <= range sessionK -->           \
   356 \            (Nonce N : analz (Key``KK Un (spies evs))) = \
   357 \            (Nonce N : analz (spies evs))";
   358 by (etac tls.induct 1);
   359 by (ClientKeyExch_tac 7);
   360 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   361 by (REPEAT_FIRST (rtac lemma));
   362 by (ALLGOALS    (*23 seconds*)
   363     (asm_simp_tac (analz_image_keys_ss 
   364 		   addsimps [range_sessionkeys_not_priK, 
   365 			     analz_image_priK, analz_insert_certificate])));
   366 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   367 (*Fake*) 
   368 by (spy_analz_tac 2);
   369 (*Base*)
   370 by (Blast_tac 1);
   371 qed_spec_mp "analz_image_keys";
   372 
   373 (*Knowing some session keys is no help in getting new nonces*)
   374 goal thy
   375  "!!evs. evs : tls ==>          \
   376 \        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
   377 \        (Nonce N : analz (spies evs))";
   378 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
   379 qed "analz_insert_key";
   380 Addsimps [analz_insert_key];
   381 
   382 goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   383 by (parts_induct_tac 1);
   384 (*ClientKeyExch: PMS is assumed to differ from any PRF.*)
   385 by (Blast_tac 1);
   386 qed "no_Notes_A_PRF";
   387 Addsimps [no_Notes_A_PRF];
   388 
   389 
   390 goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
   391 \                   evs : tls |]  \
   392 \                ==> Nonce PMS : parts (spies evs)";
   393 by (etac rev_mp 1);
   394 by (parts_induct_tac 1);
   395 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
   396 by (Fake_parts_insert_tac 1);
   397 (*Six others, all trivial or by freshness*)
   398 by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
   399                                addSEs spies_partsEs) 1));
   400 qed "MS_imp_PMS";
   401 AddSDs [MS_imp_PMS];
   402 
   403 
   404 
   405 (*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   406 
   407 (** Some lemmas about session keys, comprising clientK and serverK **)
   408 
   409 
   410 (*Lemma: session keys are never used if PMS is fresh.  
   411   Nonces don't have to agree, allowing session resumption.
   412   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   413   THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   414 goal thy 
   415  "!!evs. [| Nonce PMS ~: parts (spies evs);  \
   416 \           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
   417 \           evs : tls |]             \
   418 \  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
   419 by (etac rev_mp 1);
   420 by (hyp_subst_tac 1);
   421 by (analz_induct_tac 1);
   422 (*SpyKeys*)
   423 by (blast_tac (!claset addSEs spies_partsEs) 3);
   424 (*Fake*)
   425 by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
   426 by (Fake_parts_insert_tac 2);
   427 (** LEVEL 6 **)
   428 (*Oops*)
   429 by (fast_tac (!claset addSEs [MPair_parts]
   430 		       addDs  [Says_imp_spies RS parts.Inj]
   431 		       addss (!simpset)) 6);
   432 by (REPEAT 
   433     (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   434 				Notes_master_imp_Crypt_PMS]
   435                         addSEs spies_partsEs) 1));
   436 val lemma = result();
   437 
   438 goal thy 
   439  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   440 \  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
   441 by (blast_tac (!claset addDs [lemma]) 1);
   442 qed "PMS_sessionK_not_spied";
   443 
   444 goal thy 
   445  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   446 \  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   447 by (blast_tac (!claset addDs [lemma]) 1);
   448 qed "PMS_Crypt_sessionK_not_spied";
   449 
   450 
   451 (*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   452   Converse doesn't hold; betraying M doesn't force the keys to be sent!
   453   The strong Oops condition can be weakened later by unicity reasoning, 
   454 	with some effort.*)
   455 goal thy 
   456  "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   457 \           Nonce M ~: analz (spies evs);  evs : tls |]   \
   458 \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   459 by (etac rev_mp 1);
   460 by (etac rev_mp 1);
   461 by (analz_induct_tac 1);        (*17 seconds*)
   462 (*Oops*)
   463 by (Blast_tac 4);
   464 (*SpyKeys*)
   465 by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
   466 (*Fake*) 
   467 by (spy_analz_tac 2);
   468 (*Base*)
   469 by (Blast_tac 1);
   470 qed "sessionK_not_spied";
   471 Addsimps [sessionK_not_spied];
   472 
   473 
   474 (*** Unicity results for PMS, the pre-master-secret ***)
   475 
   476 (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   477 goal thy 
   478  "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
   479 \        ==> EX B'. ALL B.   \
   480 \              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
   481 by (etac rev_mp 1);
   482 by (parts_induct_tac 1);
   483 by (Fake_parts_insert_tac 1);
   484 (*ClientKeyExch*)
   485 by (ClientKeyExch_tac 1);
   486 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   487 by (expand_case_tac "PMS = ?y" 1 THEN
   488     blast_tac (!claset addSEs partsEs) 1);
   489 val lemma = result();
   490 
   491 goal thy 
   492  "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
   493 \           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
   494 \           Nonce PMS ~: analz (spies evs);                 \
   495 \           evs : tls |]                                          \
   496 \        ==> B=B'";
   497 by (prove_unique_tac lemma 1);
   498 qed "Crypt_unique_PMS";
   499 
   500 
   501 (** It is frustrating that we need two versions of the unicity results.
   502     But Notes A {|Agent B, Nonce PMS|} determines both A and B.  Sometimes
   503     we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 
   504     determines B alone, and only if PMS is secret.
   505 **)
   506 
   507 (*In A's internal Note, PMS determines A and B.*)
   508 goal thy "!!evs. evs : tls               \
   509 \                ==> EX A' B'. ALL A B.  \
   510 \                    Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   511 by (parts_induct_tac 1);
   512 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   513 (*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
   514 by (expand_case_tac "PMS = ?y" 1 THEN
   515     blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
   516 val lemma = result();
   517 
   518 goal thy 
   519  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   520 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   521 \           evs : tls |]                               \
   522 \        ==> A=A' & B=B'";
   523 by (prove_unique_tac lemma 1);
   524 qed "Notes_unique_PMS";
   525 
   526 
   527 
   528 (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   529 goal thy
   530  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   531 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   532 \            Nonce PMS ~: analz (spies evs)";
   533 by (analz_induct_tac 1);   (*11 seconds*)
   534 (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   535 by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
   536 (*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
   537   mostly freshness reasoning*)
   538 by (REPEAT (blast_tac (!claset addSEs partsEs
   539 			       addDs  [Notes_Crypt_parts_spies,
   540 				       impOfSubs analz_subset_parts,
   541 				       Says_imp_spies RS analz.Inj]) 3));
   542 (*SpyKeys*)
   543 by (fast_tac (!claset addss (!simpset)) 2);
   544 (*Fake*)
   545 by (spy_analz_tac 1);
   546 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   547 
   548 
   549 (*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   550   will stay secret.*)
   551 goal thy
   552  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   553 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   554 \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
   555 by (analz_induct_tac 1);   (*13 seconds*)
   556 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
   557 by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
   558 				      Says_imp_spies RS analz.Inj,
   559 				      Notes_imp_spies RS analz.Inj]) 6));
   560 (*ClientHello*)
   561 by (Blast_tac 3);
   562 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   563 by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   564 			       Says_imp_spies RS analz.Inj]) 2);
   565 (*Fake*)
   566 by (spy_analz_tac 1);
   567 (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
   568 by (REPEAT (blast_tac (!claset addSEs partsEs
   569 			       addDs  [Notes_Crypt_parts_spies,
   570 				       impOfSubs analz_subset_parts,
   571 				       Says_imp_spies RS analz.Inj]) 1));
   572 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   573 
   574 
   575 (*** Weakening the Oops conditions for leakage of clientK ***)
   576 
   577 (*If A created PMS then nobody other than the Spy would send a message
   578   using a clientK generated from that PMS.*)
   579 goal thy
   580  "!!evs. [| evs : tls;  A' ~= Spy |]                \
   581 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   582 \      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   583 \      A = A'";
   584 by (analz_induct_tac 1);	(*8 seconds*)
   585 by (ALLGOALS Clarify_tac);
   586 (*ClientFinished, ClientResume: by unicity of PMS*)
   587 by (REPEAT 
   588     (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
   589      	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
   590 (*ClientKeyExch*)
   591 by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   592 	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   593 bind_thm ("Says_clientK_unique",
   594 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   595 
   596 
   597 (*If A created PMS and has not leaked her clientK to the Spy, 
   598   then nobody has.*)
   599 goal thy
   600  "!!evs. evs : tls                         \
   601 \  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   602 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   603 \      (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   604 by (etac tls.induct 1);
   605 (*This roundabout proof sequence avoids looping in simplification*)
   606 by (ALLGOALS Simp_tac);
   607 by (ALLGOALS Clarify_tac);
   608 by (Fake_parts_insert_tac 1);
   609 by (ALLGOALS Asm_simp_tac);
   610 (*Oops*)
   611 by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
   612 (*ClientKeyExch*)
   613 by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   614 			       spies_partsEs)) 1);
   615 qed_spec_mp "clientK_Oops_ALL";
   616 
   617 
   618 
   619 (*** Weakening the Oops conditions for leakage of serverK ***)
   620 
   621 (*If A created PMS for B, then nobody other than B or the Spy would
   622   send a message using a serverK generated from that PMS.*)
   623 goal thy
   624  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
   625 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   626 \      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   627 \      B = B'";
   628 by (analz_induct_tac 1);	(*9 seconds*)
   629 by (ALLGOALS Clarify_tac);
   630 (*ServerResume, ServerFinished: by unicity of PMS*)
   631 by (REPEAT
   632     (blast_tac (!claset addSEs [MPair_parts]
   633 		        addSDs [Notes_master_imp_Crypt_PMS, 
   634 				Says_imp_spies RS parts.Inj]
   635                         addDs  [Spy_not_see_PMS, 
   636 				Notes_Crypt_parts_spies,
   637 				Crypt_unique_PMS]) 2));
   638 (*ClientKeyExch*)
   639 by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   640 	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   641 bind_thm ("Says_serverK_unique",
   642 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   643 
   644 (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   645   then nobody has.*)
   646 goal thy
   647  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                        \
   648 \  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   649 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   650 \      (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   651 by (etac tls.induct 1);
   652 (*This roundabout proof sequence avoids looping in simplification*)
   653 by (ALLGOALS Simp_tac);
   654 by (ALLGOALS Clarify_tac);
   655 by (Fake_parts_insert_tac 1);
   656 by (ALLGOALS Asm_simp_tac);
   657 (*Oops*)
   658 by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
   659 (*ClientKeyExch*)
   660 by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   661 			       spies_partsEs)) 1);
   662 qed_spec_mp "serverK_Oops_ALL";
   663 
   664 
   665 
   666 (*** Protocol goals: if A receives ServerFinished, then B is present 
   667      and has used the quoted values PA, PB, etc.  Note that it is up to A
   668      to compare PA with what she originally sent.
   669 ***)
   670 
   671 (*The mention of her name (A) in X assures A that B knows who she is.*)
   672 goal thy
   673  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   674 \           X = Crypt (serverK(Na,Nb,M))                  \
   675 \                 (Hash{|Number SID, Nonce M,             \
   676 \                        Nonce Na, Number PA, Agent A,    \
   677 \                        Nonce Nb, Number PB, Agent B|}); \
   678 \           M = PRF(PMS,NA,NB);                           \
   679 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   680 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   681 \        X : parts (spies evs) --> Says B A X : set evs";
   682 by (etac rev_mp 1);
   683 by (hyp_subst_tac 1);
   684 by (analz_induct_tac 1);        (*22 seconds*)
   685 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   686 (*proves ServerResume*)
   687 by (ALLGOALS Clarify_tac);
   688 (*ClientKeyExch*)
   689 by (fast_tac  (*blast_tac gives PROOF FAILED*)
   690     (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   691 (*Fake: the Spy doesn't have the critical session key!*)
   692 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   693 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   694 				     not_parts_not_analz]) 2);
   695 by (Fake_parts_insert_tac 1);
   696 val lemma = normalize_thm [RSspec, RSmp] (result());
   697 
   698 (*Final version*)
   699 goal thy
   700  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   701 \                 (Hash{|Number SID, Nonce M,             \
   702 \                        Nonce Na, Number PA, Agent A,    \
   703 \                        Nonce Nb, Number PB, Agent B|}); \
   704 \           M = PRF(PMS,NA,NB);                           \
   705 \           X : parts (spies evs);                        \
   706 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   707 \           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   708 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   709 \        ==> Says B A X : set evs";
   710 by (blast_tac (!claset addIs [lemma]
   711                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   712 qed_spec_mp "TrustServerFinished";
   713 
   714 
   715 
   716 (*This version refers not to ServerFinished but to any message from B.
   717   We don't assume B has received CertVerify, and an intruder could
   718   have changed A's identity in all other messages, so we can't be sure
   719   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   720   to bind A's identity with PMS, then we could replace A' by A below.*)
   721 goal thy
   722  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   723 \           evs : tls;  A ~: bad;  B ~: bad;                 \
   724 \           M = PRF(PMS,NA,NB) |]            \
   725 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   726 \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   727 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   728 by (etac rev_mp 1);
   729 by (hyp_subst_tac 1);
   730 by (analz_induct_tac 1);	(*20 seconds*)
   731 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   732 by (ALLGOALS Clarify_tac);
   733 (*ServerResume, ServerFinished: by unicity of PMS*)
   734 by (REPEAT
   735     (blast_tac (!claset addSEs [MPair_parts]
   736 		        addSDs [Notes_master_imp_Crypt_PMS, 
   737 				Says_imp_spies RS parts.Inj]
   738                         addDs  [Spy_not_see_PMS, 
   739 				Notes_Crypt_parts_spies,
   740 				Crypt_unique_PMS]) 3));
   741 (*ClientKeyExch*)
   742 by (blast_tac
   743     (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   744 (*Fake: the Spy doesn't have the critical session key!*)
   745 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   746 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   747 				     not_parts_not_analz]) 2);
   748 by (Fake_parts_insert_tac 1);
   749 val lemma = normalize_thm [RSspec, RSmp] (result());
   750 
   751 (*Final version*)
   752 goal thy
   753  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   754 \           Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
   755 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   756 \           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   757 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   758 \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
   759 by (blast_tac (!claset addIs [lemma]
   760                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   761 
   762 qed_spec_mp "TrustServerMsg";
   763 
   764 
   765 
   766 (*** Protocol goal: if B receives any message encrypted with clientK
   767      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   768      assumed here; B cannot verify it.  But if the message is
   769      ClientFinished, then B can then check the quoted values PA, PB, etc.
   770 ***)
   771 
   772 goal thy
   773  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   774 \  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
   775 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   776 \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   777 \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   778 by (analz_induct_tac 1);	(*15 seconds*)
   779 by (ALLGOALS Clarify_tac);
   780 (*ClientFinished, ClientResume: by unicity of PMS*)
   781 by (REPEAT (blast_tac (!claset delrules [conjI]
   782 		               addSDs [Notes_master_imp_Notes_PMS]
   783 	 	               addDs  [Notes_unique_PMS]) 3));
   784 (*ClientKeyExch*)
   785 by (fast_tac  (*blast_tac gives PROOF FAILED*)
   786     (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   787 (*Fake: the Spy doesn't have the critical session key!*)
   788 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   789 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   790 				     not_parts_not_analz]) 2);
   791 by (Fake_parts_insert_tac 1);
   792 val lemma = normalize_thm [RSspec, RSmp] (result());
   793 
   794 (*Final version*)
   795 goal thy
   796  "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs);  \
   797 \           Notes A {|Agent B, Nonce PMS|} : set evs;        \
   798 \           Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;  \
   799 \           evs : tls;  A ~: bad;  B ~: bad |]                         \
   800 \  ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   801 by (blast_tac (!claset addIs [lemma]
   802                        addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
   803 qed_spec_mp "TrustClientMsg";
   804 
   805 
   806 
   807 (*** Protocol goal: if B receives ClientFinished, and if B is able to
   808      check a CertVerify from A, then A has used the quoted
   809      values PA, PB, etc.  Even this one requires A to be uncompromised.
   810  ***)
   811 goal thy
   812  "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   813 \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   814 \           certificate A KA : parts (spies evs);       \
   815 \           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
   816 \             : set evs;                                                  \
   817 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   818 \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   819 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   820                        addDs  [Says_imp_spies RS parts.Inj]) 1);
   821 qed "AuthClientFinished";
   822 
   823 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
   824 (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
   825 (*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
   826 (*30/9/97: loads in 476s, after removing unused theorems*)
   827 (*30/9/97: loads in 448s, after fixing ServerResume*)