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