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