src/HOL/Auth/Message.thy
author paulson
Mon Aug 19 11:19:55 1996 +0200 (1996-08-19)
changeset 1913 2809adb15eb0
parent 1839 199243afac2b
child 1947 f19a801a2bca
permissions -rw-r--r--
Renaming of functions, and tidying
paulson@1839
     1
(*  Title:      HOL/Auth/Message
paulson@1839
     2
    ID:         $Id$
paulson@1839
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1839
     4
    Copyright   1996  University of Cambridge
paulson@1839
     5
paulson@1839
     6
Datatypes of agents and messages;
paulson@1913
     7
Inductive relations "parts", "analz" and "synth"
paulson@1839
     8
*)
paulson@1839
     9
paulson@1839
    10
Message = Arith +
paulson@1839
    11
paulson@1839
    12
(*Is there a difference between a nonce and arbitrary numerical data?
paulson@1839
    13
  Do we need a type of nonces?*)
paulson@1839
    14
paulson@1839
    15
types 
paulson@1839
    16
  key = nat
paulson@1839
    17
paulson@1839
    18
consts
paulson@1839
    19
  invKey :: key=>key
paulson@1839
    20
paulson@1839
    21
rules
paulson@1839
    22
  invKey "invKey (invKey K) = K"
paulson@1839
    23
paulson@1839
    24
  (*The inverse of a symmetric key is itself;
paulson@1839
    25
    that of a public key is the private key and vice versa*)
paulson@1839
    26
paulson@1839
    27
constdefs
paulson@1839
    28
  isSymKey :: key=>bool
paulson@1839
    29
  "isSymKey K == (invKey K = K)"
paulson@1839
    30
paulson@1839
    31
  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
paulson@1839
    32
    because Crypt is a constructor!  We assume that encryption is injective,
paulson@1839
    33
    which is not true in the real world.  The alternative is to take
paulson@1839
    34
    Crypt as an uninterpreted function symbol satisfying the equation
paulson@1839
    35
    above.  This seems to require moving to ZF and regarding msg as an
paulson@1839
    36
    inductive definition instead of a datatype.*) 
paulson@1839
    37
paulson@1839
    38
datatype  (*We allow any number of friendly agents*)
paulson@1839
    39
  agent = Server | Friend nat | Enemy
paulson@1839
    40
paulson@1839
    41
consts  
paulson@1839
    42
  isEnemy :: agent => bool
paulson@1839
    43
paulson@1839
    44
primrec isEnemy agent
paulson@1839
    45
  isEnemy_Server  "isEnemy Server  = False"
paulson@1839
    46
  isEnemy_Friend  "isEnemy (Friend i) = False"
paulson@1839
    47
  isEnemy_Enemy   "isEnemy Enemy = True"
paulson@1839
    48
paulson@1839
    49
datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
paulson@1839
    50
  msg = Agent agent
paulson@1839
    51
      | Nonce nat
paulson@1839
    52
      | Key   key
paulson@1839
    53
      | MPair msg msg
paulson@1839
    54
      | Crypt msg key
paulson@1839
    55
paulson@1839
    56
(*Allows messages of the form {|A,B,NA|}, etc...*)
paulson@1839
    57
syntax
paulson@1839
    58
  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
paulson@1839
    59
paulson@1839
    60
translations
paulson@1839
    61
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
paulson@1839
    62
  "{|x, y|}"      == "MPair x y"
paulson@1839
    63
paulson@1839
    64
paulson@1839
    65
constdefs  (*Keys useful to decrypt elements of a message set*)
paulson@1839
    66
  keysFor :: msg set => key set
paulson@1839
    67
  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
paulson@1839
    68
paulson@1839
    69
(** Inductive definition of all "parts" of a message.  **)
paulson@1839
    70
paulson@1839
    71
consts  parts   :: msg set => msg set
paulson@1839
    72
inductive "parts H"
paulson@1839
    73
  intrs 
paulson@1839
    74
    Inj     "X: H ==> X: parts H"
paulson@1839
    75
    Fst     "{|X,Y|} : parts H ==> X : parts H"
paulson@1839
    76
    Snd     "{|X,Y|} : parts H ==> Y : parts H"
paulson@1839
    77
    Body    "Crypt X K : parts H ==> X : parts H"
paulson@1839
    78
paulson@1839
    79
paulson@1913
    80
(** Inductive definition of "analz" -- what can be broken down from a set of
paulson@1839
    81
    messages, including keys.  A form of downward closure.  Pairs can
paulson@1839
    82
    be taken apart; messages decrypted with known keys.  **)
paulson@1839
    83
paulson@1913
    84
consts  analz   :: msg set => msg set
paulson@1913
    85
inductive "analz H"
paulson@1839
    86
  intrs 
paulson@1913
    87
    Inj     "X: H ==> X: analz H"
paulson@1913
    88
    Fst     "{|X,Y|} : analz H ==> X : analz H"
paulson@1913
    89
    Snd     "{|X,Y|} : analz H ==> Y : analz H"
paulson@1913
    90
    Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
paulson@1839
    91
paulson@1839
    92
paulson@1913
    93
(** Inductive definition of "synth" -- what can be built up from a set of
paulson@1839
    94
    messages.  A form of upward closure.  Pairs can be built, messages
paulson@1839
    95
    encrypted with known keys.  Agent names may be quoted.  **)
paulson@1839
    96
paulson@1913
    97
consts  synth   :: msg set => msg set
paulson@1913
    98
inductive "synth H"
paulson@1839
    99
  intrs 
paulson@1913
   100
    Inj     "X: H ==> X: synth H"
paulson@1913
   101
    Agent   "Agent agt : synth H"
paulson@1913
   102
    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
paulson@1913
   103
    Crypt   "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H"
paulson@1839
   104
paulson@1839
   105
end