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.
paulson@1934
     1
(*  Title:      HOL/Auth/Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Theory of Shared Keys (common to all symmetric-key protocols)
paulson@1934
     7
paulson@1934
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
paulson@1934
     9
*)
paulson@1934
    10
paulson@1934
    11
Shared = Message + List + 
paulson@1934
    12
paulson@1934
    13
consts
paulson@1943
    14
  shrK    :: agent => key  (*symmetric keys*)
paulson@1967
    15
paulson@1934
    16
rules
paulson@1943
    17
  isSym_shrK "isSymKey (shrK A)"
paulson@1934
    18
paulson@1934
    19
consts  (*Initial states of agents -- parameter of the construction*)
paulson@2032
    20
  initState :: [agent set, agent] => msg set
paulson@1934
    21
paulson@1934
    22
primrec initState agent
paulson@1934
    23
        (*Server knows all keys; other agents know only their own*)
paulson@2032
    24
  initState_Server  "initState lost Server     = Key `` range shrK"
paulson@2032
    25
  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
paulson@2064
    26
  initState_Spy     "initState lost Spy        = Key``shrK``lost"
paulson@2032
    27
paulson@1934
    28
paulson@1934
    29
datatype  (*Messages, and components of agent stores*)
paulson@1934
    30
  event = Says agent agent msg
paulson@1934
    31
paulson@1934
    32
consts  
paulson@1934
    33
  sees1 :: [agent, event] => msg set
paulson@1934
    34
paulson@1934
    35
primrec sees1 event
paulson@2078
    36
           (*Spy reads all traffic whether addressed to him or not*)
paulson@2078
    37
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
paulson@1934
    38
paulson@1934
    39
consts  
paulson@2032
    40
  sees :: [agent set, agent, event list] => msg set
paulson@1934
    41
paulson@1934
    42
primrec sees list
paulson@1934
    43
        (*Initial knowledge includes all public keys and own private key*)
paulson@2032
    44
  sees_Nil  "sees lost A []       = initState lost A"
paulson@2032
    45
  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
paulson@1934
    46
paulson@1934
    47
paulson@1934
    48
(*Agents generate "random" nonces.  Different traces always yield
paulson@1934
    49
  different nonces.  Same applies for keys.*)
paulson@1934
    50
consts
paulson@1934
    51
  newN :: "event list => nat"
paulson@1934
    52
  newK :: "event list => key"
paulson@1934
    53
paulson@1934
    54
rules
paulson@2032
    55
  inj_shrK      "inj shrK"
paulson@2032
    56
paulson@2032
    57
  inj_newN      "inj newN"
paulson@1934
    58
paulson@2032
    59
  inj_newK      "inj newK"
paulson@2032
    60
  newK_neq_shrK "newK evs ~= shrK A" 
paulson@2032
    61
  isSym_newK    "isSymKey (newK evs)"
paulson@1934
    62
paulson@1934
    63
end