src/HOL/Auth/Message.thy
changeset 11189 1ea763a5d186
parent 10833 c0844a30ea4e
child 11192 5fd02b905a9a
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 02 13:14:37 2001 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Mar 02 13:18:31 2001 +0100
     1.3 @@ -7,22 +7,31 @@
     1.4  Inductive relations "parts", "analz" and "synth"
     1.5  *)
     1.6  
     1.7 -Message = Main +
     1.8 +theory Message = Main
     1.9 +files ("Message_lemmas.ML"):
    1.10 +
    1.11 +(*Eliminates a commonly-occurring expression*)
    1.12 +lemma [simp] : "~ (ALL x. x~=y)"
    1.13 +by blast
    1.14 +
    1.15 +(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.16 +lemma [simp] : "A Un (B Un A) = B Un A"
    1.17 +by blast
    1.18  
    1.19  types 
    1.20    key = nat
    1.21  
    1.22  consts
    1.23 -  invKey :: key=>key
    1.24 +  invKey :: "key=>key"
    1.25  
    1.26 -rules
    1.27 -  invKey "invKey (invKey K) = K"
    1.28 +axioms
    1.29 +  invKey [simp] : "invKey (invKey K) = K"
    1.30  
    1.31    (*The inverse of a symmetric key is itself;
    1.32      that of a public key is the private key and vice versa*)
    1.33  
    1.34  constdefs
    1.35 -  isSymKey :: key=>bool
    1.36 +  isSymKey :: "key=>bool"
    1.37    "isSymKey K == (invKey K = K)"
    1.38  
    1.39  datatype  (*We allow any number of friendly agents*)
    1.40 @@ -43,7 +52,7 @@
    1.41    "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    1.42  
    1.43  syntax (xsymbols)
    1.44 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\\<lbrace>_,/ _\\<rbrace>)")
    1.45 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.46  
    1.47  translations
    1.48    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.49 @@ -52,50 +61,86 @@
    1.50  
    1.51  constdefs
    1.52    (*Message Y, paired with a MAC computed with the help of X*)
    1.53 -  HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
    1.54 +  HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    1.55      "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    1.56  
    1.57    (*Keys useful to decrypt elements of a message set*)
    1.58 -  keysFor :: msg set => key set
    1.59 +  keysFor :: "msg set => key set"
    1.60    "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
    1.61  
    1.62  (** Inductive definition of all "parts" of a message.  **)
    1.63  
    1.64 -consts  parts   :: msg set => msg set
    1.65 +consts  parts   :: "msg set => msg set"
    1.66  inductive "parts H"
    1.67 -  intrs 
    1.68 -    Inj     "X: H  ==>  X: parts H"
    1.69 -    Fst     "{|X,Y|}   : parts H ==> X : parts H"
    1.70 -    Snd     "{|X,Y|}   : parts H ==> Y : parts H"
    1.71 -    Body    "Crypt K X : parts H ==> X : parts H"
    1.72 +  intros 
    1.73 +    Inj [intro]          : "X: H  ==> X : parts H"
    1.74 +    Fst:     "{|X,Y|}   : parts H ==> X : parts H"
    1.75 +    Snd:     "{|X,Y|}   : parts H ==> Y : parts H"
    1.76 +    Body:    "Crypt K X : parts H ==> X : parts H"
    1.77 +
    1.78 +
    1.79 +(*Monotonicity*)
    1.80 +lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
    1.81 +apply auto
    1.82 +apply (erule parts.induct) 
    1.83 +apply (auto dest: Fst Snd Body) 
    1.84 +done
    1.85  
    1.86  
    1.87  (** Inductive definition of "analz" -- what can be broken down from a set of
    1.88      messages, including keys.  A form of downward closure.  Pairs can
    1.89      be taken apart; messages decrypted with known keys.  **)
    1.90  
    1.91 -consts  analz   :: msg set => msg set
    1.92 +consts  analz   :: "msg set => msg set"
    1.93  inductive "analz H"
    1.94 -  intrs 
    1.95 -    Inj     "X: H ==> X: analz H"
    1.96 -    Fst     "{|X,Y|} : analz H ==> X : analz H"
    1.97 -    Snd     "{|X,Y|} : analz H ==> Y : analz H"
    1.98 -    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
    1.99 +  intros 
   1.100 +    Inj [intro,simp] :    "X: H ==> X: analz H"
   1.101 +    Fst:     "{|X,Y|} : analz H ==> X : analz H"
   1.102 +    Snd:     "{|X,Y|} : analz H ==> Y : analz H"
   1.103 +    Decrypt [dest]: 
   1.104 +             "[|Crypt K X : analz H; Key(invKey K): analz H|] ==> X : analz H"
   1.105  
   1.106  
   1.107 +(*Monotonicity; Lemma 1 of Lowe's paper*)
   1.108 +lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
   1.109 +apply auto
   1.110 +apply (erule analz.induct) 
   1.111 +apply (auto dest: Fst Snd) 
   1.112 +done
   1.113 +
   1.114  (** Inductive definition of "synth" -- what can be built up from a set of
   1.115      messages.  A form of upward closure.  Pairs can be built, messages
   1.116      encrypted with known keys.  Agent names are public domain.
   1.117      Numbers can be guessed, but Nonces cannot be.  **)
   1.118  
   1.119 -consts  synth   :: msg set => msg set
   1.120 +consts  synth   :: "msg set => msg set"
   1.121  inductive "synth H"
   1.122 -  intrs 
   1.123 -    Inj     "X: H ==> X: synth H"
   1.124 -    Agent   "Agent agt : synth H"
   1.125 -    Number  "Number n  : synth H"
   1.126 -    Hash    "X: synth H ==> Hash X : synth H"
   1.127 -    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
   1.128 -    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
   1.129 +  intros 
   1.130 +    Inj    [intro]:   "X: H ==> X: synth H"
   1.131 +    Agent  [intro]:   "Agent agt : synth H"
   1.132 +    Number [intro]:   "Number n  : synth H"
   1.133 +    Hash   [intro]:   "X: synth H ==> Hash X : synth H"
   1.134 +    MPair  [intro]:   "[|X: synth H;  Y: synth H|] ==> {|X,Y|} : synth H"
   1.135 +    Crypt  [intro]:   "[|X: synth H;  Key(K) : H|] ==> Crypt K X : synth H"
   1.136 +
   1.137 +(*Monotonicity*)
   1.138 +lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
   1.139 +apply auto
   1.140 +apply (erule synth.induct) 
   1.141 +apply (auto dest: Fst Snd Body) 
   1.142 +done
   1.143 +
   1.144 +(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
   1.145 +inductive_cases Nonce_synth [elim!]: "Nonce n : synth H"
   1.146 +inductive_cases Key_synth   [elim!]: "Key K : synth H"
   1.147 +inductive_cases Hash_synth  [elim!]: "Hash X : synth H"
   1.148 +inductive_cases MPair_synth [elim!]: "{|X,Y|} : synth H"
   1.149 +inductive_cases Crypt_synth [elim!]: "Crypt K X : synth H"
   1.150 +
   1.151 +use "Message_lemmas.ML"
   1.152 +
   1.153 +method_setup spy_analz = {*
   1.154 +    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
   1.155 +    "for proving the Fake case when analz is involved"
   1.156  
   1.157  end