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