src/HOL/Auth/Message.thy
author paulson
Fri Jun 28 15:26:39 1996 +0200 (1996-06-28)
changeset 1839 199243afac2b
child 1913 2809adb15eb0
permissions -rw-r--r--
Proving safety properties of authentication protocols
     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", "analyze" and "synthesize"
     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 | Enemy
    40 
    41 consts  
    42   isEnemy :: agent => bool
    43 
    44 primrec isEnemy agent
    45   isEnemy_Server  "isEnemy Server  = False"
    46   isEnemy_Friend  "isEnemy (Friend i) = False"
    47   isEnemy_Enemy   "isEnemy Enemy = True"
    48 
    49 datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
    50   msg = Agent agent
    51       | Nonce nat
    52       | Key   key
    53       | MPair msg msg
    54       | Crypt msg key
    55 
    56 (*Allows messages of the form {|A,B,NA|}, etc...*)
    57 syntax
    58   "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
    59 
    60 translations
    61   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    62   "{|x, y|}"      == "MPair x y"
    63 
    64 
    65 constdefs  (*Keys useful to decrypt elements of a message set*)
    66   keysFor :: msg set => key set
    67   "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
    68 
    69 (** Inductive definition of all "parts" of a message.  **)
    70 
    71 consts  parts   :: msg set => msg set
    72 inductive "parts H"
    73   intrs 
    74     Inj     "X: H ==> X: parts H"
    75     Fst     "{|X,Y|} : parts H ==> X : parts H"
    76     Snd     "{|X,Y|} : parts H ==> Y : parts H"
    77     Body    "Crypt X K : parts H ==> X : parts H"
    78 
    79 
    80 (** Inductive definition of "analyze" -- what can be broken down from a set of
    81     messages, including keys.  A form of downward closure.  Pairs can
    82     be taken apart; messages decrypted with known keys.  **)
    83 
    84 consts  analyze   :: msg set => msg set
    85 inductive "analyze H"
    86   intrs 
    87     Inj     "X: H ==> X: analyze H"
    88 
    89     Fst     "{|X,Y|} : analyze H ==> X : analyze H"
    90 
    91     Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
    92 
    93     Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
    94              |] ==> X : analyze H"
    95 
    96 
    97 (** Inductive definition of "synthesize" -- what can be built up from a set of
    98     messages.  A form of upward closure.  Pairs can be built, messages
    99     encrypted with known keys.  Agent names may be quoted.  **)
   100 
   101 consts  synthesize   :: msg set => msg set
   102 inductive "synthesize H"
   103   intrs 
   104     Inj     "X: H ==> X: synthesize H"
   105 
   106     Agent   "Agent agt : synthesize H"
   107 
   108     MPair   "[| X: synthesize H;  Y: synthesize H
   109              |] ==> {|X,Y|} : synthesize H"
   110 
   111     Crypt   "[| X: synthesize H; Key(K): synthesize H
   112              |] ==> Crypt X K : synthesize H"
   113 
   114 end