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