src/HOL/Auth/TLS.ML

 qed "eq_certificate_iff";
 AddIffs [eq_certificate_iff];
 
 
 (*Injectiveness of key-generating functions*)
-AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
+AddIffs [inj_PRF RS inj_eq, inj_clientK RS inj_eq, inj_serverK RS inj_eq];
 
 (* invKey(clientK x) = clientK x  and similarly for serverK*)
 Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
 	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
 

 (**** Protocol Proofs ****)
 
 (*A "possibility property": there are traces that reach the end.
   This protocol has three end points and six messages to consider.*)
 
+
+(** These proofs make the further assumption that the Nonce_supply nonces 
+	(which have the form  @ N. Nonce N ~: used evs)
+    lie outside the range of PRF.  This assumption seems reasonable, but
+    as it is needed only for the possibility theorems, it is not taken
+    as an axiom.
+**)
+
+
+
 (*Possibility property ending with ServerFinished.*)
 goal thy 
- "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
-\  Says B A (Crypt (serverK(NA,NB,M))                 \
-\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
-\                   Nonce NA, Agent XA, Agent A,      \
-\                   Nonce NB, Agent XB,               \
-\                   certificate B (pubK B)|})) \
+ "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
+\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
+\  Says B A (Crypt (serverK(NA,NB,M))                       \
+\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A,      \
+\                   Nonce NB, Number XB, Agent B|})) \
 \    : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
 	  RS tls.ServerFinished) 2);
 by possibility_tac;
+by (REPEAT (Blast_tac 1));
 result();
 
 (*And one for ClientFinished.  Either FINISHED message may come first.*)
 goal thy 
- "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.              \
+ "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
+\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
 \  Says A B (Crypt (clientK(NA,NB,M))                           \
-\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},        \
-\                   Nonce NA, Agent XA, certificate A (pubK A), \
-\                   Nonce NB, Agent XB, Agent B|})) : set evs";
+\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\                   Nonce NB, Number XB, Agent B|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
 	  RS tls.ClientFinished) 2);
 by possibility_tac;
+by (REPEAT (Blast_tac 1));
 result();
 
 (*Another one, for CertVerify (which is optional)*)
 goal thy 
- "!!A B. A ~= B ==> EX NB M. EX evs: tls.   \
+ "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
+\           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
 \  Says A B (Crypt (priK A)                 \
-\            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
+\            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
 	  RS tls.CertVerify) 2);
 by possibility_tac;
+by (REPEAT (Blast_tac 1));
 result();
 
 
 (**** Inductive proofs about tls ****)
 

     etac tls.induct i   THEN
     ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
     ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
     ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
     ALLGOALS (asm_simp_tac 
-              (!simpset addsimps [not_parts_not_analz]
+              (!simpset addcongs [if_weak_cong]
                         setloop split_tac [expand_if]))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
     ALLGOALS (asm_simp_tac 
-              (!simpset addsimps [insert_absorb]
+              (!simpset addcongs [if_weak_cong]
+			addsimps [insert_absorb]
                         setloop split_tac [expand_if]));
 
 
 (*** Hashing of nonces ***)
 
-(*Every Nonce that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees Spy evs);  \
-\                   evs : tls |]  \
-\                ==> Nonce N : parts (sees Spy evs)";
+(*Every Nonce that's hashed is already in past traffic.  
+  This event occurs in CERTIFICATE VERIFY*)
+goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs);  \
+\                   NB ~: range PRF;  evs : tls |]  \
+\                ==> Nonce NB : parts (sees Spy evs)";
+by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
 by (Fake_parts_insert_tac 1);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
-	               addSEs partsEs) 1);
-qed "Hash_imp_Nonce1";
-
-(*Lemma needed to prove Hash_Hash_imp_Nonce*)
-goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
-\                       : parts (sees Spy evs);     \
-\                   evs : tls |]  \
-\                ==> Nonce M : parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
-by (Fake_parts_insert_tac 1);
-qed "Hash_imp_Nonce2";
-AddSDs [Hash_imp_Nonce2];
+(*FINISHED messages are trivial because M : range PRF*)
+by (REPEAT (Blast_tac 2));
+(*CERTIFICATE VERIFY is the only interesting case*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+qed "Hash_Nonce_CV";
 
 
 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
 \                ==> Crypt (pubK B) X : parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 by (blast_tac (!claset addIs [parts_insertI]) 1);
 qed "Notes_Crypt_parts_sees";
 
 
-(*NEEDED??*)
-goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
-\                      : parts (sees Spy evs);      \
-\                   evs : tls |]                         \
-\                ==> Nonce M : parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
-by (Fake_parts_insert_tac 1);
-by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees,
-				       Says_imp_sees_Spy RS parts.Inj]
-		               addSEs partsEs) 1));
-qed "Hash_Hash_imp_Nonce";
-
-
-(*NEEDED??
-  Every Nonce that's hashed is already in past traffic. 
-  This general formulation is tricky to prove and hard to use, since the
-  2nd premise is typically proved by simplification.*)
-goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
-\                   Nonce N : parts {X};  evs : tls |]  \
-\                ==> Nonce N : parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
-			      Says_imp_sees_Spy RS parts.Inj]
-		      addSEs partsEs) 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
-by (Fake_parts_insert_tac 1);
-(*CertVerify, ClientFinished, ServerFinished (?)*)
-by (REPEAT (Blast_tac 1));
-qed "Hash_imp_Nonce_seen";
+(*****************
+    (*NEEDED?  TRUE???
+      Every Nonce that's hashed is already in past traffic. 
+      This general formulation is tricky to prove and hard to use, since the
+      2nd premise is typically proved by simplification.*)
+    goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
+    \                   Nonce N : parts {X};  evs : tls |]  \
+    \                ==> Nonce N : parts (sees Spy evs)";
+    by (etac rev_mp 1);
+    by (parts_induct_tac 1);
+    by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
+				  Says_imp_sees_Spy RS parts.Inj]
+			  addSEs partsEs) 1);
+    by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
+    by (Fake_parts_insert_tac 1);
+    (*CertVerify, ClientFinished, ServerFinished (?)*)
+    by (REPEAT (Blast_tac 1));
+    qed "Hash_imp_Nonce_seen";
+****************************************************************)
 
 
 (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
 
 (*B can check A's signature if he has received A's certificate.
   Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   assume A~:lost; otherwise, the Spy can forge A's signature.*)
 goal thy
  "!!evs. [| X = Crypt (priK A)                                        \
-\                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
+\                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
 \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
-\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
+\    ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
 \          : set evs --> \
 \        X : parts (sees Spy evs) --> Says A B X : set evs";
 by (hyp_subst_tac 1);
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*ServerHello: nonce NB cannot be in X because it's fresh!*)
-by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
+by (blast_tac (!claset addSDs [Hash_Nonce_CV]
 	               addSEs sees_Spy_partsEs) 1);
 qed_spec_mp "TrustCertVerify";
 
 
-(*If CERTIFICATE VERIFY is present then A has chosen M.*)
-goal thy
- "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})  \
+(*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
+goal thy
+ "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
 \             : parts (sees Spy evs);                                \
 \           evs : tls;  A ~: lost |]                                      \
-\        ==> Notes A {|Agent B, Nonce M|} : set evs";
+\        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
 be rev_mp 1;
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 qed "UseCertVerify";
 

 \            (Nonce N : analz (sees Spy evs))";
 by (etac tls.induct 1);
 by (ClientCertKeyEx_tac 6);
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac lemma));
-writeln"SLOW simplification: 50 secs!??";
+writeln"SLOW simplification: 60 secs!??";
 by (ALLGOALS
     (asm_simp_tac (analz_image_keys_ss 
-                   addsimps (analz_image_priK::certificate_def::
+		   addsimps (analz_image_priK::certificate_def::
                              keys_distinct))));
-by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
 (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
 by (Blast_tac 3);
 (*Fake*) 
 by (spy_analz_tac 2);
 (*Base*)
 by (Blast_tac 1);
 qed_spec_mp "analz_image_keys";
 
 
-(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*)
+goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
+by (parts_induct_tac 1);
+(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
+by (Blast_tac 1);
+qed "no_Notes_A_PRF";
+Addsimps [no_Notes_A_PRF];
+
+
+(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
 goal thy
  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
-\        ==> Notes A {|Agent B, Nonce M|} : set evs  -->   \
-\            Nonce M ~: analz (sees Spy evs)";
-by (analz_induct_tac 1);
+\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
+\            Nonce PMS ~: analz (sees Spy evs)";
+by (analz_induct_tac 1);   (*47 seconds???*)
 (*ClientHello*)
 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
                                addSEs sees_Spy_partsEs) 3);
 (*SpyKeys*)
 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
+by (fast_tac (!claset addss (!simpset)) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
 by (REPEAT (blast_tac (!claset addSEs partsEs
 			       addDs  [Notes_Crypt_parts_sees,
 				       impOfSubs analz_subset_parts,
 				       Says_imp_sees_Spy RS analz.Inj]) 1));
-bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
+bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
+
+
+
+goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs);  \
+\                   evs : tls |]  \
+\                ==> Nonce PMS : parts (sees Spy evs)";
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (Fake_parts_insert_tac 1);
+(*Client key exchange*)
+by (Blast_tac 4);
+(*Server Hello: by freshness*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+(*Client Hello: trivial*)
+by (Blast_tac 2);
+(*SpyKeys*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+qed "MS_imp_PMS";
+AddSDs [MS_imp_PMS];
+
+
+(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
+  will stay secret.*)
+goal thy
+ "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
+\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
+\            Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
+by (analz_induct_tac 1);   (*47 seconds???*)
+(*ClientHello*)
+by (Blast_tac 3);
+(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
+by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
+by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
+			       Says_imp_sees_Spy RS analz.Inj]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
+(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
+by (REPEAT (blast_tac (!claset addSEs partsEs
+			       addDs  [MS_imp_PMS,
+				       Notes_Crypt_parts_sees,
+				       impOfSubs analz_subset_parts,
+				       Says_imp_sees_Spy RS analz.Inj]) 1));
+bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
+
 
 
 (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
 
 (** First, some lemmas about those write keys.  The proofs for serverK are 
     nearly identical to those for clientK. **)
 
-(*Lemma: those write keys are never sent if M is secure.  
+(*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
   Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
 
 goal thy 
  "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
 \        ==> Key (clientK(NA,NB,M)) ~: parts (sees Spy evs)";

 (*Fake*) 
 by (spy_analz_tac 2);
 (*Base*)
 by (Blast_tac 1);
 qed "clientK_notin_parts";
-
+bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE));
 Addsimps [clientK_notin_parts];
-AddSEs [clientK_notin_parts RSN (2, rev_notE)];
+AddSEs [clientK_in_partsE, 
+	impOfSubs analz_subset_parts RS clientK_in_partsE];
 
 goal thy 
  "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
 \        ==> Key (serverK(NA,NB,M)) ~: parts (sees Spy evs)";
 by (etac rev_mp 1);

 (*Fake*) 
 by (spy_analz_tac 2);
 (*Base*)
 by (Blast_tac 1);
 qed "serverK_notin_parts";
-
+bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE));
 Addsimps [serverK_notin_parts];
-AddSEs [serverK_notin_parts RSN (2, rev_notE)];
-
-(*Lemma: those write keys are never used if M is fresh.  
-  Converse doesn't hold; betraying M doesn't force the keys to be sent!
-  NOT suitable as safe elim rules.*)
-
-goal thy 
- "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
-\        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees Spy evs)";
+AddSEs [serverK_in_partsE, 
+	impOfSubs analz_subset_parts RS serverK_in_partsE];
+
+
+(*Lemma: those write keys are never used if PMS is fresh.  
+  Nonces don't have to agree, allowing session resumption.
+  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
+  They are NOT suitable as safe elim rules.*)
+
+goal thy 
+ "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
+\  ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*ClientFinished: since M is fresh, a different instance of clientK was used.*)
 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
-                               addSEs sees_Spy_partsEs) 3);
+                       addSEs sees_Spy_partsEs) 3);
 by (Fake_parts_insert_tac 2);
 (*Base*)
 by (Blast_tac 1);
 qed "Crypt_clientK_notin_parts";
-
 Addsimps [Crypt_clientK_notin_parts];
 AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
 
 goal thy 
- "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
-\        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees Spy evs)";
+ "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
+\  ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*ServerFinished: since M is fresh, a different instance of serverK was used.*)
 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
                                addSEs sees_Spy_partsEs) 3);

 be rev_mp 1;
 by (analz_induct_tac 1);
 qed "A_Crypt_pubB";
 
 
-(*** Unicity results for M, the pre-master-secret ***)
-
-(*M determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
-goal thy 
- "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
+(*** Unicity results for PMS, the pre-master-secret ***)
+
+(*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
+goal thy 
+ "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]   \
 \        ==> EX B'. ALL B.   \
-\              Crypt (pubK B) (Nonce M) : parts (sees Spy evs) --> B=B'";
+\              Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*ClientCertKeyEx*)
 by (ClientCertKeyEx_tac 1);
 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
-by (expand_case_tac "M = ?y" 1 THEN
+by (expand_case_tac "PMS = ?y" 1 THEN
     blast_tac (!claset addSEs partsEs) 1);
 val lemma = result();
 
 goal thy 
- "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees Spy evs); \
-\           Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \
-\           Nonce M ~: analz (sees Spy evs);                 \
+ "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (sees Spy evs); \
+\           Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \
+\           Nonce PMS ~: analz (sees Spy evs);                 \
 \           evs : tls |]                                          \
 \        ==> B=B'";
 by (prove_unique_tac lemma 1);
-qed "unique_M";
-
-
-(*In A's note to herself, M determines A and B.*)
-goal thy 
- "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]            \
+qed "unique_PMS";
+
+
+(*In A's note to herself, PMS determines A and B.*)
+goal thy 
+ "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]            \
 \ ==> EX A' B'. ALL A B.                                                   \
-\        Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
+\        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
-(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
-by (expand_case_tac "M = ?y" 1 THEN
+(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
+by (expand_case_tac "PMS = ?y" 1 THEN
     blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
 val lemma = result();
 
 goal thy 
- "!!evs. [| Notes A  {|Agent B,  Nonce M|} : set evs;  \
-\           Notes A' {|Agent B', Nonce M|} : set evs;  \
-\           Nonce M ~: analz (sees Spy evs);      \
+ "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
+\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
+\           Nonce PMS ~: analz (sees Spy evs);      \
 \           evs : tls |]                               \
 \        ==> A=A' & B=B'";
 by (prove_unique_tac lemma 1);
-qed "Notes_unique_M";
+qed "Notes_unique_PMS";
 
 
 
 (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
      and has used the quoted values XA, XB, etc.  Note that it is up to A
      to compare XA with what she originally sent.
 ***)
 
 (*The mention of her name (A) in X assumes A that B knows who she is.*)
 goal thy
- "!!evs. [| X = Crypt (serverK(NA,NB,M))                                \
-\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},           \
-\                        Nonce NA, Agent XA, Agent A,                   \
-\                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
+ "!!evs. [| X = Crypt (serverK(Na,Nb,M))                                \
+\                 (Hash{|Nonce M, Nonce NA, Number XA, Agent A,         \
+\                        Nonce NB, Number XB, Agent B|}); \
+\           M = PRF(PMS,NA,NB); \
 \           evs : tls;  A ~: lost;  B ~: lost |]                        \
-\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                 \
+\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                 \
 \        X : parts (sees Spy evs) --> Says B A X : set evs";
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);
-by (REPEAT_FIRST (rtac impI));
 (*Fake: the Spy doesn't have the critical session key!*)
 by (REPEAT (rtac impI 1));
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
+by (subgoal_tac 
+    "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 qed_spec_mp "TrustServerFinished";
 
 
 (*This version refers not to SERVER FINISHED but to any message from B.
   We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   have changed A's identity in all other messages, so we can't be sure
   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
-  to bind A's identify with M, then we could replace A' by A below.*)
-goal thy
- "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                     \
-\        ==> Notes A {|Agent B, Nonce M|} : set evs -->              \
-\            Crypt (serverK(NA,NB,M)) Y : parts (sees Spy evs)  -->  \
-\            (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
+  to bind A's identity with M, then we could replace A' by A below.*)
+goal thy
+ "!!evs. [| evs : tls;  A ~: lost;  B ~: lost;                 \
+\           M = PRF(PMS,NA,NB) |]            \
+\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
+\            Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs)  -->  \
+\            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
+by (hyp_subst_tac 1);
 by (analz_induct_tac 1);
 by (REPEAT_FIRST (rtac impI));
 (*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
+by (subgoal_tac 
+    "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 (*ServerFinished.  If the message is old then apply induction hypothesis...*)
 by (rtac conjI 1 THEN Blast_tac 2);
-(*...otherwise delete induction hyp and use unicity of M.*)
+(*...otherwise delete induction hyp and use unicity of PMS.*)
 by (thin_tac "?PP-->?QQ" 1);
 by (Step_tac 1);
-by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
+by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
 by (blast_tac (!claset addSEs [MPair_parts]
 		       addDs  [Notes_Crypt_parts_sees,
 			       Says_imp_sees_Spy RS parts.Inj,
-			       unique_M]) 1);
+			       unique_PMS]) 1);
 qed_spec_mp "TrustServerMsg";
 
 
 (*** Protocol goal: if B receives any message encrypted with clientK
-     then A has sent it, ASSUMING that A chose M.  Authentication is
+     then A has sent it, ASSUMING that A chose PMS.  Authentication is
      assumed here; B cannot verify it.  But if the message is
      CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
 ***)
 goal thy
  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
-\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
-\            Crypt (clientK(NA,NB,M)) Y : parts (sees Spy evs) -->  \
-\            Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
+\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
+\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) -->  \
+\      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
 by (analz_induct_tac 1);
 by (REPEAT_FIRST (rtac impI));
 (*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
+by (subgoal_tac 
+    "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 (*ClientFinished.  If the message is old then apply induction hypothesis...*)
 by (step_tac (!claset delrules [conjI]) 1);
-by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
+by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
 by (blast_tac (!claset addSEs [MPair_parts]
-		       addDs  [Notes_unique_M]) 1);
+		       addDs  [Notes_unique_PMS]) 1);
 qed_spec_mp "TrustClientMsg";
 
 
 (*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
      check a CERTIFICATE VERIFY from A, then A has used the quoted
      values XA, XB, etc.  Even this one requires A to be uncompromised.
  ***)
 goal thy
- "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs;             \
-\           Says B  A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
+ "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
+\           Says B  A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
 \             : set evs;                                                  \
 \           Says A'' B (Crypt (priK A)                                    \
-\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))    \
+\                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
 \             : set evs;                                                  \
 \        evs : tls;  A ~: lost;  B ~: lost |]                             \
-\     ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
+\     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed "AuthClientFinished";