src/HOL/Auth/Message.thy
author nipkow
Tue Jan 09 15:29:17 2001 +0100 (2001-01-09)
changeset 10833 c0844a30ea4e
parent 9686 87b460d72e80
child 11189 1ea763a5d186
permissions -rw-r--r--
`` -> ` and ``` -> ``
     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 = Main +
    11 
    12 types 
    13   key = nat
    14 
    15 consts
    16   invKey :: key=>key
    17 
    18 rules
    19   invKey "invKey (invKey K) = K"
    20 
    21   (*The inverse of a symmetric key is itself;
    22     that of a public key is the private key and vice versa*)
    23 
    24 constdefs
    25   isSymKey :: key=>bool
    26   "isSymKey K == (invKey K = K)"
    27 
    28 datatype  (*We allow any number of friendly agents*)
    29   agent = Server | Friend nat | Spy
    30 
    31 datatype
    32      msg = Agent  agent	    (*Agent names*)
    33          | Number nat       (*Ordinary integers, timestamps, ...*)
    34          | Nonce  nat       (*Unguessable nonces*)
    35          | Key    key       (*Crypto keys*)
    36 	 | Hash   msg       (*Hashing*)
    37 	 | MPair  msg msg   (*Compound messages*)
    38 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    39 
    40 
    41 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    42 syntax
    43   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    44 
    45 syntax (xsymbols)
    46   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\\<lbrace>_,/ _\\<rbrace>)")
    47 
    48 translations
    49   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    50   "{|x, y|}"      == "MPair x y"
    51 
    52 
    53 constdefs
    54   (*Message Y, paired with a MAC computed with the help of X*)
    55   HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
    56     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    57 
    58   (*Keys useful to decrypt elements of a message set*)
    59   keysFor :: msg set => key set
    60   "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
    61 
    62 (** Inductive definition of all "parts" of a message.  **)
    63 
    64 consts  parts   :: msg set => msg set
    65 inductive "parts H"
    66   intrs 
    67     Inj     "X: H  ==>  X: parts H"
    68     Fst     "{|X,Y|}   : parts H ==> X : parts H"
    69     Snd     "{|X,Y|}   : parts H ==> Y : parts H"
    70     Body    "Crypt K X : parts H ==> X : parts H"
    71 
    72 
    73 (** Inductive definition of "analz" -- what can be broken down from a set of
    74     messages, including keys.  A form of downward closure.  Pairs can
    75     be taken apart; messages decrypted with known keys.  **)
    76 
    77 consts  analz   :: msg set => msg set
    78 inductive "analz H"
    79   intrs 
    80     Inj     "X: H ==> X: analz H"
    81     Fst     "{|X,Y|} : analz H ==> X : analz H"
    82     Snd     "{|X,Y|} : analz H ==> Y : analz H"
    83     Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
    84 
    85 
    86 (** Inductive definition of "synth" -- what can be built up from a set of
    87     messages.  A form of upward closure.  Pairs can be built, messages
    88     encrypted with known keys.  Agent names are public domain.
    89     Numbers can be guessed, but Nonces cannot be.  **)
    90 
    91 consts  synth   :: msg set => msg set
    92 inductive "synth H"
    93   intrs 
    94     Inj     "X: H ==> X: synth H"
    95     Agent   "Agent agt : synth H"
    96     Number  "Number n  : synth H"
    97     Hash    "X: synth H ==> Hash X : synth H"
    98     MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    99     Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
   100 
   101 end