src/HOL/Auth/TLS.thy

   PRF  :: "nat*nat*nat => nat"
 
   (*Client, server write keys generated uniformly by function sessionK
     to avoid duplicating their properties.
     Theyimplicitly include the MAC secrets.*)
-  sessionK :: "bool*nat*nat*nat => key"
+  sessionK :: "(nat*nat*nat)*bool => key"
 
   certificate      :: "[agent,key] => msg"
 
 defs
   certificate_def

 
 syntax
     clientK, serverK :: "nat*nat*nat => key"
 
 translations
-  "clientK (x)"	== "sessionK(True,x)"
-  "serverK (x)"	== "sessionK(False,x)"
+  "clientK (x)"	== "sessionK(x,True)"
+  "serverK (x)"	== "sessionK(x,False)"
 
 rules
   inj_PRF       "inj PRF"	
 
   (*sessionK is collision-free and makes symmetric keys*)

 			(Hash{|Nonce M, Number SID,
 			       Nonce NA, Number XA, Agent A, 
 			       Nonce NB, Number XB, Agent B|}))
               # evsCR  :  tls"
 
-  (**Oops message??**)
+    Oops 
+         (*The most plausible compromise is of an old session key.  Losing
+           the MASTER SECRET or PREMASTER SECRET is more serious but
+           rather unlikely.*)
+         "[| evso: tls;  A ~= Spy;  
+	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
+          ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
 
 end