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