src/HOL/Auth/TLS.ML
author paulson
Fri Jul 11 13:30:01 1997 +0200 (1997-07-11)
changeset 3515 d8a71f6eaf40
parent 3506 a36e0a49d2cd
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Now uses the Notes constructor to distinguish the Client (who has chosen M)
from the Spy (who may have replayed her messages)
     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 CERTIFICATE VERIFY knows that A is present (But this
    11     message is optional!)
    12 
    13 * A upon receiving SERVER FINISHED 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 XA and XB (thus foiling
    17   rollback attacks).
    18 *)
    19 
    20 open TLS;
    21 
    22 proof_timing:=true;
    23 HOL_quantifiers := false;
    24 
    25 AddIffs [Spy_in_lost, Server_not_lost];
    26 Addsimps [certificate_def];
    27 
    28 goal thy "!!A. A ~: lost ==> A ~= Spy";
    29 by (Blast_tac 1);
    30 qed "not_lost_not_eq_Spy";
    31 Addsimps [not_lost_not_eq_Spy];
    32 
    33 (*Injectiveness of key-generating functions*)
    34 AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
    35 
    36 (* invKey(clientK x) = clientK x  and similarly for serverK*)
    37 Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    38 	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
    39 
    40 
    41 (*Replacing the variable by a constant improves search speed by 50%!*)
    42 val Says_imp_sees_Spy' = 
    43     read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    44 
    45 
    46 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    47 
    48 goal thy "pubK A ~= clientK arg";
    49 br notI 1;
    50 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    51 by (Full_simp_tac 1);
    52 qed "pubK_neq_clientK";
    53 
    54 goal thy "pubK A ~= serverK arg";
    55 br notI 1;
    56 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    57 by (Full_simp_tac 1);
    58 qed "pubK_neq_serverK";
    59 
    60 goal thy "priK A ~= clientK arg";
    61 br notI 1;
    62 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    63 by (Full_simp_tac 1);
    64 qed "priK_neq_clientK";
    65 
    66 goal thy "priK A ~= serverK 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_serverK";
    71 
    72 (*clientK and serverK have disjoint ranges*)
    73 goal thy "clientK arg ~= serverK arg'";
    74 by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
    75 by (Blast_tac 1);
    76 qed "clientK_neq_serverK";
    77 
    78 val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, 
    79 		     priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    80 AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    81 
    82 
    83 (**** Protocol Proofs ****)
    84 
    85 (*A "possibility property": there are traces that reach the end.
    86   This protocol has three end points and six messages to consider.*)
    87 
    88 (*Possibility property ending with ServerFinished.*)
    89 goal thy 
    90  "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
    91 \  Says B A (Crypt (serverK(NA,NB,M))                 \
    92 \            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
    93 \                   Nonce NA, Agent XA, Agent A,      \
    94 \                   Nonce NB, Agent XB,               \
    95 \                   certificate B (pubK B)|})) \
    96 \    : set evs";
    97 by (REPEAT (resolve_tac [exI,bexI] 1));
    98 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    99 	  RS tls.ServerFinished) 2);
   100 by possibility_tac;
   101 result();
   102 
   103 (*And one for ClientFinished.  Either FINISHED message may come first.*)
   104 goal thy 
   105  "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
   106 \  Says A B (Crypt (clientK(NA,NB,M))                 \
   107 \            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
   108 \                   Nonce NA, Agent XA,               \
   109 \                   certificate A (pubK A),      \
   110 \                   Nonce NB, Agent XB, Agent B|})) : set evs";
   111 by (REPEAT (resolve_tac [exI,bexI] 1));
   112 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   113 	  RS tls.ClientFinished) 2);
   114 by possibility_tac;
   115 result();
   116 
   117 (*Another one, for CertVerify (which is optional)*)
   118 goal thy 
   119  "!!A B. A ~= B ==> EX NB M. EX evs: tls.     \
   120 \  Says A B (Crypt (priK A)                 \
   121 \            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
   122 by (REPEAT (resolve_tac [exI,bexI] 1));
   123 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   124 	  RS tls.CertVerify) 2);
   125 by possibility_tac;
   126 result();
   127 
   128 
   129 (**** Inductive proofs about tls ****)
   130 
   131 (*Nobody sends themselves messages*)
   132 goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   133 by (etac tls.induct 1);
   134 by (Auto_tac());
   135 qed_spec_mp "not_Says_to_self";
   136 Addsimps [not_Says_to_self];
   137 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   138 
   139 
   140 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   141     sends messages containing X! **)
   142 
   143 (*Spy never sees another agent's private key! (unless it's lost at start)*)
   144 goal thy 
   145  "!!evs. evs : tls \
   146 \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
   147 by (etac tls.induct 1);
   148 by (prove_simple_subgoals_tac 1);
   149 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2);
   150 by (Fake_parts_insert_tac 1);
   151 qed "Spy_see_priK";
   152 Addsimps [Spy_see_priK];
   153 
   154 goal thy 
   155  "!!evs. evs : tls \
   156 \        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
   157 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   158 qed "Spy_analz_priK";
   159 Addsimps [Spy_analz_priK];
   160 
   161 goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
   162 \                  evs : tls |] ==> A:lost";
   163 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
   164 qed "Spy_see_priK_D";
   165 
   166 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
   167 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
   168 
   169 
   170 (*This lemma says that no false certificates exist.  One might extend the
   171   model to include bogus certificates for the lost agents, but there seems
   172   little point in doing so: the loss of their private keys is a worse
   173   breach of security.*)
   174 goalw thy [certificate_def]
   175  "!!evs. evs : tls     \
   176 \        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
   177 by (etac tls.induct 1);
   178 by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
   179 by (Fake_parts_insert_tac 2);
   180 by (Blast_tac 1);
   181 bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   182 
   183 
   184 (*Replace key KB in ClientCertKeyEx by (pubK B) *)
   185 val ClientCertKeyEx_tac = 
   186     forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
   187 		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
   188     THEN' assume_tac
   189     THEN' hyp_subst_tac;
   190 
   191 fun analz_induct_tac i = 
   192     etac tls.induct i   THEN
   193     ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
   194     ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
   195     ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
   196     rewrite_goals_tac  [certificate_def]  THEN
   197     ALLGOALS (asm_simp_tac 
   198               (!simpset addsimps [not_parts_not_analz]
   199                         setloop split_tac [expand_if]))  THEN
   200     (*Remove instances of pubK B:  the Spy already knows all public keys.
   201       Combining the two simplifier calls makes them run extremely slowly.*)
   202     ALLGOALS (asm_simp_tac 
   203               (!simpset addsimps [insert_absorb]
   204                         setloop split_tac [expand_if]));
   205 
   206 
   207 (*** Hashing of nonces ***)
   208 
   209 (*Every Nonce that's hashed is already in past traffic. *)
   210 goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
   211 \                   evs : tls |]  \
   212 \                ==> Nonce N : parts (sees lost Spy evs)";
   213 by (etac rev_mp 1);
   214 by (etac tls.induct 1);
   215 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
   216 			             setloop split_tac [expand_if])));
   217 by (Fake_parts_insert_tac 2);
   218 by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   219 		               addSEs partsEs) 1));
   220 qed "Hash_imp_Nonce1";
   221 
   222 (*Lemma needed to prove Hash_Hash_imp_Nonce*)
   223 goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
   224 \                       : parts (sees lost Spy evs);     \
   225 \                   evs : tls |]  \
   226 \                ==> Nonce M : parts (sees lost Spy evs)";
   227 by (etac rev_mp 1);
   228 by (etac tls.induct 1);
   229 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
   230 			             setloop split_tac [expand_if])));
   231 by (Fake_parts_insert_tac 2);
   232 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   233 		       addSEs partsEs) 1);
   234 qed "Hash_imp_Nonce2";
   235 AddSDs [Hash_imp_Nonce2];
   236 
   237 
   238 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   239 \                ==> Crypt (pubK B) X : parts (sees lost Spy evs)";
   240 by (etac rev_mp 1);
   241 by (analz_induct_tac 1);
   242 by (blast_tac (!claset addIs [parts_insertI]) 1);
   243 qed "Notes_Crypt_parts_sees";
   244 
   245 
   246 (*NEEDED??*)
   247 goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
   248 \                      : parts (sees lost Spy evs);      \
   249 \                   evs : tls |]                         \
   250 \                ==> Nonce M : parts (sees lost Spy evs)";
   251 by (etac rev_mp 1);
   252 by (etac tls.induct 1);
   253 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
   254 			             setloop split_tac [expand_if])));
   255 by (Fake_parts_insert_tac 2);
   256 by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   257 			      Says_imp_sees_Spy' RS parts.Inj]
   258 		      addSEs partsEs) 1);
   259 qed "Hash_Hash_imp_Nonce";
   260 
   261 
   262 (*NEEDED??
   263   Every Nonce that's hashed is already in past traffic. 
   264   This general formulation is tricky to prove and hard to use, since the
   265   2nd premise is typically proved by simplification.*)
   266 goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
   267 \                   Nonce N : parts {X};  evs : tls |]  \
   268 \                ==> Nonce N : parts (sees lost Spy evs)";
   269 by (etac rev_mp 1);
   270 by (etac tls.induct 1);
   271 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   272 by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   273 			      Says_imp_sees_Spy' RS parts.Inj]
   274 		      addSEs partsEs) 1);
   275 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   276 by (Fake_parts_insert_tac 1);
   277 (*CertVerify, ClientFinished, ServerFinished (?)*)
   278 by (REPEAT (Blast_tac 1));
   279 qed "Hash_imp_Nonce_seen";
   280 
   281 
   282 (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   283 
   284 (*B can check A's signature if he has received A's certificate.
   285   Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   286   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   287   assume A~:lost; otherwise, the Spy can forge A's signature.*)
   288 goalw thy [certificate_def]
   289  "!!evs. [| X = Crypt (priK A)                                        \
   290 \                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
   291 \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
   292 \    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   293 \          : set evs --> \
   294 \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
   295 by (hyp_subst_tac 1);
   296 by (etac tls.induct 1);
   297 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   298 by (Fake_parts_insert_tac 1);
   299 (*ServerHello: nonce NB cannot be in X because it's fresh!*)
   300 by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
   301 	               addSEs sees_Spy_partsEs) 1);
   302 qed_spec_mp "TrustCertVerify";
   303 
   304 
   305 (*If CERTIFICATE VERIFY is present then A has chosen M.*)
   306 goal thy
   307  "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})  \
   308 \             : parts (sees lost Spy evs);                                \
   309 \           evs : tls;  A ~: lost |]                                      \
   310 \        ==> Notes A {|Agent B, Nonce M|} : set evs";
   311 be rev_mp 1;
   312 by (etac tls.induct 1);
   313 by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
   314 by (Fake_parts_insert_tac 2);
   315 by (Blast_tac 1);
   316 qed "UseCertVerify";
   317 
   318 
   319 (*No collection of keys can help the spy get new private keys*)
   320 goal thy  
   321  "!!evs. evs : tls ==>                                    \
   322 \  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
   323 \            (priK B : KK | B : lost)";
   324 by (etac tls.induct 1);
   325 by (ALLGOALS
   326     (asm_simp_tac (analz_image_keys_ss 
   327 		   addsimps (certificate_def::keys_distinct))));
   328 (*Fake*) 
   329 by (spy_analz_tac 2);
   330 (*Base*)
   331 by (Blast_tac 1);
   332 qed_spec_mp "analz_image_priK";
   333 
   334 
   335 (*Lemma for the trivial direction of the if-and-only-if*)
   336 goal thy  
   337  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   338 \        (X : analz (G Un H))  =  (X : analz H)";
   339 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   340 val lemma = result();
   341 
   342 (*Knowing some clientKs and serverKs is no help in getting new nonces*)
   343 goal thy  
   344  "!!evs. evs : tls ==>                                 \
   345 \    ALL KK. KK <= (range clientK Un range serverK) -->           \
   346 \            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
   347 \            (Nonce N : analz (sees lost Spy evs))";
   348 by (etac tls.induct 1);
   349 by (ClientCertKeyEx_tac 6);
   350 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   351 by (REPEAT_FIRST (rtac lemma));
   352 writeln"SLOW simplification: 50 secs!??";
   353 by (ALLGOALS
   354     (asm_simp_tac (analz_image_keys_ss 
   355 		   addsimps (analz_image_priK::certificate_def::
   356 			     keys_distinct))));
   357 by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
   358 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   359 (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
   360 by (Blast_tac 3);
   361 (*Fake*) 
   362 by (spy_analz_tac 2);
   363 (*Base*)
   364 by (Blast_tac 1);
   365 qed_spec_mp "analz_image_keys";
   366 
   367 
   368 (*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*)
   369 goal thy
   370  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   371 \        ==> Notes A {|Agent B, Nonce M|} : set evs  -->   \
   372 \            Nonce M ~: analz (sees lost Spy evs)";
   373 by (analz_induct_tac 1);
   374 (*ClientHello*)
   375 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   376                                addSEs sees_Spy_partsEs) 3);
   377 (*SpyKeys*)
   378 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   379 (*Fake*)
   380 by (spy_analz_tac 1);
   381 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   382 by (REPEAT (blast_tac (!claset addSEs partsEs
   383 			       addDs  [Notes_Crypt_parts_sees,
   384 				       impOfSubs analz_subset_parts,
   385 				       Says_imp_sees_Spy' RS analz.Inj]) 1));
   386 bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
   387 
   388 
   389 (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   390 
   391 (** First, some lemmas about those write keys.  The proofs for serverK are 
   392     nearly identical to those for clientK. **)
   393 
   394 (*Lemma: those write keys are never sent if M is secure.  
   395   Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   396 
   397 goal thy 
   398  "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
   399 \        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   400 by (etac rev_mp 1);
   401 by (analz_induct_tac 1);
   402 (*SpyKeys*)
   403 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   404 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
   405 (*Fake*) 
   406 by (spy_analz_tac 2);
   407 (*Base*)
   408 by (Blast_tac 1);
   409 qed "clientK_notin_parts";
   410 
   411 Addsimps [clientK_notin_parts];
   412 AddSEs [clientK_notin_parts RSN (2, rev_notE)];
   413 
   414 goal thy 
   415  "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
   416 \        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   417 by (etac rev_mp 1);
   418 by (analz_induct_tac 1);
   419 (*SpyKeys*)
   420 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   421 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
   422 (*Fake*) 
   423 by (spy_analz_tac 2);
   424 (*Base*)
   425 by (Blast_tac 1);
   426 qed "serverK_notin_parts";
   427 
   428 Addsimps [serverK_notin_parts];
   429 AddSEs [serverK_notin_parts RSN (2, rev_notE)];
   430 
   431 (*Lemma: those write keys are never used if M is fresh.  
   432   Converse doesn't hold; betraying M doesn't force the keys to be sent!
   433   NOT suitable as safe elim rules.*)
   434 
   435 goal thy 
   436  "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
   437 \        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
   438 by (etac rev_mp 1);
   439 by (analz_induct_tac 1);
   440 (*ClientFinished: since M is fresh, a different instance of clientK was used.*)
   441 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   442                                addSEs sees_Spy_partsEs) 3);
   443 by (Fake_parts_insert_tac 2);
   444 (*Base*)
   445 by (Blast_tac 1);
   446 qed "Crypt_clientK_notin_parts";
   447 
   448 Addsimps [Crypt_clientK_notin_parts];
   449 AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
   450 
   451 goal thy 
   452  "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
   453 \        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
   454 by (etac rev_mp 1);
   455 by (analz_induct_tac 1);
   456 (*ServerFinished: since M is fresh, a different instance of serverK was used.*)
   457 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   458                                addSEs sees_Spy_partsEs) 3);
   459 by (Fake_parts_insert_tac 2);
   460 (*Base*)
   461 by (Blast_tac 1);
   462 qed "Crypt_serverK_notin_parts";
   463 
   464 Addsimps [Crypt_serverK_notin_parts];
   465 AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
   466 
   467 
   468 (*Weakening A~:lost to A~=Spy would complicate later uses of the rule*)
   469 goal thy
   470  "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
   471 \           A ~: lost;  evs : tls |] ==> KB = pubK B";
   472 be rev_mp 1;
   473 by (analz_induct_tac 1);
   474 qed "A_Crypt_pubB";
   475 
   476 
   477 (*** Unicity results for M, the pre-master-secret ***)
   478 
   479 (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   480   It simplifies the proof by discarding needless information about
   481 	analz (insert X (sees lost Spy evs)) 
   482 *)
   483 fun analz_mono_parts_induct_tac i = 
   484     etac tls.induct i           THEN 
   485     ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
   486     REPEAT_FIRST analz_mono_contra_tac;
   487 
   488 
   489 (*M determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   490 goal thy 
   491  "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
   492 \        ==> EX B'. ALL B.   \
   493 \              Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'";
   494 by (etac rev_mp 1);
   495 by (analz_mono_parts_induct_tac 1);
   496 by (prove_simple_subgoals_tac 1);
   497 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]
   498                            setloop split_tac [expand_if]) 2);
   499 (*ClientCertKeyEx*)
   500 by (expand_case_tac "M = ?y" 2 THEN
   501     REPEAT (blast_tac (!claset addSEs partsEs) 2));
   502 by (Fake_parts_insert_tac 1);
   503 val lemma = result();
   504 
   505 goal thy 
   506  "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees lost Spy evs); \
   507 \           Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \
   508 \           Nonce M ~: analz (sees lost Spy evs);                 \
   509 \           evs : tls |]                                          \
   510 \        ==> B=B'";
   511 by (prove_unique_tac lemma 1);
   512 qed "unique_M";
   513 
   514 
   515 (*In A's note to herself, M determines A and B.*)
   516 goal thy 
   517  "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]            \
   518 \ ==> EX A' B'. ALL A B.                                                   \
   519 \        Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
   520 by (etac rev_mp 1);
   521 by (analz_mono_parts_induct_tac 1);
   522 by (prove_simple_subgoals_tac 1);
   523 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   524 (*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
   525 by (expand_case_tac "M = ?y" 1 THEN
   526     blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
   527 val lemma = result();
   528 
   529 goal thy 
   530  "!!evs. [| Notes A  {|Agent B,  Nonce M|} : set evs;  \
   531 \           Notes A' {|Agent B', Nonce M|} : set evs;  \
   532 \           Nonce M ~: analz (sees lost Spy evs);      \
   533 \           evs : tls |]                               \
   534 \        ==> A=A' & B=B'";
   535 by (prove_unique_tac lemma 1);
   536 qed "Notes_unique_M";
   537 
   538 
   539 
   540 (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   541      and has used the quoted values XA, XB, etc.  Note that it is up to A
   542      to compare XA with what she originally sent.
   543 ***)
   544 
   545 (*The mention of her name (A) in X assumes A that B knows who she is.*)
   546 goal thy
   547  "!!evs. [| X = Crypt (serverK(NA,NB,M))                                \
   548 \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},           \
   549 \                        Nonce NA, Agent XA, Agent A,                   \
   550 \                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
   551 \           evs : tls;  A ~: lost;  B ~: lost |]                        \
   552 \        ==> Notes A {|Agent B, Nonce M|} : set evs -->                 \
   553 \        X : parts (sees lost Spy evs) --> Says B A X : set evs";
   554 by (hyp_subst_tac 1);
   555 by (analz_induct_tac 1);
   556 by (REPEAT_FIRST (rtac impI));
   557 (*Fake: the Spy doesn't have the critical session key!*)
   558 by (REPEAT (rtac impI 1));
   559 by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   560 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   561 				     not_parts_not_analz]) 2);
   562 by (Fake_parts_insert_tac 1);
   563 qed_spec_mp "TrustServerFinished";
   564 
   565 
   566 (*This version refers not to SERVER FINISHED but to any message from B.
   567   We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   568   have changed A's identity in all other messages, so we can't be sure
   569   that B sends his message to A.*)
   570 goal thy
   571  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
   572 \        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
   573 \            Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs)  --> \
   574 \            (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
   575 by (analz_induct_tac 1);
   576 by (REPEAT_FIRST (rtac impI));
   577 (*Fake: the Spy doesn't have the critical session key!*)
   578 by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   579 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   580 				     not_parts_not_analz]) 2);
   581 by (Fake_parts_insert_tac 1);
   582 (*ServerFinished.  If the message is old then apply induction hypothesis...*)
   583 by (rtac conjI 1 THEN Blast_tac 2);
   584 (*...otherwise delete induction hyp and use unicity of M.*)
   585 by (thin_tac "?PP-->?QQ" 1);
   586 by (Step_tac 1);
   587 by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
   588 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
   589 by (blast_tac (!claset addSEs [MPair_parts]
   590 		       addDs  [Notes_Crypt_parts_sees,
   591 			       Says_imp_sees_Spy' RS parts.Inj,
   592 			       unique_M]) 1);
   593 qed_spec_mp "TrustServerMsg";
   594 
   595 
   596 (*** Protocol goal: if B receives any message encrypted with clientK
   597      then A has sent it, ASSUMING that A chose M.  Authentication is
   598      assumed here; B cannot verify it.  But if the message is
   599      CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
   600 ***)
   601 goal thy
   602  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
   603 \        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
   604 \            Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) -->  \
   605 \            Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
   606 by (analz_induct_tac 1);
   607 by (REPEAT_FIRST (rtac impI));
   608 (*Fake: the Spy doesn't have the critical session key!*)
   609 by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   610 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   611 				     not_parts_not_analz]) 2);
   612 by (Fake_parts_insert_tac 1);
   613 (*ClientFinished.  If the message is old then apply induction hypothesis...*)
   614 by (step_tac (!claset delrules [conjI]) 1);
   615 by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
   616 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
   617 by (blast_tac (!claset addSEs [MPair_parts]
   618 		       addDs  [Notes_unique_M]) 1);
   619 qed_spec_mp "TrustClientMsg";
   620 
   621 
   622 (*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
   623      check a CERTIFICATE VERIFY from A, then A has used the quoted
   624      values XA, XB, etc.  Even this one requires A to be uncompromised.
   625  ***)
   626 goal thy
   627  "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs;             \
   628 \           Says B  A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   629 \             : set evs;                                                  \
   630 \           Says A'' B (Crypt (priK A)                                    \
   631 \                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))    \
   632 \             : set evs;                                                  \
   633 \        evs : tls;  A ~: lost;  B ~: lost |]                             \
   634 \     ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
   635 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   636                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   637 qed "AuthClientFinished";