Updating of comments
authorpaulson
Thu Dec 05 18:56:18 1996 +0100 (1996-12-05)
changeset 231995f0d5243c85
parent 2318 6d3f7c7f70b0
child 2320 41289907faed
Updating of comments
src/HOL/Auth/Shared.thy
     1.1 --- a/src/HOL/Auth/Shared.thy	Thu Dec 05 18:07:27 1996 +0100
     1.2 +++ b/src/HOL/Auth/Shared.thy	Thu Dec 05 18:56:18 1996 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    initState :: [agent set, agent] => msg set
     1.5  
     1.6  primrec initState agent
     1.7 -        (*Server knows all keys; other agents know only their own*)
     1.8 +        (*Server knows all long-term keys; other agents know only their own*)
     1.9    initState_Server  "initState lost Server     = Key `` range shrK"
    1.10    initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
    1.11    initState_Spy     "initState lost Spy        = Key``shrK``lost"
    1.12 @@ -40,13 +40,12 @@
    1.13    sees :: [agent set, agent, event list] => msg set
    1.14  
    1.15  primrec sees list
    1.16 -        (*Initial knowledge includes all public keys and own private key*)
    1.17    sees_Nil  "sees lost A []       = initState lost A"
    1.18    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    1.19  
    1.20  
    1.21 -(*Agents generate "random" nonces.  Different traces always yield
    1.22 -  different nonces.  Same applies for keys.*)
    1.23 +(*Agents generate "random" nonces and keys.  These are uniquely determined by
    1.24 +  the length of their argument, a trace.*)
    1.25  consts
    1.26    newN :: "event list => nat"
    1.27    newK :: "event list => key"