src/HOL/Auth/Event.thy
changeset 1913 2809adb15eb0
parent 1893 fa58f4a06f21
child 1929 f0839bab4b00
--- a/src/HOL/Auth/Event.thy	Mon Aug 19 11:19:16 1996 +0200
+++ b/src/HOL/Auth/Event.thy	Mon Aug 19 11:19:55 1996 +0200
@@ -60,7 +60,7 @@
 
 constdefs
   knownBy :: [event list, msg] => agent set
-  "knownBy evs X == {A. X: analyze (sees A evs)}"
+  "knownBy evs X == {A. X: analz (sees A evs)}"
 
 
 (*Agents generate "random" nonces.  Different traces always yield
@@ -95,7 +95,7 @@
     (*The enemy MAY say anything he CAN say.  We do not expect him to
       invent new nonces here, but he can also use NS1.*)
     Fake "[| evs: traces;  B ~= Enemy;  
-             X: synthesize(analyze(sees Enemy evs))
+             X: synth(analz(sees Enemy evs))
           |] ==> (Says Enemy B X) # evs : traces"
 
     NS1  "[| evs: traces;  A ~= Server
@@ -118,15 +118,15 @@
                               (serverKey A))) 
                    # evs';
              A = Friend i;
-             (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
+             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs'
           |] ==> (Says A B X) # evs : traces"
 
 (*Initial version of NS2 had 
 
         {|Agent A, Agent B, Key (newK evs), Nonce NA|}
 
-  for the encrypted part; the version above is LESS transparent, hence
-  maybe HARDER to prove.  Also it is precisely as in the BAN paper.
+  for the encrypted part; the version above is LESS explicit, hence
+  HARDER to prove.  Also it is precisely as in the BAN paper.
 *)
 
 end