src/HOL/Auth/Shared.thy
author paulson
Fri Dec 13 10:42:58 1996 +0100 (1996-12-13)
changeset 2376 f5c61fd9b9b6
parent 2319 95f0d5243c85
child 2451 ce85a2aafc7a
permissions -rw-r--r--
Temporary additions (random) for the nested Otway-Rees protocol
They will need to be rationalized
     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" numbers for use as symmetric keys, as well as
    48   nonces.*)
    49 
    50 consts
    51   random :: "nat*nat => nat"
    52 
    53 constdefs
    54   newN   :: event list => nat
    55   "newN evs == random (length evs, 0)"
    56 
    57   newK   :: event list => nat
    58   "newK evs == random (length evs, 1)"
    59 
    60 rules
    61   inj_shrK        "inj shrK"
    62   inj_random      "inj random"
    63 
    64   random_neq_shrK "random ij ~= shrK A" 
    65   isSym_random    "isSymKey (random ij)"
    66 
    67 end