src/HOL/Auth/Event.thy
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 3683 aafe719dff14
child 5183 89f162de39cf
permissions -rw-r--r--
Fixed spelling error
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@3683
     8
Datatype of events; function "spies"; freshness
paulson@3678
     9
paulson@3683
    10
"bad" agents have been broken by the Spy; their private keys and internal
paulson@3678
    11
    stores are visible to him
paulson@3512
    12
*)
paulson@3512
    13
paulson@3512
    14
Event = Message + List + 
paulson@3512
    15
paulson@3512
    16
consts  (*Initial states of agents -- parameter of the construction*)
paulson@3519
    17
  initState :: agent => msg set
paulson@3512
    18
paulson@3512
    19
datatype  (*Messages--could add another constructor for agent knowledge*)
paulson@3512
    20
  event = Says  agent agent msg
paulson@3512
    21
        | Notes agent       msg
paulson@3512
    22
paulson@3512
    23
consts  
paulson@3683
    24
  bad    :: agent set        (*compromised agents*)
paulson@3683
    25
  spies  :: event list => msg set
paulson@3519
    26
paulson@3519
    27
rules
paulson@3519
    28
  (*Spy has access to his own key for spoof messages, but Server is secure*)
paulson@3683
    29
  Spy_in_bad     "Spy: bad"
paulson@3683
    30
  Server_not_bad "Server ~: bad"
paulson@3512
    31
paulson@3683
    32
primrec spies list
paulson@3678
    33
           (*Spy reads all traffic whether addressed to him or not*)
paulson@3683
    34
  spies_Nil   "spies []       = initState Spy"
paulson@3683
    35
  spies_Cons  "spies (ev # evs) =
paulson@3683
    36
	         (case ev of
paulson@3683
    37
		    Says A B X => insert X (spies evs)
paulson@3683
    38
		  | Notes A X  => 
paulson@3683
    39
	              if A:bad then insert X (spies evs) else spies evs)"
paulson@3678
    40
paulson@3683
    41
consts
paulson@3683
    42
  (*Set of items that might be visible to somebody:
paulson@3683
    43
    complement of the set of fresh items*)
paulson@3683
    44
  used :: event list => msg set
paulson@3512
    45
paulson@3683
    46
primrec used list
paulson@3683
    47
  used_Nil   "used []         = (UN B. parts (initState B))"
paulson@3683
    48
  used_Cons  "used (ev # evs) =
paulson@3683
    49
	         (case ev of
paulson@3683
    50
		    Says A B X => parts {X} Un (used evs)
paulson@3683
    51
		  | Notes A X  => parts {X} Un (used evs))"
paulson@3512
    52
paulson@3512
    53
end