src/HOL/Auth/Event.thy
changeset 3512 9dcb4daa15e8
child 3519 ab0a9fbed4c0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Jul 11 13:26:15 1997 +0200
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      HOL/Auth/Event
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Theory of events for security protocols
    1.10 +
    1.11 +Datatype of events; function "sees"; freshness
    1.12 +*)
    1.13 +
    1.14 +Event = Message + List + 
    1.15 +
    1.16 +consts  (*Initial states of agents -- parameter of the construction*)
    1.17 +  initState :: [agent set, agent] => msg set
    1.18 +
    1.19 +datatype  (*Messages--could add another constructor for agent knowledge*)
    1.20 +  event = Says  agent agent msg
    1.21 +        | Notes agent       msg
    1.22 +
    1.23 +consts  
    1.24 +  sees1 :: [agent, event] => msg set
    1.25 +
    1.26 +primrec sees1 event
    1.27 +           (*Spy reads all traffic whether addressed to him or not*)
    1.28 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    1.29 +  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
    1.30 +
    1.31 +consts  
    1.32 +  sees :: [agent set, agent, event list] => msg set
    1.33 +
    1.34 +primrec sees list
    1.35 +  sees_Nil  "sees lost A []       = initState lost A"
    1.36 +  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    1.37 +
    1.38 +
    1.39 +constdefs
    1.40 +  (*Set of items that might be visible to somebody: complement of the set
    1.41 +        of fresh items*)
    1.42 +  used :: event list => msg set
    1.43 +    "used evs == parts (UN lost B. sees lost B evs)"
    1.44 +
    1.45 +end