src/HOL/Auth/Event.thy
changeset 11104 f2024fed9f0c
parent 6399 4a9040b85e2e
child 11189 1ea763a5d186
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Feb 13 01:32:54 2001 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Feb 13 13:16:27 2001 +0100
     1.3 @@ -11,10 +11,17 @@
     1.4      stores are visible to him
     1.5  *)
     1.6  
     1.7 -Event = Message + List + 
     1.8 +theory Event = Message
     1.9 +files ("Event_lemmas.ML"):
    1.10 +
    1.11 +(*from Message.ML*)
    1.12 +method_setup spy_analz = {*
    1.13 +    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
    1.14 +    "for proving the Fake case when analz is involved"
    1.15 +
    1.16  
    1.17  consts  (*Initial states of agents -- parameter of the construction*)
    1.18 -  initState :: agent => msg set
    1.19 +  initState :: "agent => msg set"
    1.20  
    1.21  datatype
    1.22    event = Says  agent agent msg
    1.23 @@ -22,26 +29,26 @@
    1.24          | Notes agent       msg
    1.25         
    1.26  consts 
    1.27 -  bad    :: agent set        (*compromised agents*)
    1.28 -  knows  :: agent => event list => msg set
    1.29 +  bad    :: "agent set"				(*compromised agents*)
    1.30 +  knows  :: "agent => event list => msg set"
    1.31  
    1.32  
    1.33  (*"spies" is retained for compability's sake*)
    1.34  syntax
    1.35 -  spies  :: event list => msg set
    1.36 +  spies  :: "event list => msg set"
    1.37  
    1.38  translations
    1.39    "spies"   => "knows Spy"
    1.40  
    1.41  
    1.42 -rules
    1.43 +axioms
    1.44    (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.45 -  Spy_in_bad     "Spy: bad"
    1.46 -  Server_not_bad "Server ~: bad"
    1.47 +  Spy_in_bad     [iff] :     "Spy: bad"
    1.48 +  Server_not_bad [iff] : "Server ~: bad"
    1.49  
    1.50  primrec
    1.51 -  knows_Nil   "knows A []         = initState A"
    1.52 -  knows_Cons
    1.53 +  knows_Nil:   "knows A [] = initState A"
    1.54 +  knows_Cons:
    1.55      "knows A (ev # evs) =
    1.56         (if A = Spy then 
    1.57  	(case ev of
    1.58 @@ -67,16 +74,22 @@
    1.59  consts
    1.60    (*Set of items that might be visible to somebody:
    1.61      complement of the set of fresh items*)
    1.62 -  used :: event list => msg set
    1.63 +  used :: "event list => msg set"
    1.64  
    1.65  primrec
    1.66 -  used_Nil   "used []         = (UN B. parts (initState B))"
    1.67 -  used_Cons  "used (ev # evs) =
    1.68 -	         (case ev of
    1.69 -		    Says A B X => parts {X} Un (used evs)
    1.70 -		  | Gets A X   => used evs
    1.71 -		  | Notes A X  => parts {X} Un (used evs))"
    1.72 +  used_Nil:   "used []         = (UN B. parts (initState B))"
    1.73 +  used_Cons:  "used (ev # evs) =
    1.74 +		     (case ev of
    1.75 +			Says A B X => parts {X} Un (used evs)
    1.76 +		      | Gets A X   => used evs
    1.77 +		      | Notes A X  => parts {X} Un (used evs))"
    1.78  
    1.79  
    1.80 +use "Event_lemmas.ML"
    1.81 +
    1.82 +method_setup analz_mono_contra = {*
    1.83 +    Method.no_args
    1.84 +      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    1.85 +    "for proving theorems of the form X ~: analz (knows Spy evs) --> P"
    1.86  
    1.87  end