src/HOL/Auth/NS_Shared.thy

--- a/src/HOL/Auth/NS_Shared.thy	Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Thu Jun 26 13:20:50 1997 +0200
@@ -35,7 +35,7 @@
 	   Server doesn't know who the true sender is, hence the A' in
                the sender field.*)
     NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
-             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
+             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
           ==> Says Server A 
                 (Crypt (shrK A)
                    {|Nonce NA, Agent B, Key KAB,
@@ -46,14 +46,14 @@
             Can inductively show A ~= Server*)
     NS3  "[| evs: ns_shared lost;  A ~= B;
              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
-               : set_of_list evs;
-             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
+               : set evs;
+             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
           ==> Says A B X # evs : ns_shared lost"
 
          (*Bob's nonce exchange.  He does not know who the message came
            from, but responds to A because she is mentioned inside.*)
     NS4  "[| evs: ns_shared lost;  A ~= B;  Nonce NB ~: used evs;
-             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
+             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
           ==> Says B A (Crypt K (Nonce NB)) # evs
                 : ns_shared lost"
 
@@ -63,18 +63,18 @@
            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 K (Nonce NB)) : set_of_list evs;
+             Says B' A (Crypt K (Nonce NB)) : set evs;
              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
-               : set_of_list evs |]
+               : set evs |]
           ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
   
          (*This message models possible leaks of session keys.
            The two Nonces identify the protocol run: the rule insists upon
            the true senders in order to make them accurate.*)
     Oops "[| evs: ns_shared lost;  A ~= Spy;
-             Says B A (Crypt K (Nonce NB)) : set_of_list evs;
+             Says B A (Crypt K (Nonce NB)) : set evs;
              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
-               : set_of_list evs |]
+               : set evs |]
           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
 
 end