# HG changeset patch
# User paulson
# Date 844762864 -7200
# Node ID a1c623f70407eb48393f6c803c5b7f253c5da090
# Parent  0d05468dc80c5b9aa8efc9c06096d79ba375c488
Addition of Revl rule, and tidying

diff -r 0d05468dc80c -r a1c623f70407 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Tue Oct 08 10:19:31 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Tue Oct 08 10:21:04 1996 +0200
@@ -55,15 +55,23 @@
              Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
           ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
 
-         (*Alice responds with the Nonce, if she has seen the key before.
-           We do NOT use N-1 or similar as the Spy cannot spoof such things.
-           Allowing the Spy to add or subtract 1 allows him to send ALL
-               nonces.  Instead we distinguish the messages by sending the
-               nonce twice.*)
+         (*Alice responds with Nonce NB if she has seen the key before.
+           Maybe should somehow check Nonce NA again.
+           We do NOT send NB-1 or similar as the Spy cannot spoof such things.
+           Letting the Spy add or subtract 1 lets him send ALL nonces.
+           Instead we distinguish the messages by sending the nonce twice.*)
     NS5  "[| evs: ns_shared lost;  A ~= B;  
-             Says B' A (Crypt (Nonce N) K) : set_of_list evs;
+             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
              Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
                : set_of_list evs |]
-          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared lost"
+          ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
+  
+         (*This message models possible leaks of session keys.
+           The two Nonces identify the protocol run.*)
+    Revl "[| evs: ns_shared lost;  A ~= Spy;
+             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
+             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+               : set_of_list evs |]
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
 
 end