src/HOL/Auth/Message.thy
author paulson
Fri Apr 25 11:18:14 2003 +0200 (2003-04-25)
changeset 13922 75ae4244a596
parent 11270 a315a3862bb4
child 13926 6e62e5357a10
permissions -rw-r--r--
Changes required by the certified email protocol

Public-key model now provides separate signature/encryption keys and also
long-term symmetric keys.
     1 (*  Title:      HOL/Auth/Message
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Datatypes of agents and messages;
     7 Inductive relations "parts", "analz" and "synth"
     8 *)
     9 
    10 theory Message = Main
    11 files ("Message_lemmas.ML"):
    12 
    13 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    14 lemma [simp] : "A Un (B Un A) = B Un A"
    15 by blast
    16 
    17 types 
    18   key = nat
    19 
    20 consts
    21   invKey :: "key=>key"
    22 
    23 axioms
    24   invKey [simp] : "invKey (invKey K) = K"
    25 
    26   (*The inverse of a symmetric key is itself;
    27     that of a public key is the private key and vice versa*)
    28 
    29 constdefs
    30   symKeys :: "key set"
    31   "symKeys == {K. invKey K = K}"
    32 
    33 datatype  (*We allow any number of friendly agents*)
    34   agent = Server | Friend nat | Spy
    35 
    36 datatype
    37      msg = Agent  agent	    (*Agent names*)
    38          | Number nat       (*Ordinary integers, timestamps, ...*)
    39          | Nonce  nat       (*Unguessable nonces*)
    40          | Key    key       (*Crypto keys*)
    41 	 | Hash   msg       (*Hashing*)
    42 	 | MPair  msg msg   (*Compound messages*)
    43 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    44 
    45 
    46 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    47 syntax
    48   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    49 
    50 syntax (xsymbols)
    51   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    52 
    53 translations
    54   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    55   "{|x, y|}"      == "MPair x y"
    56 
    57 
    58 constdefs
    59   (*Message Y, paired with a MAC computed with the help of X*)
    60   HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    61     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    62 
    63   (*Keys useful to decrypt elements of a message set*)
    64   keysFor :: "msg set => key set"
    65   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    66 
    67 (** Inductive definition of all "parts" of a message.  **)
    68 
    69 consts  parts   :: "msg set => msg set"
    70 inductive "parts H"
    71   intros 
    72     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    73     Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    74     Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    75     Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    76 
    77 
    78 (*Monotonicity*)
    79 lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
    80 apply auto
    81 apply (erule parts.induct) 
    82 apply (auto dest: Fst Snd Body) 
    83 done
    84 
    85 
    86 (** Inductive definition of "analz" -- what can be broken down from a set of
    87     messages, including keys.  A form of downward closure.  Pairs can
    88     be taken apart; messages decrypted with known keys.  **)
    89 
    90 consts  analz   :: "msg set => msg set"
    91 inductive "analz H"
    92   intros 
    93     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
    94     Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    95     Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    96     Decrypt [dest]: 
    97              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
    98 
    99 
   100 (*Monotonicity; Lemma 1 of Lowe's paper*)
   101 lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
   102 apply auto
   103 apply (erule analz.induct) 
   104 apply (auto dest: Fst Snd) 
   105 done
   106 
   107 (** Inductive definition of "synth" -- what can be built up from a set of
   108     messages.  A form of upward closure.  Pairs can be built, messages
   109     encrypted with known keys.  Agent names are public domain.
   110     Numbers can be guessed, but Nonces cannot be.  **)
   111 
   112 consts  synth   :: "msg set => msg set"
   113 inductive "synth H"
   114   intros 
   115     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   116     Agent  [intro]:   "Agent agt \<in> synth H"
   117     Number [intro]:   "Number n  \<in> synth H"
   118     Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   119     MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   120     Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   121 
   122 (*Monotonicity*)
   123 lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
   124 apply auto
   125 apply (erule synth.induct) 
   126 apply (auto dest: Fst Snd Body) 
   127 done
   128 
   129 (*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
   130 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   131 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   132 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   133 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   134 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   135 
   136 use "Message_lemmas.ML"
   137 
   138 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
   139 by auto
   140 
   141 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
   142 by auto
   143 
   144 lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
   145 by (simp add: synth_mono analz_mono) 
   146 
   147 lemma Fake_analz_eq [simp]:
   148      "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
   149 apply (drule Fake_analz_insert[of _ _ "H"])
   150 apply (simp add: synth_increasing[THEN Un_absorb2])
   151 apply (drule synth_mono)
   152 apply (simp add: synth_idem)
   153 apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 
   154 done
   155 
   156 
   157 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   158 
   159 lemma Fake_parts_insert_in_Un:
   160      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   161       ==> Z \<in>  synth (analz H) \<union> parts H";
   162 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   163 
   164 text{*Two generalizations of @{text analz_insert_eq}*}
   165 lemma gen_analz_insert_eq [rule_format]:
   166      "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
   167 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
   168 
   169 lemma synth_analz_insert_eq [rule_format]:
   170      "X \<in> synth (analz H) 
   171       ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
   172 apply (erule synth.induct) 
   173 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
   174 done
   175 
   176 lemma Fake_parts_sing:
   177      "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) Un parts H";
   178 apply (rule subset_trans) 
   179  apply (erule_tac [2] Fake_parts_insert) 
   180 apply (simp add: parts_mono) 
   181 done
   182 
   183 method_setup spy_analz = {*
   184     Method.ctxt_args (fn ctxt =>
   185         Method.METHOD (fn facts => 
   186             gen_spy_analz_tac (Classical.get_local_claset ctxt,
   187                                Simplifier.get_local_simpset ctxt) 1)) *}
   188     "for proving the Fake case when analz is involved"
   189 
   190 method_setup atomic_spy_analz = {*
   191     Method.ctxt_args (fn ctxt =>
   192         Method.METHOD (fn facts => 
   193             atomic_spy_analz_tac (Classical.get_local_claset ctxt,
   194                                   Simplifier.get_local_simpset ctxt) 1)) *}
   195     "for debugging spy_analz"
   196 
   197 method_setup Fake_insert_simp = {*
   198     Method.ctxt_args (fn ctxt =>
   199         Method.METHOD (fn facts =>
   200             Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
   201     "for debugging spy_analz"
   202 
   203 end