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