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