src/HOL/Auth/Event.thy
changeset 14126 28824746d046
parent 13956 8fe7e12290e1
child 14200 d8598e24f8fa
     1.1 --- a/src/HOL/Auth/Event.thy	Thu Jul 24 16:35:51 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Jul 24 16:36:29 2003 +0200
     1.3 @@ -26,18 +26,21 @@
     1.4    knows  :: "agent => event list => msg set"
     1.5  
     1.6  
     1.7 -(*"spies" is retained for compatibility's sake*)
     1.8 +text{*The constant "spies" is retained for compatibility's sake*}
     1.9  syntax
    1.10    spies  :: "event list => msg set"
    1.11  
    1.12  translations
    1.13    "spies"   => "knows Spy"
    1.14  
    1.15 +text{*Spy has access to his own key for spoof messages, but Server is secure*}
    1.16 +specification (bad)
    1.17 +  bad_properties: "Spy \<in> bad & Server \<notin> bad"
    1.18 +    by (rule exI [of _ "{Spy}"], simp)
    1.19  
    1.20 -axioms
    1.21 -  (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.22 -  Spy_in_bad     [iff] :    "Spy \<in> bad"
    1.23 -  Server_not_bad [iff] : "Server \<notin> bad"
    1.24 +lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff]
    1.25 +lemmas Server_not_bad = bad_properties [THEN conjunct2, iff]
    1.26 +
    1.27  
    1.28  primrec
    1.29    knows_Nil:   "knows A [] = initState A"