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