src/HOL/Auth/Event.thy
changeset 38964 b1a7bef0907a
parent 37936 1e4c5015a72e
child 41693 47532fe9e075
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Aug 31 15:21:56 2010 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Aug 31 18:38:30 2010 +0200
     1.3 @@ -22,14 +22,6 @@
     1.4         
     1.5  consts 
     1.6    bad    :: "agent set"                         -- {* compromised agents *}
     1.7 -  knows  :: "agent => event list => msg set"
     1.8 -
     1.9 -
    1.10 -text{*The constant "spies" is retained for compatibility's sake*}
    1.11 -
    1.12 -abbreviation (input)
    1.13 -  spies  :: "event list => msg set" where
    1.14 -  "spies == knows Spy"
    1.15  
    1.16  text{*Spy has access to his own key for spoof messages, but Server is secure*}
    1.17  specification (bad)
    1.18 @@ -37,9 +29,10 @@
    1.19    Server_not_bad [iff]: "Server \<notin> bad"
    1.20      by (rule exI [of _ "{Spy}"], simp)
    1.21  
    1.22 -primrec
    1.23 +primrec knows :: "agent => event list => msg set"
    1.24 +where
    1.25    knows_Nil:   "knows A [] = initState A"
    1.26 -  knows_Cons:
    1.27 +| knows_Cons:
    1.28      "knows A (ev # evs) =
    1.29         (if A = Spy then 
    1.30          (case ev of
    1.31 @@ -62,14 +55,20 @@
    1.32    therefore the oops case must use Notes
    1.33  *)
    1.34  
    1.35 -consts
    1.36 -  (*Set of items that might be visible to somebody:
    1.37 +text{*The constant "spies" is retained for compatibility's sake*}
    1.38 +
    1.39 +abbreviation (input)
    1.40 +  spies  :: "event list => msg set" where
    1.41 +  "spies == knows Spy"
    1.42 +
    1.43 +
    1.44 +(*Set of items that might be visible to somebody:
    1.45      complement of the set of fresh items*)
    1.46 -  used :: "event list => msg set"
    1.47  
    1.48 -primrec
    1.49 +primrec used :: "event list => msg set"
    1.50 +where
    1.51    used_Nil:   "used []         = (UN B. parts (initState B))"
    1.52 -  used_Cons:  "used (ev # evs) =
    1.53 +| used_Cons:  "used (ev # evs) =
    1.54                       (case ev of
    1.55                          Says A B X => parts {X} \<union> used evs
    1.56                        | Gets A X   => used evs