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