src/HOL/Auth/Message.thy
author paulson
Mon Aug 03 10:37:34 1998 +0200 (1998-08-03)
changeset 5234 701fa0ed77b7
parent 5183 89f162de39cf
child 5652 fe5f5510aef4
permissions -rw-r--r--
Better comments
     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 = Datatype +
    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 
    35 (*Datatype msg is (awkwardly) split into two parts to avoid having freeness
    36   expressed using natural numbers.*)
    37 datatype  
    38   atomic = AGENT  agent	(*Agent names*)
    39          | NUMBER nat   (*Ordinary integers, timestamps, ...*)
    40          | NONCE  nat   (*Unguessable nonces*)
    41          | KEY    key   (*Crypto keys*)
    42 
    43 datatype
    44      msg = Atomic atomic
    45 	 | Hash   msg       (*Hashing*)
    46 	 | MPair  msg msg   (*Compound messages*)
    47 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    48 
    49 (*These translations complete the illustion that "msg" has seven constructors*)
    50 syntax
    51   Agent       :: agent => msg
    52   Number      :: nat   => msg
    53   Nonce       :: nat   => msg
    54   Key         :: key   => msg
    55 
    56 translations
    57   "Agent x"   == "Atomic (AGENT x)"
    58   "Number x"  == "Atomic (NUMBER x)"
    59   "Nonce x"   == "Atomic (NONCE x)"
    60   "Key x"     == "Atomic (KEY x)"
    61   "Key``x"    == "Atomic `` (KEY `` x)"
    62 
    63 
    64 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    65 syntax
    66   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    67 
    68 translations
    69   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    70   "{|x, y|}"      == "MPair x y"
    71 
    72 
    73 constdefs
    74   (*Message Y, paired with a MAC computed with the help of X*)
    75   HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
    76     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    77 
    78   (*Keys useful to decrypt elements of a message set*)
    79   keysFor :: msg set => key set
    80   "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    81 
    82 (** Inductive definition of all "parts" of a message.  **)
    83 
    84 consts  parts   :: msg set => msg set
    85 inductive "parts H"
    86   intrs 
    87     Inj     "X: H  ==>  X: parts H"
    88     Fst     "{|X,Y|}   : parts H ==> X : parts H"
    89     Snd     "{|X,Y|}   : parts H ==> Y : parts H"
    90     Body    "Crypt K X : parts H ==> X : parts H"
    91 
    92 
    93 (** Inductive definition of "analz" -- what can be broken down from a set of
    94     messages, including keys.  A form of downward closure.  Pairs can
    95     be taken apart; messages decrypted with known keys.  **)
    96 
    97 consts  analz   :: msg set => msg set
    98 inductive "analz H"
    99   intrs 
   100     Inj     "X: H ==> X: analz H"
   101     Fst     "{|X,Y|} : analz H ==> X : analz H"
   102     Snd     "{|X,Y|} : analz H ==> Y : analz H"
   103     Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
   104 
   105 
   106 (** Inductive definition of "synth" -- what can be built up from a set of
   107     messages.  A form of upward closure.  Pairs can be built, messages
   108     encrypted with known keys.  Agent names are public domain.
   109     Numbers can be guessed, but Nonces cannot be.  **)
   110 
   111 consts  synth   :: msg set => msg set
   112 inductive "synth H"
   113   intrs 
   114     Inj     "X: H ==> X: synth H"
   115     Agent   "Agent agt : synth H"
   116     Number  "Number n  : synth H"
   117     Hash    "X: synth H ==> Hash X : synth H"
   118     MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
   119     Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
   120 
   121 end