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