src/HOL/Auth/Event.thy
changeset 3683 aafe719dff14
parent 3678 414e04d7c2d6
child 5183 89f162de39cf
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -5,9 +5,9 @@
     1.4  
     1.5  Theory of events for security protocols
     1.6  
     1.7 -Datatype of events; function "sees"; freshness
     1.8 +Datatype of events; function "spies"; freshness
     1.9  
    1.10 -"lost" agents have been broken by the Spy; their private keys and internal
    1.11 +"bad" agents have been broken by the Spy; their private keys and internal
    1.12      stores are visible to him
    1.13  *)
    1.14  
    1.15 @@ -21,31 +21,33 @@
    1.16          | Notes agent       msg
    1.17  
    1.18  consts  
    1.19 -  lost :: agent set        (*compromised agents*)
    1.20 -  sees :: [agent, event list] => msg set
    1.21 +  bad    :: agent set        (*compromised agents*)
    1.22 +  spies  :: event list => msg set
    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_lost     "Spy: lost"
    1.27 -  Server_not_lost "Server ~: lost"
    1.28 +  Spy_in_bad     "Spy: bad"
    1.29 +  Server_not_bad "Server ~: bad"
    1.30  
    1.31 -consts  
    1.32 -  sees1 :: [agent, event] => msg set
    1.33 -
    1.34 -primrec sees1 event
    1.35 +primrec spies list
    1.36             (*Spy reads all traffic whether addressed to him or not*)
    1.37 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    1.38 -  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
    1.39 -					 else {})"
    1.40 +  spies_Nil   "spies []       = initState Spy"
    1.41 +  spies_Cons  "spies (ev # evs) =
    1.42 +	         (case ev of
    1.43 +		    Says A B X => insert X (spies evs)
    1.44 +		  | Notes A X  => 
    1.45 +	              if A:bad then insert X (spies evs) else spies evs)"
    1.46  
    1.47 -primrec sees list
    1.48 -  sees_Nil  "sees A []       = initState A"
    1.49 -  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    1.50 +consts
    1.51 +  (*Set of items that might be visible to somebody:
    1.52 +    complement of the set of fresh items*)
    1.53 +  used :: event list => msg set
    1.54  
    1.55 -constdefs
    1.56 -  (*Set of items that might be visible to somebody: complement of the set
    1.57 -        of fresh items*)
    1.58 -  used :: event list => msg set
    1.59 -    "used evs == parts (UN B. sees B evs)"
    1.60 +primrec used list
    1.61 +  used_Nil   "used []         = (UN B. parts (initState B))"
    1.62 +  used_Cons  "used (ev # evs) =
    1.63 +	         (case ev of
    1.64 +		    Says A B X => parts {X} Un (used evs)
    1.65 +		  | Notes A X  => parts {X} Un (used evs))"
    1.66  
    1.67  end