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