author paulson
Tue, 13 Feb 2001 13:16:27 +0100
changeset 11104 f2024fed9f0c
parent 6399 4a9040b85e2e
child 11189 1ea763a5d186
permissions -rw-r--r--
partial conversion to Isar script style simplified unicity proofs

(*  Title:      HOL/Auth/Event
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Theory of events for security protocols

Datatype of events; function "spies"; freshness

"bad" agents have been broken by the Spy; their private keys and internal
    stores are visible to him

theory Event = Message
files ("Event_lemmas.ML"):

(*from Message.ML*)
method_setup spy_analz = {*
    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
    "for proving the Fake case when analz is involved"

consts  (*Initial states of agents -- parameter of the construction*)
  initState :: "agent => msg set"

  event = Says  agent agent msg
        | Gets  agent       msg
        | Notes agent       msg
  bad    :: "agent set"				(*compromised agents*)
  knows  :: "agent => event list => msg set"

(*"spies" is retained for compability's sake*)
  spies  :: "event list => msg set"

  "spies"   => "knows Spy"

  (*Spy has access to his own key for spoof messages, but Server is secure*)
  Spy_in_bad     [iff] :     "Spy: bad"
  Server_not_bad [iff] : "Server ~: bad"

  knows_Nil:   "knows A [] = initState A"
    "knows A (ev # evs) =
       (if A = Spy then 
	(case ev of
	   Says A' B X => insert X (knows Spy evs)
	 | Gets A' X => knows Spy evs
	 | Notes A' X  => 
	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
	(case ev of
	   Says A' B X => 
	     if A'=A then insert X (knows A evs) else knows A evs
	 | Gets A' X    => 
	     if A'=A then insert X (knows A evs) else knows A evs
	 | Notes A' X    => 
	     if A'=A then insert X (knows A evs) else knows A evs))"

  Case A=Spy on the Gets event
  enforces the fact that if a message is received then it must have been sent,
  therefore the oops case must use Notes

  (*Set of items that might be visible to somebody:
    complement of the set of fresh items*)
  used :: "event list => msg set"

  used_Nil:   "used []         = (UN B. parts (initState B))"
  used_Cons:  "used (ev # evs) =
		     (case ev of
			Says A B X => parts {X} Un (used evs)
		      | Gets A X   => used evs
		      | Notes A X  => parts {X} Un (used evs))"

use "Event_lemmas.ML"

method_setup analz_mono_contra = {*
      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    "for proving theorems of the form X ~: analz (knows Spy evs) --> P"