src/HOL/Auth/TLS.thy

           ==> Says Spy B X # evs : tls"
 
     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)
 	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
 	   It is uninterpreted but will be confirmed in the FINISHED messages.

            and another MASTER SECRET is highly unlikely (even though
 	   both items have the same length, 48 bytes).
            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"
 
     CertVerify