src/HOL/Auth/Message.thy
author paulson
Thu Jun 10 10:36:41 1999 +0200 (1999-06-10)
changeset 6807 6737af18317e
parent 5652 fe5f5510aef4
child 7057 b9ddbb925939
permissions -rw-r--r--
new translation to allow images over Nonce
paulson@1839
     1
(*  Title:      HOL/Auth/Message
paulson@1839
     2
    ID:         $Id$
paulson@1839
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1839
     4
    Copyright   1996  University of Cambridge
paulson@1839
     5
paulson@1839
     6
Datatypes of agents and messages;
paulson@1913
     7
Inductive relations "parts", "analz" and "synth"
paulson@1839
     8
*)
paulson@1839
     9
paulson@5652
    10
Message = Main +
paulson@1839
    11
paulson@1839
    12
types 
paulson@1839
    13
  key = nat
paulson@1839
    14
paulson@1839
    15
consts
paulson@1839
    16
  invKey :: key=>key
paulson@1839
    17
paulson@1839
    18
rules
paulson@1839
    19
  invKey "invKey (invKey K) = K"
paulson@1839
    20
paulson@1839
    21
  (*The inverse of a symmetric key is itself;
paulson@1839
    22
    that of a public key is the private key and vice versa*)
paulson@1839
    23
paulson@1839
    24
constdefs
paulson@1839
    25
  isSymKey :: key=>bool
paulson@1839
    26
  "isSymKey K == (invKey K = K)"
paulson@1839
    27
paulson@1839
    28
datatype  (*We allow any number of friendly agents*)
paulson@2032
    29
  agent = Server | Friend nat | Spy
paulson@1839
    30
paulson@5234
    31
paulson@5234
    32
(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
paulson@5234
    33
  expressed using natural numbers.*)
paulson@3668
    34
datatype  
paulson@3668
    35
  atomic = AGENT  agent	(*Agent names*)
paulson@3668
    36
         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
paulson@3668
    37
         | NONCE  nat   (*Unguessable nonces*)
paulson@3668
    38
         | KEY    key   (*Crypto keys*)
paulson@3668
    39
paulson@3668
    40
datatype
paulson@5234
    41
     msg = Atomic atomic
paulson@5234
    42
	 | Hash   msg       (*Hashing*)
paulson@5234
    43
	 | MPair  msg msg   (*Compound messages*)
paulson@5234
    44
	 | Crypt  key msg   (*Encryption, public- or shared-key*)
paulson@1839
    45
paulson@5234
    46
(*These translations complete the illustion that "msg" has seven constructors*)
paulson@1839
    47
syntax
paulson@5234
    48
  Agent       :: agent => msg
paulson@5234
    49
  Number      :: nat   => msg
paulson@5234
    50
  Nonce       :: nat   => msg
paulson@5234
    51
  Key         :: key   => msg
paulson@5234
    52
paulson@5234
    53
translations
paulson@5234
    54
  "Agent x"   == "Atomic (AGENT x)"
paulson@5234
    55
  "Number x"  == "Atomic (NUMBER x)"
paulson@5234
    56
  "Nonce x"   == "Atomic (NONCE x)"
paulson@6807
    57
  "Nonce``x"  == "Atomic `` (NONCE `` x)"
paulson@5234
    58
  "Key x"     == "Atomic (KEY x)"
paulson@5234
    59
  "Key``x"    == "Atomic `` (KEY `` x)"
paulson@5234
    60
paulson@5234
    61
paulson@5234
    62
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
paulson@5234
    63
syntax
paulson@2516
    64
  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
paulson@1839
    65
paulson@1839
    66
translations
paulson@1839
    67
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
paulson@1839
    68
  "{|x, y|}"      == "MPair x y"
paulson@1839
    69
paulson@1839
    70
paulson@2484
    71
constdefs
paulson@2484
    72
  (*Message Y, paired with a MAC computed with the help of X*)
paulson@2516
    73
  HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
paulson@2516
    74
    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
paulson@2484
    75
paulson@2484
    76
  (*Keys useful to decrypt elements of a message set*)
paulson@1839
    77
  keysFor :: msg set => key set
paulson@2284
    78
  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
paulson@1839
    79
paulson@1839
    80
(** Inductive definition of all "parts" of a message.  **)
paulson@1839
    81
paulson@1839
    82
consts  parts   :: msg set => msg set
paulson@1839
    83
inductive "parts H"
paulson@1839
    84
  intrs 
paulson@2373
    85
    Inj     "X: H  ==>  X: parts H"
paulson@2373
    86
    Fst     "{|X,Y|}   : parts H ==> X : parts H"
paulson@2373
    87
    Snd     "{|X,Y|}   : parts H ==> Y : parts H"
paulson@2284
    88
    Body    "Crypt K X : parts H ==> X : parts H"
paulson@1839
    89
paulson@1839
    90
paulson@1913
    91
(** Inductive definition of "analz" -- what can be broken down from a set of
paulson@1839
    92
    messages, including keys.  A form of downward closure.  Pairs can
paulson@1839
    93
    be taken apart; messages decrypted with known keys.  **)
paulson@1839
    94
paulson@1913
    95
consts  analz   :: msg set => msg set
paulson@1913
    96
inductive "analz H"
paulson@1839
    97
  intrs 
paulson@1913
    98
    Inj     "X: H ==> X: analz H"
paulson@1913
    99
    Fst     "{|X,Y|} : analz H ==> X : analz H"
paulson@1913
   100
    Snd     "{|X,Y|} : analz H ==> Y : analz H"
paulson@2284
   101
    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
paulson@1839
   102
paulson@1839
   103
paulson@1913
   104
(** Inductive definition of "synth" -- what can be built up from a set of
paulson@1839
   105
    messages.  A form of upward closure.  Pairs can be built, messages
paulson@3668
   106
    encrypted with known keys.  Agent names are public domain.
paulson@3668
   107
    Numbers can be guessed, but Nonces cannot be.  **)
paulson@1839
   108
paulson@1913
   109
consts  synth   :: msg set => msg set
paulson@1913
   110
inductive "synth H"
paulson@1839
   111
  intrs 
paulson@1913
   112
    Inj     "X: H ==> X: synth H"
paulson@1913
   113
    Agent   "Agent agt : synth H"
paulson@3668
   114
    Number  "Number n  : synth H"
paulson@2373
   115
    Hash    "X: synth H ==> Hash X : synth H"
paulson@1913
   116
    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
paulson@2373
   117
    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
paulson@1839
   118
paulson@1839
   119
end