author paulson
Tue, 09 Mar 1999 11:01:39 +0100
changeset 6308 76f3865a2b1d
parent 5183 89f162de39cf
child 6399 4a9040b85e2e
permissions -rw-r--r--
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories. Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a translation.

(*  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
        | Gets  agent       msg
  bad    :: agent set        (*compromised agents*)
  knows  :: agent => event list => msg set

(*"spies" is retained for compability's sake*)
  spies  :: event list => msg set

  "spies"   => "knows Spy"

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

  knows_Nil   "knows A []         = initState A"
  knows_Cons  "knows A (ev # evs) =
	        (if A = Spy then 
                  (case ev of
		    Says A' B X => insert X (knows Spy evs)
		  | Notes A' X  => 
                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
                  | Gets A' X => knows Spy evs)
                  (case ev of
		    Says A' B X => 
                      if A'=A then insert X (knows A evs) else knows A evs
		  | Notes A' X    => 
                      if A'=A then insert X (knows A evs) else knows A evs
		  | Gets A' X    => 
                      if A'=A then insert X (knows A evs) else knows A evs))"

  Case A=Spy on the Gets event
  enforces the fact that if a message is received then it must have been sent,
  therefore the oops case must use Notes

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

  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)
		  | Gets A X   => used evs)"