src/HOL/Auth/Message.thy
author paulson
Mon Mar 05 12:31:31 2001 +0100 (2001-03-05)
changeset 11192 5fd02b905a9a
parent 11189 1ea763a5d186
child 11230 756c5034f08b
permissions -rw-r--r--
a few basic X-symbols
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@11189
    10
theory Message = Main
paulson@11189
    11
files ("Message_lemmas.ML"):
paulson@11189
    12
paulson@11189
    13
(*Eliminates a commonly-occurring expression*)
paulson@11192
    14
lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
paulson@11189
    15
by blast
paulson@11189
    16
paulson@11189
    17
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
paulson@11189
    18
lemma [simp] : "A Un (B Un A) = B Un A"
paulson@11189
    19
by blast
paulson@1839
    20
paulson@1839
    21
types 
paulson@1839
    22
  key = nat
paulson@1839
    23
paulson@1839
    24
consts
paulson@11189
    25
  invKey :: "key=>key"
paulson@1839
    26
paulson@11189
    27
axioms
paulson@11189
    28
  invKey [simp] : "invKey (invKey K) = K"
paulson@1839
    29
paulson@1839
    30
  (*The inverse of a symmetric key is itself;
paulson@1839
    31
    that of a public key is the private key and vice versa*)
paulson@1839
    32
paulson@1839
    33
constdefs
paulson@11189
    34
  isSymKey :: "key=>bool"
paulson@1839
    35
  "isSymKey K == (invKey K = K)"
paulson@1839
    36
paulson@1839
    37
datatype  (*We allow any number of friendly agents*)
paulson@2032
    38
  agent = Server | Friend nat | Spy
paulson@1839
    39
paulson@3668
    40
datatype
paulson@7057
    41
     msg = Agent  agent	    (*Agent names*)
paulson@7057
    42
         | Number nat       (*Ordinary integers, timestamps, ...*)
paulson@7057
    43
         | Nonce  nat       (*Unguessable nonces*)
paulson@7057
    44
         | Key    key       (*Crypto keys*)
paulson@5234
    45
	 | Hash   msg       (*Hashing*)
paulson@5234
    46
	 | MPair  msg msg   (*Compound messages*)
paulson@5234
    47
	 | Crypt  key msg   (*Encryption, public- or shared-key*)
paulson@1839
    48
paulson@5234
    49
paulson@5234
    50
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
paulson@5234
    51
syntax
paulson@2516
    52
  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
paulson@1839
    53
paulson@9686
    54
syntax (xsymbols)
paulson@11189
    55
  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
paulson@9686
    56
paulson@1839
    57
translations
paulson@1839
    58
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
paulson@1839
    59
  "{|x, y|}"      == "MPair x y"
paulson@1839
    60
paulson@1839
    61
paulson@2484
    62
constdefs
paulson@2484
    63
  (*Message Y, paired with a MAC computed with the help of X*)
paulson@11189
    64
  HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
paulson@2516
    65
    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
paulson@2484
    66
paulson@2484
    67
  (*Keys useful to decrypt elements of a message set*)
paulson@11189
    68
  keysFor :: "msg set => key set"
paulson@11192
    69
  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
paulson@1839
    70
paulson@1839
    71
(** Inductive definition of all "parts" of a message.  **)
paulson@1839
    72
paulson@11189
    73
consts  parts   :: "msg set => msg set"
paulson@1839
    74
inductive "parts H"
paulson@11189
    75
  intros 
paulson@11192
    76
    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
paulson@11192
    77
    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
paulson@11192
    78
    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
paulson@11192
    79
    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
paulson@11189
    80
paulson@11189
    81
paulson@11189
    82
(*Monotonicity*)
paulson@11189
    83
lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
paulson@11189
    84
apply auto
paulson@11189
    85
apply (erule parts.induct) 
paulson@11189
    86
apply (auto dest: Fst Snd Body) 
paulson@11189
    87
done
paulson@1839
    88
paulson@1839
    89
paulson@1913
    90
(** Inductive definition of "analz" -- what can be broken down from a set of
paulson@1839
    91
    messages, including keys.  A form of downward closure.  Pairs can
paulson@1839
    92
    be taken apart; messages decrypted with known keys.  **)
paulson@1839
    93
paulson@11189
    94
consts  analz   :: "msg set => msg set"
paulson@1913
    95
inductive "analz H"
paulson@11189
    96
  intros 
paulson@11192
    97
    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
paulson@11192
    98
    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
paulson@11192
    99
    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
paulson@11189
   100
    Decrypt [dest]: 
paulson@11192
   101
             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
paulson@1839
   102
paulson@1839
   103
paulson@11189
   104
(*Monotonicity; Lemma 1 of Lowe's paper*)
paulson@11189
   105
lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
paulson@11189
   106
apply auto
paulson@11189
   107
apply (erule analz.induct) 
paulson@11189
   108
apply (auto dest: Fst Snd) 
paulson@11189
   109
done
paulson@11189
   110
paulson@1913
   111
(** Inductive definition of "synth" -- what can be built up from a set of
paulson@1839
   112
    messages.  A form of upward closure.  Pairs can be built, messages
paulson@3668
   113
    encrypted with known keys.  Agent names are public domain.
paulson@3668
   114
    Numbers can be guessed, but Nonces cannot be.  **)
paulson@1839
   115
paulson@11189
   116
consts  synth   :: "msg set => msg set"
paulson@1913
   117
inductive "synth H"
paulson@11189
   118
  intros 
paulson@11192
   119
    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
paulson@11192
   120
    Agent  [intro]:   "Agent agt \<in> synth H"
paulson@11192
   121
    Number [intro]:   "Number n  \<in> synth H"
paulson@11192
   122
    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
paulson@11192
   123
    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
paulson@11192
   124
    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
paulson@11189
   125
paulson@11189
   126
(*Monotonicity*)
paulson@11189
   127
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
paulson@11189
   128
apply auto
paulson@11189
   129
apply (erule synth.induct) 
paulson@11189
   130
apply (auto dest: Fst Snd Body) 
paulson@11189
   131
done
paulson@11189
   132
paulson@11189
   133
(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
paulson@11192
   134
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
paulson@11192
   135
inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
paulson@11192
   136
inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
paulson@11192
   137
inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
paulson@11192
   138
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
paulson@11189
   139
paulson@11189
   140
use "Message_lemmas.ML"
paulson@11189
   141
paulson@11189
   142
method_setup spy_analz = {*
paulson@11189
   143
    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
paulson@11189
   144
    "for proving the Fake case when analz is involved"
paulson@1839
   145
paulson@1839
   146
end