doc-src/TutorialI/Protocol/Message.thy
author wenzelm
Thu Feb 11 21:33:25 2010 +0100 (2010-02-11)
changeset 35109 0015a0a99ae9
parent 32960 69916a850301
child 35416 d8d7d1b785af
permissions -rw-r--r--
modernized syntax/translations;
     1 (*  Title:      HOL/Auth/Message
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1996  University of Cambridge
     4 
     5 Datatypes of agents and messages;
     6 Inductive relations "parts", "analz" and "synth"
     7 *)(*<*)
     8 
     9 header{*Theory of Agents and Messages for Security Protocols*}
    10 
    11 theory Message imports Main uses "../../antiquote_setup.ML" begin
    12 
    13 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    14 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
    15 by blast
    16 (*>*)
    17 
    18 section{* Agents and Messages *}
    19 
    20 text {*
    21 All protocol specifications refer to a syntactic theory of messages. 
    22 Datatype
    23 @{text agent} introduces the constant @{text Server} (a trusted central
    24 machine, needed for some protocols), an infinite population of
    25 friendly agents, and the~@{text Spy}:
    26 *}
    27 
    28 datatype agent = Server | Friend nat | Spy
    29 
    30 text {*
    31 Keys are just natural numbers.  Function @{text invKey} maps a public key to
    32 the matching private key, and vice versa:
    33 *}
    34 
    35 types key = nat
    36 consts invKey :: "key \<Rightarrow> key"
    37 (*<*)
    38 consts all_symmetric :: bool        --{*true if all keys are symmetric*}
    39 
    40 specification (invKey)
    41   invKey [simp]: "invKey (invKey K) = K"
    42   invKey_symmetric: "all_symmetric --> invKey = id"
    43     by (rule exI [of _ id], auto)
    44 
    45 
    46 text{*The inverse of a symmetric key is itself; that of a public key
    47       is the private key and vice versa*}
    48 
    49 constdefs
    50   symKeys :: "key set"
    51   "symKeys == {K. invKey K = K}"
    52 (*>*)
    53 
    54 text {*
    55 Datatype
    56 @{text msg} introduces the message forms, which include agent names, nonces,
    57 keys, compound messages, and encryptions.  
    58 *}
    59 
    60 datatype
    61      msg = Agent  agent
    62          | Nonce  nat
    63          | Key    key
    64          | MPair  msg msg
    65          | Crypt  key msg
    66 
    67 text {*
    68 \noindent
    69 The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$
    70 abbreviates
    71 $\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$.
    72 
    73 Since datatype constructors are injective, we have the theorem
    74 @{thm [display,indent=0] msg.inject(5) [THEN iffD1, of K X K' X']}
    75 A ciphertext can be decrypted using only one key and
    76 can yield only one plaintext.  In the real world, decryption with the
    77 wrong key succeeds but yields garbage.  Our model of encryption is
    78 realistic if encryption adds some redundancy to the plaintext, such as a
    79 checksum, so that garbage can be detected.
    80 *}
    81 
    82 (*<*)
    83 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
    84 syntax
    85   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    86 
    87 syntax (xsymbols)
    88   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    89 
    90 translations
    91   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    92   "{|x, y|}"      == "CONST MPair x y"
    93 
    94 
    95 constdefs
    96   keysFor :: "msg set => key set"
    97     --{*Keys useful to decrypt elements of a message set*}
    98   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    99 
   100 
   101 subsubsection{*Inductive Definition of All Parts" of a Message*}
   102 
   103 inductive_set
   104   parts :: "msg set => msg set"
   105   for H :: "msg set"
   106   where
   107     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
   108   | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
   109   | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
   110   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
   111 
   112 
   113 text{*Monotonicity*}
   114 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
   115 apply auto
   116 apply (erule parts.induct) 
   117 apply (blast dest: parts.Fst parts.Snd parts.Body)+
   118 done
   119 
   120 
   121 text{*Equations hold because constructors are injective.*}
   122 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
   123 by auto
   124 
   125 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
   126 by auto
   127 
   128 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
   129 by auto
   130 
   131 
   132 subsubsection{*Inverse of keys *}
   133 
   134 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   135 apply safe
   136 apply (drule_tac f = invKey in arg_cong, simp)
   137 done
   138 
   139 
   140 subsection{*keysFor operator*}
   141 
   142 lemma keysFor_empty [simp]: "keysFor {} = {}"
   143 by (unfold keysFor_def, blast)
   144 
   145 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
   146 by (unfold keysFor_def, blast)
   147 
   148 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
   149 by (unfold keysFor_def, blast)
   150 
   151 text{*Monotonicity*}
   152 lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
   153 by (unfold keysFor_def, blast)
   154 
   155 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
   156 by (unfold keysFor_def, auto)
   157 
   158 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
   159 by (unfold keysFor_def, auto)
   160 
   161 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
   162 by (unfold keysFor_def, auto)
   163 
   164 lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
   165 by (unfold keysFor_def, auto)
   166 
   167 lemma keysFor_insert_Crypt [simp]: 
   168     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
   169 by (unfold keysFor_def, auto)
   170 
   171 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
   172 by (unfold keysFor_def, auto)
   173 
   174 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
   175 by (unfold keysFor_def, blast)
   176 
   177 
   178 subsection{*Inductive relation "parts"*}
   179 
   180 lemma MPair_parts:
   181      "[| {|X,Y|} \<in> parts H;        
   182          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
   183 by (blast dest: parts.Fst parts.Snd) 
   184 
   185 declare MPair_parts [elim!]  parts.Body [dest!]
   186 text{*NB These two rules are UNSAFE in the formal sense, as they discard the
   187      compound message.  They work well on THIS FILE.  
   188   @{text MPair_parts} is left as SAFE because it speeds up proofs.
   189   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
   190 
   191 lemma parts_increasing: "H \<subseteq> parts(H)"
   192 by blast
   193 
   194 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
   195 
   196 lemma parts_empty [simp]: "parts{} = {}"
   197 apply safe
   198 apply (erule parts.induct, blast+)
   199 done
   200 
   201 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
   202 by simp
   203 
   204 text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
   205 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
   206 by (erule parts.induct, fast+)
   207 
   208 
   209 subsubsection{*Unions *}
   210 
   211 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
   212 by (intro Un_least parts_mono Un_upper1 Un_upper2)
   213 
   214 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
   215 apply (rule subsetI)
   216 apply (erule parts.induct, blast+)
   217 done
   218 
   219 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
   220 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
   221 
   222 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
   223 apply (subst insert_is_Un [of _ H])
   224 apply (simp only: parts_Un)
   225 done
   226 
   227 text{*TWO inserts to avoid looping.  This rewrite is better than nothing.
   228   Not suitable for Addsimps: its behaviour can be strange.*}
   229 lemma parts_insert2:
   230      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   231 apply (simp add: Un_assoc)
   232 apply (simp add: parts_insert [symmetric])
   233 done
   234 
   235 lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
   236 by (intro UN_least parts_mono UN_upper)
   237 
   238 lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
   239 apply (rule subsetI)
   240 apply (erule parts.induct, blast+)
   241 done
   242 
   243 lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
   244 by (intro equalityI parts_UN_subset1 parts_UN_subset2)
   245 
   246 text{*Added to simplify arguments to parts, analz and synth.
   247   NOTE: the UN versions are no longer used!*}
   248 
   249 
   250 text{*This allows @{text blast} to simplify occurrences of 
   251   @{term "parts(G\<union>H)"} in the assumption.*}
   252 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
   253 declare in_parts_UnE [elim!]
   254 
   255 
   256 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
   257 by (blast intro: parts_mono [THEN [2] rev_subsetD])
   258 
   259 subsubsection{*Idempotence and transitivity *}
   260 
   261 lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
   262 by (erule parts.induct, blast+)
   263 
   264 lemma parts_idem [simp]: "parts (parts H) = parts H"
   265 by blast
   266 
   267 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
   268 apply (rule iffI)
   269 apply (iprover intro: subset_trans parts_increasing)  
   270 apply (frule parts_mono, simp) 
   271 done
   272 
   273 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   274 by (drule parts_mono, blast)
   275 
   276 text{*Cut*}
   277 lemma parts_cut:
   278      "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)" 
   279 by (blast intro: parts_trans) 
   280 
   281 
   282 lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
   283 by (force dest!: parts_cut intro: parts_insertI)
   284 
   285 
   286 subsubsection{*Rewrite rules for pulling out atomic messages *}
   287 
   288 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   289 
   290 
   291 lemma parts_insert_Agent [simp]:
   292      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   293 apply (rule parts_insert_eq_I) 
   294 apply (erule parts.induct, auto) 
   295 done
   296 
   297 lemma parts_insert_Nonce [simp]:
   298      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   299 apply (rule parts_insert_eq_I) 
   300 apply (erule parts.induct, auto) 
   301 done
   302 
   303 lemma parts_insert_Key [simp]:
   304      "parts (insert (Key K) H) = insert (Key K) (parts H)"
   305 apply (rule parts_insert_eq_I) 
   306 apply (erule parts.induct, auto) 
   307 done
   308 
   309 lemma parts_insert_Crypt [simp]:
   310      "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
   311 apply (rule equalityI)
   312 apply (rule subsetI)
   313 apply (erule parts.induct, auto)
   314 apply (blast intro: parts.Body)
   315 done
   316 
   317 lemma parts_insert_MPair [simp]:
   318      "parts (insert {|X,Y|} H) =  
   319           insert {|X,Y|} (parts (insert X (insert Y H)))"
   320 apply (rule equalityI)
   321 apply (rule subsetI)
   322 apply (erule parts.induct, auto)
   323 apply (blast intro: parts.Fst parts.Snd)+
   324 done
   325 
   326 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
   327 apply auto
   328 apply (erule parts.induct, auto)
   329 done
   330 
   331 
   332 text{*In any message, there is an upper bound N on its greatest nonce.*}
   333 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   334 apply (induct_tac "msg")
   335 apply (simp_all (no_asm_simp) add: exI parts_insert2)
   336  txt{*MPair case: blast works out the necessary sum itself!*}
   337  prefer 2 apply auto apply (blast elim!: add_leE)
   338 txt{*Nonce case*}
   339 apply (rule_tac x = "N + Suc nat" in exI, auto) 
   340 done
   341 (*>*)
   342 
   343 section{* Modelling the Adversary *}
   344 
   345 text {*
   346 The spy is part of the system and must be built into the model.  He is
   347 a malicious user who does not have to follow the protocol.  He
   348 watches the network and uses any keys he knows to decrypt messages.
   349 Thus he accumulates additional keys and nonces.  These he can use to
   350 compose new messages, which he may send to anybody.  
   351 
   352 Two functions enable us to formalize this behaviour: @{text analz} and
   353 @{text synth}.  Each function maps a sets of messages to another set of
   354 messages. The set @{text "analz H"} formalizes what the adversary can learn
   355 from the set of messages~$H$.  The closure properties of this set are
   356 defined inductively.
   357 *}
   358 
   359 inductive_set
   360   analz :: "msg set \<Rightarrow> msg set"
   361   for H :: "msg set"
   362   where
   363     Inj [intro,simp] : "X \<in> H \<Longrightarrow> X \<in> analz H"
   364   | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> X \<in> analz H"
   365   | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> Y \<in> analz H"
   366   | Decrypt [dest]: 
   367              "\<lbrakk>Crypt K X \<in> analz H; Key(invKey K) \<in> analz H\<rbrakk>
   368               \<Longrightarrow> X \<in> analz H"
   369 (*<*)
   370 text{*Monotonicity; Lemma 1 of Lowe's paper*}
   371 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   372 apply auto
   373 apply (erule analz.induct) 
   374 apply (auto dest: analz.Fst analz.Snd) 
   375 done
   376 
   377 text{*Making it safe speeds up proofs*}
   378 lemma MPair_analz [elim!]:
   379      "[| {|X,Y|} \<in> analz H;        
   380              [| X \<in> analz H; Y \<in> analz H |] ==> P   
   381           |] ==> P"
   382 by (blast dest: analz.Fst analz.Snd)
   383 
   384 lemma analz_increasing: "H \<subseteq> analz(H)"
   385 by blast
   386 
   387 lemma analz_subset_parts: "analz H \<subseteq> parts H"
   388 apply (rule subsetI)
   389 apply (erule analz.induct, blast+)
   390 done
   391 
   392 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   393 
   394 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   395 
   396 
   397 lemma parts_analz [simp]: "parts (analz H) = parts H"
   398 apply (rule equalityI)
   399 apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
   400 apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
   401 done
   402 
   403 lemma analz_parts [simp]: "analz (parts H) = parts H"
   404 apply auto
   405 apply (erule analz.induct, auto)
   406 done
   407 
   408 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   409 
   410 subsubsection{*General equational properties *}
   411 
   412 lemma analz_empty [simp]: "analz{} = {}"
   413 apply safe
   414 apply (erule analz.induct, blast+)
   415 done
   416 
   417 text{*Converse fails: we can analz more from the union than from the 
   418   separate parts, as a key in one might decrypt a message in the other*}
   419 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   420 by (intro Un_least analz_mono Un_upper1 Un_upper2)
   421 
   422 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   423 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   424 
   425 subsubsection{*Rewrite rules for pulling out atomic messages *}
   426 
   427 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   428 
   429 lemma analz_insert_Agent [simp]:
   430      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   431 apply (rule analz_insert_eq_I) 
   432 apply (erule analz.induct, auto) 
   433 done
   434 
   435 lemma analz_insert_Nonce [simp]:
   436      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   437 apply (rule analz_insert_eq_I) 
   438 apply (erule analz.induct, auto) 
   439 done
   440 
   441 text{*Can only pull out Keys if they are not needed to decrypt the rest*}
   442 lemma analz_insert_Key [simp]: 
   443     "K \<notin> keysFor (analz H) ==>   
   444           analz (insert (Key K) H) = insert (Key K) (analz H)"
   445 apply (unfold keysFor_def)
   446 apply (rule analz_insert_eq_I) 
   447 apply (erule analz.induct, auto) 
   448 done
   449 
   450 lemma analz_insert_MPair [simp]:
   451      "analz (insert {|X,Y|} H) =  
   452           insert {|X,Y|} (analz (insert X (insert Y H)))"
   453 apply (rule equalityI)
   454 apply (rule subsetI)
   455 apply (erule analz.induct, auto)
   456 apply (erule analz.induct)
   457 apply (blast intro: analz.Fst analz.Snd)+
   458 done
   459 
   460 text{*Can pull out enCrypted message if the Key is not known*}
   461 lemma analz_insert_Crypt:
   462      "Key (invKey K) \<notin> analz H 
   463       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   464 apply (rule analz_insert_eq_I) 
   465 apply (erule analz.induct, auto) 
   466 
   467 done
   468 
   469 lemma lemma1: "Key (invKey K) \<in> analz H ==>   
   470                analz (insert (Crypt K X) H) \<subseteq>  
   471                insert (Crypt K X) (analz (insert X H))"
   472 apply (rule subsetI)
   473 apply (erule_tac x = x in analz.induct, auto)
   474 done
   475 
   476 lemma lemma2: "Key (invKey K) \<in> analz H ==>   
   477                insert (Crypt K X) (analz (insert X H)) \<subseteq>  
   478                analz (insert (Crypt K X) H)"
   479 apply auto
   480 apply (erule_tac x = x in analz.induct, auto)
   481 apply (blast intro: analz_insertI analz.Decrypt)
   482 done
   483 
   484 lemma analz_insert_Decrypt:
   485      "Key (invKey K) \<in> analz H ==>   
   486                analz (insert (Crypt K X) H) =  
   487                insert (Crypt K X) (analz (insert X H))"
   488 by (intro equalityI lemma1 lemma2)
   489 
   490 text{*Case analysis: either the message is secure, or it is not! Effective,
   491 but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
   492 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
   493 (Crypt K X) H)"} *} 
   494 lemma analz_Crypt_if [simp]:
   495      "analz (insert (Crypt K X) H) =                 
   496           (if (Key (invKey K) \<in> analz H)                 
   497            then insert (Crypt K X) (analz (insert X H))  
   498            else insert (Crypt K X) (analz H))"
   499 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   500 
   501 
   502 text{*This rule supposes "for the sake of argument" that we have the key.*}
   503 lemma analz_insert_Crypt_subset:
   504      "analz (insert (Crypt K X) H) \<subseteq>   
   505            insert (Crypt K X) (analz (insert X H))"
   506 apply (rule subsetI)
   507 apply (erule analz.induct, auto)
   508 done
   509 
   510 
   511 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   512 apply auto
   513 apply (erule analz.induct, auto)
   514 done
   515 
   516 
   517 subsubsection{*Idempotence and transitivity *}
   518 
   519 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   520 by (erule analz.induct, blast+)
   521 
   522 lemma analz_idem [simp]: "analz (analz H) = analz H"
   523 by blast
   524 
   525 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
   526 apply (rule iffI)
   527 apply (iprover intro: subset_trans analz_increasing)  
   528 apply (frule analz_mono, simp) 
   529 done
   530 
   531 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   532 by (drule analz_mono, blast)
   533 
   534 text{*Cut; Lemma 2 of Lowe*}
   535 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   536 by (erule analz_trans, blast)
   537 
   538 (*Cut can be proved easily by induction on
   539    "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   540 *)
   541 
   542 text{*This rewrite rule helps in the simplification of messages that involve
   543   the forwarding of unknown components (X).  Without it, removing occurrences
   544   of X can be very complicated. *}
   545 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   546 by (blast intro: analz_cut analz_insertI)
   547 
   548 
   549 text{*A congruence rule for "analz" *}
   550 
   551 lemma analz_subset_cong:
   552      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
   553       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   554 apply simp
   555 apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) 
   556 done
   557 
   558 lemma analz_cong:
   559      "[| analz G = analz G'; analz H = analz H' |] 
   560       ==> analz (G \<union> H) = analz (G' \<union> H')"
   561 by (intro equalityI analz_subset_cong, simp_all) 
   562 
   563 lemma analz_insert_cong:
   564      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   565 by (force simp only: insert_def intro!: analz_cong)
   566 
   567 text{*If there are no pairs or encryptions then analz does nothing*}
   568 lemma analz_trivial:
   569      "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   570 apply safe
   571 apply (erule analz.induct, blast+)
   572 done
   573 
   574 text{*These two are obsolete (with a single Spy) but cost little to prove...*}
   575 lemma analz_UN_analz_lemma:
   576      "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   577 apply (erule analz.induct)
   578 apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   579 done
   580 
   581 lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   582 by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   583 (*>*)
   584 text {*
   585 Note the @{text Decrypt} rule: the spy can decrypt a
   586 message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. 
   587 Properties proved by rule induction include the following:
   588 @{named_thms [display,indent=0] analz_mono [no_vars] (analz_mono) analz_idem [no_vars] (analz_idem)}
   589 
   590 The set of fake messages that an intruder could invent
   591 starting from~@{text H} is @{text "synth(analz H)"}, where @{text "synth H"}
   592 formalizes what the adversary can build from the set of messages~$H$.  
   593 *}
   594 
   595 inductive_set
   596   synth :: "msg set \<Rightarrow> msg set"
   597   for H :: "msg set"
   598   where
   599     Inj    [intro]: "X \<in> H \<Longrightarrow> X \<in> synth H"
   600   | Agent  [intro]: "Agent agt \<in> synth H"
   601   | MPair  [intro]:
   602               "\<lbrakk>X \<in> synth H;  Y \<in> synth H\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> synth H"
   603   | Crypt  [intro]:
   604               "\<lbrakk>X \<in> synth H;  Key K \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
   605 (*<*)
   606 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   607   by (auto, erule synth.induct, auto)  
   608 
   609 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   610 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   611 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   612 
   613 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   614 apply (rule equalityI)
   615 apply (rule subsetI)
   616 apply (erule analz.induct)
   617 prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
   618 apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
   619 done
   620 
   621 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   622 apply (cut_tac H = "{}" in analz_synth_Un)
   623 apply (simp (no_asm_use))
   624 done
   625 (*>*)
   626 text {*
   627 The set includes all agent names.  Nonces and keys are assumed to be
   628 unguessable, so none are included beyond those already in~$H$.   Two
   629 elements of @{term "synth H"} can be combined, and an element can be encrypted
   630 using a key present in~$H$.
   631 
   632 Like @{text analz}, this set operator is monotone and idempotent.  It also
   633 satisfies an interesting equation involving @{text analz}:
   634 @{named_thms [display,indent=0] analz_synth [no_vars] (analz_synth)}
   635 Rule inversion plays a major role in reasoning about @{text synth}, through
   636 declarations such as this one:
   637 *}
   638 
   639 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   640 
   641 text {*
   642 \noindent
   643 The resulting elimination rule replaces every assumption of the form
   644 @{term "Nonce n \<in> synth H"} by @{term "Nonce n \<in> H"},
   645 expressing that a nonce cannot be guessed.  
   646 
   647 A third operator, @{text parts}, is useful for stating correctness
   648 properties.  The set
   649 @{term "parts H"} consists of the components of elements of~$H$.  This set
   650 includes~@{text H} and is closed under the projections from a compound
   651 message to its immediate parts. 
   652 Its definition resembles that of @{text analz} except in the rule
   653 corresponding to the constructor @{text Crypt}: 
   654 @{thm [display,indent=5] parts.Body [no_vars]}
   655 The body of an encrypted message is always regarded as part of it.  We can
   656 use @{text parts} to express general well-formedness properties of a protocol,
   657 for example, that an uncompromised agent's private key will never be
   658 included as a component of any message.
   659 *}
   660 (*<*)
   661 lemma synth_increasing: "H \<subseteq> synth(H)"
   662 by blast
   663 
   664 subsubsection{*Unions *}
   665 
   666 text{*Converse fails: we can synth more from the union than from the 
   667   separate parts, building a compound message using elements of each.*}
   668 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   669 by (intro Un_least synth_mono Un_upper1 Un_upper2)
   670 
   671 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   672 by (blast intro: synth_mono [THEN [2] rev_subsetD])
   673 
   674 subsubsection{*Idempotence and transitivity *}
   675 
   676 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   677 by (erule synth.induct, blast+)
   678 
   679 lemma synth_idem: "synth (synth H) = synth H"
   680 by blast
   681 
   682 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
   683 apply (rule iffI)
   684 apply (iprover intro: subset_trans synth_increasing)  
   685 apply (frule synth_mono, simp add: synth_idem) 
   686 done
   687 
   688 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   689 by (drule synth_mono, blast)
   690 
   691 text{*Cut; Lemma 2 of Lowe*}
   692 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   693 by (erule synth_trans, blast)
   694 
   695 lemma Agent_synth [simp]: "Agent A \<in> synth H"
   696 by blast
   697 
   698 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   699 by blast
   700 
   701 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   702 by blast
   703 
   704 lemma Crypt_synth_eq [simp]:
   705      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   706 by blast
   707 
   708 
   709 lemma keysFor_synth [simp]: 
   710     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   711 by (unfold keysFor_def, blast)
   712 
   713 
   714 subsubsection{*Combinations of parts, analz and synth *}
   715 
   716 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   717 apply (rule equalityI)
   718 apply (rule subsetI)
   719 apply (erule parts.induct)
   720 apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] 
   721                     parts.Fst parts.Snd parts.Body)+
   722 done
   723 
   724 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   725 apply (intro equalityI analz_subset_cong)+
   726 apply simp_all
   727 done
   728 
   729 
   730 subsubsection{*For reasoning about the Fake rule in traces *}
   731 
   732 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   733 by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   734 
   735 text{*More specifically for Fake.  Very occasionally we could do with a version
   736   of the form  @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"} *}
   737 lemma Fake_parts_insert:
   738      "X \<in> synth (analz H) ==>  
   739       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   740 apply (drule parts_insert_subset_Un)
   741 apply (simp (no_asm_use))
   742 apply blast
   743 done
   744 
   745 lemma Fake_parts_insert_in_Un:
   746      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   747       ==> Z \<in>  synth (analz H) \<union> parts H";
   748 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   749 
   750 text{*@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put 
   751   @{term "G=H"}.*}
   752 lemma Fake_analz_insert:
   753      "X\<in> synth (analz G) ==>  
   754       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   755 apply (rule subsetI)
   756 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   757 prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
   758 apply (simp (no_asm_use))
   759 apply blast
   760 done
   761 
   762 lemma analz_conj_parts [simp]:
   763      "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   764 by (blast intro: analz_subset_parts [THEN subsetD])
   765 
   766 lemma analz_disj_parts [simp]:
   767      "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   768 by (blast intro: analz_subset_parts [THEN subsetD])
   769 
   770 text{*Without this equation, other rules for synth and analz would yield
   771   redundant cases*}
   772 lemma MPair_synth_analz [iff]:
   773      "({|X,Y|} \<in> synth (analz H)) =  
   774       (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   775 by blast
   776 
   777 lemma Crypt_synth_analz:
   778      "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   779        ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
   780 by blast
   781 
   782 
   783 text{*We do NOT want Crypt... messages broken up in protocols!!*}
   784 declare parts.Body [rule del]
   785 
   786 
   787 text{*Rewrites to push in Key and Crypt messages, so that other messages can
   788     be pulled out using the @{text analz_insert} rules*}
   789 
   790 lemmas pushKeys [standard] =
   791   insert_commute [of "Key K" "Agent C"]
   792   insert_commute [of "Key K" "Nonce N"]
   793   insert_commute [of "Key K" "Number N"]
   794   insert_commute [of "Key K" "Hash X"]
   795   insert_commute [of "Key K" "MPair X Y"]
   796   insert_commute [of "Key K" "Crypt X K'"]
   797 
   798 lemmas pushCrypts [standard] =
   799   insert_commute [of "Crypt X K" "Agent C"]
   800   insert_commute [of "Crypt X K" "Agent C"]
   801   insert_commute [of "Crypt X K" "Nonce N"]
   802   insert_commute [of "Crypt X K" "Number N"]
   803   insert_commute [of "Crypt X K" "Hash X'"]
   804   insert_commute [of "Crypt X K" "MPair X' Y"]
   805 
   806 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   807   re-ordered. *}
   808 lemmas pushes = pushKeys pushCrypts
   809 
   810 
   811 subsection{*Tactics useful for many protocol proofs*}
   812 ML
   813 {*
   814 val invKey = thm "invKey"
   815 val keysFor_def = thm "keysFor_def"
   816 val symKeys_def = thm "symKeys_def"
   817 val parts_mono = thm "parts_mono";
   818 val analz_mono = thm "analz_mono";
   819 val synth_mono = thm "synth_mono";
   820 val analz_increasing = thm "analz_increasing";
   821 
   822 val analz_insertI = thm "analz_insertI";
   823 val analz_subset_parts = thm "analz_subset_parts";
   824 val Fake_parts_insert = thm "Fake_parts_insert";
   825 val Fake_analz_insert = thm "Fake_analz_insert";
   826 val pushes = thms "pushes";
   827 
   828 
   829 (*Prove base case (subgoal i) and simplify others.  A typical base case
   830   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   831   alone.*)
   832 fun prove_simple_subgoals_tac (cs, ss) i = 
   833     force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
   834     ALLGOALS (asm_simp_tac ss)
   835 
   836 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   837   but this application is no longer necessary if analz_insert_eq is used.
   838   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   839   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   840 
   841 (*Apply rules to break down assumptions of the form
   842   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
   843 *)
   844 fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
   845 
   846 val Fake_insert_tac = 
   847     dresolve_tac [impOfSubs Fake_analz_insert,
   848                   impOfSubs Fake_parts_insert] THEN'
   849     eresolve_tac [asm_rl, thm"synth.Inj"];
   850 
   851 fun Fake_insert_simp_tac ss i = 
   852     REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
   853 
   854 fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
   855     (Fake_insert_simp_tac ss 1
   856      THEN
   857      IF_UNSOLVED (Blast.depth_tac
   858                   (cs addIs [analz_insertI,
   859                                    impOfSubs analz_subset_parts]) 4 1))
   860 
   861 fun spy_analz_tac (cs,ss) i =
   862   DETERM
   863    (SELECT_GOAL
   864      (EVERY 
   865       [  (*push in occurrences of X...*)
   866        (REPEAT o CHANGED)
   867            (res_inst_tac (Simplifier.the_context ss)
   868             [(("x", 1), "X")] (insert_commute RS ssubst) 1),
   869        (*...allowing further simplifications*)
   870        simp_tac ss 1,
   871        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   872        DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
   873 *}
   874 
   875 text{*By default only @{text o_apply} is built-in.  But in the presence of
   876 eta-expansion this means that some terms displayed as @{term "f o g"} will be
   877 rewritten, and others will not!*}
   878 declare o_def [simp]
   879 
   880 
   881 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
   882 by auto
   883 
   884 lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
   885 by (iprover intro: synth_mono analz_mono) 
   886 
   887 lemma Fake_analz_eq [simp]:
   888      "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
   889 apply (drule Fake_analz_insert[of _ _ "H"])
   890 apply (simp add: synth_increasing[THEN Un_absorb2])
   891 apply (drule synth_mono)
   892 apply (simp add: synth_idem)
   893 apply (rule equalityI)
   894 apply (simp add: );
   895 apply (rule synth_analz_mono, blast)   
   896 done
   897 
   898 text{*Two generalizations of @{text analz_insert_eq}*}
   899 lemma gen_analz_insert_eq [rule_format]:
   900      "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
   901 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
   902 
   903 lemma synth_analz_insert_eq [rule_format]:
   904      "X \<in> synth (analz H) 
   905       ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
   906 apply (erule synth.induct) 
   907 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
   908 done
   909 
   910 lemma Fake_parts_sing:
   911      "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
   912 apply (rule subset_trans) 
   913  apply (erule_tac [2] Fake_parts_insert)
   914 apply (rule parts_mono, blast)
   915 done
   916 
   917 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
   918 
   919 method_setup spy_analz = {*
   920     Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o clasimpset_of) *}
   921     "for proving the Fake case when analz is involved"
   922 
   923 method_setup atomic_spy_analz = {*
   924     Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o clasimpset_of) *}
   925     "for debugging spy_analz"
   926 
   927 method_setup Fake_insert_simp = {*
   928     Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *}
   929     "for debugging spy_analz"
   930 
   931 
   932 end
   933 (*>*)