src/HOL/Auth/Shared.thy
author paulson
Thu Dec 05 18:56:18 1996 +0100 (1996-12-05)
changeset 2319 95f0d5243c85
parent 2264 f298678bd54a
child 2376 f5c61fd9b9b6
permissions -rw-r--r--
Updating of comments
     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 long-term 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   sees_Nil  "sees lost A []       = initState lost A"
    44   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    45 
    46 
    47 (*Agents generate "random" nonces and keys.  These are uniquely determined by
    48   the length of their argument, a trace.*)
    49 consts
    50   newN :: "event list => nat"
    51   newK :: "event list => key"
    52 
    53 rules
    54   inj_shrK      "inj shrK"
    55 
    56   newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
    57   newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
    58 
    59   newK_neq_shrK "newK evs ~= shrK A" 
    60   isSym_newK    "isSymKey (newK evs)"
    61 
    62 end