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