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