src/HOL/Auth/Event.thy
author paulson
Thu Mar 18 10:41:00 1999 +0100 (1999-03-18)
changeset 6399 4a9040b85e2e
parent 6308 76f3865a2b1d
child 11104 f2024fed9f0c
permissions -rw-r--r--
exchanged the order of Gets and Notes in datatype event
     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
    20   event = Says  agent agent msg
    21         | Gets  agent       msg
    22         | Notes agent       msg
    23        
    24 consts 
    25   bad    :: agent set        (*compromised agents*)
    26   knows  :: agent => event list => msg set
    27 
    28 
    29 (*"spies" is retained for compability's sake*)
    30 syntax
    31   spies  :: event list => msg set
    32 
    33 translations
    34   "spies"   => "knows Spy"
    35 
    36 
    37 rules
    38   (*Spy has access to his own key for spoof messages, but Server is secure*)
    39   Spy_in_bad     "Spy: bad"
    40   Server_not_bad "Server ~: bad"
    41 
    42 primrec
    43   knows_Nil   "knows A []         = initState A"
    44   knows_Cons
    45     "knows A (ev # evs) =
    46        (if A = Spy then 
    47 	(case ev of
    48 	   Says A' B X => insert X (knows Spy evs)
    49 	 | Gets A' X => knows Spy evs
    50 	 | Notes A' X  => 
    51 	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
    52 	else
    53 	(case ev of
    54 	   Says A' B X => 
    55 	     if A'=A then insert X (knows A evs) else knows A evs
    56 	 | Gets A' X    => 
    57 	     if A'=A then insert X (knows A evs) else knows A evs
    58 	 | Notes A' X    => 
    59 	     if A'=A then insert X (knows A evs) else knows A evs))"
    60 
    61 (*
    62   Case A=Spy on the Gets event
    63   enforces the fact that if a message is received then it must have been sent,
    64   therefore the oops case must use Notes
    65 *)
    66 
    67 consts
    68   (*Set of items that might be visible to somebody:
    69     complement of the set of fresh items*)
    70   used :: event list => msg set
    71 
    72 primrec
    73   used_Nil   "used []         = (UN B. parts (initState B))"
    74   used_Cons  "used (ev # evs) =
    75 	         (case ev of
    76 		    Says A B X => parts {X} Un (used evs)
    77 		  | Gets A X   => used evs
    78 		  | Notes A X  => parts {X} Un (used evs))"
    79 
    80 
    81 
    82 end