src/HOL/Auth/Message.thy
author paulson
Fri Mar 02 13:18:31 2001 +0100 (2001-03-02)
changeset 11189 1ea763a5d186
parent 10833 c0844a30ea4e
child 11192 5fd02b905a9a
permissions -rw-r--r--
conversion of Message.thy to Isar format
     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] : "~ (ALL x. x~=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. EX X. Crypt K X : 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: H  ==> X : parts H"
    77     Fst:     "{|X,Y|}   : parts H ==> X : parts H"
    78     Snd:     "{|X,Y|}   : parts H ==> Y : parts H"
    79     Body:    "Crypt K X : parts H ==> X : 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: H ==> X: analz H"
    98     Fst:     "{|X,Y|} : analz H ==> X : analz H"
    99     Snd:     "{|X,Y|} : analz H ==> Y : analz H"
   100     Decrypt [dest]: 
   101              "[|Crypt K X : analz H; Key(invKey K): analz H|] ==> X : 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: H ==> X: synth H"
   120     Agent  [intro]:   "Agent agt : synth H"
   121     Number [intro]:   "Number n  : synth H"
   122     Hash   [intro]:   "X: synth H ==> Hash X : synth H"
   123     MPair  [intro]:   "[|X: synth H;  Y: synth H|] ==> {|X,Y|} : synth H"
   124     Crypt  [intro]:   "[|X: synth H;  Key(K) : H|] ==> Crypt K X : 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 : synth H"
   135 inductive_cases Key_synth   [elim!]: "Key K : synth H"
   136 inductive_cases Hash_synth  [elim!]: "Hash X : synth H"
   137 inductive_cases MPair_synth [elim!]: "{|X,Y|} : synth H"
   138 inductive_cases Crypt_synth [elim!]: "Crypt K X : 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