src/HOL/Auth/TLS.ML
changeset 3772 6ee707a73248
parent 3760 77f71f650433
child 3919 c036caebfc75
--- a/src/HOL/Auth/TLS.ML	Thu Oct 02 22:54:00 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Fri Oct 03 10:32:50 1997 +0200
@@ -23,30 +23,8 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
-(** We mostly DO NOT unfold the definition of "certificate".  The attached
-    lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
-    contexts.
-**)
-
-goalw thy [certificate_def] 
-    "parts (insert (certificate B KB) H) =  \
-\    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
-by (rtac refl 1);
-qed "parts_insert_certificate";
-
-goalw thy [certificate_def] 
-    "analz (insert (certificate B KB) H) =  \
-\    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
-by (rtac refl 1);
-qed "analz_insert_certificate";
-Addsimps [parts_insert_certificate, analz_insert_certificate];
-
-goalw thy [certificate_def] 
-    "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
-by (Blast_tac 1);
-qed "eq_certificate_iff";
-AddIffs [eq_certificate_iff];
-
+(*Automatically unfold the definition of "certificate"*)
+Addsimps [certificate_def];
 
 (*Injectiveness of key-generating functions*)
 AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
@@ -75,15 +53,14 @@
 
 (**** Protocol Proofs ****)
 
-(*A "possibility property": there are traces that reach the end.
-  This protocol has three end points and six messages to consider.*)
+(*Possibility properties state that some traces run the protocol to the end.
+  Four paths and 12 rules are considered.*)
 
 
-(** These proofs make the further assumption that the Nonce_supply nonces 
+(** These proofs assume 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.
+    lie outside the range of PRF.  It seems reasonable, but as it is needed
+    only for the possibility theorems, it is not taken as an axiom.
 **)
 
 
@@ -202,15 +179,17 @@
   little point in doing so: the loss of their private keys is a worse
   breach of security.*)
 goalw thy [certificate_def]
- "!!evs. evs : tls ==> certificate B KB : parts (spies evs) --> KB = pubK B";
+ "!!evs. [| certificate B KB : parts (spies evs);  evs : tls |]  \
+\        ==> pubK B = KB";
+by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
-bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
+qed "certificate_valid";
 
 
 (*Replace key KB in ClientKeyExch by (pubK B) *)
 val ClientKeyExch_tac = 
-    forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
+    forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid]
     THEN' assume_tac
     THEN' hyp_subst_tac;
 
@@ -268,9 +247,9 @@
 
 (*B can check A's signature if he has received A's certificate.*)
 goal thy
- "!!evs. [| X : parts (spies evs);          \
-\           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});      \
-\           evs : tls;  A ~: bad |]                       \
+ "!!evs. [| X : parts (spies evs);                          \
+\           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});  \
+\           evs : tls;  A ~: bad |]                         \
 \    ==> Says A B X : set evs";
 by (etac rev_mp 1);
 by (hyp_subst_tac 1);
@@ -280,20 +259,20 @@
 
 (*Final version: B checks X using the distributed KA instead of priK A*)
 goal thy
- "!!evs. [| X : parts (spies evs);          \
-\           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});      \
-\           certificate A KA : parts (spies evs);       \
-\           evs : tls;  A ~: bad |]                       \
+ "!!evs. [| X : parts (spies evs);                            \
+\           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
+\           certificate A KA : parts (spies evs);             \
+\           evs : tls;  A ~: bad |]                           \
 \    ==> Says A B X : set evs";
-by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
+by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1);
 qed "TrustCertVerify";
 
 
 (*If CertVerify is present then A has chosen PMS.*)
 goal thy
- "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|})  \
-\             : parts (spies evs);                                \
-\           evs : tls;  A ~: bad |]                                      \
+ "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
+\             : parts (spies evs);                          \
+\           evs : tls;  A ~: bad |]                         \
 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
 be rev_mp 1;
 by (parts_induct_tac 1);
@@ -302,83 +281,15 @@
 
 (*Final version using the distributed KA instead of priK A*)
 goal thy
- "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})  \
-\             : parts (spies evs);                                \
-\           certificate A KA : parts (spies evs);       \
-\           evs : tls;  A ~: bad |]                                      \
+ "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
+\             : parts (spies evs);                             \
+\           certificate A KA : parts (spies evs);              \
+\           evs : tls;  A ~: bad |]                            \
 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
-by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
+by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1);
 qed "UseCertVerify";
 
 
-(*Key compromise lemma needed to prove analz_image_keys.
-  No collection of keys can help the spy get new private keys.*)
-goal thy  
- "!!evs. evs : tls ==>                                    \
-\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
-\          (priK B : KK | B : bad)";
-by (etac tls.induct 1);
-by (ALLGOALS
-    (asm_simp_tac (analz_image_keys_ss
-		   addsimps (analz_insert_certificate::keys_distinct))));
-(*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed_spec_mp "analz_image_priK";
-
-
-(*slightly speeds up the big simplification below*)
-goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
-by (Blast_tac 1);
-val range_sessionkeys_not_priK = result();
-
-(*Lemma for the trivial direction of the if-and-only-if*)
-goal thy  
- "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
-\        (X : analz (G Un H))  =  (X : analz H)";
-by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
-val lemma = result();
-
-(** It is a mystery to me why the following formulation is actually slower
-    in simplification:
-
-\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
-\           (Nonce N : analz (spies evs))";
-
-More so as it can take advantage of unconditional rewrites such as 
-     priK B ~: sessionK``Z
-**)
-
-goal thy  
- "!!evs. evs : tls ==>                                 \
-\    ALL KK. KK <= range sessionK -->           \
-\            (Nonce N : analz (Key``KK Un (spies evs))) = \
-\            (Nonce N : analz (spies evs))";
-by (etac tls.induct 1);
-by (ClientKeyExch_tac 7);
-by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac lemma));
-by (ALLGOALS    (*23 seconds*)
-    (asm_simp_tac (analz_image_keys_ss 
-		   addsimps [range_sessionkeys_not_priK, 
-			     analz_image_priK, analz_insert_certificate])));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
-(*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed_spec_mp "analz_image_keys";
-
-(*Knowing some session keys is no help in getting new nonces*)
-goal thy
- "!!evs. evs : tls ==>          \
-\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
-\        (Nonce N : analz (spies evs))";
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
-qed "analz_insert_key";
-Addsimps [analz_insert_key];
-
 goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
 by (parts_induct_tac 1);
 (*ClientKeyExch: PMS is assumed to differ from any PRF.*)
@@ -402,75 +313,6 @@
 
 
 
-(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
-
-(** Some lemmas about session keys, comprising clientK and serverK **)
-
-
-(*Lemma: session 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 ~: parts (spies evs);  \
-\           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
-\           evs : tls |]             \
-\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
-by (etac rev_mp 1);
-by (hyp_subst_tac 1);
-by (analz_induct_tac 1);
-(*SpyKeys*)
-by (blast_tac (!claset addSEs spies_partsEs) 3);
-(*Fake*)
-by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
-by (Fake_parts_insert_tac 2);
-(** LEVEL 6 **)
-(*Oops*)
-by (fast_tac (!claset addSEs [MPair_parts]
-		       addDs  [Says_imp_spies RS parts.Inj]
-		       addss (!simpset)) 6);
-by (REPEAT 
-    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
-				Notes_master_imp_Crypt_PMS]
-                        addSEs spies_partsEs) 1));
-val lemma = result();
-
-goal thy 
- "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
-\  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
-by (blast_tac (!claset addDs [lemma]) 1);
-qed "PMS_sessionK_not_spied";
-
-goal thy 
- "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
-\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
-by (blast_tac (!claset addDs [lemma]) 1);
-qed "PMS_Crypt_sessionK_not_spied";
-
-
-(*Lemma: 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!
-  The strong Oops condition can be weakened later by unicity reasoning, 
-	with some effort.*)
-goal thy 
- "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
-\           Nonce M ~: analz (spies evs);  evs : tls |]   \
-\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1);        (*17 seconds*)
-(*Oops*)
-by (Blast_tac 4);
-(*SpyKeys*)
-by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
-(*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed "sessionK_not_spied";
-Addsimps [sessionK_not_spied];
-
-
 (*** Unicity results for PMS, the pre-master-secret ***)
 
 (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
@@ -525,6 +367,144 @@
 
 
 
+(**** Secrecy Theorems ****)
+
+(*Key compromise lemma needed to prove analz_image_keys.
+  No collection of keys can help the spy get new private keys.*)
+goal thy  
+ "!!evs. evs : tls ==>                                      \
+\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
+\          (priK B : KK | B : bad)";
+by (etac tls.induct 1);
+by (ALLGOALS
+    (asm_simp_tac (analz_image_keys_ss
+		   addsimps (certificate_def::keys_distinct))));
+(*Fake*) 
+by (spy_analz_tac 2);
+(*Base*)
+by (Blast_tac 1);
+qed_spec_mp "analz_image_priK";
+
+
+(*slightly speeds up the big simplification below*)
+goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
+by (Blast_tac 1);
+val range_sessionkeys_not_priK = result();
+
+(*Lemma for the trivial direction of the if-and-only-if*)
+goal thy  
+ "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
+\        (X : analz (G Un H))  =  (X : analz H)";
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
+val lemma = result();
+
+(** Strangely, the following version doesn't work:
+\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
+\           (Nonce N : analz (spies evs))";
+**)
+
+goal thy  
+ "!!evs. evs : tls ==>                                    \
+\    ALL KK. KK <= range sessionK -->                     \
+\            (Nonce N : analz (Key``KK Un (spies evs))) = \
+\            (Nonce N : analz (spies evs))";
+by (etac tls.induct 1);
+by (ClientKeyExch_tac 7);
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac lemma));
+by (ALLGOALS    (*24 seconds*)
+    (asm_simp_tac (analz_image_keys_ss 
+		   addsimps [range_sessionkeys_not_priK, 
+                             analz_image_priK, certificate_def])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
+(*Fake*) 
+by (spy_analz_tac 2);
+(*Base*)
+by (Blast_tac 1);
+qed_spec_mp "analz_image_keys";
+
+(*Knowing some session keys is no help in getting new nonces*)
+goal thy
+ "!!evs. evs : tls ==>          \
+\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
+\        (Nonce N : analz (spies evs))";
+by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
+qed "analz_insert_key";
+Addsimps [analz_insert_key];
+
+
+(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
+
+(** Some lemmas about session keys, comprising clientK and serverK **)
+
+
+(*Lemma: session 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 ~: parts (spies evs);  \
+\           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
+\           evs : tls |]             \
+\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
+by (etac rev_mp 1);
+by (hyp_subst_tac 1);
+by (analz_induct_tac 1);
+(*SpyKeys*)
+by (blast_tac (!claset addSEs spies_partsEs) 3);
+(*Fake*)
+by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
+by (Fake_parts_insert_tac 2);
+(** LEVEL 6 **)
+(*Oops*)
+by (fast_tac (!claset addSEs [MPair_parts]
+		       addDs  [Says_imp_spies RS parts.Inj]
+		       addss (!simpset)) 6);
+by (REPEAT 
+    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
+				Notes_master_imp_Crypt_PMS]
+                        addSEs spies_partsEs) 1));
+val lemma = result();
+
+goal thy 
+ "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
+\  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
+by (blast_tac (!claset addDs [lemma]) 1);
+qed "PMS_sessionK_not_spied";
+bind_thm ("PMS_sessionK_spiedE", 
+	  PMS_sessionK_not_spied RSN (2,rev_notE));
+
+goal thy 
+ "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
+\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
+by (blast_tac (!claset addDs [lemma]) 1);
+qed "PMS_Crypt_sessionK_not_spied";
+bind_thm ("PMS_Crypt_sessionK_spiedE", 
+	  PMS_Crypt_sessionK_not_spied RSN (2,rev_notE));
+
+(*Lemma: 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!
+  The strong Oops condition can be weakened later by unicity reasoning, 
+	with some effort.*)
+goal thy 
+ "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
+\           Nonce M ~: analz (spies evs);  evs : tls |]   \
+\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (analz_induct_tac 1);        (*17 seconds*)
+(*Oops*)
+by (Blast_tac 4);
+(*SpyKeys*)
+by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
+(*Fake*) 
+by (spy_analz_tac 2);
+(*Base*)
+by (Blast_tac 1);
+qed "sessionK_not_spied";
+Addsimps [sessionK_not_spied];
+
+
 (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
 goal thy
  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
@@ -588,7 +568,7 @@
     (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
      	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
 (*ClientKeyExch*)
-by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
+by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE]
 	               addSDs [Says_imp_spies RS parts.Inj]) 1);
 bind_thm ("Says_clientK_unique",
 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
@@ -610,8 +590,7 @@
 (*Oops*)
 by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
 (*ClientKeyExch*)
-by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
-			       spies_partsEs)) 1);
+by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
 qed_spec_mp "clientK_Oops_ALL";
 
 
@@ -636,7 +615,7 @@
 				Notes_Crypt_parts_spies,
 				Crypt_unique_PMS]) 2));
 (*ClientKeyExch*)
-by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
+by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE]
 	               addSDs [Says_imp_spies RS parts.Inj]) 1);
 bind_thm ("Says_serverK_unique",
 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
@@ -657,8 +636,7 @@
 (*Oops*)
 by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
 (*ClientKeyExch*)
-by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
-			       spies_partsEs)) 1);
+by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
 qed_spec_mp "serverK_Oops_ALL";
 
 
@@ -670,16 +648,15 @@
 
 (*The mention of her name (A) in X assures A that B knows who she is.*)
 goal thy
- "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
-\           X = Crypt (serverK(Na,Nb,M))                  \
+ "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
 \                 (Hash{|Number SID, Nonce M,             \
 \                        Nonce Na, Number PA, Agent A,    \
 \                        Nonce Nb, Number PB, Agent B|}); \
 \           M = PRF(PMS,NA,NB);                           \
-\           evs : tls;  A ~: bad;  B ~: bad |]          \
-\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\        X : parts (spies evs) --> Says B A X : set evs";
-by (etac rev_mp 1);
+\           evs : tls;  A ~: bad;  B ~: bad |]            \
+\        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
+\            Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\            X : parts (spies evs) --> Says B A X : set evs";
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);        (*22 seconds*)
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -687,13 +664,13 @@
 by (ALLGOALS Clarify_tac);
 (*ClientKeyExch*)
 by (fast_tac  (*blast_tac gives PROOF FAILED*)
-    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
+    (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
 (*Fake: the Spy doesn't have the critical session key!*)
 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
-val lemma = normalize_thm [RSspec, RSmp] (result());
+val lemma = normalize_thm [RSmp] (result());
 
 (*Final version*)
 goal thy
@@ -719,13 +696,11 @@
   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   to bind A's identity with PMS, then we could replace A' by A below.*)
 goal thy
- "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
-\           evs : tls;  A ~: bad;  B ~: bad;                 \
-\           M = PRF(PMS,NA,NB) |]            \
-\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
+ "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |]     \
+\        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
+\            Notes A {|Agent B, Nonce PMS|} : set evs -->              \
 \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
-by (etac rev_mp 1);
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);	(*20 seconds*)
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -740,13 +715,13 @@
 				Crypt_unique_PMS]) 3));
 (*ClientKeyExch*)
 by (blast_tac
-    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
+    (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
 (*Fake: the Spy doesn't have the critical session key!*)
 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
-val lemma = normalize_thm [RSspec, RSmp] (result());
+val lemma = normalize_thm [RSmp] (result());
 
 (*Final version*)
 goal thy
@@ -758,7 +733,6 @@
 \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
 by (blast_tac (!claset addIs [lemma]
                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
-
 qed_spec_mp "TrustServerMsg";
 
 
@@ -770,11 +744,12 @@
 ***)
 
 goal thy
- "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
-\  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
-\      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
-\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
-\      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
+ "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |] \
+\    ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
+\        Notes A {|Agent B, Nonce PMS|} : set evs -->               \
+\        Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) -->         \
+\        Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
+by (hyp_subst_tac 1);
 by (analz_induct_tac 1);	(*15 seconds*)
 by (ALLGOALS Clarify_tac);
 (*ClientFinished, ClientResume: by unicity of PMS*)
@@ -783,24 +758,25 @@
 	 	               addDs  [Notes_unique_PMS]) 3));
 (*ClientKeyExch*)
 by (fast_tac  (*blast_tac gives PROOF FAILED*)
-    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
+    (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
 (*Fake: the Spy doesn't have the critical session key!*)
 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
-val lemma = normalize_thm [RSspec, RSmp] (result());
+val lemma = normalize_thm [RSmp] (result());
 
 (*Final version*)
 goal thy
- "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs);  \
+ "!!evs. [| M = PRF(PMS,NA,NB);                           \
+\           Crypt (clientK(Na,Nb,M)) Y : parts (spies evs);  \
 \           Notes A {|Agent B, Nonce PMS|} : set evs;        \
-\           Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;  \
+\           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;  \
 \           evs : tls;  A ~: bad;  B ~: bad |]                         \
-\  ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
+\  ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
 by (blast_tac (!claset addIs [lemma]
                        addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
-qed_spec_mp "TrustClientMsg";
+qed "TrustClientMsg";
 
 
 
@@ -809,13 +785,14 @@
      values PA, PB, etc.  Even this one requires A to be uncompromised.
  ***)
 goal thy
- "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
-\           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
+ "!!evs. [| M = PRF(PMS,NA,NB);                           \
+\           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
+\           Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
 \           certificate A KA : parts (spies evs);       \
 \           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
 \             : set evs;                                                  \
 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
-\     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
+\     ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
                        addDs  [Says_imp_spies RS parts.Inj]) 1);
 qed "AuthClientFinished";