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