src/HOL/Auth/Message.thy
author paulson
Fri, 28 Jun 1996 15:26:39 +0200
changeset 1839 199243afac2b
child 1913 2809adb15eb0
permissions -rw-r--r--
Proving safety properties of authentication protocols
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Message
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     2
    ID:         $Id$
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     5
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     6
Datatypes of agents and messages;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     7
Inductive relations "parts", "analyze" and "synthesize"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     8
*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     9
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    10
Message = Arith +
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    11
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    12
(*Is there a difference between a nonce and arbitrary numerical data?
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    13
  Do we need a type of nonces?*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    14
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    15
types 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    16
  key = nat
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    17
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    18
consts
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    19
  invKey :: key=>key
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    20
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    21
rules
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    22
  invKey "invKey (invKey K) = K"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    23
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    24
  (*The inverse of a symmetric key is itself;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    25
    that of a public key is the private key and vice versa*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    26
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    27
constdefs
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    28
  isSymKey :: key=>bool
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    29
  "isSymKey K == (invKey K = K)"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    30
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    31
  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    32
    because Crypt is a constructor!  We assume that encryption is injective,
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    33
    which is not true in the real world.  The alternative is to take
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    34
    Crypt as an uninterpreted function symbol satisfying the equation
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    35
    above.  This seems to require moving to ZF and regarding msg as an
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    36
    inductive definition instead of a datatype.*) 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    37
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    38
datatype  (*We allow any number of friendly agents*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    39
  agent = Server | Friend nat | Enemy
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    40
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    41
consts  
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    42
  isEnemy :: agent => bool
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    43
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    44
primrec isEnemy agent
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    45
  isEnemy_Server  "isEnemy Server  = False"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    46
  isEnemy_Friend  "isEnemy (Friend i) = False"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    47
  isEnemy_Enemy   "isEnemy Enemy = True"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    48
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    49
datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    50
  msg = Agent agent
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    51
      | Nonce nat
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    52
      | Key   key
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    53
      | MPair msg msg
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    54
      | Crypt msg key
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    55
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    56
(*Allows messages of the form {|A,B,NA|}, etc...*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    57
syntax
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    58
  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    59
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    60
translations
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    61
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    62
  "{|x, y|}"      == "MPair x y"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    63
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    64
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    65
constdefs  (*Keys useful to decrypt elements of a message set*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    66
  keysFor :: msg set => key set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    67
  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    68
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    69
(** Inductive definition of all "parts" of a message.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    70
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    71
consts  parts   :: msg set => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    72
inductive "parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    73
  intrs 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    74
    Inj     "X: H ==> X: parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    75
    Fst     "{|X,Y|} : parts H ==> X : parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    76
    Snd     "{|X,Y|} : parts H ==> Y : parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    77
    Body    "Crypt X K : parts H ==> X : parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    78
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    79
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    80
(** Inductive definition of "analyze" -- what can be broken down from a set of
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    81
    messages, including keys.  A form of downward closure.  Pairs can
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    82
    be taken apart; messages decrypted with known keys.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    83
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    84
consts  analyze   :: msg set => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    85
inductive "analyze H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    86
  intrs 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    87
    Inj     "X: H ==> X: analyze H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    88
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    89
    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    90
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    91
    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    92
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    93
    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    94
             |] ==> X : analyze H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    95
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    96
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    97
(** Inductive definition of "synthesize" -- what can be built up from a set of
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    98
    messages.  A form of upward closure.  Pairs can be built, messages
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    99
    encrypted with known keys.  Agent names may be quoted.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   100
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   101
consts  synthesize   :: msg set => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   102
inductive "synthesize H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   103
  intrs 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   104
    Inj     "X: H ==> X: synthesize H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   105
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   106
    Agent   "Agent agt : synthesize H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   107
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   108
    MPair   "[| X: synthesize H;  Y: synthesize H
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   109
             |] ==> {|X,Y|} : synthesize H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   110
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   111
    Crypt   "[| X: synthesize H; Key(K): synthesize H
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   112
             |] ==> Crypt X K : synthesize H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   113
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   114
end