23449

1 
(* Title: HOL/MetisTest/Message.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 


5 
Testing the metis method


6 
*)


7 


8 
theory Message imports Main begin


9 


10 
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)


11 
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"


12 
by blast


13 


14 
types


15 
key = nat


16 


17 
consts


18 
all_symmetric :: bool {*true if all keys are symmetric*}


19 
invKey :: "key=>key" {*inverse of a symmetric key*}


20 


21 
specification (invKey)


22 
invKey [simp]: "invKey (invKey K) = K"


23 
invKey_symmetric: "all_symmetric > invKey = id"


24 
by (rule exI [of _ id], auto)


25 


26 


27 
text{*The inverse of a symmetric key is itself; that of a public key


28 
is the private key and vice versa*}


29 


30 
constdefs


31 
symKeys :: "key set"


32 
"symKeys == {K. invKey K = K}"


33 


34 
datatype {*We allow any number of friendly agents*}


35 
agent = Server  Friend nat  Spy


36 


37 
datatype


38 
msg = Agent agent {*Agent names*}


39 
 Number nat {*Ordinary integers, timestamps, ...*}


40 
 Nonce nat {*Unguessable nonces*}


41 
 Key key {*Crypto keys*}


42 
 Hash msg {*Hashing*}


43 
 MPair msg msg {*Compound messages*}


44 
 Crypt key msg {*Encryption, public or sharedkey*}


45 


46 


47 
text{*Concrete syntax: messages appear as {A,B,NA}, etc...*}


48 
syntax


49 
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})")


50 


51 
syntax (xsymbols)


52 
"@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")


53 


54 
translations


55 
"{x, y, z}" == "{x, {y, z}}"


56 
"{x, y}" == "MPair x y"


57 


58 


59 
constdefs


60 
HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000])


61 
{*Message Y paired with a MAC computed with the help of X*}


62 
"Hash[X] Y == { Hash{X,Y}, Y}"


63 


64 
keysFor :: "msg set => key set"


65 
{*Keys useful to decrypt elements of a message set*}


66 
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"


67 


68 


69 
subsubsection{*Inductive Definition of All Parts" of a Message*}


70 


71 
consts parts :: "msg set => msg set"


72 
inductive "parts H"


73 
intros


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 
ML{*ResAtp.problem_name := "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 
ML{*ResAtp.problem_name := "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 blast+


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 
ML{*ResAtp.problem_name := "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 insert_commute 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 
ML{*ResAtp.problem_name := "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_Un parts_idem parts_increasing 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 
ML{*ResAtp.problem_name := "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_subset_iff Un_upper1 Un_upper2 insert_subset parts_Un parts_increasing parts_trans)


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 
ML{*ResAtp.problem_name := "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 
consts analz :: "msg set => msg set"


333 
inductive "analz H"


334 
intros


335 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"


336 
Fst: "{X,Y} \<in> analz H ==> X \<in> analz H"


337 
Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H"


338 
Decrypt [dest]:


339 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H"


340 


341 


342 
text{*Monotonicity; Lemma 1 of Lowe's paper*}


343 
lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"


344 
apply auto


345 
apply (erule analz.induct)


346 
apply (auto dest: analz.Fst analz.Snd)


347 
done


348 


349 
text{*Making it safe speeds up proofs*}


350 
lemma MPair_analz [elim!]:


351 
"[ {X,Y} \<in> analz H;


352 
[ X \<in> analz H; Y \<in> analz H ] ==> P


353 
] ==> P"


354 
by (blast dest: analz.Fst analz.Snd)


355 


356 
lemma analz_increasing: "H \<subseteq> analz(H)"


357 
by blast


358 


359 
lemma analz_subset_parts: "analz H \<subseteq> parts H"


360 
apply (rule subsetI)


361 
apply (erule analz.induct, blast+)


362 
done


363 


364 
lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]


365 


366 
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]


367 


368 


369 
ML{*ResAtp.problem_name := "Message__parts_analz"*}


370 
lemma parts_analz [simp]: "parts (analz H) = parts H"


371 
apply (rule equalityI)


372 
apply (metis analz_subset_parts parts_subset_iff)


373 
apply (metis analz_increasing parts_mono)


374 
done


375 


376 


377 
lemma analz_parts [simp]: "analz (parts H) = parts H"


378 
apply auto


379 
apply (erule analz.induct, auto)


380 
done


381 


382 
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]


383 


384 
subsubsection{*General equational properties *}


385 


386 
lemma analz_empty [simp]: "analz{} = {}"


387 
apply safe


388 
apply (erule analz.induct, blast+)


389 
done


390 


391 
text{*Converse fails: we can analz more from the union than from the


392 
separate parts, as a key in one might decrypt a message in the other*}


393 
lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"


394 
by (intro Un_least analz_mono Un_upper1 Un_upper2)


395 


396 
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"


397 
by (blast intro: analz_mono [THEN [2] rev_subsetD])


398 


399 
subsubsection{*Rewrite rules for pulling out atomic messages *}


400 


401 
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]


402 


403 
lemma analz_insert_Agent [simp]:


404 
"analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"


405 
apply (rule analz_insert_eq_I)


406 
apply (erule analz.induct, auto)


407 
done


408 


409 
lemma analz_insert_Nonce [simp]:


410 
"analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"


411 
apply (rule analz_insert_eq_I)


412 
apply (erule analz.induct, auto)


413 
done


414 


415 
lemma analz_insert_Number [simp]:


416 
"analz (insert (Number N) H) = insert (Number N) (analz H)"


417 
apply (rule analz_insert_eq_I)


418 
apply (erule analz.induct, auto)


419 
done


420 


421 
lemma analz_insert_Hash [simp]:


422 
"analz (insert (Hash X) H) = insert (Hash X) (analz H)"


423 
apply (rule analz_insert_eq_I)


424 
apply (erule analz.induct, auto)


425 
done


426 


427 
text{*Can only pull out Keys if they are not needed to decrypt the rest*}


428 
lemma analz_insert_Key [simp]:


429 
"K \<notin> keysFor (analz H) ==>


430 
analz (insert (Key K) H) = insert (Key K) (analz H)"


431 
apply (unfold keysFor_def)


432 
apply (rule analz_insert_eq_I)


433 
apply (erule analz.induct, auto)


434 
done


435 


436 
lemma analz_insert_MPair [simp]:


437 
"analz (insert {X,Y} H) =


438 
insert {X,Y} (analz (insert X (insert Y H)))"


439 
apply (rule equalityI)


440 
apply (rule subsetI)


441 
apply (erule analz.induct, auto)


442 
apply (erule analz.induct)


443 
apply (blast intro: analz.Fst analz.Snd)+


444 
done


445 


446 
text{*Can pull out enCrypted message if the Key is not known*}


447 
lemma analz_insert_Crypt:


448 
"Key (invKey K) \<notin> analz H


449 
==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"


450 
apply (rule analz_insert_eq_I)


451 
apply (erule analz.induct, auto)


452 


453 
done


454 


455 
lemma lemma1: "Key (invKey K) \<in> analz H ==>


456 
analz (insert (Crypt K X) H) \<subseteq>


457 
insert (Crypt K X) (analz (insert X H))"


458 
apply (rule subsetI)


459 
apply (erule_tac xa = x in analz.induct, auto)


460 
done


461 


462 
lemma lemma2: "Key (invKey K) \<in> analz H ==>


463 
insert (Crypt K X) (analz (insert X H)) \<subseteq>


464 
analz (insert (Crypt K X) H)"


465 
apply auto


466 
apply (erule_tac xa = x in analz.induct, auto)


467 
apply (blast intro: analz_insertI analz.Decrypt)


468 
done


469 


470 
lemma analz_insert_Decrypt:


471 
"Key (invKey K) \<in> analz H ==>


472 
analz (insert (Crypt K X) H) =


473 
insert (Crypt K X) (analz (insert X H))"


474 
by (intro equalityI lemma1 lemma2)


475 


476 
text{*Case analysis: either the message is secure, or it is not! Effective,


477 
but can cause subgoals to blow up! Use with @{text "split_if"}; apparently


478 
@{text "split_tac"} does not cope with patterns such as @{term"analz (insert


479 
(Crypt K X) H)"} *}


480 
lemma analz_Crypt_if [simp]:


481 
"analz (insert (Crypt K X) H) =


482 
(if (Key (invKey K) \<in> analz H)


483 
then insert (Crypt K X) (analz (insert X H))


484 
else insert (Crypt K X) (analz H))"


485 
by (simp add: analz_insert_Crypt analz_insert_Decrypt)


486 


487 


488 
text{*This rule supposes "for the sake of argument" that we have the key.*}


489 
lemma analz_insert_Crypt_subset:


490 
"analz (insert (Crypt K X) H) \<subseteq>


491 
insert (Crypt K X) (analz (insert X H))"


492 
apply (rule subsetI)


493 
apply (erule analz.induct, auto)


494 
done


495 


496 


497 
lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"


498 
apply auto


499 
apply (erule analz.induct, auto)


500 
done


501 


502 


503 
subsubsection{*Idempotence and transitivity *}


504 


505 
lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"


506 
by (erule analz.induct, blast+)


507 


508 
lemma analz_idem [simp]: "analz (analz H) = analz H"


509 
by blast


510 


511 
lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"


512 
apply (rule iffI)


513 
apply (iprover intro: subset_trans analz_increasing)


514 
apply (frule analz_mono, simp)


515 
done


516 


517 
lemma analz_trans: "[ X\<in> analz G; G \<subseteq> analz H ] ==> X\<in> analz H"


518 
by (drule analz_mono, blast)


519 


520 


521 
ML{*ResAtp.problem_name := "Message__analz_cut"*}


522 
declare analz_trans[intro]


523 
lemma analz_cut: "[ Y\<in> analz (insert X H); X\<in> analz H ] ==> Y\<in> analz H"


524 
(*TOO SLOW


525 
by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) {*317s*}


526 
??*)


527 
by (erule analz_trans, blast)


528 


529 


530 
text{*This rewrite rule helps in the simplification of messages that involve


531 
the forwarding of unknown components (X). Without it, removing occurrences


532 
of X can be very complicated. *}


533 
lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"


534 
by (blast intro: analz_cut analz_insertI)


535 


536 


537 
text{*A congruence rule for "analz" *}


538 


539 
ML{*ResAtp.problem_name := "Message__analz_subset_cong"*}


540 
lemma analz_subset_cong:


541 
"[ analz G \<subseteq> analz G'; analz H \<subseteq> analz H' ]


542 
==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"


543 
apply simp


544 
apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)


545 
done


546 


547 


548 
lemma analz_cong:


549 
"[ analz G = analz G'; analz H = analz H'


550 
] ==> analz (G \<union> H) = analz (G' \<union> H')"


551 
by (intro equalityI analz_subset_cong, simp_all)


552 


553 
lemma analz_insert_cong:


554 
"analz H = analz H' ==> analz(insert X H) = analz(insert X H')"


555 
by (force simp only: insert_def intro!: analz_cong)


556 


557 
text{*If there are no pairs or encryptions then analz does nothing*}


558 
lemma analz_trivial:


559 
"[ \<forall>X Y. {X,Y} \<notin> H; \<forall>X K. Crypt K X \<notin> H ] ==> analz H = H"


560 
apply safe


561 
apply (erule analz.induct, blast+)


562 
done


563 


564 
text{*These two are obsolete (with a single Spy) but cost little to prove...*}


565 
lemma analz_UN_analz_lemma:


566 
"X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"


567 
apply (erule analz.induct)


568 
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+


569 
done


570 


571 
lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"


572 
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])


573 


574 


575 
subsection{*Inductive relation "synth"*}


576 


577 
text{*Inductive definition of "synth"  what can be built up from a set of


578 
messages. A form of upward closure. Pairs can be built, messages


579 
encrypted with known keys. Agent names are public domain.


580 
Numbers can be guessed, but Nonces cannot be. *}


581 


582 
consts synth :: "msg set => msg set"


583 
inductive "synth H"


584 
intros


585 
Inj [intro]: "X \<in> H ==> X \<in> synth H"


586 
Agent [intro]: "Agent agt \<in> synth H"


587 
Number [intro]: "Number n \<in> synth H"


588 
Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"


589 
MPair [intro]: "[X \<in> synth H; Y \<in> synth H] ==> {X,Y} \<in> synth H"


590 
Crypt [intro]: "[X \<in> synth H; Key(K) \<in> H] ==> Crypt K X \<in> synth H"


591 


592 
text{*Monotonicity*}


593 
lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"


594 
by (auto, erule synth.induct, auto)


595 


596 
text{*NO @{text Agent_synth}, as any Agent name can be synthesized.


597 
The same holds for @{term Number}*}


598 
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"


599 
inductive_cases Key_synth [elim!]: "Key K \<in> synth H"


600 
inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"


601 
inductive_cases MPair_synth [elim!]: "{X,Y} \<in> synth H"


602 
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"


603 


604 


605 
lemma synth_increasing: "H \<subseteq> synth(H)"


606 
by blast


607 


608 
subsubsection{*Unions *}


609 


610 
text{*Converse fails: we can synth more from the union than from the


611 
separate parts, building a compound message using elements of each.*}


612 
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"


613 
by (intro Un_least synth_mono Un_upper1 Un_upper2)


614 


615 


616 
ML{*ResAtp.problem_name := "Message__synth_insert"*}


617 


618 
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"


619 
by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)


620 


621 
subsubsection{*Idempotence and transitivity *}


622 


623 
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"


624 
by (erule synth.induct, blast+)


625 


626 
lemma synth_idem: "synth (synth H) = synth H"


627 
by blast


628 


629 
lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"


630 
apply (rule iffI)


631 
apply (iprover intro: subset_trans synth_increasing)


632 
apply (frule synth_mono, simp add: synth_idem)


633 
done


634 


635 
lemma synth_trans: "[ X\<in> synth G; G \<subseteq> synth H ] ==> X\<in> synth H"


636 
by (drule synth_mono, blast)


637 


638 
ML{*ResAtp.problem_name := "Message__synth_cut"*}


639 
lemma synth_cut: "[ Y\<in> synth (insert X H); X\<in> synth H ] ==> Y\<in> synth H"


640 
(*TOO SLOW


641 
by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)


642 
*)


643 
by (erule synth_trans, blast)


644 


645 


646 
lemma Agent_synth [simp]: "Agent A \<in> synth H"


647 
by blast


648 


649 
lemma Number_synth [simp]: "Number n \<in> synth H"


650 
by blast


651 


652 
lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"


653 
by blast


654 


655 
lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"


656 
by blast


657 


658 
lemma Crypt_synth_eq [simp]:


659 
"Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"


660 
by blast


661 


662 


663 
lemma keysFor_synth [simp]:


664 
"keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"


665 
by (unfold keysFor_def, blast)


666 


667 


668 
subsubsection{*Combinations of parts, analz and synth *}


669 


670 
ML{*ResAtp.problem_name := "Message__parts_synth"*}


671 
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"


672 
apply (rule equalityI)


673 
apply (rule subsetI)


674 
apply (erule parts.induct)


675 
apply (metis UnCI)


676 
apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)


677 
apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)


678 
apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)


679 
apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)


680 
done


681 


682 


683 


684 


685 
ML{*ResAtp.problem_name := "Message__analz_analz_Un"*}


686 
lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"


687 
apply (rule equalityI);


688 
apply (metis analz_idem analz_subset_cong order_eq_refl)


689 
apply (metis analz_increasing analz_subset_cong order_eq_refl)


690 
done


691 


692 
ML{*ResAtp.problem_name := "Message__analz_synth_Un"*}


693 
declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]


694 
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"


695 
apply (rule equalityI)


696 
apply (rule subsetI)


697 
apply (erule analz.induct)


698 
apply (metis UnCI UnE Un_commute analz.Inj)


699 
apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)


700 
apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)


701 
apply (blast intro: analz.Decrypt)


702 
apply (metis Diff_Int Diff_empty Diff_subset_conv Int_empty_right Un_commute Un_subset_iff Un_upper1 analz_increasing analz_mono synth_increasing)


703 
done


704 


705 


706 
ML{*ResAtp.problem_name := "Message__analz_synth"*}


707 
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"


708 
proof (neg_clausify)


709 
assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"


710 
have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"


711 
by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)


712 
have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"


713 
by (metis 0 sup_set_eq)


714 
have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"


715 
by (metis 1 Un_commute sup_set_eq sup_set_eq)


716 
have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"


717 
by (metis 3 Un_empty_right sup_set_eq)


718 
have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"


719 
by (metis 4 Un_empty_right sup_set_eq)


720 
have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"


721 
by (metis 5 Un_commute sup_set_eq sup_set_eq)


722 
show "False"


723 
by (metis 2 6)


724 
qed


725 


726 


727 
subsubsection{*For reasoning about the Fake rule in traces *}


728 


729 
ML{*ResAtp.problem_name := "Message__parts_insert_subset_Un"*}


730 
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"


731 
proof (neg_clausify)


732 
assume 0: "X \<in> G"


733 
assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"


734 
have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"


735 
by (metis 1 parts_Un)


736 
have 3: "\<not> insert X H \<subseteq> G \<union> H"


737 
by (metis 2 parts_mono)


738 
have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"


739 
by (metis 3 insert_subset)


740 
have 5: "X \<notin> G \<union> H"


741 
by (metis 4 Un_upper2)


742 
have 6: "X \<notin> G"


743 
by (metis 5 UnCI)


744 
show "False"


745 
by (metis 6 0)


746 
qed


747 


748 
ML{*ResAtp.problem_name := "Message__Fake_parts_insert"*}


749 
lemma Fake_parts_insert:


750 
"X \<in> synth (analz H) ==>


751 
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"


752 
proof (neg_clausify)


753 
assume 0: "X \<in> synth (analz H)"


754 
assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"


755 
have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"


756 
by (metis parts_synth parts_analz)


757 
have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"


758 
by (metis analz_synth analz_idem)


759 
have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"


760 
by (metis Un_upper1 analz_synth)


761 
have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"


762 
by (metis 1 Un_commute)


763 
have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"


764 
by (metis 5 2)


765 
have 7: "\<not> insert X H \<subseteq> synth (analz H)"


766 
by (metis 6 parts_mono)


767 
have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"


768 
by (metis 7 insert_subset)


769 
have 9: "\<not> H \<subseteq> synth (analz H)"


770 
by (metis 8 0)


771 
have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"


772 
by (metis analz_subset_iff 4)


773 
have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"


774 
by (metis analz_subset_iff 10)


775 
have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>


776 
\<not> analz X3 \<subseteq> synth (analz X3)"


777 
by (metis Un_absorb1 3)


778 
have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"


779 
by (metis 12 synth_increasing)


780 
have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"


781 
by (metis 11 13)


782 
show "False"


783 
by (metis 9 14)


784 
qed


785 


786 
lemma Fake_parts_insert_in_Un:


787 
"[Z \<in> parts (insert X H); X: synth (analz H)]


788 
==> Z \<in> synth (analz H) \<union> parts H";


789 
by (blast dest: Fake_parts_insert [THEN subsetD, dest])


790 


791 
ML{*ResAtp.problem_name := "Message__Fake_analz_insert"*}


792 
declare analz_mono [intro] synth_mono [intro]


793 
lemma Fake_analz_insert:


794 
"X\<in> synth (analz G) ==>


795 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"


796 
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))


797 


798 
ML{*ResAtp.problem_name := "Message__Fake_analz_insert_simpler"*}


799 
(*simpler problems? BUT METIS CAN'T PROVE


800 
lemma Fake_analz_insert_simpler:


801 
"X\<in> synth (analz G) ==>


802 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"


803 
apply (rule subsetI)


804 
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")


805 
apply (metis Un_commute analz_analz_Un analz_synth_Un)


806 
apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)


807 
done


808 
*)


809 


810 
end
