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