src/HOL/Auth/Event.thy
author paulson
Thu, 18 Sep 1997 13:24:04 +0200
changeset 3683 aafe719dff14
parent 3678 414e04d7c2d6
child 5183 89f162de39cf
permissions -rw-r--r--
Global change: lost->bad and sees Spy->spies First change just gives a more sensible name. Second change eliminates the agent parameter of "sees" to simplify definitions and theorems

(*  Title:      HOL/Auth/Event
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Theory of events for security protocols

Datatype of events; function "spies"; freshness

"bad" agents have been broken by the Spy; their private keys and internal
    stores are visible to him
*)

Event = Message + List + 

consts  (*Initial states of agents -- parameter of the construction*)
  initState :: agent => msg set

datatype  (*Messages--could add another constructor for agent knowledge*)
  event = Says  agent agent msg
        | Notes agent       msg

consts  
  bad    :: agent set        (*compromised agents*)
  spies  :: event list => msg set

rules
  (*Spy has access to his own key for spoof messages, but Server is secure*)
  Spy_in_bad     "Spy: bad"
  Server_not_bad "Server ~: bad"

primrec spies list
           (*Spy reads all traffic whether addressed to him or not*)
  spies_Nil   "spies []       = initState Spy"
  spies_Cons  "spies (ev # evs) =
	         (case ev of
		    Says A B X => insert X (spies evs)
		  | Notes A X  => 
	              if A:bad then insert X (spies evs) else spies evs)"

consts
  (*Set of items that might be visible to somebody:
    complement of the set of fresh items*)
  used :: event list => msg set

primrec used list
  used_Nil   "used []         = (UN B. parts (initState B))"
  used_Cons  "used (ev # evs) =
	         (case ev of
		    Says A B X => parts {X} Un (used evs)
		  | Notes A X  => parts {X} Un (used evs))"

end