src/HOL/Auth/Event.thy
changeset 1885 a18a6dc14f76
parent 1852 289ce6cb5c84
child 1893 fa58f4a06f21
     1.1 --- a/src/HOL/Auth/Event.thy	Fri Jul 26 12:18:50 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Jul 26 12:19:46 1996 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  primrec initState agent
     1.6          (*Server knows all keys; other agents know only their own*)
     1.7 -  initState_Server  "initState Server     = range (Key o serverKey)"
     1.8 +  initState_Server  "initState Server     = Key `` range serverKey"
     1.9    initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    1.10    initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    1.11  
    1.12 @@ -111,7 +111,7 @@
    1.13                     (serverKey A))) # evs : traces"
    1.14  
    1.15             (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.16 -             May assume WLOG that she is NOT the Enemy, as the Fake rule.
    1.17 +             May assume WLOG that she is NOT the Enemy: the Fake rule
    1.18               covers this case.  Can inductively show A ~= Server*)
    1.19      NS3  "[| evs: traces;  A ~= B;
    1.20               evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}