src/HOL/Auth/Message.thy
changeset 7057 b9ddbb925939
parent 6807 6737af18317e
child 9686 87b460d72e80
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Jul 21 15:20:26 1999 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Jul 21 15:22:11 1999 +0200
     1.3 @@ -28,36 +28,15 @@
     1.4  datatype  (*We allow any number of friendly agents*)
     1.5    agent = Server | Friend nat | Spy
     1.6  
     1.7 -
     1.8 -(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
     1.9 -  expressed using natural numbers.*)
    1.10 -datatype  
    1.11 -  atomic = AGENT  agent	(*Agent names*)
    1.12 -         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
    1.13 -         | NONCE  nat   (*Unguessable nonces*)
    1.14 -         | KEY    key   (*Crypto keys*)
    1.15 -
    1.16  datatype
    1.17 -     msg = Atomic atomic
    1.18 +     msg = Agent  agent	    (*Agent names*)
    1.19 +         | Number nat       (*Ordinary integers, timestamps, ...*)
    1.20 +         | Nonce  nat       (*Unguessable nonces*)
    1.21 +         | Key    key       (*Crypto keys*)
    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 -(*These translations complete the illustion that "msg" has seven constructors*)
    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 -
    1.33 -translations
    1.34 -  "Agent x"   == "Atomic (AGENT x)"
    1.35 -  "Number x"  == "Atomic (NUMBER x)"
    1.36 -  "Nonce x"   == "Atomic (NONCE 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  
    1.42  (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    1.43  syntax