src/HOL/Auth/TLS.thy
changeset 3683 aafe719dff14
parent 3677 f2569416d18b
child 3685 5b8c0c8f576e
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  
     1.5      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
     1.6           "[| evs: tls;  B ~= Spy;  
     1.7 -             X: synth (analz (sees Spy evs)) |]
     1.8 +             X: synth (analz (spies evs)) |]
     1.9            ==> Says Spy B X # evs : tls"
    1.10  
    1.11      SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)