src/HOL/Auth/Shared.thy
author paulson
Wed Oct 09 13:43:51 1996 +0200 (1996-10-09)
changeset 2078 b198b3d46fb4
parent 2064 5a5e508e2a2b
child 2264 f298678bd54a
permissions -rw-r--r--
New version of axiom sees1_Says:
Previously it only allowed the SENDER to see the content of messages...
Now instead the RECIPIENT sees the messages. This change had no effect
on subsequent proofs because protocol rules refer specifically to the
relevant messages sent to an agent.
     1 (*  Title:      HOL/Auth/Shared
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of Shared Keys (common to all symmetric-key protocols)
     7 
     8 Server keys; initial states of agents; new nonces and keys; function "sees" 
     9 *)
    10 
    11 Shared = Message + List + 
    12 
    13 consts
    14   shrK    :: agent => key  (*symmetric keys*)
    15 
    16 rules
    17   isSym_shrK "isSymKey (shrK A)"
    18 
    19 consts  (*Initial states of agents -- parameter of the construction*)
    20   initState :: [agent set, agent] => msg set
    21 
    22 primrec initState agent
    23         (*Server knows all keys; other agents know only their own*)
    24   initState_Server  "initState lost Server     = Key `` range shrK"
    25   initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
    26   initState_Spy     "initState lost Spy        = Key``shrK``lost"
    27 
    28 
    29 datatype  (*Messages, and components of agent stores*)
    30   event = Says agent agent msg
    31 
    32 consts  
    33   sees1 :: [agent, event] => msg set
    34 
    35 primrec sees1 event
    36            (*Spy reads all traffic whether addressed to him or not*)
    37   sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    38 
    39 consts  
    40   sees :: [agent set, agent, event list] => msg set
    41 
    42 primrec sees list
    43         (*Initial knowledge includes all public keys and own private key*)
    44   sees_Nil  "sees lost A []       = initState lost A"
    45   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    46 
    47 
    48 (*Agents generate "random" nonces.  Different traces always yield
    49   different nonces.  Same applies for keys.*)
    50 consts
    51   newN :: "event list => nat"
    52   newK :: "event list => key"
    53 
    54 rules
    55   inj_shrK      "inj shrK"
    56 
    57   inj_newN      "inj newN"
    58 
    59   inj_newK      "inj newK"
    60   newK_neq_shrK "newK evs ~= shrK A" 
    61   isSym_newK    "isSymKey (newK evs)"
    62 
    63 end