src/HOL/Auth/Message.thy
author paulson
Fri Apr 27 17:16:21 2001 +0200 (2001-04-27)
changeset 11270 a315a3862bb4
parent 11264 a47a9288f3f6
child 13922 75ae4244a596
permissions -rw-r--r--
better treatment of methods: uses Method.ctxt_args to refer to current
simpset and claset. Needed to fix problems with Recur.thy
     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 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   139 
   140 lemma Fake_parts_insert_in_Un:
   141      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   142       ==> Z \<in>  synth (analz H) \<union> parts H";
   143 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   144 
   145 method_setup spy_analz = {*
   146     Method.ctxt_args (fn ctxt =>
   147         Method.METHOD (fn facts => 
   148             gen_spy_analz_tac (Classical.get_local_claset ctxt,
   149                                Simplifier.get_local_simpset ctxt) 1)) *}
   150     "for proving the Fake case when analz is involved"
   151 
   152 method_setup atomic_spy_analz = {*
   153     Method.ctxt_args (fn ctxt =>
   154         Method.METHOD (fn facts => 
   155             atomic_spy_analz_tac (Classical.get_local_claset ctxt,
   156                                   Simplifier.get_local_simpset ctxt) 1)) *}
   157     "for debugging spy_analz"
   158 
   159 method_setup Fake_insert_simp = {*
   160     Method.ctxt_args (fn ctxt =>
   161         Method.METHOD (fn facts =>
   162             Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
   163     "for debugging spy_analz"
   164 
   165 end