src/HOL/Auth/Event.thy
author paulson
Mon Jul 14 12:47:21 1997 +0200 (1997-07-14)
changeset 3519 ab0a9fbed4c0
parent 3512 9dcb4daa15e8
child 3678 414e04d7c2d6
permissions -rw-r--r--
Changing "lost" from a parameter of protocol definitions to a constant.

Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
     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 "sees"; freshness
     9 *)
    10 
    11 Event = Message + List + 
    12 
    13 consts  (*Initial states of agents -- parameter of the construction*)
    14   initState :: agent => msg set
    15 
    16 datatype  (*Messages--could add another constructor for agent knowledge*)
    17   event = Says  agent agent msg
    18         | Notes agent       msg
    19 
    20 consts  
    21   sees1 :: [agent, event] => msg set
    22 
    23 primrec sees1 event
    24            (*Spy reads all traffic whether addressed to him or not*)
    25   sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    26   sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
    27 
    28 consts  
    29   lost :: agent set        (*agents whose private keys have been compromised*)
    30   sees :: [agent, event list] => msg set
    31 
    32 rules
    33   (*Spy has access to his own key for spoof messages, but Server is secure*)
    34   Spy_in_lost     "Spy: lost"
    35   Server_not_lost "Server ~: lost"
    36 
    37 primrec sees list
    38   sees_Nil  "sees A []       = initState A"
    39   sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    40 
    41 constdefs
    42   (*Set of items that might be visible to somebody: complement of the set
    43         of fresh items*)
    44   used :: event list => msg set
    45     "used evs == parts (UN B. sees B evs)"
    46 
    47 end