src/HOL/Auth/Event.thy
changeset 1893 fa58f4a06f21
parent 1885 a18a6dc14f76
child 1913 2809adb15eb0
--- a/src/HOL/Auth/Event.thy	Mon Jul 29 18:30:01 1996 +0200
+++ b/src/HOL/Auth/Event.thy	Mon Jul 29 18:31:39 1996 +0200
@@ -102,9 +102,9 @@
           |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
                  # evs : traces"
 
-          (*We can't trust the sender field: change that A to A'?  *)
-    NS2  "[| evs: traces;  A ~= B;
-             evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
+          (*We can't trust the sender field, hence the A' in it  *)
+    NS2  "[| evs: traces;  A ~= B;  A ~= Server;
+             evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs'
           |] ==> (Says Server A 
                   (Crypt {|Nonce NA, Agent B, Key (newK evs),   
                            (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}