src/HOL/Auth/Shared.thy
author paulson
Fri Jan 17 12:49:31 1997 +0100 (1997-01-17)
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 3414 804c8a178a7f
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
     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 + Finite +
    12 
    13 consts
    14   shrK    :: agent => key  (*symmetric keys*)
    15 
    16 rules
    17   (*ALL keys are symmetric*)
    18   isSym_keys "isSymKey K"
    19 
    20 consts  (*Initial states of agents -- parameter of the construction*)
    21   initState :: [agent set, agent] => msg set
    22 
    23 primrec initState agent
    24         (*Server knows all long-term keys; other agents know only their own*)
    25   initState_Server  "initState lost Server     = Key `` range shrK"
    26   initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
    27   initState_Spy     "initState lost Spy        = Key``shrK``lost"
    28 
    29 
    30 datatype  (*Messages, and components of agent stores*)
    31   event = Says agent agent msg
    32 
    33 consts  
    34   sees1 :: [agent, event] => msg set
    35 
    36 primrec sees1 event
    37            (*Spy reads all traffic whether addressed to him or not*)
    38   sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    39 
    40 consts  
    41   sees :: [agent set, agent, event list] => msg set
    42 
    43 primrec sees list
    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 constdefs
    49   (*Set of items that might be visible to somebody: complement of the set
    50         of fresh items*)
    51   used :: event list => msg set
    52     "used evs == parts (UN lost B. sees lost B evs)"
    53 
    54 
    55 rules
    56   (*Unlike the corresponding property of nonces, this cannot be proved.
    57     We have infinitely many agents and there is nothing to stop their
    58     long-term keys from exhausting all the natural numbers.  The axiom
    59     assumes that their keys are dispersed so as to leave room for infinitely
    60     many fresh session keys.  We could, alternatively, restrict agents to
    61     an unspecified finite number.*)
    62   Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
    63 
    64 
    65 (*Agents generate random (symmetric) keys and nonces.
    66   The numeric argument is typically the length of the current trace.
    67   An injective pairing function allows multiple keys/nonces to be generated
    68 	in one protocol round.  A typical candidate for npair(i,j) is
    69 	2^j(2i+1)
    70 *)
    71 
    72 consts
    73   nPair :: "nat*nat => nat"
    74   newN  :: "nat => nat"
    75   newK  :: "nat => key"
    76 
    77 rules
    78   inj_shrK        "inj shrK"
    79   inj_nPair       "inj nPair"
    80   inj_newN        "inj newN"
    81   inj_newK        "inj newK"
    82 
    83   newK_neq_shrK   "newK i ~= shrK A" 
    84 
    85 end