Theory Message_derivation

(*******************************************************************************

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Message_derivation.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Message_derivation.thy 132885 2016-12-23 18:41:32Z csprenge $
  Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  A theory of message derivations (analz, synth, parts).
  Based on Larry Paulson's theory HOL/Auth/Message.thy, but extended with
  - composed keys
  - including ephemeral asymmetric keys
  - Diffie-Hellman exponentiation and associated equational theory

  Copyright (c) 2015-2016 Joseph Lallemand and Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

section ‹Message theory›

theory Message_derivation
imports Messages
begin

text ‹This theory is adapted from Larry Paulson's original Message theory.›


(****************************************************************************************)
subsection ‹Message composition›
(****************************************************************************************)

text ‹Dolev-Yao message synthesis.›

inductive_set
  synth :: "msg set ⇒ msg set"
  for H :: "msg set"
  where
    Ax [intro]: "X ∈ H ⟹ X ∈ synth H"
  | Agent [simp, intro]: "Agent A ∈ synth H"
  | Number [simp, intro]: "Number n ∈ synth H"
  | NonceA [simp, intro]: "NonceA n ∈ synth H"
  | EpubKA [simp, intro]: "epubKA n ∈ synth H"
  | EpriKA [simp, intro]: "epriKA n ∈ synth H"
  | Hash [intro]: "X ∈ synth H ⟹ Hash X ∈ synth H"
  | Pair [intro]: "X ∈ synth H ⟹ Y ∈ synth H ⟹ (Pair X Y) ∈ synth H"
  | Enc [intro]: "X ∈ synth H ⟹ Y ∈ synth H ⟹ (Enc X Y) ∈ synth H"
  | Aenc [intro]: "X ∈ synth H ⟹ Y ∈ synth H ⟹ (Aenc X Y) ∈ synth H"
  | Sign [intro]: "X ∈ synth H ⟹ Y ∈ synth H ⟹ Sign X Y ∈ synth H"
  | Exp [intro]: "X ∈ synth H ⟹ Y ∈ synth H ⟹ (Exp X Y) ∈ synth H"


text ‹Lemmas about Dolev-Yao message synthesis.›

lemma synth_mono [mono_set]: "G ⊆ H ⟹ synth G ⊆ synth H"
  by (auto, erule synth.induct, auto)

lemmas synth_monotone = synth_mono [THEN [2] rev_subsetD]

― ‹‹[elim!]› slows down certain proofs, e.g., ‹⟦ synth H ∩ B ⊆ {} ⟧ ⟹ P››
inductive_cases NonceF_synth: "NonceF n ∈ synth H"
inductive_cases LtK_synth: "LtK K ∈ synth H"
inductive_cases EpubKF_synth: "epubKF K ∈ synth H"
inductive_cases EpriKF_synth: "epriKF K ∈ synth H"
inductive_cases Hash_synth: "Hash X ∈ synth H"
inductive_cases Pair_synth: "Pair X Y ∈ synth H"
inductive_cases Enc_synth: "Enc X K ∈ synth H"
inductive_cases Aenc_synth: "Aenc X K ∈ synth H"
inductive_cases Sign_synth: "Sign X K ∈ synth H"
inductive_cases Tag_synth: "Tag t ∈ synth H"

lemma EpriK_synth [elim]: "epriK K ∈ synth H ⟹
       epriK K ∈ H ∨ (∃ N. epriK K = epriKA N)"
by (cases K, auto elim: EpriKF_synth)

lemma EpubK_synth [elim]: "epubK K ∈ synth H ⟹
       epubK K ∈ H ∨ (∃ N. epubK K = epubKA N)"
by (cases K, auto elim: EpubKF_synth)

lemmas synth_inversion [elim] =
  NonceF_synth LtK_synth EpubKF_synth EpriKF_synth Hash_synth Pair_synth
  Enc_synth Aenc_synth Sign_synth Tag_synth


lemma synth_increasing: "H ⊆ synth H"
by blast

lemma synth_Int1: "x ∈ synth (A ∩ B) ⟹ x ∈ synth A "
  by (erule synth.induct) (auto)

lemma synth_Int2: "x ∈ synth (A ∩ B) ⟹ x ∈ synth B"
  by (erule synth.induct) (auto)

lemma synth_Int: "x ∈ synth (A ∩ B) ⟹ x ∈ synth A ∩ synth B"
  by (blast intro: synth_Int1 synth_Int2)

lemma synth_Un: "synth G ∪ synth H ⊆ synth (G ∪ H)"
by (intro Un_least synth_mono Un_upper1 Un_upper2)

lemma synth_insert: "insert X (synth H) ⊆ synth (insert X H)"
by (blast intro: synth_mono [THEN [2] rev_subsetD])

lemma synth_synthD [dest!]: "X ∈ synth (synth H) ⟹ X ∈ synth H"
by (erule synth.induct, blast+)

lemma synth_idem [simp]: "synth (synth H) = synth H"
by blast

lemma synth_subset_iff: "synth G ⊆ synth H ⟷ G ⊆ synth H"
by (blast dest: synth_mono)

lemma synth_trans: "⟦ X ∈ synth G; G ⊆ synth H ⟧ ⟹ X ∈ synth H"
by (drule synth_mono, blast)

lemma synth_cut: "⟦ Y ∈ synth (insert X H); X ∈ synth H ⟧ ⟹ Y ∈ synth H"
by (erule synth_trans, blast)


lemma Nonce_synth_eq [simp]: "(NonceF N ∈ synth H) = (NonceF N ∈ H)"
by blast

lemma LtK_synth_eq [simp]: "(LtK K ∈ synth H) = (LtK K ∈ H)"
by blast

lemma EpubKF_synth_eq [simp]: "(epubKF K ∈ synth H) = (epubKF K ∈ H)"
by blast

lemma EpriKF_synth_eq [simp]: "(epriKF K ∈ synth H) = (epriKF K ∈ H)"
by blast

lemma Enc_synth_eq1 [simp]:
     "K ∉ synth H ⟹ (Enc X K ∈ synth H) = (Enc X K ∈ H)"
by blast

lemma Enc_synth_eq2 [simp]:
     "X ∉ synth H ⟹ (Enc X K ∈ synth H) = (Enc X K ∈ H)"
by blast

lemma Aenc_synth_eq1 [simp]:
     "K ∉ synth H ⟹ (Aenc X K ∈ synth H) = (Aenc X K ∈ H)"
by blast

lemma Aenc_synth_eq2 [simp]:
     "X ∉ synth H ⟹ (Aenc X K ∈ synth H) = (Aenc X K ∈ H)"
by blast

lemma Sign_synth_eq1 [simp]:
     "K ∉ synth H ⟹ (Sign X K ∈ synth H) = (Sign X K ∈ H)"
by blast

lemma Sign_synth_eq2 [simp]:
     "X ∉ synth H ⟹ (Sign X K ∈ synth H) = (Sign X K ∈ H)"
by blast

(****************************************************************************************)
subsection ‹Message decomposition›
(****************************************************************************************)

text ‹Dolev-Yao message decomposition using known keys.›

inductive_set
  analz :: "msg set ⇒ msg set"
  for H :: "msg set"
  where
    Ax [intro]: "X ∈ H ⟹ X ∈ analz H"
  | Fst: "Pair X Y ∈ analz H ⟹ X ∈ analz H"
  | Snd: "Pair X Y ∈ analz H ⟹ Y ∈ analz H"
  | Dec [dest]:
      "⟦ Enc X Y ∈ analz H; Y ∈ synth (analz H) ⟧ ⟹ X ∈ analz H"
  | Adec_lt [dest]:
      "⟦ Aenc X (LtK (publK Y)) ∈ analz H; priK Y ∈ analz H ⟧ ⟹ X ∈ analz H"
  | Adec_eph [dest]:
      "⟦ Aenc X (EphK (epublK Y)) ∈ analz H; epriK Y ∈ synth (analz H) ⟧ ⟹ X ∈ analz H"
  | Sign_getmsg [dest]:
      "Sign X (priK Y) ∈ analz H ⟹ pubK Y ∈ analz H ⟹ X ∈ analz H"


text ‹Lemmas about Dolev-Yao message decomposition.›

lemma analz_mono: "G ⊆ H ⟹ analz(G) ⊆ analz(H)"
by (safe, erule analz.induct) (auto dest: Fst Snd synth_Int2)

lemmas analz_monotone = analz_mono [THEN [2] rev_subsetD]


lemma Pair_analz [elim!]:
  "⟦ Pair X Y ∈ analz H; ⟦ X ∈ analz H; Y ∈ analz H ⟧ ⟹ P ⟧ ⟹ P"
by (blast dest: analz.Fst analz.Snd)


lemma analz_empty [simp]: "analz {} = {}"
by (safe, erule analz.induct) (blast+)

lemma analz_increasing: "H ⊆ analz(H)"
by auto

lemma analz_analzD [dest!]: "X ∈ analz (analz H) ⟹ X ∈ analz H"
by (induction X rule: analz.induct) (auto dest: synth_monotone)

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


lemma analz_Un: "analz G ∪ analz H ⊆ analz (G ∪ H)"
by (intro Un_least analz_mono Un_upper1 Un_upper2)

lemma analz_insertI: "X ∈ analz H ⟹ X ∈ analz (insert Y H)"
by (blast intro: analz_monotone)

lemma analz_insert: "insert X (analz H) ⊆ analz (insert X H)"
by (blast intro: analz_monotone)

lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]


lemma analz_subset_iff [simp]: "analz G ⊆ analz H ⟷ G ⊆ analz H"
by (blast dest: analz_mono)

lemma analz_trans: "X ∈ analz G ⟹  G ⊆ analz H ⟹ X ∈ analz H"
by (drule analz_mono) blast

lemma analz_cut: "Y ∈ analz (insert X H) ⟹  X ∈ analz H ⟹ Y ∈ analz H"
by (erule analz_trans) blast

lemma analz_insert_eq: "X ∈ analz H ⟹ analz (insert X H) = analz H"
by (blast intro: analz_cut analz_insertI)


lemma analz_subset_cong:
  "analz G ⊆ analz G' ⟹
   analz H ⊆ analz H' ⟹
   analz (G ∪ H) ⊆ analz (G' ∪ H')"
apply simp
apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
done

lemma analz_cong:
  "analz G = analz G' ⟹
   analz H = analz H' ⟹
   analz (G ∪ H) = analz (G' ∪ H')"
by (intro equalityI analz_subset_cong, simp_all)

lemma analz_insert_cong:
  "analz H = analz H' ⟹
   analz (insert X H) = analz (insert X H')"
by (force simp only: insert_def intro!: analz_cong)

lemma analz_trivial:
  "∀X Y. Pair X Y ∉ H ⟹
   ∀X Y. Enc X Y ∉ H ⟹
   ∀X Y. Aenc X Y ∉ H ⟹
   ∀X Y. Sign X Y ∉ H ⟹
   analz H = H"
apply safe
apply (erule analz.induct, blast+)
done


lemma analz_analz_Un [simp]: "analz (analz G ∪ H) = analz (G ∪ H)"
apply (intro equalityI analz_subset_cong)+
apply simp_all
done

lemma analz_Un_analz [simp]: "analz (G ∪ analz H) = analz (G ∪ H)"
by (subst Un_commute, auto)+


text ‹Lemmas about analz and insert.›

lemma analz_insert_Agent [simp]:
  "analz (insert (Agent A) H) = insert (Agent A) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct)
thm analz.induct
apply fastforce
apply fastforce
apply fastforce
defer 1
apply fastforce
defer 1
apply fastforce

apply (rename_tac x X Y)
apply (subgoal_tac "Y ∈ synth (analz H)", auto)
apply (thin_tac "Enc X Y ∈ Z" for Z)+
apply (drule synth_Int2, auto)
apply (erule synth.induct, auto)

apply (rename_tac X Y)
apply (subgoal_tac "epriK Y ∈ synth (analz H)", auto)
apply (thin_tac "Aenc X (epubK Y) ∈ Z" for Z)+
apply (erule synth.induct, auto)
done



(****************************************************************************************)
subsection ‹Lemmas about combined composition/decomposition›
(****************************************************************************************)

lemma synth_analz_incr: "H ⊆ synth (analz H)"
by auto

lemmas synth_analz_increasing = synth_analz_incr [THEN [2] rev_subsetD]

lemma synth_analz_mono: "G ⊆ H ⟹ synth (analz G) ⊆ synth (analz H)"
by (blast intro!: analz_mono synth_mono)

lemmas synth_analz_monotone = synth_analz_mono [THEN [2] rev_subsetD]

lemma lem1:
  "Y ∈ synth (analz (synth G ∪ H) ∩ (analz (G ∪ H) ∪ synth G))
⟹ Y ∈ synth (analz (G ∪ H))"
apply (rule subsetD, auto simp add: synth_subset_iff intro: analz_increasing synth_monotone)
done

lemma lem2: "{a. a ∈ analz (G ∪ H) ∨ a ∈ synth G} = analz (G ∪ H) ∪ synth G" by auto

lemma analz_synth_Un: "analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G"
proof (intro equalityI subsetI)
  fix x
  assume "x ∈ analz (synth G ∪ H)"
  thus "x ∈ analz (G ∪ H) ∪ synth G"
  by (induction x rule: analz.induct)
     (auto simp add: lem2 intro: analz_monotone Fst Snd Dec Adec_eph Adec_lt Sign_getmsg
           dest: lem1)
next
  fix x
  assume "x ∈ analz (G ∪ H) ∪ synth G"
  thus "x ∈ analz (synth G ∪ H)"
    by (blast intro: analz_monotone)
qed


lemma analz_synth: "analz (synth H) = analz H ∪ synth H"
by (rule analz_synth_Un [where H="{}", simplified])


lemma analz_synth_Un2 [simp]: "analz (G ∪ synth H) = analz (G ∪ H) ∪ synth H"
by (subst Un_commute, auto simp add: analz_synth_Un)+


lemma synth_analz_synth [simp]: "synth (analz (synth H)) = synth (analz H)"
by (auto del:subsetI) (auto simp add: synth_subset_iff analz_synth)

lemma analz_synth_analz [simp]: "analz (synth (analz H)) = synth (analz H)"
by (auto simp add: analz_synth)

lemma synth_analz_idem [simp]: "synth (analz (synth (analz H))) = synth (analz H)"
by (simp only: analz_synth_analz) simp


lemma insert_subset_synth_analz [simp]:
  "X ∈ synth (analz H) ⟹ insert X H ⊆ synth (analz H)"
by auto


lemma synth_analz_insert [simp]:
  assumes "X ∈ synth (analz H)"
  shows "synth (analz (insert X H)) = synth (analz H)"
using assms
proof (intro equalityI subsetI)
  fix Z
  assume "Z ∈ synth (analz (insert X H))"
  hence "Z ∈ synth (analz (synth (analz H)))" using assms
    by - (erule synth_analz_monotone, rule insert_subset_synth_analz)
  thus "Z ∈ synth (analz H)" using assms by simp
qed (auto intro: synth_analz_monotone)


(****************************************************************************************)
subsection ‹Accessible message parts›
(****************************************************************************************)

text ‹Accessible message parts: all subterms that are in principle extractable
by the Dolev-Yao attacker, i.e., provided he knows all keys. Note that keys in
key positions and messages under hashes are not message parts in this sense.›

inductive_set
  parts :: "msg set => msg set"
  for H :: "msg set"
where
    Inj [intro]: "X ∈ H ⟹ X ∈ parts H"
  | Fst [intro]: "Pair X Y ∈ parts H ⟹ X ∈ parts H"
  | Snd [intro]: "Pair X Y ∈ parts H ⟹ Y ∈ parts H"
  | Dec [intro]: "Enc X Y ∈ parts H ⟹ X ∈ parts H"
  | Adec [intro]: "Aenc X Y ∈ parts H ⟹ X ∈ parts H"
  | Sign_getmsg [intro]: "Sign X Y ∈ parts H ⟹ X ∈ parts H"


text ‹Lemmas about accessible message parts.›

lemma parts_mono [mono_set]: "G ⊆ H ⟹ parts G ⊆ parts H"
by (auto, erule parts.induct, auto)

lemmas parts_monotone = parts_mono [THEN [2] rev_subsetD]


lemma Pair_parts [elim]:
  "⟦ Pair X Y ∈ parts H; ⟦ X ∈ parts H; Y ∈ parts H ⟧ ⟹ P ⟧ ⟹ P"
by blast


lemma parts_increasing: "H ⊆ parts H"
by blast

lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]

lemma parts_empty [simp]: "parts {} = {}"
by (safe, erule parts.induct, auto)

lemma parts_atomic [simp]: "atomic x ⟹ parts {x} = {x}"
by (auto, erule parts.induct, auto)

lemma parts_InsecTag [simp]: "parts {Tag t} = {Tag t}"
by (safe, erule parts.induct) (auto)

lemma parts_emptyE [elim!]: "X ∈ parts {} ⟹ P"
by simp

lemma parts_Tags [simp]:
  "parts Tags = Tags"
by (rule, rule, erule parts.induct, auto)

lemma parts_singleton: "X ∈ parts H ⟹ ∃ Y∈H. X ∈ parts {Y}"
by (erule parts.induct, blast+)

lemma parts_Agents [simp]:
  "parts (Agent` G) = Agent` G"
by (auto elim: parts.induct)

lemma parts_Un [simp]: "parts (G ∪ H) = parts G ∪ parts H"
proof
  show "parts (G ∪ H) ⊆ parts G ∪ parts H"
    by (rule, erule parts.induct) (auto)
next
  show "parts G ∪ parts H ⊆ parts (G ∪ H)"
    by (intro Un_least parts_mono Un_upper1 Un_upper2)
qed

lemma parts_insert_subset_Un:
  assumes "X ∈ G"
  shows "parts (insert X H) ⊆ parts G ∪ parts H"
proof -
  from assms have "parts (insert X H) ⊆ parts (G ∪ H)" by (blast intro!: parts_mono)
  thus ?thesis by simp
qed

lemma parts_insert: "parts (insert X H) = parts {X} ∪ parts H"
by (blast intro!: parts_insert_subset_Un intro: parts_monotone)

lemma parts_insert2:
  "parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H"
apply (simp add: Un_assoc)
apply (simp add: parts_insert [symmetric])
done


lemmas in_parts_UnE [elim!] = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]


lemma parts_insert_subset: "insert X (parts H) ⊆ parts (insert X H)"
by (blast intro: parts_mono [THEN [2] rev_subsetD])


lemma parts_partsD [dest!]: "X ∈ parts (parts H) ⟹ X ∈ parts H"
by (erule parts.induct, blast+)

lemma parts_idem [simp]: "parts (parts H) = parts H"
by blast

lemma parts_subset_iff [simp]: "(parts G ⊆ parts H) ⟷ (G ⊆ parts H)"
by (blast dest: parts_mono)

lemma parts_trans: "X ∈ parts G ⟹  G ⊆ parts H ⟹ X ∈ parts H"
by (drule parts_mono, blast)


lemma parts_cut:
  "Y ∈ parts (insert X G) ⟹  X ∈ parts H ⟹ Y ∈ parts (G ∪ H)"
by (blast intro: parts_trans)


lemma parts_cut_eq [simp]: "X ∈ parts H ⟹ parts (insert X H) = parts H"
by (force dest!: parts_cut intro: parts_insertI)


lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]


lemma parts_insert_Agent [simp]:
  "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
by (rule parts_insert_eq_I, erule parts.induct, auto)

lemma parts_insert_Nonce [simp]:
  "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
by (rule parts_insert_eq_I, erule parts.induct, auto)

lemma parts_insert_Number [simp]:
  "parts (insert (Number N) H) = insert (Number N) (parts H)"
by (rule parts_insert_eq_I, erule parts.induct, auto)

lemma parts_insert_LtK [simp]:
  "parts (insert (LtK K) H) = insert (LtK K) (parts H)"
by (rule parts_insert_eq_I, erule parts.induct, auto)

lemma parts_insert_Hash [simp]:
  "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
by (rule parts_insert_eq_I, erule parts.induct, auto)


lemma parts_insert_Enc [simp]:
  "parts (insert (Enc X Y) H) = insert (Enc X Y) (parts {X} ∪ parts H)"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
done

lemma parts_insert_Aenc [simp]:
  "parts (insert (Aenc X Y) H) = insert (Aenc X Y) (parts {X} ∪ parts H)"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
done

lemma parts_insert_Sign [simp]:
  "parts (insert (Sign X Y) H) = insert (Sign X Y) (parts {X} ∪ parts H)"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
done

lemma parts_insert_Pair [simp]:
  "parts (insert (Pair X Y) H) = insert (Pair X Y) (parts {X} ∪ parts {Y} ∪ parts H)"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
done


subsubsection ‹Lemmas about combinations with composition and decomposition›
(****************************************************************************************)

lemma analz_subset_parts: "analz H ⊆ parts H"
apply (rule subsetI)
apply (erule analz.induct, blast+)
done

lemmas analz_into_parts [simp] = analz_subset_parts [THEN subsetD]

lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]


lemma parts_analz [simp]: "parts (analz H) = parts H"
apply (rule equalityI)
apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
done

lemma analz_parts [simp]: "analz (parts H) = parts H"
apply auto
apply (erule analz.induct, auto)
done


lemma parts_synth [simp]: "parts (synth H) = parts H ∪ synth H"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct)
apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] )+
done

lemma Fake_parts_insert:
  "X ∈ synth (analz H) ⟹ parts (insert X H) ⊆ synth (analz H) ∪ parts H"
apply (drule parts_insert_subset_Un)
apply (simp (no_asm_use))
apply blast
done

lemma Fake_parts_insert_in_Un:
  "Z ∈ parts (insert X H) ⟹
   X ∈ synth (analz H) ⟹
   Z ∈  synth (analz H) ∪ parts H"
by (blast dest: Fake_parts_insert [THEN subsetD, dest])


lemma analz_conj_parts [simp]:
  "X ∈ analz H ∧ X ∈ parts H ⟷ X ∈ analz H"
by (blast intro: analz_subset_parts [THEN subsetD])

lemma analz_disj_parts [simp]:
  "X ∈ analz H ∨ X ∈ parts H ⟷ X ∈ parts H"
by (blast intro: analz_subset_parts [THEN subsetD])


(****************************************************************************************)
subsection ‹More lemmas about combinations of closures›
(****************************************************************************************)

text ‹Combinations of @{term synth} and @{term analz}.›

lemma Pair_synth_analz [simp]:
  "Pair X Y ∈ synth (analz H) ⟷ X ∈ synth (analz H) ∧ Y ∈ synth (analz H)"
by blast

lemma Enc_synth_analz:
  "Y ∈ synth (analz H) ⟹
   (Enc X Y ∈ synth (analz H)) ⟷ (X ∈ synth (analz H))"
by blast

lemma Hash_synth_analz [simp]:
  "X ∉ synth (analz H) ⟹
   (Hash (Pair X Y) ∈ synth (analz H)) ⟷ (Hash (Pair X Y) ∈ analz H)"
by blast


lemma gen_analz_insert_eq:
  "⟦ X ∈ analz G; G ⊆ H ⟧ ⟹ analz (insert X H) = analz H"
by (blast intro: analz_cut analz_insertI analz_monotone)

lemma synth_analz_insert_eq:
  "⟦ X ∈ synth (analz G); G ⊆ H ⟧ ⟹ synth (analz (insert X H)) = synth (analz H)"
by (blast intro!: synth_analz_insert synth_analz_monotone)

lemma Fake_parts_sing:
  "X ∈ synth (analz H) ⟹ parts {X} ⊆ synth (analz H) ∪ parts H"
apply (rule subset_trans)
apply (erule_tac [2] Fake_parts_insert)
apply (rule parts_mono, blast)
done

lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]


lemma analz_hash_nonce [simp]:
  "analz {M. ∃N. M = Hash (Nonce N)} = {M. ∃N. M = Hash (Nonce N)}"
by (auto, rule analz.induct, auto)

lemma synth_analz_hash_nonce [simp]:
  "NonceF N ∉ synth (analz {M. ∃N. M = Hash (Nonce N)})"
by auto

lemma synth_analz_idem_mono:
  "S ⊆ synth (analz S') ⟹ synth (analz S) ⊆ synth (analz S')"
by (frule synth_analz_mono, auto)

lemmas synth_analz_idem_monoI =
  synth_analz_idem_mono [THEN [2] rev_subsetD]



lemma analz_synth_subset:
  "analz X ⊆ synth (analz X') ⟹
   analz Y ⊆ synth (analz Y') ⟹
   analz (X ∪ Y) ⊆ synth (analz (X' ∪ Y'))"
proof -
  assume "analz X ⊆ synth (analz X')"
  then have HX:"analz X ⊆ analz (synth (analz X'))" by blast
  assume "analz Y ⊆ synth (analz Y')"
  then have HY:"analz Y ⊆ analz (synth (analz Y'))" by blast
  from analz_subset_cong [OF HX HY]
  have "analz (X ∪ Y) ⊆ analz (synth (analz X') ∪ synth (analz Y'))"
    by blast
  also have "... ⊆ analz (synth (analz X' ∪ analz Y'))"
    by (intro analz_mono synth_Un)
  also have "... ⊆ analz (synth (analz (X' ∪ Y')))"
    by (intro synth_mono analz_mono analz_Un)
  also have "... ⊆ synth (analz (X' ∪ Y'))"
    by auto
  finally show "analz (X ∪ Y) ⊆ synth (analz (X' ∪ Y'))"
    by auto
qed


lemma analz_synth_subset_Un1 :
  "analz X ⊆ synth (analz X') ⟹ analz (X ∪ Y) ⊆ synth (analz (X' ∪ Y))"
using analz_synth_subset by blast

lemma analz_synth_subset_Un2 :
  "analz X ⊆ synth (analz X') ⟹ analz (Y ∪ X) ⊆ synth (analz (Y ∪ X'))"
using analz_synth_subset by blast

lemma analz_synth_insert:
  "analz X ⊆ synth (analz X') ⟹ analz (insert Y X) ⊆ synth (analz (insert Y X'))"
by (metis analz_synth_subset_Un2 insert_def)

lemma Fake_analz_insert_Un:
  assumes "Y ∈ analz (insert X H)" and "X ∈ synth (analz G)"
  shows "Y ∈ synth (analz G) ∪ analz (G ∪ H)"
proof -
  from assms have "Y ∈ analz (synth (analz G) ∪ H)"
    by (blast intro: analz_mono [THEN [2] rev_subsetD]
                     analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
  thus ?thesis by (simp add: sup.commute)
qed



end