(*  Title:      HOL/Auth/Message

    ID:         $Id$

    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

    Copyright   1996  University of Cambridge

Datatypes of agents and messages;

Inductive relations "parts", "analz" and "synth"

*)

Message = Arith +

(*Is there a difference between a nonce and arbitrary numerical data?

  Do we need a type of nonces?*)

types 

  key = nat

consts

  invKey :: key=>key

rules

  invKey "invKey (invKey K) = K"

  (*The inverse of a symmetric key is itself;

    that of a public key is the private key and vice versa*)

constdefs

  isSymKey :: key=>bool

  "isSymKey K == (invKey K = K)"

datatype  (*We allow any number of friendly agents*)

  agent = Server | Friend nat | Spy

datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)

  msg = Agent agent

      | Nonce nat

      | Key   key

      | Hash  msg

      | MPair msg msg

      | Crypt key msg

(*Allows messages of the form {|A,B,NA|}, etc...*)

syntax

  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")

translations

  "{|x, y, z|}"   == "{|x, {|y, z|}|}"

  "{|x, y|}"      == "MPair x y"

constdefs

  (*Message Y, paired with a MAC computed with the help of X*)

  HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])

    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"

  (*Keys useful to decrypt elements of a message set*)

  keysFor :: msg set => key set

  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"

(** Inductive definition of all "parts" of a message.  **)

consts  parts   :: msg set => msg set

inductive "parts H"

  intrs 

    Inj     "X: H  ==>  X: parts H"

    Fst     "{|X,Y|}   : parts H ==> X : parts H"

    Snd     "{|X,Y|}   : parts H ==> Y : parts H"

    Body    "Crypt K X : parts H ==> X : parts H"

(** Inductive definition of "analz" -- what can be broken down from a set of

    messages, including keys.  A form of downward closure.  Pairs can

    be taken apart; messages decrypted with known keys.  **)

consts  analz   :: msg set => msg set

inductive "analz H"

  intrs 

    Inj     "X: H ==> X: analz H"

    Fst     "{|X,Y|} : analz H ==> X : analz H"

    Snd     "{|X,Y|} : analz H ==> Y : analz H"

    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"

(** Inductive definition of "synth" -- what can be built up from a set of

    messages.  A form of upward closure.  Pairs can be built, messages

    encrypted with known keys.  Agent names may be quoted.  **)

consts  synth   :: msg set => msg set

inductive "synth H"

  intrs 

    Inj     "X: H ==> X: synth H"

    Agent   "Agent agt : synth H"

    Hash    "X: synth H ==> Hash X : synth H"

    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"

    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"

end