src/HOL/Auth/Shared.thy
author paulson
Wed, 09 Oct 1996 13:43:51 +0200
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.

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

Theory of Shared Keys (common to all symmetric-key protocols)

Server keys; initial states of agents; new nonces and keys; function "sees" 
*)

Shared = Message + List + 

consts
  shrK    :: agent => key  (*symmetric keys*)

rules
  isSym_shrK "isSymKey (shrK A)"

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

primrec initState agent
        (*Server knows all keys; other agents know only their own*)
  initState_Server  "initState lost Server     = Key `` range shrK"
  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
  initState_Spy     "initState lost Spy        = Key``shrK``lost"


datatype  (*Messages, and components of agent stores*)
  event = Says agent agent msg

consts  
  sees1 :: [agent, event] => msg set

primrec sees1 event
           (*Spy reads all traffic whether addressed to him or not*)
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"

consts  
  sees :: [agent set, agent, event list] => msg set

primrec sees list
        (*Initial knowledge includes all public keys and own private key*)
  sees_Nil  "sees lost A []       = initState lost A"
  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"


(*Agents generate "random" nonces.  Different traces always yield
  different nonces.  Same applies for keys.*)
consts
  newN :: "event list => nat"
  newK :: "event list => key"

rules
  inj_shrK      "inj shrK"

  inj_newN      "inj newN"

  inj_newK      "inj newK"
  newK_neq_shrK "newK evs ~= shrK A" 
  isSym_newK    "isSymKey (newK evs)"

end