src/HOL/Auth/TLS.thy
changeset 5359 bd539b72d484
parent 5074 753d4daff1df
child 5434 9b4bed3f394c
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Aug 21 15:56:12 1998 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Aug 21 16:14:34 1998 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  
     1.5      SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
     1.6           "[| evsSK: tls;
     1.7 -	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
     1.8 +	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
     1.9            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
    1.10  			   Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
    1.11