src/HOL/Auth/Message.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9686 87b460d72e80
child 10833 c0844a30ea4e
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
5652
fe5f5510aef4 parent is Main
paulson
parents: 5234
diff changeset
    10
Message = Main +
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    11
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    12
types 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    13
  key = nat
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    14
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    15
consts
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    16
  invKey :: key=>key
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    17
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    18
rules
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    19
  invKey "invKey (invKey K) = K"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    20
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    21
  (*The inverse of a symmetric key is itself;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    22
    that of a public key is the private key and vice versa*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    23
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    24
constdefs
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    25
  isSymKey :: key=>bool
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    26
  "isSymKey K == (invKey K = K)"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    27
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    28
datatype  (*We allow any number of friendly agents*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2010
diff changeset
    29
  agent = Server | Friend nat | Spy
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    30
3668
a39baf59ea47 Split base cases from "msg" to "atomic" in order
paulson
parents: 2516
diff changeset
    31
datatype
7057
b9ddbb925939 tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents: 6807
diff changeset
    32
     msg = Agent  agent	    (*Agent names*)
b9ddbb925939 tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents: 6807
diff changeset
    33
         | Number nat       (*Ordinary integers, timestamps, ...*)
b9ddbb925939 tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents: 6807
diff changeset
    34
         | Nonce  nat       (*Unguessable nonces*)
b9ddbb925939 tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents: 6807
diff changeset
    35
         | Key    key       (*Crypto keys*)
5234
701fa0ed77b7 Better comments
paulson
parents: 5183
diff changeset
    36
	 | Hash   msg       (*Hashing*)
701fa0ed77b7 Better comments
paulson
parents: 5183
diff changeset
    37
	 | MPair  msg msg   (*Compound messages*)
701fa0ed77b7 Better comments
paulson
parents: 5183
diff changeset
    38
	 | Crypt  key msg   (*Encryption, public- or shared-key*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    39
5234
701fa0ed77b7 Better comments
paulson
parents: 5183
diff changeset
    40
701fa0ed77b7 Better comments
paulson
parents: 5183
diff changeset
    41
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
701fa0ed77b7 Better comments
paulson
parents: 5183
diff changeset
    42
syntax
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2484
diff changeset
    43
  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    44
9686
87b460d72e80 xsymbols for {| and |}
paulson
parents: 7057
diff changeset
    45
syntax (xsymbols)
87b460d72e80 xsymbols for {| and |}
paulson
parents: 7057
diff changeset
    46
  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\\<lbrace>_,/ _\\<rbrace>)")
87b460d72e80 xsymbols for {| and |}
paulson
parents: 7057
diff changeset
    47
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    48
translations
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    49
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    50
  "{|x, y|}"      == "MPair x y"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    51
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    52
2484
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    53
constdefs
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    54
  (*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
    55
  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
    56
    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
2484
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    57
596a5b5a68ff Incorporation of HPair into Message
paulson
parents: 2373
diff changeset
    58
  (*Keys useful to decrypt elements of a message set*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    59
  keysFor :: msg set => key set
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2121
diff changeset
    60
  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    61
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    62
(** Inductive definition of all "parts" of a message.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    63
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    64
consts  parts   :: msg set => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    65
inductive "parts H"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    66
  intrs 
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    67
    Inj     "X: H  ==>  X: parts H"
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    68
    Fst     "{|X,Y|}   : parts H ==> X : parts H"
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    69
    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
    70
    Body    "Crypt K X : parts H ==> X : parts H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    71
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    72
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    73
(** 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
    74
    messages, including keys.  A form of downward closure.  Pairs can
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    75
    be taken apart; messages decrypted with known keys.  **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    76
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    77
consts  analz   :: msg set => msg set
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    78
inductive "analz H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    79
  intrs 
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    80
    Inj     "X: H ==> X: analz H"
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    81
    Fst     "{|X,Y|} : analz H ==> X : analz H"
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    82
    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
    83
    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
    84
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    85
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    86
(** 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
    87
    messages.  A form of upward closure.  Pairs can be built, messages
3668
a39baf59ea47 Split base cases from "msg" to "atomic" in order
paulson
parents: 2516
diff changeset
    88
    encrypted with known keys.  Agent names are public domain.
a39baf59ea47 Split base cases from "msg" to "atomic" in order
paulson
parents: 2516
diff changeset
    89
    Numbers can be guessed, but Nonces cannot be.  **)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    90
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    91
consts  synth   :: msg set => msg set
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    92
inductive "synth H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    93
  intrs 
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    94
    Inj     "X: H ==> X: synth H"
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    95
    Agent   "Agent agt : synth H"
3668
a39baf59ea47 Split base cases from "msg" to "atomic" in order
paulson
parents: 2516
diff changeset
    96
    Number  "Number n  : synth H"
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    97
    Hash    "X: synth H ==> Hash X : synth H"
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1839
diff changeset
    98
    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
2373
490ffa16952e Addition of the Hash constructor
paulson
parents: 2284
diff changeset
    99
    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   100
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   101
end