src/HOL/Auth/Message.thy
author paulson
Fri Dec 13 10:17:35 1996 +0100 (1996-12-13)
changeset 2373 490ffa16952e
parent 2284 80ebd1a213fd
child 2484 596a5b5a68ff
permissions -rw-r--r--
Addition of the Hash constructor
Strengthening spy_analz_tac
     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 datatype  (*We allow any number of friendly agents*)
    32   agent = Server | Friend nat | Spy
    33 
    34 datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
    35   msg = Agent agent
    36       | Nonce nat
    37       | Key   key
    38       | Hash  msg
    39       | MPair msg msg
    40       | Crypt key msg
    41 
    42 (*Allows messages of the form {|A,B,NA|}, etc...*)
    43 syntax
    44   "@MTuple"      :: "['a, args] => 'a * 'b"            ("(2{|_,/ _|})")
    45 
    46 translations
    47   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    48   "{|x, y|}"      == "MPair x y"
    49 
    50 
    51 constdefs  (*Keys useful to decrypt elements of a message set*)
    52   keysFor :: msg set => key set
    53   "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    54 
    55 (** Inductive definition of all "parts" of a message.  **)
    56 
    57 consts  parts   :: msg set => msg set
    58 inductive "parts H"
    59   intrs 
    60     Inj     "X: H  ==>  X: parts H"
    61     Fst     "{|X,Y|}   : parts H ==> X : parts H"
    62     Snd     "{|X,Y|}   : parts H ==> Y : parts H"
    63     Body    "Crypt K X : parts H ==> X : parts H"
    64 
    65 
    66 (** Inductive definition of "analz" -- what can be broken down from a set of
    67     messages, including keys.  A form of downward closure.  Pairs can
    68     be taken apart; messages decrypted with known keys.  **)
    69 
    70 consts  analz   :: msg set => msg set
    71 inductive "analz H"
    72   intrs 
    73     Inj     "X: H ==> X: analz H"
    74     Fst     "{|X,Y|} : analz H ==> X : analz H"
    75     Snd     "{|X,Y|} : analz H ==> Y : analz H"
    76     Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
    77 
    78 
    79 (** Inductive definition of "synth" -- what can be built up from a set of
    80     messages.  A form of upward closure.  Pairs can be built, messages
    81     encrypted with known keys.  Agent names may be quoted.  **)
    82 
    83 consts  synth   :: msg set => msg set
    84 inductive "synth H"
    85   intrs 
    86     Inj     "X: H ==> X: synth H"
    87     Agent   "Agent agt : synth H"
    88     Hash    "X: synth H ==> Hash X : synth H"
    89     MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    90     Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
    91 
    92 end