src/HOL/Auth/Message.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 2516 4d68fbe6378b
child 3668 a39baf59ea47
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
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;
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
     7
Inductive relations "parts", "analz" and "synth"
1839
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
datatype  (*We allow any number of friendly agents*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2010
diff changeset
    32
  agent = Server | Friend nat | Spy
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    33
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    34
datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    35
  msg = Agent agent
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    36
      | Nonce nat
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    37
      | Key   key
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    38
      | Hash  msg
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    39
      | MPair msg msg
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2121
diff changeset
    40
      | Crypt key msg
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    41
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    42
(*Allows messages of the form {|A,B,NA|}, etc...*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    43
syntax
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2484
diff changeset
    44
  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    45
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    46
translations
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    47
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    48
  "{|x, y|}"      == "MPair x y"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    49
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    50
2484
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    51
constdefs
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    52
  (*Message Y, paired with a MAC computed with the help of X*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2484
diff changeset
    53
  HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2484
diff changeset
    54
    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
2484
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    55
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    56
  (*Keys useful to decrypt elements of a message set*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    57
  keysFor :: msg set => key set
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2121
diff changeset
    58
  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    59
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    60
(** Inductive definition of all "parts" of a message.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    61
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    62
consts  parts   :: msg set => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    63
inductive "parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    64
  intrs 
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    65
    Inj     "X: H  ==>  X: parts H"
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    66
    Fst     "{|X,Y|}   : parts H ==> X : parts H"
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    67
    Snd     "{|X,Y|}   : parts H ==> Y : parts H"
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2121
diff changeset
    68
    Body    "Crypt K X : parts H ==> X : parts H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    69
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    70
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    71
(** Inductive definition of "analz" -- what can be broken down from a set of
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    72
    messages, including keys.  A form of downward closure.  Pairs can
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    73
    be taken apart; messages decrypted with known keys.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    74
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    75
consts  analz   :: msg set => msg set
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    76
inductive "analz H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    77
  intrs 
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    78
    Inj     "X: H ==> X: analz H"
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    79
    Fst     "{|X,Y|} : analz H ==> X : analz H"
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    80
    Snd     "{|X,Y|} : analz H ==> Y : analz H"
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2121
diff changeset
    81
    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    82
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    83
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    84
(** Inductive definition of "synth" -- what can be built up from a set of
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    85
    messages.  A form of upward closure.  Pairs can be built, messages
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    86
    encrypted with known keys.  Agent names may be quoted.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    87
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    88
consts  synth   :: msg set => msg set
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    89
inductive "synth H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    90
  intrs 
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    91
    Inj     "X: H ==> X: synth H"
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    92
    Agent   "Agent agt : synth H"
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    93
    Hash    "X: synth H ==> Hash X : synth H"
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    94
    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    95
    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    96
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    97
end