src/HOL/Auth/Yahalom.thy
changeset 3481 256f38c01b98
parent 3465 e85c24717cad
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Tue Jul 01 17:37:42 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Tue Jul 01 17:38:49 1997 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5           (*Alice receives the Server's (?) message, checks her Nonce, and
     1.6             uses the new session key to send Bob his Nonce.*)
     1.7 -    YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
     1.8 +    YM4  "[| evs: yahalom lost;  A ~= Server;  
     1.9               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
    1.10                          X|}  : set evs;
    1.11               Says A B {|Agent A, Nonce NA|} : set evs |]