src/HOL/Auth/Message.thy
changeset 1839 199243afac2b
child 1913 2809adb15eb0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Jun 28 15:26:39 1996 +0200
     1.3 @@ -0,0 +1,114 @@
     1.4 +(*  Title:      HOL/Auth/Message
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Datatypes of agents and messages;
    1.10 +Inductive relations "parts", "analyze" and "synthesize"
    1.11 +*)
    1.12 +
    1.13 +Message = Arith +
    1.14 +
    1.15 +(*Is there a difference between a nonce and arbitrary numerical data?
    1.16 +  Do we need a type of nonces?*)
    1.17 +
    1.18 +types 
    1.19 +  key = nat
    1.20 +
    1.21 +consts
    1.22 +  invKey :: key=>key
    1.23 +
    1.24 +rules
    1.25 +  invKey "invKey (invKey K) = K"
    1.26 +
    1.27 +  (*The inverse of a symmetric key is itself;
    1.28 +    that of a public key is the private key and vice versa*)
    1.29 +
    1.30 +constdefs
    1.31 +  isSymKey :: key=>bool
    1.32 +  "isSymKey K == (invKey K = K)"
    1.33 +
    1.34 +  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
    1.35 +    because Crypt is a constructor!  We assume that encryption is injective,
    1.36 +    which is not true in the real world.  The alternative is to take
    1.37 +    Crypt as an uninterpreted function symbol satisfying the equation
    1.38 +    above.  This seems to require moving to ZF and regarding msg as an
    1.39 +    inductive definition instead of a datatype.*) 
    1.40 +
    1.41 +datatype  (*We allow any number of friendly agents*)
    1.42 +  agent = Server | Friend nat | Enemy
    1.43 +
    1.44 +consts  
    1.45 +  isEnemy :: agent => bool
    1.46 +
    1.47 +primrec isEnemy agent
    1.48 +  isEnemy_Server  "isEnemy Server  = False"
    1.49 +  isEnemy_Friend  "isEnemy (Friend i) = False"
    1.50 +  isEnemy_Enemy   "isEnemy Enemy = True"
    1.51 +
    1.52 +datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
    1.53 +  msg = Agent agent
    1.54 +      | Nonce nat
    1.55 +      | Key   key
    1.56 +      | MPair msg msg
    1.57 +      | Crypt msg key
    1.58 +
    1.59 +(*Allows messages of the form {|A,B,NA|}, etc...*)
    1.60 +syntax
    1.61 +  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
    1.62 +
    1.63 +translations
    1.64 +  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.65 +  "{|x, y|}"      == "MPair x y"
    1.66 +
    1.67 +
    1.68 +constdefs  (*Keys useful to decrypt elements of a message set*)
    1.69 +  keysFor :: msg set => key set
    1.70 +  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
    1.71 +
    1.72 +(** Inductive definition of all "parts" of a message.  **)
    1.73 +
    1.74 +consts  parts   :: msg set => msg set
    1.75 +inductive "parts H"
    1.76 +  intrs 
    1.77 +    Inj     "X: H ==> X: parts H"
    1.78 +    Fst     "{|X,Y|} : parts H ==> X : parts H"
    1.79 +    Snd     "{|X,Y|} : parts H ==> Y : parts H"
    1.80 +    Body    "Crypt X K : parts H ==> X : parts H"
    1.81 +
    1.82 +
    1.83 +(** Inductive definition of "analyze" -- what can be broken down from a set of
    1.84 +    messages, including keys.  A form of downward closure.  Pairs can
    1.85 +    be taken apart; messages decrypted with known keys.  **)
    1.86 +
    1.87 +consts  analyze   :: msg set => msg set
    1.88 +inductive "analyze H"
    1.89 +  intrs 
    1.90 +    Inj     "X: H ==> X: analyze H"
    1.91 +
    1.92 +    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
    1.93 +
    1.94 +    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
    1.95 +
    1.96 +    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
    1.97 +             |] ==> X : analyze H"
    1.98 +
    1.99 +
   1.100 +(** Inductive definition of "synthesize" -- what can be built up from a set of
   1.101 +    messages.  A form of upward closure.  Pairs can be built, messages
   1.102 +    encrypted with known keys.  Agent names may be quoted.  **)
   1.103 +
   1.104 +consts  synthesize   :: msg set => msg set
   1.105 +inductive "synthesize H"
   1.106 +  intrs 
   1.107 +    Inj     "X: H ==> X: synthesize H"
   1.108 +
   1.109 +    Agent   "Agent agt : synthesize H"
   1.110 +
   1.111 +    MPair   "[| X: synthesize H;  Y: synthesize H
   1.112 +             |] ==> {|X,Y|} : synthesize H"
   1.113 +
   1.114 +    Crypt   "[| X: synthesize H; Key(K): synthesize H
   1.115 +             |] ==> Crypt X K : synthesize H"
   1.116 +
   1.117 +end