src/HOL/Auth/Shared.thy
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 3683 aafe719dff14
child 5183 89f162de39cf
permissions -rw-r--r--
Fixed spelling error
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@3512
     8
Shared, long-term keys; initial states of agents
paulson@1934
     9
*)
paulson@1934
    10
paulson@3512
    11
Shared = Event + Finite +
paulson@1934
    12
paulson@1934
    13
consts
paulson@1943
    14
  shrK    :: agent => key  (*symmetric keys*)
paulson@1967
    15
paulson@1934
    16
rules
paulson@3472
    17
  isSym_keys "isSymKey K"	(*All keys are symmetric*)
paulson@3472
    18
  inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
paulson@1934
    19
paulson@1934
    20
primrec initState agent
paulson@2319
    21
        (*Server knows all long-term keys; other agents know only their own*)
paulson@3519
    22
  initState_Server  "initState Server     = Key `` range shrK"
paulson@3519
    23
  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
paulson@3683
    24
  initState_Spy     "initState Spy        = Key``shrK``bad"
paulson@2032
    25
paulson@1934
    26
paulson@2516
    27
rules
paulson@2516
    28
  (*Unlike the corresponding property of nonces, this cannot be proved.
paulson@2516
    29
    We have infinitely many agents and there is nothing to stop their
paulson@2516
    30
    long-term keys from exhausting all the natural numbers.  The axiom
paulson@2516
    31
    assumes that their keys are dispersed so as to leave room for infinitely
paulson@2516
    32
    many fresh session keys.  We could, alternatively, restrict agents to
paulson@2516
    33
    an unspecified finite number.*)
nipkow@3414
    34
  Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
paulson@2516
    35
paulson@1934
    36
end