src/HOL/Auth/NS_Shared.thy
changeset 2131 3106a99d30a5
parent 2069 a1c623f70407
child 2284 80ebd1a213fd
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Sun Oct 27 13:47:02 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Mon Oct 28 12:55:24 1996 +0100
     1.3 @@ -67,10 +67,11 @@
     1.4            ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
     1.5    
     1.6           (*This message models possible leaks of session keys.
     1.7 -           The two Nonces identify the protocol run.*)
     1.8 -    Revl "[| evs: ns_shared lost;  A ~= Spy;
     1.9 -             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    1.10 -             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    1.11 +           The two Nonces identify the protocol run: the rule insists upon
    1.12 +           the true senders in order to make them accurate.*)
    1.13 +    Oops "[| evs: ns_shared lost;  A ~= Spy;
    1.14 +             Says B A (Crypt (Nonce NB) K) : set_of_list evs;
    1.15 +             Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    1.16                 : set_of_list evs |]
    1.17            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    1.18