src/HOL/Auth/OtwayRees_AN.thy
changeset 3466 30791e5a69c4
parent 3465 e85c24717cad
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jun 26 13:20:50 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Jun 27 10:47:13 1997 +0200
     1.3 @@ -56,8 +56,7 @@
     1.4           (*Bob receives the Server's (?) message and compares the Nonces with
     1.5  	   those in the message he previously sent the Server.*)
     1.6      OR4  "[| evs: otway lost;  A ~= B;
     1.7 -             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
     1.8 -               : set evs;
     1.9 +             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
    1.10               Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    1.11                 : set evs |]
    1.12            ==> Says B A X # evs : otway lost"