src/HOL/Auth/Event.thy
changeset 3519 ab0a9fbed4c0
parent 3512 9dcb4daa15e8
child 3678 414e04d7c2d6
     1.1 --- a/src/HOL/Auth/Event.thy	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  Event = Message + List + 
     1.5  
     1.6  consts  (*Initial states of agents -- parameter of the construction*)
     1.7 -  initState :: [agent set, agent] => msg set
     1.8 +  initState :: agent => msg set
     1.9  
    1.10  datatype  (*Messages--could add another constructor for agent knowledge*)
    1.11    event = Says  agent agent msg
    1.12 @@ -26,17 +26,22 @@
    1.13    sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
    1.14  
    1.15  consts  
    1.16 -  sees :: [agent set, agent, event list] => msg set
    1.17 +  lost :: agent set        (*agents whose private keys have been compromised*)
    1.18 +  sees :: [agent, event list] => msg set
    1.19 +
    1.20 +rules
    1.21 +  (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.22 +  Spy_in_lost     "Spy: lost"
    1.23 +  Server_not_lost "Server ~: lost"
    1.24  
    1.25  primrec sees list
    1.26 -  sees_Nil  "sees lost A []       = initState lost A"
    1.27 -  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    1.28 -
    1.29 +  sees_Nil  "sees A []       = initState A"
    1.30 +  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    1.31  
    1.32  constdefs
    1.33    (*Set of items that might be visible to somebody: complement of the set
    1.34          of fresh items*)
    1.35    used :: event list => msg set
    1.36 -    "used evs == parts (UN lost B. sees lost B evs)"
    1.37 +    "used evs == parts (UN B. sees B evs)"
    1.38  
    1.39  end