src/HOL/Auth/Event.thy
author paulson
Fri Jul 11 13:26:15 1997 +0200 (1997-07-11)
changeset 3512 9dcb4daa15e8
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared"
and "Public" to "Event". NB the original "Event" theory was later renamed "Shared".

Addition of the Notes constructor to datatype "event".
paulson@3512
     1
(*  Title:      HOL/Auth/Event
paulson@3512
     2
    ID:         $Id$
paulson@3512
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3512
     4
    Copyright   1996  University of Cambridge
paulson@3512
     5
paulson@3512
     6
Theory of events for security protocols
paulson@3512
     7
paulson@3512
     8
Datatype of events; function "sees"; freshness
paulson@3512
     9
*)
paulson@3512
    10
paulson@3512
    11
Event = Message + List + 
paulson@3512
    12
paulson@3512
    13
consts  (*Initial states of agents -- parameter of the construction*)
paulson@3512
    14
  initState :: [agent set, agent] => msg set
paulson@3512
    15
paulson@3512
    16
datatype  (*Messages--could add another constructor for agent knowledge*)
paulson@3512
    17
  event = Says  agent agent msg
paulson@3512
    18
        | Notes agent       msg
paulson@3512
    19
paulson@3512
    20
consts  
paulson@3512
    21
  sees1 :: [agent, event] => msg set
paulson@3512
    22
paulson@3512
    23
primrec sees1 event
paulson@3512
    24
           (*Spy reads all traffic whether addressed to him or not*)
paulson@3512
    25
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
paulson@3512
    26
  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
paulson@3512
    27
paulson@3512
    28
consts  
paulson@3512
    29
  sees :: [agent set, agent, event list] => msg set
paulson@3512
    30
paulson@3512
    31
primrec sees list
paulson@3512
    32
  sees_Nil  "sees lost A []       = initState lost A"
paulson@3512
    33
  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
paulson@3512
    34
paulson@3512
    35
paulson@3512
    36
constdefs
paulson@3512
    37
  (*Set of items that might be visible to somebody: complement of the set
paulson@3512
    38
        of fresh items*)
paulson@3512
    39
  used :: event list => msg set
paulson@3512
    40
    "used evs == parts (UN lost B. sees lost B evs)"
paulson@3512
    41
paulson@3512
    42
end