src/HOL/Auth/Message.thy
author paulson
Mon May 05 18:22:01 2003 +0200 (2003-05-05)
changeset 13956 8fe7e12290e1
parent 13926 6e62e5357a10
child 14126 28824746d046
permissions -rw-r--r--
improved presentation of HOL/Auth theories
     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 header{*Theory of Agents and Messages for Security Protocols*}
    11 
    12 theory Message = Main:
    13 
    14 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    15 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
    16 by blast
    17 
    18 types 
    19   key = nat
    20 
    21 consts
    22   invKey :: "key=>key"
    23 
    24 axioms
    25   invKey [simp] : "invKey (invKey K) = K"
    26 
    27   (*The inverse of a symmetric key is itself;
    28     that of a public key is the private key and vice versa*)
    29 
    30 constdefs
    31   symKeys :: "key set"
    32   "symKeys == {K. invKey K = K}"
    33 
    34 datatype  (*We allow any number of friendly agents*)
    35   agent = Server | Friend nat | Spy
    36 
    37 datatype
    38      msg = Agent  agent	    (*Agent names*)
    39          | Number nat       (*Ordinary integers, timestamps, ...*)
    40          | Nonce  nat       (*Unguessable nonces*)
    41          | Key    key       (*Crypto keys*)
    42 	 | Hash   msg       (*Hashing*)
    43 	 | MPair  msg msg   (*Compound messages*)
    44 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    45 
    46 
    47 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    48 syntax
    49   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    50 
    51 syntax (xsymbols)
    52   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    53 
    54 translations
    55   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    56   "{|x, y|}"      == "MPair x y"
    57 
    58 
    59 constdefs
    60   (*Message Y, paired with a MAC computed with the help of X*)
    61   HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    62     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    63 
    64   (*Keys useful to decrypt elements of a message set*)
    65   keysFor :: "msg set => key set"
    66   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    67 
    68 (** Inductive definition of all "parts" of a message.  **)
    69 
    70 consts  parts   :: "msg set => msg set"
    71 inductive "parts H"
    72   intros 
    73     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    74     Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    75     Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    76     Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    77 
    78 
    79 (*Monotonicity*)
    80 lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
    81 apply auto
    82 apply (erule parts.induct) 
    83 apply (auto dest: Fst Snd Body) 
    84 done
    85 
    86 
    87 (*Equations hold because constructors are injective; cannot prove for all f*)
    88 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    89 by auto
    90 
    91 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
    92 by auto
    93 
    94 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
    95 by auto
    96 
    97 
    98 (** Inverse of keys **)
    99 
   100 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   101 apply safe
   102 apply (drule_tac f = invKey in arg_cong, simp)
   103 done
   104 
   105 
   106 subsection{*keysFor operator*}
   107 
   108 lemma keysFor_empty [simp]: "keysFor {} = {}"
   109 by (unfold keysFor_def, blast)
   110 
   111 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
   112 by (unfold keysFor_def, blast)
   113 
   114 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
   115 by (unfold keysFor_def, blast)
   116 
   117 (*Monotonicity*)
   118 lemma keysFor_mono: "G\<subseteq>H ==> keysFor(G) \<subseteq> keysFor(H)"
   119 by (unfold keysFor_def, blast)
   120 
   121 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
   122 by (unfold keysFor_def, auto)
   123 
   124 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
   125 by (unfold keysFor_def, auto)
   126 
   127 lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
   128 by (unfold keysFor_def, auto)
   129 
   130 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
   131 by (unfold keysFor_def, auto)
   132 
   133 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
   134 by (unfold keysFor_def, auto)
   135 
   136 lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
   137 by (unfold keysFor_def, auto)
   138 
   139 lemma keysFor_insert_Crypt [simp]: 
   140     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
   141 apply (unfold keysFor_def, auto)
   142 done
   143 
   144 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
   145 by (unfold keysFor_def, auto)
   146 
   147 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
   148 by (unfold keysFor_def, blast)
   149 
   150 
   151 subsection{*Inductive relation "parts"*}
   152 
   153 lemma MPair_parts:
   154      "[| {|X,Y|} \<in> parts H;        
   155          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
   156 by (blast dest: parts.Fst parts.Snd) 
   157 
   158 declare MPair_parts [elim!]  parts.Body [dest!]
   159 text{*NB These two rules are UNSAFE in the formal sense, as they discard the
   160      compound message.  They work well on THIS FILE.  
   161   @{text MPair_parts} is left as SAFE because it speeds up proofs.
   162   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
   163 
   164 lemma parts_increasing: "H \<subseteq> parts(H)"
   165 by blast
   166 
   167 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
   168 
   169 lemma parts_empty [simp]: "parts{} = {}"
   170 apply safe
   171 apply (erule parts.induct, blast+)
   172 done
   173 
   174 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
   175 by simp
   176 
   177 (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
   178 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
   179 by (erule parts.induct, blast+)
   180 
   181 
   182 (** Unions **)
   183 
   184 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
   185 by (intro Un_least parts_mono Un_upper1 Un_upper2)
   186 
   187 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
   188 apply (rule subsetI)
   189 apply (erule parts.induct, blast+)
   190 done
   191 
   192 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
   193 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
   194 
   195 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
   196 apply (subst insert_is_Un [of _ H])
   197 apply (simp only: parts_Un)
   198 done
   199 
   200 (*TWO inserts to avoid looping.  This rewrite is better than nothing.
   201   Not suitable for Addsimps: its behaviour can be strange.*)
   202 lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   203 apply (simp add: Un_assoc)
   204 apply (simp add: parts_insert [symmetric])
   205 done
   206 
   207 lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
   208 by (intro UN_least parts_mono UN_upper)
   209 
   210 lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
   211 apply (rule subsetI)
   212 apply (erule parts.induct, blast+)
   213 done
   214 
   215 lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
   216 by (intro equalityI parts_UN_subset1 parts_UN_subset2)
   217 
   218 (*Added to simplify arguments to parts, analz and synth.
   219   NOTE: the UN versions are no longer used!*)
   220 
   221 
   222 text{*This allows @{text blast} to simplify occurrences of 
   223   @{term "parts(G\<union>H)"} in the assumption.*}
   224 declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!] 
   225 
   226 
   227 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
   228 by (blast intro: parts_mono [THEN [2] rev_subsetD])
   229 
   230 (** Idempotence and transitivity **)
   231 
   232 lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
   233 by (erule parts.induct, blast+)
   234 
   235 lemma parts_idem [simp]: "parts (parts H) = parts H"
   236 by blast
   237 
   238 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   239 by (drule parts_mono, blast)
   240 
   241 (*Cut*)
   242 lemma parts_cut: "[| Y\<in> parts (insert X G);  X\<in> parts H |]  
   243                ==> Y\<in> parts (G \<union> H)"
   244 apply (erule parts_trans, auto)
   245 done
   246 
   247 lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
   248 by (force dest!: parts_cut intro: parts_insertI)
   249 
   250 
   251 (** Rewrite rules for pulling out atomic messages **)
   252 
   253 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   254 
   255 
   256 lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   257 apply (rule parts_insert_eq_I) 
   258 apply (erule parts.induct, auto) 
   259 done
   260 
   261 lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   262 apply (rule parts_insert_eq_I) 
   263 apply (erule parts.induct, auto) 
   264 done
   265 
   266 lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)"
   267 apply (rule parts_insert_eq_I) 
   268 apply (erule parts.induct, auto) 
   269 done
   270 
   271 lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)"
   272 apply (rule parts_insert_eq_I) 
   273 apply (erule parts.induct, auto) 
   274 done
   275 
   276 lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   277 apply (rule parts_insert_eq_I) 
   278 apply (erule parts.induct, auto) 
   279 done
   280 
   281 lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) =  
   282           insert (Crypt K X) (parts (insert X H))"
   283 apply (rule equalityI)
   284 apply (rule subsetI)
   285 apply (erule parts.induct, auto)
   286 apply (erule parts.induct)
   287 apply (blast intro: parts.Body)+
   288 done
   289 
   290 lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) =  
   291           insert {|X,Y|} (parts (insert X (insert Y H)))"
   292 apply (rule equalityI)
   293 apply (rule subsetI)
   294 apply (erule parts.induct, auto)
   295 apply (erule parts.induct)
   296 apply (blast intro: parts.Fst parts.Snd)+
   297 done
   298 
   299 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
   300 apply auto
   301 apply (erule parts.induct, auto)
   302 done
   303 
   304 
   305 (*In any message, there is an upper bound N on its greatest nonce.*)
   306 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   307 apply (induct_tac "msg")
   308 apply (simp_all (no_asm_simp) add: exI parts_insert2)
   309 (*MPair case: blast_tac works out the necessary sum itself!*)
   310 prefer 2 apply (blast elim!: add_leE)
   311 (*Nonce case*)
   312 apply (rule_tac x = "N + Suc nat" in exI)
   313 apply (auto elim!: add_leE)
   314 done
   315 
   316 
   317 subsection{*Inductive relation "analz"*}
   318 
   319 (** Inductive definition of "analz" -- what can be broken down from a set of
   320     messages, including keys.  A form of downward closure.  Pairs can
   321     be taken apart; messages decrypted with known keys.  **)
   322 
   323 consts  analz   :: "msg set => msg set"
   324 inductive "analz H"
   325   intros 
   326     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   327     Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   328     Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   329     Decrypt [dest]: 
   330              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   331 
   332 
   333 (*Monotonicity; Lemma 1 of Lowe's paper*)
   334 lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
   335 apply auto
   336 apply (erule analz.induct) 
   337 apply (auto dest: Fst Snd) 
   338 done
   339 
   340 text{*Making it safe speeds up proofs*}
   341 lemma MPair_analz [elim!]:
   342      "[| {|X,Y|} \<in> analz H;        
   343              [| X \<in> analz H; Y \<in> analz H |] ==> P   
   344           |] ==> P"
   345 by (blast dest: analz.Fst analz.Snd)
   346 
   347 lemma analz_increasing: "H \<subseteq> analz(H)"
   348 by blast
   349 
   350 lemma analz_subset_parts: "analz H \<subseteq> parts H"
   351 apply (rule subsetI)
   352 apply (erule analz.induct, blast+)
   353 done
   354 
   355 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   356 
   357 
   358 lemma parts_analz [simp]: "parts (analz H) = parts H"
   359 apply (rule equalityI)
   360 apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
   361 apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
   362 done
   363 
   364 lemma analz_parts [simp]: "analz (parts H) = parts H"
   365 apply auto
   366 apply (erule analz.induct, auto)
   367 done
   368 
   369 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   370 
   371 (** General equational properties **)
   372 
   373 lemma analz_empty [simp]: "analz{} = {}"
   374 apply safe
   375 apply (erule analz.induct, blast+)
   376 done
   377 
   378 (*Converse fails: we can analz more from the union than from the 
   379   separate parts, as a key in one might decrypt a message in the other*)
   380 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   381 by (intro Un_least analz_mono Un_upper1 Un_upper2)
   382 
   383 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   384 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   385 
   386 (** Rewrite rules for pulling out atomic messages **)
   387 
   388 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   389 
   390 lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   391 apply (rule analz_insert_eq_I) 
   392 apply (erule analz.induct, auto) 
   393 done
   394 
   395 lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   396 apply (rule analz_insert_eq_I) 
   397 apply (erule analz.induct, auto) 
   398 done
   399 
   400 lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)"
   401 apply (rule analz_insert_eq_I) 
   402 apply (erule analz.induct, auto) 
   403 done
   404 
   405 lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   406 apply (rule analz_insert_eq_I) 
   407 apply (erule analz.induct, auto) 
   408 done
   409 
   410 (*Can only pull out Keys if they are not needed to decrypt the rest*)
   411 lemma analz_insert_Key [simp]: 
   412     "K \<notin> keysFor (analz H) ==>   
   413           analz (insert (Key K) H) = insert (Key K) (analz H)"
   414 apply (unfold keysFor_def)
   415 apply (rule analz_insert_eq_I) 
   416 apply (erule analz.induct, auto) 
   417 done
   418 
   419 lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) =  
   420           insert {|X,Y|} (analz (insert X (insert Y H)))"
   421 apply (rule equalityI)
   422 apply (rule subsetI)
   423 apply (erule analz.induct, auto)
   424 apply (erule analz.induct)
   425 apply (blast intro: analz.Fst analz.Snd)+
   426 done
   427 
   428 (*Can pull out enCrypted message if the Key is not known*)
   429 lemma analz_insert_Crypt:
   430      "Key (invKey K) \<notin> analz H 
   431       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   432 apply (rule analz_insert_eq_I) 
   433 apply (erule analz.induct, auto) 
   434 
   435 done
   436 
   437 lemma lemma1: "Key (invKey K) \<in> analz H ==>   
   438                analz (insert (Crypt K X) H) \<subseteq>  
   439                insert (Crypt K X) (analz (insert X H))"
   440 apply (rule subsetI)
   441 apply (erule_tac xa = x in analz.induct, auto)
   442 done
   443 
   444 lemma lemma2: "Key (invKey K) \<in> analz H ==>   
   445                insert (Crypt K X) (analz (insert X H)) \<subseteq>  
   446                analz (insert (Crypt K X) H)"
   447 apply auto
   448 apply (erule_tac xa = x in analz.induct, auto)
   449 apply (blast intro: analz_insertI analz.Decrypt)
   450 done
   451 
   452 lemma analz_insert_Decrypt: "Key (invKey K) \<in> analz H ==>   
   453                analz (insert (Crypt K X) H) =  
   454                insert (Crypt K X) (analz (insert X H))"
   455 by (intro equalityI lemma1 lemma2)
   456 
   457 (*Case analysis: either the message is secure, or it is not!
   458   Effective, but can cause subgoals to blow up!
   459   Use with split_if;  apparently split_tac does not cope with patterns
   460   such as "analz (insert (Crypt K X) H)" *)
   461 lemma analz_Crypt_if [simp]:
   462      "analz (insert (Crypt K X) H) =                 
   463           (if (Key (invKey K) \<in> analz H)                 
   464            then insert (Crypt K X) (analz (insert X H))  
   465            else insert (Crypt K X) (analz H))"
   466 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   467 
   468 
   469 (*This rule supposes "for the sake of argument" that we have the key.*)
   470 lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \<subseteq>   
   471            insert (Crypt K X) (analz (insert X H))"
   472 apply (rule subsetI)
   473 apply (erule analz.induct, auto)
   474 done
   475 
   476 
   477 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   478 apply auto
   479 apply (erule analz.induct, auto)
   480 done
   481 
   482 
   483 (** Idempotence and transitivity **)
   484 
   485 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   486 by (erule analz.induct, blast+)
   487 
   488 lemma analz_idem [simp]: "analz (analz H) = analz H"
   489 by blast
   490 
   491 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   492 by (drule analz_mono, blast)
   493 
   494 (*Cut; Lemma 2 of Lowe*)
   495 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   496 by (erule analz_trans, blast)
   497 
   498 (*Cut can be proved easily by induction on
   499    "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   500 *)
   501 
   502 (*This rewrite rule helps in the simplification of messages that involve
   503   the forwarding of unknown components (X).  Without it, removing occurrences
   504   of X can be very complicated. *)
   505 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   506 by (blast intro: analz_cut analz_insertI)
   507 
   508 
   509 (** A congruence rule for "analz" **)
   510 
   511 lemma analz_subset_cong: "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
   512                |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   513 apply clarify
   514 apply (erule analz.induct)
   515 apply (best intro: analz_mono [THEN subsetD])+
   516 done
   517 
   518 lemma analz_cong: "[| analz G = analz G'; analz H = analz H'  
   519                |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   520 apply (intro equalityI analz_subset_cong, simp_all) 
   521 done
   522 
   523 
   524 lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   525 by (force simp only: insert_def intro!: analz_cong)
   526 
   527 (*If there are no pairs or encryptions then analz does nothing*)
   528 lemma analz_trivial: "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   529 apply safe
   530 apply (erule analz.induct, blast+)
   531 done
   532 
   533 (*These two are obsolete (with a single Spy) but cost little to prove...*)
   534 lemma analz_UN_analz_lemma: "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   535 apply (erule analz.induct)
   536 apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   537 done
   538 
   539 lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   540 by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   541 
   542 
   543 subsection{*Inductive relation "synth"*}
   544 
   545 (** Inductive definition of "synth" -- what can be built up from a set of
   546     messages.  A form of upward closure.  Pairs can be built, messages
   547     encrypted with known keys.  Agent names are public domain.
   548     Numbers can be guessed, but Nonces cannot be.  **)
   549 
   550 consts  synth   :: "msg set => msg set"
   551 inductive "synth H"
   552   intros 
   553     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   554     Agent  [intro]:   "Agent agt \<in> synth H"
   555     Number [intro]:   "Number n  \<in> synth H"
   556     Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   557     MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   558     Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   559 
   560 (*Monotonicity*)
   561 lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
   562 apply auto
   563 apply (erule synth.induct) 
   564 apply (auto dest: Fst Snd Body) 
   565 done
   566 
   567 (*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
   568 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   569 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   570 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   571 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   572 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   573 
   574 
   575 lemma synth_increasing: "H \<subseteq> synth(H)"
   576 by blast
   577 
   578 (** Unions **)
   579 
   580 (*Converse fails: we can synth more from the union than from the 
   581   separate parts, building a compound message using elements of each.*)
   582 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   583 by (intro Un_least synth_mono Un_upper1 Un_upper2)
   584 
   585 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   586 by (blast intro: synth_mono [THEN [2] rev_subsetD])
   587 
   588 (** Idempotence and transitivity **)
   589 
   590 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   591 by (erule synth.induct, blast+)
   592 
   593 lemma synth_idem: "synth (synth H) = synth H"
   594 by blast
   595 
   596 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   597 by (drule synth_mono, blast)
   598 
   599 (*Cut; Lemma 2 of Lowe*)
   600 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   601 by (erule synth_trans, blast)
   602 
   603 lemma Agent_synth [simp]: "Agent A \<in> synth H"
   604 by blast
   605 
   606 lemma Number_synth [simp]: "Number n \<in> synth H"
   607 by blast
   608 
   609 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   610 by blast
   611 
   612 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   613 by blast
   614 
   615 lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   616 by blast
   617 
   618 
   619 lemma keysFor_synth [simp]: 
   620     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   621 apply (unfold keysFor_def, blast)
   622 done
   623 
   624 
   625 (*** Combinations of parts, analz and synth ***)
   626 
   627 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   628 apply (rule equalityI)
   629 apply (rule subsetI)
   630 apply (erule parts.induct)
   631 apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] 
   632                     parts.Fst parts.Snd parts.Body)+
   633 done
   634 
   635 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   636 apply (intro equalityI analz_subset_cong)+
   637 apply simp_all
   638 done
   639 
   640 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   641 apply (rule equalityI)
   642 apply (rule subsetI)
   643 apply (erule analz.induct)
   644 prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
   645 apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
   646 done
   647 
   648 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   649 apply (cut_tac H = "{}" in analz_synth_Un)
   650 apply (simp (no_asm_use))
   651 done
   652 
   653 
   654 (** For reasoning about the Fake rule in traces **)
   655 
   656 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   657 by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   658 
   659 (*More specifically for Fake.  Very occasionally we could do with a version
   660   of the form  parts{X} \<subseteq> synth (analz H) \<union> parts H *)
   661 lemma Fake_parts_insert: "X \<in> synth (analz H) ==>  
   662       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   663 apply (drule parts_insert_subset_Un)
   664 apply (simp (no_asm_use))
   665 apply blast
   666 done
   667 
   668 (*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   669 lemma Fake_analz_insert: "X\<in> synth (analz G) ==>  
   670       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   671 apply (rule subsetI)
   672 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   673 prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
   674 apply (simp (no_asm_use))
   675 apply blast
   676 done
   677 
   678 lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   679 by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
   680 
   681 lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   682 by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
   683 
   684 (*Without this equation, other rules for synth and analz would yield
   685   redundant cases*)
   686 lemma MPair_synth_analz [iff]:
   687      "({|X,Y|} \<in> synth (analz H)) =  
   688       (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   689 by blast
   690 
   691 lemma Crypt_synth_analz: "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   692        ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
   693 by blast
   694 
   695 
   696 lemma Hash_synth_analz [simp]: "X \<notin> synth (analz H)  
   697       ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
   698 by blast
   699 
   700 
   701 subsection{*HPair: a combination of Hash and MPair*}
   702 
   703 (*** Freeness ***)
   704 
   705 lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
   706 by (unfold HPair_def, simp)
   707 
   708 lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
   709 by (unfold HPair_def, simp)
   710 
   711 lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
   712 by (unfold HPair_def, simp)
   713 
   714 lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
   715 by (unfold HPair_def, simp)
   716 
   717 lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
   718 by (unfold HPair_def, simp)
   719 
   720 lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
   721 by (unfold HPair_def, simp)
   722 
   723 lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair 
   724                     Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
   725 
   726 declare HPair_neqs [iff]
   727 declare HPair_neqs [symmetric, iff]
   728 
   729 lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
   730 by (simp add: HPair_def)
   731 
   732 lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
   733 by (simp add: HPair_def)
   734 
   735 lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
   736 by (auto simp add: HPair_def)
   737 
   738 
   739 (*** Specialized laws, proved in terms of those for Hash and MPair ***)
   740 
   741 lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
   742 by (simp add: HPair_def)
   743 
   744 lemma parts_insert_HPair [simp]: 
   745     "parts (insert (Hash[X] Y) H) =  
   746      insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
   747 by (simp add: HPair_def)
   748 
   749 lemma analz_insert_HPair [simp]: 
   750     "analz (insert (Hash[X] Y) H) =  
   751      insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
   752 by (simp add: HPair_def)
   753 
   754 lemma HPair_synth_analz [simp]:
   755      "X \<notin> synth (analz H)  
   756     ==> (Hash[X] Y \<in> synth (analz H)) =  
   757         (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
   758 by (simp add: HPair_def)
   759 
   760 
   761 (*We do NOT want Crypt... messages broken up in protocols!!*)
   762 declare parts.Body [rule del]
   763 
   764 
   765 ML
   766 {*
   767 (*ML bindings for definitions and axioms*)
   768 
   769 val invKey = thm "invKey"
   770 val keysFor_def = thm "keysFor_def"
   771 val HPair_def = thm "HPair_def"
   772 val symKeys_def = thm "symKeys_def"
   773 
   774 structure parts =
   775   struct
   776   val induct = thm "parts.induct"
   777   val Inj    = thm "parts.Inj"
   778   val Fst    = thm "parts.Fst"
   779   val Snd    = thm "parts.Snd"
   780   val Body   = thm "parts.Body"
   781   end
   782 
   783 structure analz =
   784   struct
   785   val induct = thm "analz.induct"
   786   val Inj    = thm "analz.Inj"
   787   val Fst    = thm "analz.Fst"
   788   val Snd    = thm "analz.Snd"
   789   val Decrypt = thm "analz.Decrypt"
   790   end
   791 
   792 
   793 (** Rewrites to push in Key and Crypt messages, so that other messages can
   794     be pulled out using the analz_insert rules **)
   795 
   796 fun insComm x y = inst "x" x (inst "y" y insert_commute);
   797 
   798 bind_thms ("pushKeys",
   799            map (insComm "Key ?K") 
   800                    ["Agent ?C", "Nonce ?N", "Number ?N", 
   801 		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
   802 
   803 bind_thms ("pushCrypts",
   804            map (insComm "Crypt ?X ?K") 
   805                      ["Agent ?C", "Nonce ?N", "Number ?N", 
   806 		      "Hash ?X'", "MPair ?X' ?Y"]);
   807 *}
   808 
   809 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   810   re-ordered. *}
   811 lemmas pushes = pushKeys pushCrypts
   812 
   813 
   814 subsection{*Tactics useful for many protocol proofs*}
   815 ML
   816 {*
   817 val parts_mono = thm "parts_mono";
   818 val analz_mono = thm "analz_mono";
   819 val Key_image_eq = thm "Key_image_eq";
   820 val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
   821 val keysFor_Un = thm "keysFor_Un";
   822 val keysFor_mono = thm "keysFor_mono";
   823 val keysFor_image_Key = thm "keysFor_image_Key";
   824 val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
   825 val MPair_parts = thm "MPair_parts";
   826 val parts_increasing = thm "parts_increasing";
   827 val parts_insertI = thm "parts_insertI";
   828 val parts_empty = thm "parts_empty";
   829 val parts_emptyE = thm "parts_emptyE";
   830 val parts_singleton = thm "parts_singleton";
   831 val parts_Un_subset1 = thm "parts_Un_subset1";
   832 val parts_Un_subset2 = thm "parts_Un_subset2";
   833 val parts_insert = thm "parts_insert";
   834 val parts_insert2 = thm "parts_insert2";
   835 val parts_UN_subset1 = thm "parts_UN_subset1";
   836 val parts_UN_subset2 = thm "parts_UN_subset2";
   837 val parts_UN = thm "parts_UN";
   838 val parts_insert_subset = thm "parts_insert_subset";
   839 val parts_partsD = thm "parts_partsD";
   840 val parts_trans = thm "parts_trans";
   841 val parts_cut = thm "parts_cut";
   842 val parts_cut_eq = thm "parts_cut_eq";
   843 val parts_insert_eq_I = thm "parts_insert_eq_I";
   844 val parts_image_Key = thm "parts_image_Key";
   845 val MPair_analz = thm "MPair_analz";
   846 val analz_increasing = thm "analz_increasing";
   847 val analz_subset_parts = thm "analz_subset_parts";
   848 val not_parts_not_analz = thm "not_parts_not_analz";
   849 val parts_analz = thm "parts_analz";
   850 val analz_parts = thm "analz_parts";
   851 val analz_insertI = thm "analz_insertI";
   852 val analz_empty = thm "analz_empty";
   853 val analz_Un = thm "analz_Un";
   854 val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
   855 val analz_image_Key = thm "analz_image_Key";
   856 val analz_analzD = thm "analz_analzD";
   857 val analz_trans = thm "analz_trans";
   858 val analz_cut = thm "analz_cut";
   859 val analz_insert_eq = thm "analz_insert_eq";
   860 val analz_subset_cong = thm "analz_subset_cong";
   861 val analz_cong = thm "analz_cong";
   862 val analz_insert_cong = thm "analz_insert_cong";
   863 val analz_trivial = thm "analz_trivial";
   864 val analz_UN_analz = thm "analz_UN_analz";
   865 val synth_mono = thm "synth_mono";
   866 val synth_increasing = thm "synth_increasing";
   867 val synth_Un = thm "synth_Un";
   868 val synth_insert = thm "synth_insert";
   869 val synth_synthD = thm "synth_synthD";
   870 val synth_trans = thm "synth_trans";
   871 val synth_cut = thm "synth_cut";
   872 val Agent_synth = thm "Agent_synth";
   873 val Number_synth = thm "Number_synth";
   874 val Nonce_synth_eq = thm "Nonce_synth_eq";
   875 val Key_synth_eq = thm "Key_synth_eq";
   876 val Crypt_synth_eq = thm "Crypt_synth_eq";
   877 val keysFor_synth = thm "keysFor_synth";
   878 val parts_synth = thm "parts_synth";
   879 val analz_analz_Un = thm "analz_analz_Un";
   880 val analz_synth_Un = thm "analz_synth_Un";
   881 val analz_synth = thm "analz_synth";
   882 val parts_insert_subset_Un = thm "parts_insert_subset_Un";
   883 val Fake_parts_insert = thm "Fake_parts_insert";
   884 val Fake_analz_insert = thm "Fake_analz_insert";
   885 val analz_conj_parts = thm "analz_conj_parts";
   886 val analz_disj_parts = thm "analz_disj_parts";
   887 val MPair_synth_analz = thm "MPair_synth_analz";
   888 val Crypt_synth_analz = thm "Crypt_synth_analz";
   889 val Hash_synth_analz = thm "Hash_synth_analz";
   890 val pushes = thms "pushes";
   891 
   892 
   893 (*Prove base case (subgoal i) and simplify others.  A typical base case
   894   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   895   alone.*)
   896 fun prove_simple_subgoals_tac i = 
   897     force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
   898     ALLGOALS Asm_simp_tac
   899 
   900 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   901   but this application is no longer necessary if analz_insert_eq is used.
   902   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   903   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   904 
   905 (*Apply rules to break down assumptions of the form
   906   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
   907 *)
   908 val Fake_insert_tac = 
   909     dresolve_tac [impOfSubs Fake_analz_insert,
   910                   impOfSubs Fake_parts_insert] THEN'
   911     eresolve_tac [asm_rl, thm"synth.Inj"];
   912 
   913 fun Fake_insert_simp_tac ss i = 
   914     REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
   915 
   916 fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
   917     (Fake_insert_simp_tac ss 1
   918      THEN
   919      IF_UNSOLVED (Blast.depth_tac
   920 		  (cs addIs [analz_insertI,
   921 				   impOfSubs analz_subset_parts]) 4 1))
   922 
   923 (*The explicit claset and simpset arguments help it work with Isar*)
   924 fun gen_spy_analz_tac (cs,ss) i =
   925   DETERM
   926    (SELECT_GOAL
   927      (EVERY 
   928       [  (*push in occurrences of X...*)
   929        (REPEAT o CHANGED)
   930            (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   931        (*...allowing further simplifications*)
   932        simp_tac ss 1,
   933        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   934        DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
   935 
   936 fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
   937 *}
   938 
   939 (*By default only o_apply is built-in.  But in the presence of eta-expansion
   940   this means that some terms displayed as (f o g) will be rewritten, and others
   941   will not!*)
   942 declare o_def [simp]
   943 
   944 
   945 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
   946 by auto
   947 
   948 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
   949 by auto
   950 
   951 lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
   952 by (simp add: synth_mono analz_mono) 
   953 
   954 lemma Fake_analz_eq [simp]:
   955      "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
   956 apply (drule Fake_analz_insert[of _ _ "H"])
   957 apply (simp add: synth_increasing[THEN Un_absorb2])
   958 apply (drule synth_mono)
   959 apply (simp add: synth_idem)
   960 apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 
   961 done
   962 
   963 
   964 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   965 
   966 lemma Fake_parts_insert_in_Un:
   967      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   968       ==> Z \<in>  synth (analz H) \<union> parts H";
   969 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   970 
   971 text{*Two generalizations of @{text analz_insert_eq}*}
   972 lemma gen_analz_insert_eq [rule_format]:
   973      "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
   974 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
   975 
   976 lemma synth_analz_insert_eq [rule_format]:
   977      "X \<in> synth (analz H) 
   978       ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
   979 apply (erule synth.induct) 
   980 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
   981 done
   982 
   983 lemma Fake_parts_sing:
   984      "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
   985 apply (rule subset_trans) 
   986  apply (erule_tac [2] Fake_parts_insert) 
   987 apply (simp add: parts_mono) 
   988 done
   989 
   990 method_setup spy_analz = {*
   991     Method.ctxt_args (fn ctxt =>
   992         Method.METHOD (fn facts => 
   993             gen_spy_analz_tac (Classical.get_local_claset ctxt,
   994                                Simplifier.get_local_simpset ctxt) 1)) *}
   995     "for proving the Fake case when analz is involved"
   996 
   997 method_setup atomic_spy_analz = {*
   998     Method.ctxt_args (fn ctxt =>
   999         Method.METHOD (fn facts => 
  1000             atomic_spy_analz_tac (Classical.get_local_claset ctxt,
  1001                                   Simplifier.get_local_simpset ctxt) 1)) *}
  1002     "for debugging spy_analz"
  1003 
  1004 method_setup Fake_insert_simp = {*
  1005     Method.ctxt_args (fn ctxt =>
  1006         Method.METHOD (fn facts =>
  1007             Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
  1008     "for debugging spy_analz"
  1009 
  1010 
  1011 end