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