src/HOL/Metis_Examples/Message.thy
 author wenzelm Thu Feb 11 21:33:25 2010 +0100 (2010-02-11) changeset 35109 0015a0a99ae9 parent 35095 6cdf9bbd0342 child 35416 d8d7d1b785af permissions -rw-r--r--
modernized syntax/translations;
```     1 (*  Title:      HOL/MetisTest/Message.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3
```
```     4 Testing the metis method.
```
```     5 *)
```
```     6
```
```     7 theory Message imports Main begin
```
```     8
```
```     9 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
```
```    10 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
```
```    11 by blast
```
```    12
```
```    13 types
```
```    14   key = nat
```
```    15
```
```    16 consts
```
```    17   all_symmetric :: bool        --{*true if all keys are symmetric*}
```
```    18   invKey        :: "key=>key"  --{*inverse of a symmetric key*}
```
```    19
```
```    20 specification (invKey)
```
```    21   invKey [simp]: "invKey (invKey K) = K"
```
```    22   invKey_symmetric: "all_symmetric --> invKey = id"
```
```    23     by (rule exI [of _ id], auto)
```
```    24
```
```    25
```
```    26 text{*The inverse of a symmetric key is itself; that of a public key
```
```    27       is the private key and vice versa*}
```
```    28
```
```    29 constdefs
```
```    30   symKeys :: "key set"
```
```    31   "symKeys == {K. invKey K = K}"
```
```    32
```
```    33 datatype  --{*We allow any number of friendly agents*}
```
```    34   agent = Server | Friend nat | Spy
```
```    35
```
```    36 datatype
```
```    37      msg = Agent  agent     --{*Agent names*}
```
```    38          | Number nat       --{*Ordinary integers, timestamps, ...*}
```
```    39          | Nonce  nat       --{*Unguessable nonces*}
```
```    40          | Key    key       --{*Crypto keys*}
```
```    41          | Hash   msg       --{*Hashing*}
```
```    42          | MPair  msg msg   --{*Compound messages*}
```
```    43          | Crypt  key msg   --{*Encryption, public- or shared-key*}
```
```    44
```
```    45
```
```    46 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
```
```    47 syntax
```
```    48   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
```
```    49
```
```    50 syntax (xsymbols)
```
```    51   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
```
```    52
```
```    53 translations
```
```    54   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
```
```    55   "{|x, y|}"      == "CONST MPair x y"
```
```    56
```
```    57
```
```    58 constdefs
```
```    59   HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
```
```    60     --{*Message Y paired with a MAC computed with the help of X*}
```
```    61     "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
```
```    62
```
```    63   keysFor :: "msg set => key set"
```
```    64     --{*Keys useful to decrypt elements of a message set*}
```
```    65   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
```
```    66
```
```    67
```
```    68 subsubsection{*Inductive Definition of All Parts" of a Message*}
```
```    69
```
```    70 inductive_set
```
```    71   parts :: "msg set => msg set"
```
```    72   for H :: "msg set"
```
```    73   where
```
```    74     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
```
```    75   | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
```
```    76   | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
```
```    77   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
```
```    78
```
```    79
```
```    80 declare [[ atp_problem_prefix = "Message__parts_mono" ]]
```
```    81 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
```
```    82 apply auto
```
```    83 apply (erule parts.induct)
```
```    84 apply (metis Inj set_mp)
```
```    85 apply (metis Fst)
```
```    86 apply (metis Snd)
```
```    87 apply (metis Body)
```
```    88 done
```
```    89
```
```    90
```
```    91 text{*Equations hold because constructors are injective.*}
```
```    92 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
```
```    93 by auto
```
```    94
```
```    95 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
```
```    96 by auto
```
```    97
```
```    98 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
```
```    99 by auto
```
```   100
```
```   101
```
```   102 subsubsection{*Inverse of keys *}
```
```   103
```
```   104 declare [[ atp_problem_prefix = "Message__invKey_eq" ]]
```
```   105 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
```
```   106 by (metis invKey)
```
```   107
```
```   108
```
```   109 subsection{*keysFor operator*}
```
```   110
```
```   111 lemma keysFor_empty [simp]: "keysFor {} = {}"
```
```   112 by (unfold keysFor_def, blast)
```
```   113
```
```   114 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
```
```   115 by (unfold keysFor_def, blast)
```
```   116
```
```   117 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
```
```   118 by (unfold keysFor_def, blast)
```
```   119
```
```   120 text{*Monotonicity*}
```
```   121 lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
```
```   122 by (unfold keysFor_def, blast)
```
```   123
```
```   124 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
```
```   125 by (unfold keysFor_def, auto)
```
```   126
```
```   127 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
```
```   128 by (unfold keysFor_def, auto)
```
```   129
```
```   130 lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
```
```   131 by (unfold keysFor_def, auto)
```
```   132
```
```   133 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
```
```   134 by (unfold keysFor_def, auto)
```
```   135
```
```   136 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
```
```   137 by (unfold keysFor_def, auto)
```
```   138
```
```   139 lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
```
```   140 by (unfold keysFor_def, auto)
```
```   141
```
```   142 lemma keysFor_insert_Crypt [simp]:
```
```   143     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
```
```   144 by (unfold keysFor_def, auto)
```
```   145
```
```   146 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
```
```   147 by (unfold keysFor_def, auto)
```
```   148
```
```   149 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
```
```   150 by (unfold keysFor_def, blast)
```
```   151
```
```   152
```
```   153 subsection{*Inductive relation "parts"*}
```
```   154
```
```   155 lemma MPair_parts:
```
```   156      "[| {|X,Y|} \<in> parts H;
```
```   157          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
```
```   158 by (blast dest: parts.Fst parts.Snd)
```
```   159
```
```   160     declare MPair_parts [elim!]  parts.Body [dest!]
```
```   161 text{*NB These two rules are UNSAFE in the formal sense, as they discard the
```
```   162      compound message.  They work well on THIS FILE.
```
```   163   @{text MPair_parts} is left as SAFE because it speeds up proofs.
```
```   164   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
```
```   165
```
```   166 lemma parts_increasing: "H \<subseteq> parts(H)"
```
```   167 by blast
```
```   168
```
```   169 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
```
```   170
```
```   171 lemma parts_empty [simp]: "parts{} = {}"
```
```   172 apply safe
```
```   173 apply (erule parts.induct)
```
```   174 apply blast+
```
```   175 done
```
```   176
```
```   177 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
```
```   178 by simp
```
```   179
```
```   180 text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
```
```   181 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
```
```   182 apply (erule parts.induct)
```
```   183 apply fast+
```
```   184 done
```
```   185
```
```   186
```
```   187 subsubsection{*Unions *}
```
```   188
```
```   189 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
```
```   190 by (intro Un_least parts_mono Un_upper1 Un_upper2)
```
```   191
```
```   192 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
```
```   193 apply (rule subsetI)
```
```   194 apply (erule parts.induct, blast+)
```
```   195 done
```
```   196
```
```   197 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
```
```   198 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
```
```   199
```
```   200 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
```
```   201 apply (subst insert_is_Un [of _ H])
```
```   202 apply (simp only: parts_Un)
```
```   203 done
```
```   204
```
```   205 declare [[ atp_problem_prefix = "Message__parts_insert_two" ]]
```
```   206 lemma parts_insert2:
```
```   207      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
```
```   208 by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
```
```   209
```
```   210
```
```   211 lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
```
```   212 by (intro UN_least parts_mono UN_upper)
```
```   213
```
```   214 lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
```
```   215 apply (rule subsetI)
```
```   216 apply (erule parts.induct, blast+)
```
```   217 done
```
```   218
```
```   219 lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
```
```   220 by (intro equalityI parts_UN_subset1 parts_UN_subset2)
```
```   221
```
```   222 text{*Added to simplify arguments to parts, analz and synth.
```
```   223   NOTE: the UN versions are no longer used!*}
```
```   224
```
```   225
```
```   226 text{*This allows @{text blast} to simplify occurrences of
```
```   227   @{term "parts(G\<union>H)"} in the assumption.*}
```
```   228 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
```
```   229 declare in_parts_UnE [elim!]
```
```   230
```
```   231 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
```
```   232 by (blast intro: parts_mono [THEN [2] rev_subsetD])
```
```   233
```
```   234 subsubsection{*Idempotence and transitivity *}
```
```   235
```
```   236 lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
```
```   237 by (erule parts.induct, blast+)
```
```   238
```
```   239 lemma parts_idem [simp]: "parts (parts H) = parts H"
```
```   240 by blast
```
```   241
```
```   242 declare [[ atp_problem_prefix = "Message__parts_subset_iff" ]]
```
```   243 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
```
```   244 apply (rule iffI)
```
```   245 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
```
```   246 apply (metis parts_idem parts_mono)
```
```   247 done
```
```   248
```
```   249 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
```
```   250 by (blast dest: parts_mono);
```
```   251
```
```   252
```
```   253 declare [[ atp_problem_prefix = "Message__parts_cut" ]]
```
```   254 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
```
```   255 by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
```
```   256
```
```   257
```
```   258
```
```   259 subsubsection{*Rewrite rules for pulling out atomic messages *}
```
```   260
```
```   261 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
```
```   262
```
```   263
```
```   264 lemma parts_insert_Agent [simp]:
```
```   265      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
```
```   266 apply (rule parts_insert_eq_I)
```
```   267 apply (erule parts.induct, auto)
```
```   268 done
```
```   269
```
```   270 lemma parts_insert_Nonce [simp]:
```
```   271      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
```
```   272 apply (rule parts_insert_eq_I)
```
```   273 apply (erule parts.induct, auto)
```
```   274 done
```
```   275
```
```   276 lemma parts_insert_Number [simp]:
```
```   277      "parts (insert (Number N) H) = insert (Number N) (parts H)"
```
```   278 apply (rule parts_insert_eq_I)
```
```   279 apply (erule parts.induct, auto)
```
```   280 done
```
```   281
```
```   282 lemma parts_insert_Key [simp]:
```
```   283      "parts (insert (Key K) H) = insert (Key K) (parts H)"
```
```   284 apply (rule parts_insert_eq_I)
```
```   285 apply (erule parts.induct, auto)
```
```   286 done
```
```   287
```
```   288 lemma parts_insert_Hash [simp]:
```
```   289      "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
```
```   290 apply (rule parts_insert_eq_I)
```
```   291 apply (erule parts.induct, auto)
```
```   292 done
```
```   293
```
```   294 lemma parts_insert_Crypt [simp]:
```
```   295      "parts (insert (Crypt K X) H) =
```
```   296           insert (Crypt K X) (parts (insert X H))"
```
```   297 apply (rule equalityI)
```
```   298 apply (rule subsetI)
```
```   299 apply (erule parts.induct, auto)
```
```   300 apply (blast intro: parts.Body)
```
```   301 done
```
```   302
```
```   303 lemma parts_insert_MPair [simp]:
```
```   304      "parts (insert {|X,Y|} H) =
```
```   305           insert {|X,Y|} (parts (insert X (insert Y H)))"
```
```   306 apply (rule equalityI)
```
```   307 apply (rule subsetI)
```
```   308 apply (erule parts.induct, auto)
```
```   309 apply (blast intro: parts.Fst parts.Snd)+
```
```   310 done
```
```   311
```
```   312 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
```
```   313 apply auto
```
```   314 apply (erule parts.induct, auto)
```
```   315 done
```
```   316
```
```   317
```
```   318 declare [[ atp_problem_prefix = "Message__msg_Nonce_supply" ]]
```
```   319 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
```
```   320 apply (induct_tac "msg")
```
```   321 apply (simp_all add: parts_insert2)
```
```   322 apply (metis Suc_n_not_le_n)
```
```   323 apply (metis le_trans linorder_linear)
```
```   324 done
```
```   325
```
```   326 subsection{*Inductive relation "analz"*}
```
```   327
```
```   328 text{*Inductive definition of "analz" -- what can be broken down from a set of
```
```   329     messages, including keys.  A form of downward closure.  Pairs can
```
```   330     be taken apart; messages decrypted with known keys.  *}
```
```   331
```
```   332 inductive_set
```
```   333   analz :: "msg set => msg set"
```
```   334   for H :: "msg set"
```
```   335   where
```
```   336     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
```
```   337   | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
```
```   338   | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
```
```   339   | Decrypt [dest]:
```
```   340              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
```
```   341
```
```   342
```
```   343 text{*Monotonicity; Lemma 1 of Lowe's paper*}
```
```   344 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
```
```   345 apply auto
```
```   346 apply (erule analz.induct)
```
```   347 apply (auto dest: analz.Fst analz.Snd)
```
```   348 done
```
```   349
```
```   350 text{*Making it safe speeds up proofs*}
```
```   351 lemma MPair_analz [elim!]:
```
```   352      "[| {|X,Y|} \<in> analz H;
```
```   353              [| X \<in> analz H; Y \<in> analz H |] ==> P
```
```   354           |] ==> P"
```
```   355 by (blast dest: analz.Fst analz.Snd)
```
```   356
```
```   357 lemma analz_increasing: "H \<subseteq> analz(H)"
```
```   358 by blast
```
```   359
```
```   360 lemma analz_subset_parts: "analz H \<subseteq> parts H"
```
```   361 apply (rule subsetI)
```
```   362 apply (erule analz.induct, blast+)
```
```   363 done
```
```   364
```
```   365 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
```
```   366
```
```   367 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
```
```   368
```
```   369
```
```   370 declare [[ atp_problem_prefix = "Message__parts_analz" ]]
```
```   371 lemma parts_analz [simp]: "parts (analz H) = parts H"
```
```   372 apply (rule equalityI)
```
```   373 apply (metis analz_subset_parts parts_subset_iff)
```
```   374 apply (metis analz_increasing parts_mono)
```
```   375 done
```
```   376
```
```   377
```
```   378 lemma analz_parts [simp]: "analz (parts H) = parts H"
```
```   379 apply auto
```
```   380 apply (erule analz.induct, auto)
```
```   381 done
```
```   382
```
```   383 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
```
```   384
```
```   385 subsubsection{*General equational properties *}
```
```   386
```
```   387 lemma analz_empty [simp]: "analz{} = {}"
```
```   388 apply safe
```
```   389 apply (erule analz.induct, blast+)
```
```   390 done
```
```   391
```
```   392 text{*Converse fails: we can analz more from the union than from the
```
```   393   separate parts, as a key in one might decrypt a message in the other*}
```
```   394 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
```
```   395 by (intro Un_least analz_mono Un_upper1 Un_upper2)
```
```   396
```
```   397 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
```
```   398 by (blast intro: analz_mono [THEN [2] rev_subsetD])
```
```   399
```
```   400 subsubsection{*Rewrite rules for pulling out atomic messages *}
```
```   401
```
```   402 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
```
```   403
```
```   404 lemma analz_insert_Agent [simp]:
```
```   405      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
```
```   406 apply (rule analz_insert_eq_I)
```
```   407 apply (erule analz.induct, auto)
```
```   408 done
```
```   409
```
```   410 lemma analz_insert_Nonce [simp]:
```
```   411      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
```
```   412 apply (rule analz_insert_eq_I)
```
```   413 apply (erule analz.induct, auto)
```
```   414 done
```
```   415
```
```   416 lemma analz_insert_Number [simp]:
```
```   417      "analz (insert (Number N) H) = insert (Number N) (analz H)"
```
```   418 apply (rule analz_insert_eq_I)
```
```   419 apply (erule analz.induct, auto)
```
```   420 done
```
```   421
```
```   422 lemma analz_insert_Hash [simp]:
```
```   423      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
```
```   424 apply (rule analz_insert_eq_I)
```
```   425 apply (erule analz.induct, auto)
```
```   426 done
```
```   427
```
```   428 text{*Can only pull out Keys if they are not needed to decrypt the rest*}
```
```   429 lemma analz_insert_Key [simp]:
```
```   430     "K \<notin> keysFor (analz H) ==>
```
```   431           analz (insert (Key K) H) = insert (Key K) (analz H)"
```
```   432 apply (unfold keysFor_def)
```
```   433 apply (rule analz_insert_eq_I)
```
```   434 apply (erule analz.induct, auto)
```
```   435 done
```
```   436
```
```   437 lemma analz_insert_MPair [simp]:
```
```   438      "analz (insert {|X,Y|} H) =
```
```   439           insert {|X,Y|} (analz (insert X (insert Y H)))"
```
```   440 apply (rule equalityI)
```
```   441 apply (rule subsetI)
```
```   442 apply (erule analz.induct, auto)
```
```   443 apply (erule analz.induct)
```
```   444 apply (blast intro: analz.Fst analz.Snd)+
```
```   445 done
```
```   446
```
```   447 text{*Can pull out enCrypted message if the Key is not known*}
```
```   448 lemma analz_insert_Crypt:
```
```   449      "Key (invKey K) \<notin> analz H
```
```   450       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
```
```   451 apply (rule analz_insert_eq_I)
```
```   452 apply (erule analz.induct, auto)
```
```   453
```
```   454 done
```
```   455
```
```   456 lemma lemma1: "Key (invKey K) \<in> analz H ==>
```
```   457                analz (insert (Crypt K X) H) \<subseteq>
```
```   458                insert (Crypt K X) (analz (insert X H))"
```
```   459 apply (rule subsetI)
```
```   460 apply (erule_tac x = x in analz.induct, auto)
```
```   461 done
```
```   462
```
```   463 lemma lemma2: "Key (invKey K) \<in> analz H ==>
```
```   464                insert (Crypt K X) (analz (insert X H)) \<subseteq>
```
```   465                analz (insert (Crypt K X) H)"
```
```   466 apply auto
```
```   467 apply (erule_tac x = x in analz.induct, auto)
```
```   468 apply (blast intro: analz_insertI analz.Decrypt)
```
```   469 done
```
```   470
```
```   471 lemma analz_insert_Decrypt:
```
```   472      "Key (invKey K) \<in> analz H ==>
```
```   473                analz (insert (Crypt K X) H) =
```
```   474                insert (Crypt K X) (analz (insert X H))"
```
```   475 by (intro equalityI lemma1 lemma2)
```
```   476
```
```   477 text{*Case analysis: either the message is secure, or it is not! Effective,
```
```   478 but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
```
```   479 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
```
```   480 (Crypt K X) H)"} *}
```
```   481 lemma analz_Crypt_if [simp]:
```
```   482      "analz (insert (Crypt K X) H) =
```
```   483           (if (Key (invKey K) \<in> analz H)
```
```   484            then insert (Crypt K X) (analz (insert X H))
```
```   485            else insert (Crypt K X) (analz H))"
```
```   486 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
```
```   487
```
```   488
```
```   489 text{*This rule supposes "for the sake of argument" that we have the key.*}
```
```   490 lemma analz_insert_Crypt_subset:
```
```   491      "analz (insert (Crypt K X) H) \<subseteq>
```
```   492            insert (Crypt K X) (analz (insert X H))"
```
```   493 apply (rule subsetI)
```
```   494 apply (erule analz.induct, auto)
```
```   495 done
```
```   496
```
```   497
```
```   498 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
```
```   499 apply auto
```
```   500 apply (erule analz.induct, auto)
```
```   501 done
```
```   502
```
```   503
```
```   504 subsubsection{*Idempotence and transitivity *}
```
```   505
```
```   506 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
```
```   507 by (erule analz.induct, blast+)
```
```   508
```
```   509 lemma analz_idem [simp]: "analz (analz H) = analz H"
```
```   510 by blast
```
```   511
```
```   512 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
```
```   513 apply (rule iffI)
```
```   514 apply (iprover intro: subset_trans analz_increasing)
```
```   515 apply (frule analz_mono, simp)
```
```   516 done
```
```   517
```
```   518 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
```
```   519 by (drule analz_mono, blast)
```
```   520
```
```   521
```
```   522 declare [[ atp_problem_prefix = "Message__analz_cut" ]]
```
```   523     declare analz_trans[intro]
```
```   524 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
```
```   525 (*TOO SLOW
```
```   526 by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
```
```   527 ??*)
```
```   528 by (erule analz_trans, blast)
```
```   529
```
```   530
```
```   531 text{*This rewrite rule helps in the simplification of messages that involve
```
```   532   the forwarding of unknown components (X).  Without it, removing occurrences
```
```   533   of X can be very complicated. *}
```
```   534 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
```
```   535 by (blast intro: analz_cut analz_insertI)
```
```   536
```
```   537
```
```   538 text{*A congruence rule for "analz" *}
```
```   539
```
```   540 declare [[ atp_problem_prefix = "Message__analz_subset_cong" ]]
```
```   541 lemma analz_subset_cong:
```
```   542      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
```
```   543       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
```
```   544 apply simp
```
```   545 apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)
```
```   546 done
```
```   547
```
```   548
```
```   549 lemma analz_cong:
```
```   550      "[| analz G = analz G'; analz H = analz H'
```
```   551                |] ==> analz (G \<union> H) = analz (G' \<union> H')"
```
```   552 by (intro equalityI analz_subset_cong, simp_all)
```
```   553
```
```   554 lemma analz_insert_cong:
```
```   555      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
```
```   556 by (force simp only: insert_def intro!: analz_cong)
```
```   557
```
```   558 text{*If there are no pairs or encryptions then analz does nothing*}
```
```   559 lemma analz_trivial:
```
```   560      "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
```
```   561 apply safe
```
```   562 apply (erule analz.induct, blast+)
```
```   563 done
```
```   564
```
```   565 text{*These two are obsolete (with a single Spy) but cost little to prove...*}
```
```   566 lemma analz_UN_analz_lemma:
```
```   567      "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
```
```   568 apply (erule analz.induct)
```
```   569 apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
```
```   570 done
```
```   571
```
```   572 lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
```
```   573 by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
```
```   574
```
```   575
```
```   576 subsection{*Inductive relation "synth"*}
```
```   577
```
```   578 text{*Inductive definition of "synth" -- what can be built up from a set of
```
```   579     messages.  A form of upward closure.  Pairs can be built, messages
```
```   580     encrypted with known keys.  Agent names are public domain.
```
```   581     Numbers can be guessed, but Nonces cannot be.  *}
```
```   582
```
```   583 inductive_set
```
```   584   synth :: "msg set => msg set"
```
```   585   for H :: "msg set"
```
```   586   where
```
```   587     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
```
```   588   | Agent  [intro]:   "Agent agt \<in> synth H"
```
```   589   | Number [intro]:   "Number n  \<in> synth H"
```
```   590   | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
```
```   591   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
```
```   592   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
```
```   593
```
```   594 text{*Monotonicity*}
```
```   595 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
```
```   596   by (auto, erule synth.induct, auto)
```
```   597
```
```   598 text{*NO @{text Agent_synth}, as any Agent name can be synthesized.
```
```   599   The same holds for @{term Number}*}
```
```   600 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
```
```   601 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
```
```   602 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
```
```   603 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
```
```   604 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
```
```   605
```
```   606
```
```   607 lemma synth_increasing: "H \<subseteq> synth(H)"
```
```   608 by blast
```
```   609
```
```   610 subsubsection{*Unions *}
```
```   611
```
```   612 text{*Converse fails: we can synth more from the union than from the
```
```   613   separate parts, building a compound message using elements of each.*}
```
```   614 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
```
```   615 by (intro Un_least synth_mono Un_upper1 Un_upper2)
```
```   616
```
```   617
```
```   618 declare [[ atp_problem_prefix = "Message__synth_insert" ]]
```
```   619
```
```   620 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
```
```   621 by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
```
```   622
```
```   623 subsubsection{*Idempotence and transitivity *}
```
```   624
```
```   625 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
```
```   626 by (erule synth.induct, blast+)
```
```   627
```
```   628 lemma synth_idem: "synth (synth H) = synth H"
```
```   629 by blast
```
```   630
```
```   631 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
```
```   632 apply (rule iffI)
```
```   633 apply (iprover intro: subset_trans synth_increasing)
```
```   634 apply (frule synth_mono, simp add: synth_idem)
```
```   635 done
```
```   636
```
```   637 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
```
```   638 by (drule synth_mono, blast)
```
```   639
```
```   640 declare [[ atp_problem_prefix = "Message__synth_cut" ]]
```
```   641 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
```
```   642 (*TOO SLOW
```
```   643 by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
```
```   644 *)
```
```   645 by (erule synth_trans, blast)
```
```   646
```
```   647
```
```   648 lemma Agent_synth [simp]: "Agent A \<in> synth H"
```
```   649 by blast
```
```   650
```
```   651 lemma Number_synth [simp]: "Number n \<in> synth H"
```
```   652 by blast
```
```   653
```
```   654 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
```
```   655 by blast
```
```   656
```
```   657 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
```
```   658 by blast
```
```   659
```
```   660 lemma Crypt_synth_eq [simp]:
```
```   661      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
```
```   662 by blast
```
```   663
```
```   664
```
```   665 lemma keysFor_synth [simp]:
```
```   666     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
```
```   667 by (unfold keysFor_def, blast)
```
```   668
```
```   669
```
```   670 subsubsection{*Combinations of parts, analz and synth *}
```
```   671
```
```   672 declare [[ atp_problem_prefix = "Message__parts_synth" ]]
```
```   673 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
```
```   674 apply (rule equalityI)
```
```   675 apply (rule subsetI)
```
```   676 apply (erule parts.induct)
```
```   677 apply (metis UnCI)
```
```   678 apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)
```
```   679 apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)
```
```   680 apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)
```
```   681 apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
```
```   682 done
```
```   683
```
```   684
```
```   685
```
```   686
```
```   687 declare [[ atp_problem_prefix = "Message__analz_analz_Un" ]]
```
```   688 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
```
```   689 apply (rule equalityI);
```
```   690 apply (metis analz_idem analz_subset_cong order_eq_refl)
```
```   691 apply (metis analz_increasing analz_subset_cong order_eq_refl)
```
```   692 done
```
```   693
```
```   694 declare [[ atp_problem_prefix = "Message__analz_synth_Un" ]]
```
```   695     declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
```
```   696 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
```
```   697 apply (rule equalityI)
```
```   698 apply (rule subsetI)
```
```   699 apply (erule analz.induct)
```
```   700 apply (metis UnCI UnE Un_commute analz.Inj)
```
```   701 apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
```
```   702 apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
```
```   703 apply (blast intro: analz.Decrypt)
```
```   704 apply blast
```
```   705 done
```
```   706
```
```   707 declare [[ atp_problem_prefix = "Message__analz_synth" ]]
```
```   708 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
```
```   709 proof (neg_clausify)
```
```   710 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
```
```   711 have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
```
```   712   by (metis analz_synth_Un)
```
```   713 have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
```
```   714   by (metis 0)
```
```   715 have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
```
```   716   by (metis 1 Un_commute)
```
```   717 have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
```
```   718   by (metis 3 Un_empty_right)
```
```   719 have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
```
```   720   by (metis 4 Un_empty_right)
```
```   721 have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
```
```   722   by (metis 5 Un_commute)
```
```   723 show "False"
```
```   724   by (metis 2 6)
```
```   725 qed
```
```   726
```
```   727
```
```   728 subsubsection{*For reasoning about the Fake rule in traces *}
```
```   729
```
```   730 declare [[ atp_problem_prefix = "Message__parts_insert_subset_Un" ]]
```
```   731 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
```
```   732 proof (neg_clausify)
```
```   733 assume 0: "X \<in> G"
```
```   734 assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
```
```   735 have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
```
```   736   by (metis 1 parts_Un)
```
```   737 have 3: "\<not> insert X H \<subseteq> G \<union> H"
```
```   738   by (metis 2 parts_mono)
```
```   739 have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
```
```   740   by (metis 3 insert_subset)
```
```   741 have 5: "X \<notin> G \<union> H"
```
```   742   by (metis 4 Un_upper2)
```
```   743 have 6: "X \<notin> G"
```
```   744   by (metis 5 UnCI)
```
```   745 show "False"
```
```   746   by (metis 6 0)
```
```   747 qed
```
```   748
```
```   749 declare [[ atp_problem_prefix = "Message__Fake_parts_insert" ]]
```
```   750 lemma Fake_parts_insert:
```
```   751      "X \<in> synth (analz H) ==>
```
```   752       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
```
```   753 proof (neg_clausify)
```
```   754 assume 0: "X \<in> synth (analz H)"
```
```   755 assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
```
```   756 have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
```
```   757   by (metis parts_synth parts_analz)
```
```   758 have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
```
```   759   by (metis analz_synth analz_idem)
```
```   760 have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
```
```   761   by (metis Un_upper1 analz_synth)
```
```   762 have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
```
```   763   by (metis 1 Un_commute)
```
```   764 have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
```
```   765   by (metis 5 2)
```
```   766 have 7: "\<not> insert X H \<subseteq> synth (analz H)"
```
```   767   by (metis 6 parts_mono)
```
```   768 have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
```
```   769   by (metis 7 insert_subset)
```
```   770 have 9: "\<not> H \<subseteq> synth (analz H)"
```
```   771   by (metis 8 0)
```
```   772 have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
```
```   773   by (metis analz_subset_iff 4)
```
```   774 have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
```
```   775   by (metis analz_subset_iff 10)
```
```   776 have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
```
```   777      \<not> analz X3 \<subseteq> synth (analz X3)"
```
```   778   by (metis Un_absorb1 3)
```
```   779 have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
```
```   780   by (metis 12 synth_increasing)
```
```   781 have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
```
```   782   by (metis 11 13)
```
```   783 show "False"
```
```   784   by (metis 9 14)
```
```   785 qed
```
```   786
```
```   787 lemma Fake_parts_insert_in_Un:
```
```   788      "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
```
```   789       ==> Z \<in>  synth (analz H) \<union> parts H";
```
```   790 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
```
```   791
```
```   792 declare [[ atp_problem_prefix = "Message__Fake_analz_insert" ]]
```
```   793     declare analz_mono [intro] synth_mono [intro]
```
```   794 lemma Fake_analz_insert:
```
```   795      "X\<in> synth (analz G) ==>
```
```   796       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
```
```   797 by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
```
```   798
```
```   799 declare [[ atp_problem_prefix = "Message__Fake_analz_insert_simpler" ]]
```
```   800 (*simpler problems?  BUT METIS CAN'T PROVE
```
```   801 lemma Fake_analz_insert_simpler:
```
```   802      "X\<in> synth (analz G) ==>
```
```   803       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
```
```   804 apply (rule subsetI)
```
```   805 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
```
```   806 apply (metis Un_commute analz_analz_Un analz_synth_Un)
```
```   807 apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
```
```   808 done
```
```   809 *)
```
```   810
```
```   811 end
```