# HG changeset patch
# User paulson
# Date 882281738 -3600
# Node ID 88639289be39298b5a13b2759e4f829b6813cda5
# Parent  16b92885de6bc1b9eb7c9cd815cadda6226cb53a
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson

diff -r 16b92885de6b -r 88639289be39 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Tue Dec 16 12:37:11 1997 +0100
+++ b/src/HOL/Auth/TLS.thy	Tue Dec 16 15:15:38 1997 +0100
@@ -89,8 +89,8 @@
     SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
          "[| evsSK: tls;
 	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
-          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
-			    Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
+          ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
+			   Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
 
     ClientHello
 	 (*(7.4.1.2)
@@ -129,8 +129,7 @@
            The Note event records in the trace that she knows PMS
                (see REMARK at top). *)
          "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
-             Says B'  A {|Nonce NB, Number SID, Number PB|} : set evsCX;
-             Says B'' A (certificate B KB) : set evsCX |]
+             Says B' A (certificate B KB) : set evsCX |]
           ==> Says A B (Crypt KB (Nonce PMS))
 	      # Notes A {|Agent B, Nonce PMS|}
 	      # evsCX  :  tls"