src/HOL/Auth/Event.thy
changeset 6308 76f3865a2b1d
parent 5183 89f162de39cf
child 6399 4a9040b85e2e
     1.1 --- a/src/HOL/Auth/Event.thy	Mon Mar 08 13:49:53 1999 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Mar 09 11:01:39 1999 +0100
     1.3 @@ -19,24 +19,49 @@
     1.4  datatype  (*Messages--could add another constructor for agent knowledge*)
     1.5    event = Says  agent agent msg
     1.6          | Notes agent       msg
     1.7 +        | Gets  agent       msg
     1.8 +       
     1.9 +consts 
    1.10 +  bad    :: agent set        (*compromised agents*)
    1.11 +  knows  :: agent => event list => msg set
    1.12  
    1.13 -consts  
    1.14 -  bad    :: agent set        (*compromised agents*)
    1.15 +
    1.16 +(*"spies" is retained for compability's sake*)
    1.17 +syntax
    1.18    spies  :: event list => msg set
    1.19  
    1.20 +translations
    1.21 +  "spies"   => "knows Spy"
    1.22 +
    1.23 +
    1.24  rules
    1.25    (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.26    Spy_in_bad     "Spy: bad"
    1.27    Server_not_bad "Server ~: bad"
    1.28  
    1.29  primrec
    1.30 -           (*Spy reads all traffic whether addressed to him or not*)
    1.31 -  spies_Nil   "spies []       = initState Spy"
    1.32 -  spies_Cons  "spies (ev # evs) =
    1.33 -	         (case ev of
    1.34 -		    Says A B X => insert X (spies evs)
    1.35 -		  | Notes A X  => 
    1.36 -	              if A:bad then insert X (spies evs) else spies evs)"
    1.37 +  knows_Nil   "knows A []         = initState A"
    1.38 +  knows_Cons  "knows A (ev # evs) =
    1.39 +	        (if A = Spy then 
    1.40 +                  (case ev of
    1.41 +		    Says A' B X => insert X (knows Spy evs)
    1.42 +		  | Notes A' X  => 
    1.43 +                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
    1.44 +                  | Gets A' X => knows Spy evs)
    1.45 +                 else
    1.46 +                  (case ev of
    1.47 +		    Says A' B X => 
    1.48 +                      if A'=A then insert X (knows A evs) else knows A evs
    1.49 +		  | Notes A' X    => 
    1.50 +                      if A'=A then insert X (knows A evs) else knows A evs
    1.51 +		  | Gets A' X    => 
    1.52 +                      if A'=A then insert X (knows A evs) else knows A evs))"
    1.53 +
    1.54 +(*
    1.55 +  Case A=Spy on the Gets event
    1.56 +  enforces the fact that if a message is received then it must have been sent,
    1.57 +  therefore the oops case must use Notes
    1.58 +*)
    1.59  
    1.60  consts
    1.61    (*Set of items that might be visible to somebody:
    1.62 @@ -48,6 +73,9 @@
    1.63    used_Cons  "used (ev # evs) =
    1.64  	         (case ev of
    1.65  		    Says A B X => parts {X} Un (used evs)
    1.66 -		  | Notes A X  => parts {X} Un (used evs))"
    1.67 +		  | Notes A X  => parts {X} Un (used evs)
    1.68 +		  | Gets A X   => used evs)"
    1.69 +
    1.70 +
    1.71  
    1.72  end