src/HOL/Auth/Message.thy
changeset 3668 a39baf59ea47
parent 2516 4d68fbe6378b
child 5102 8c782c25a11e
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Sep 11 12:22:31 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Sep 11 12:24:28 1997 +0200
     1.3 @@ -31,19 +31,33 @@
     1.4  datatype  (*We allow any number of friendly agents*)
     1.5    agent = Server | Friend nat | Spy
     1.6  
     1.7 -datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
     1.8 -  msg = Agent agent
     1.9 -      | Nonce nat
    1.10 -      | Key   key
    1.11 -      | Hash  msg
    1.12 -      | MPair msg msg
    1.13 -      | Crypt key msg
    1.14 +datatype  
    1.15 +  atomic = AGENT  agent	(*Agent names*)
    1.16 +         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
    1.17 +         | NONCE  nat   (*Unguessable nonces*)
    1.18 +         | KEY    key   (*Crypto keys*)
    1.19 +
    1.20 +datatype
    1.21 +  msg = Atomic atomic
    1.22 +      | Hash   msg       (*Hashing*)
    1.23 +      | MPair  msg msg   (*Compound messages*)
    1.24 +      | Crypt  key msg   (*Encryption, public- or shared-key*)
    1.25  
    1.26  (*Allows messages of the form {|A,B,NA|}, etc...*)
    1.27  syntax
    1.28 +  Agent          :: agent => msg
    1.29 +  Number         :: nat   => msg
    1.30 +  Nonce          :: nat   => msg
    1.31 +  Key            :: key   => msg
    1.32    "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    1.33  
    1.34  translations
    1.35 +  "Agent x"       == "Atomic (AGENT x)"
    1.36 +  "Number x"	  == "Atomic (NUMBER x)"
    1.37 +  "Nonce x"	  == "Atomic (NONCE x)"
    1.38 +  "Key x"	  == "Atomic (KEY x)"
    1.39 +  "Key``x"	  == "Atomic `` (KEY `` x)"
    1.40 +
    1.41    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.42    "{|x, y|}"      == "MPair x y"
    1.43  
    1.44 @@ -83,13 +97,15 @@
    1.45  
    1.46  (** Inductive definition of "synth" -- what can be built up from a set of
    1.47      messages.  A form of upward closure.  Pairs can be built, messages
    1.48 -    encrypted with known keys.  Agent names may be quoted.  **)
    1.49 +    encrypted with known keys.  Agent names are public domain.
    1.50 +    Numbers can be guessed, but Nonces cannot be.  **)
    1.51  
    1.52  consts  synth   :: msg set => msg set
    1.53  inductive "synth H"
    1.54    intrs 
    1.55      Inj     "X: H ==> X: synth H"
    1.56      Agent   "Agent agt : synth H"
    1.57 +    Number  "Number n  : synth H"
    1.58      Hash    "X: synth H ==> Hash X : synth H"
    1.59      MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    1.60      Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"