src/HOL/Auth/Message.thy
changeset 7057 b9ddbb925939
parent 6807 6737af18317e
child 9686 87b460d72e80
equal deleted inserted replaced
7056:522a7013d7df 7057:b9ddbb925939
    26   "isSymKey K == (invKey K = K)"
    26   "isSymKey K == (invKey K = K)"
    27 
    27 
    28 datatype  (*We allow any number of friendly agents*)
    28 datatype  (*We allow any number of friendly agents*)
    29   agent = Server | Friend nat | Spy
    29   agent = Server | Friend nat | Spy
    30 
    30 
    31 
       
    32 (*Datatype msg is (awkwardly) split into two parts to avoid having freeness
       
    33   expressed using natural numbers.*)
       
    34 datatype  
       
    35   atomic = AGENT  agent	(*Agent names*)
       
    36          | NUMBER nat   (*Ordinary integers, timestamps, ...*)
       
    37          | NONCE  nat   (*Unguessable nonces*)
       
    38          | KEY    key   (*Crypto keys*)
       
    39 
       
    40 datatype
    31 datatype
    41      msg = Atomic atomic
    32      msg = Agent  agent	    (*Agent names*)
       
    33          | Number nat       (*Ordinary integers, timestamps, ...*)
       
    34          | Nonce  nat       (*Unguessable nonces*)
       
    35          | Key    key       (*Crypto keys*)
    42 	 | Hash   msg       (*Hashing*)
    36 	 | Hash   msg       (*Hashing*)
    43 	 | MPair  msg msg   (*Compound messages*)
    37 	 | MPair  msg msg   (*Compound messages*)
    44 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    38 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    45 
       
    46 (*These translations complete the illustion that "msg" has seven constructors*)
       
    47 syntax
       
    48   Agent       :: agent => msg
       
    49   Number      :: nat   => msg
       
    50   Nonce       :: nat   => msg
       
    51   Key         :: key   => msg
       
    52 
       
    53 translations
       
    54   "Agent x"   == "Atomic (AGENT x)"
       
    55   "Number x"  == "Atomic (NUMBER x)"
       
    56   "Nonce x"   == "Atomic (NONCE x)"
       
    57   "Nonce``x"  == "Atomic `` (NONCE `` x)"
       
    58   "Key x"     == "Atomic (KEY x)"
       
    59   "Key``x"    == "Atomic `` (KEY `` x)"
       
    60 
    39 
    61 
    40 
    62 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    41 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    63 syntax
    42 syntax
    64   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    43   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")