Addition of Revl rule, and tidying
authorpaulson
Tue Oct 08 10:21:04 1996 +0200 (1996-10-08)
changeset 2069a1c623f70407
parent 2068 0d05468dc80c
child 2070 84f4572a6b20
Addition of Revl rule, and tidying
src/HOL/Auth/NS_Shared.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Tue Oct 08 10:19:31 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Tue Oct 08 10:21:04 1996 +0200
     1.3 @@ -55,15 +55,23 @@
     1.4               Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
     1.5            ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
     1.6  
     1.7 -         (*Alice responds with the Nonce, if she has seen the key before.
     1.8 -           We do NOT use N-1 or similar as the Spy cannot spoof such things.
     1.9 -           Allowing the Spy to add or subtract 1 allows him to send ALL
    1.10 -               nonces.  Instead we distinguish the messages by sending the
    1.11 -               nonce twice.*)
    1.12 +         (*Alice responds with Nonce NB if she has seen the key before.
    1.13 +           Maybe should somehow check Nonce NA again.
    1.14 +           We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.15 +           Letting the Spy add or subtract 1 lets him send ALL nonces.
    1.16 +           Instead we distinguish the messages by sending the nonce twice.*)
    1.17      NS5  "[| evs: ns_shared lost;  A ~= B;  
    1.18 -             Says B' A (Crypt (Nonce N) K) : set_of_list evs;
    1.19 +             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    1.20               Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    1.21                 : set_of_list evs |]
    1.22 -          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared lost"
    1.23 +          ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
    1.24 +  
    1.25 +         (*This message models possible leaks of session keys.
    1.26 +           The two Nonces identify the protocol run.*)
    1.27 +    Revl "[| evs: ns_shared lost;  A ~= Spy;
    1.28 +             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    1.29 +             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    1.30 +               : set_of_list evs |]
    1.31 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    1.32  
    1.33  end