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
     1 (*  Title:      HOL/Auth/Event
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of events for security protocols
     7 
     8 Datatype of events; function "spies"; freshness
     9 
    10 "bad" agents have been broken by the Spy; their private keys and internal
    11     stores are visible to him
    12 *)
    13 
    14 Event = Message + List + 
    15 
    16 consts  (*Initial states of agents -- parameter of the construction*)
    17   initState :: agent => msg set
    18 
    19 datatype  (*Messages--could add another constructor for agent knowledge*)
    20   event = Says  agent agent msg
    21         | Notes agent       msg
    22 
    23 consts  
    24   bad    :: agent set        (*compromised agents*)
    25   spies  :: event list => msg set
    26 
    27 rules
    28   (*Spy has access to his own key for spoof messages, but Server is secure*)
    29   Spy_in_bad     "Spy: bad"
    30   Server_not_bad "Server ~: bad"
    31 
    32 primrec spies list
    33            (*Spy reads all traffic whether addressed to him or not*)
    34   spies_Nil   "spies []       = initState Spy"
    35   spies_Cons  "spies (ev # evs) =
    36 	         (case ev of
    37 		    Says A B X => insert X (spies evs)
    38 		  | Notes A X  => 
    39 	              if A:bad then insert X (spies evs) else spies evs)"
    40 
    41 consts
    42   (*Set of items that might be visible to somebody:
    43     complement of the set of fresh items*)
    44   used :: event list => msg set
    45 
    46 primrec used list
    47   used_Nil   "used []         = (UN B. parts (initState B))"
    48   used_Cons  "used (ev # evs) =
    49 	         (case ev of
    50 		    Says A B X => parts {X} Un (used evs)
    51 		  | Notes A X  => parts {X} Un (used evs))"
    52 
    53 end