src/HOL/Auth/Event.thy
author paulson
Tue Feb 13 13:16:27 2001 +0100 (2001-02-13)
changeset 11104 f2024fed9f0c
parent 6399 4a9040b85e2e
child 11189 1ea763a5d186
permissions -rw-r--r--
partial conversion to Isar script style
simplified unicity proofs
     1 (*  Title:      HOL/Auth/Event
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of events for security protocols
     7 
     8 Datatype of events; function "spies"; freshness
     9 
    10 "bad" agents have been broken by the Spy; their private keys and internal
    11     stores are visible to him
    12 *)
    13 
    14 theory Event = Message
    15 files ("Event_lemmas.ML"):
    16 
    17 (*from Message.ML*)
    18 method_setup spy_analz = {*
    19     Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
    20     "for proving the Fake case when analz is involved"
    21 
    22 
    23 consts  (*Initial states of agents -- parameter of the construction*)
    24   initState :: "agent => msg set"
    25 
    26 datatype
    27   event = Says  agent agent msg
    28         | Gets  agent       msg
    29         | Notes agent       msg
    30        
    31 consts 
    32   bad    :: "agent set"				(*compromised agents*)
    33   knows  :: "agent => event list => msg set"
    34 
    35 
    36 (*"spies" is retained for compability's sake*)
    37 syntax
    38   spies  :: "event list => msg set"
    39 
    40 translations
    41   "spies"   => "knows Spy"
    42 
    43 
    44 axioms
    45   (*Spy has access to his own key for spoof messages, but Server is secure*)
    46   Spy_in_bad     [iff] :     "Spy: bad"
    47   Server_not_bad [iff] : "Server ~: bad"
    48 
    49 primrec
    50   knows_Nil:   "knows A [] = initState A"
    51   knows_Cons:
    52     "knows A (ev # evs) =
    53        (if A = Spy then 
    54 	(case ev of
    55 	   Says A' B X => insert X (knows Spy evs)
    56 	 | Gets A' X => knows Spy evs
    57 	 | Notes A' X  => 
    58 	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
    59 	else
    60 	(case ev of
    61 	   Says A' B X => 
    62 	     if A'=A then insert X (knows A evs) else knows A evs
    63 	 | Gets A' X    => 
    64 	     if A'=A then insert X (knows A evs) else knows A evs
    65 	 | Notes A' X    => 
    66 	     if A'=A then insert X (knows A evs) else knows A evs))"
    67 
    68 (*
    69   Case A=Spy on the Gets event
    70   enforces the fact that if a message is received then it must have been sent,
    71   therefore the oops case must use Notes
    72 *)
    73 
    74 consts
    75   (*Set of items that might be visible to somebody:
    76     complement of the set of fresh items*)
    77   used :: "event list => msg set"
    78 
    79 primrec
    80   used_Nil:   "used []         = (UN B. parts (initState B))"
    81   used_Cons:  "used (ev # evs) =
    82 		     (case ev of
    83 			Says A B X => parts {X} Un (used evs)
    84 		      | Gets A X   => used evs
    85 		      | Notes A X  => parts {X} Un (used evs))"
    86 
    87 
    88 use "Event_lemmas.ML"
    89 
    90 method_setup analz_mono_contra = {*
    91     Method.no_args
    92       (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    93     "for proving theorems of the form X ~: analz (knows Spy evs) --> P"
    94 
    95 end