Theory Implem_lemmas

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Implem_lemmas.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Implem_lemmas.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>
  
  Auxiliary notions and lemmas for channel implementations.
  - message abstraction = inverse of (valid) impl, lifted to sets
  - extractable messages (those of non-confidential and "broken" channels)
  - lemmas for proving L2-L3 intruder refinement

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

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

section ‹Lemmas Following from Channel Message Implementation Assumptions›

theory Implem_lemmas
imports Implem
begin

text ‹These lemmas require the assumptions added in the @{locale "valid_implem"} locale.›

context semivalid_implem
begin
(**************************************************************************************************)
subsection ‹Message implementations and abstractions›
(**************************************************************************************************)

text ‹Abstracting a set of messages into channel messages.›

definition
  abs :: "msg set ⇒ chan set"
where
  "abs S ≡ {Chan x A B M | x A B M. M ∈ payload ∧ implem (Chan x A B M) ∈ S}"

lemma absE [elim]: 
  "⟦ X ∈ abs H;
     ⋀ x A B M. X = Chan x A B M ⟹ M ∈ payload ⟹ implem X ∈ H ⟹ P ⟧
  ⟹ P"
by (auto simp add: abs_def)

lemma absI [intro]: "M ∈ payload ⟹ implem (Chan x A B M) ∈ H ⟹ Chan x A B M ∈ abs H"
by (auto simp add: abs_def)

lemma abs_mono: "G ⊆ H ⟹ abs G ⊆ abs H"
by (auto simp add: abs_def)

lemmas abs_monotone [simp] = abs_mono [THEN [2] rev_subsetD]

lemma abs_empty [simp]: "abs {} = {}"
by (auto simp add: abs_def)

lemma abs_Un_eq: "abs (G ∪ H) = abs G ∪ abs H"
by (auto simp add: abs_def)

text ‹General lemmas about implementations and @{term abs}.›
lemma abs_insert_payload [simp]: "M ∈ payload ⟹ abs (insert M S) = abs S"
by (auto simp add: abs_def)

lemma abs_insert_impl [simp]:
  "M ∈ payload ⟹ abs (insert (implem (Chan x A B M)) S) = insert (Chan x A B M) (abs S)"
by (auto simp add: abs_def)

lemma extr_payload [simp, intro]:
  "⟦ X ∈ extr Bad NI (abs I); NI ⊆ payload ⟧ ⟹ X ∈ payload"
by (erule extr.induct, blast, auto)

lemma abs_Un_LtK:
  "K ⊆ range LtK ⟹ abs (K ∪ S) = abs S"
by (auto simp add: abs_Un_eq)

lemma abs_Un_keys_of [simp]:
  "abs (keys_of A ∪ S) = abs S"
by (auto intro!: abs_Un_LtK)


text ‹Lemmas about @{term valid} and @{term abs}›

lemma abs_validSet: "abs (S ∩ valid) = abs S"
by (auto elim: absE intro: validI)

lemma valid_abs: "M ∈ valid ⟹ ∃ M'. M' ∈ abs {M}"
by (auto elim: validE)


(**************************************************************************************************)
subsection ‹Extractable messages›
(**************************************************************************************************)

text ‹‹extractable K I›: subset of messages in $I$ which are implementations 
(not necessarily valid since we do not require that they are payload) and can be extracted 
using the keys in K. It corresponds to L2 @{term extr}.›

definition
  extractable :: "msg set ⇒ msg set ⇒ msg set"
where
  "extractable K I ≡
    {implInsec A B M | A B M. implInsec A B M ∈ I} ∪
    {implAuth A B M | A B M. implAuth A B M ∈ I} ∪
    {implConfid A B M | A B M. implConfid A B M ∈ I ∧ (A, B) ∈ broken K} ∪
    {implSecure A B M | A B M. implSecure A B M ∈ I ∧ (A, B) ∈ broken K}"

lemma extractable_red: "extractable K I ⊆ I"
by (auto simp add: extractable_def)

lemma extractableI:
  "implem (Chan x A B M) ∈ I ⟹
   x = insec ∨ x = auth ∨ ((x = confid ∨ x = secure) ∧ (A, B) ∈ broken K) ⟹   
   implem (Chan x A B M) ∈ extractable K I"
by (auto simp add: extractable_def)

lemma extractableE:
  "X ∈ extractable K I ⟹
   (⋀A B M. X = implInsec A B M ⟹ X ∈ I ⟹ P) ⟹
   (⋀A B M. X = implAuth A B M ⟹ X ∈ I ⟹ P) ⟹
   (⋀A B M. X = implConfid A B M ⟹ X ∈ I ⟹ (A, B) ∈ broken K ⟹ P) ⟹
   (⋀A B M. X = implSecure A B M ⟹ X ∈ I ⟹ (A, B) ∈ broken K ⟹ P) ⟹
  P"
by (auto simp add: extractable_def brokenI)

text ‹General lemmas about implementations and extractable.›
lemma implem_extractable [simp]:
  "⟦ Keys_bad K Bad; implem (Chan x A B M) ∈ extractable K I; M ∈ payload ⟧ 
 ⟹ M ∈ extr Bad NI (abs I)"
by (erule extractableE, auto)


text ‹Auxiliary lemmas about extractable messages: they are implementations.›
lemma valid_extractable [simp]: "I ⊆ valid ⟹ extractable K I ⊆ valid"
by (auto intro: subset_trans extractable_red del: subsetI)

lemma LtKeys_parts_extractable:
  "I ⊆ valid ⟹ parts (extractable K I) ∩ range LtK = {}"
by (auto dest: valid_extractable intro!: parts_valid_LtKeys_disjoint)

lemma LtKeys_parts_extractable_elt [simp]:  
  "I ⊆ valid ⟹ LtK ltk ∉ parts (extractable K I)"
by (blast dest: LtKeys_parts_extractable)


lemma LtKeys_parts_implSecureSet:   (* FIX: possibly problematic: not in normal form *)
  "parts (implSecureSet Ag payload) ∩ range LtK = {}"
by (auto intro!: parts_valid_LtKeys_disjoint intro: validI)

lemma LtKeys_parts_implSecureSet_elt: 
  "LtK K ∉ parts (implSecureSet Ag payload)"
using LtKeys_parts_implSecureSet
by auto

lemmas LtKeys_parts = LtKeys_parts_payload parts_valid_LtKeys_disjoint
                      LtKeys_parts_extractable LtKeys_parts_implSecureSet 
                      LtKeys_parts_implSecureSet_elt


subsubsection‹Partition $I$ to keep only the extractable messages›
(**************************************************************************************************)

text ‹Partition the implementation set.›

lemma impl_partition:
  "⟦ NI ⊆ payload; I ⊆ valid ⟧ ⟹
  I ⊆ extractable K I ∪
      implConfidSet (UNIV - broken K) payload ∪
      implSecureSet (UNIV - broken K) payload"
by (auto dest!: subsetD [where A=I] elim!: valid_cases intro:  extractableI)


subsubsection ‹Partition of @{term "extractable"}›
(**************************************************************************************************)

text ‹We partition the @{term "extractable"} set into insecure, confidential, authentic 
implementations.›

lemma extractable_partition:
  "⟦Keys_bad K Bad; NI ⊆ payload; I ⊆ valid⟧ ⟹
  extractable K I ⊆ 
  implInsecSet (extr Bad NI (abs I)) ∪
  implConfidSet UNIV (extr Bad NI (abs I)) ∪
  implAuthSet (extr Bad NI (abs I)) ∪
  implSecureSet UNIV (extr Bad NI (abs I))"
apply (rule, frule valid_extractable, drule subsetD [where A="extractable K I"], fast)
apply (erule valid_cases, auto)
done


(**************************************************************************************************)
subsection ‹Lemmas for proving intruder refinement (L2-L3)›
(**************************************************************************************************)

text ‹Chain of lemmas used to prove the refinement for ‹l3_dy›. 
The ultimate goal is to show @{prop [display] 
  "synth (analz (NI ∪ I ∪ K ∪ Tags)) ⊆ synth (analz (extr Bad NI (abs I))) ∪ -payload"
}›

subsubsection ‹First: we only keep the extractable messages›

― ‹the ‹synth› is probably not needed›
lemma analz_NI_I_K_analz_NI_EI:
assumes HNI: "NI ⊆ payload"
    and HK: "K ⊆ range LtK"
    and HI: "I ⊆ valid"
shows "analz (NI ∪ I ∪ K ∪ Tags) ⊆
       synth (analz (NI ∪ extractable K I ∪ K ∪ Tags)) ∪ -payload"
proof -
  from HNI HI
  have "analz (NI ∪ I ∪ K ∪ Tags) ⊆ 
        analz (NI ∪ (extractable K I ∪
                     implConfidSet (UNIV - broken K) payload ∪
                     implSecureSet (UNIV - broken K) payload)
                ∪ K ∪ Tags)"
    by (intro analz_mono Un_mono impl_partition, simp_all)
  also have "... ⊆ analz (implConfidSet (UNIV - broken K) payload ∪
                    (implSecureSet (UNIV - broken K) payload ∪
                    (extractable K I ∪ NI ∪ K ∪ Tags)))"
    by (auto)
  also have "... ⊆ synth (analz (implSecureSet (UNIV - broken K) payload ∪
                  (extractable K I ∪ NI ∪ K ∪ Tags))) ∪ -payload"
    proof (rule analz_Un_implConfidSet_2)
      show "Enc_keys_clean (implSecureSet (UNIV - broken K) payload 
                              ∪ (extractable K I ∪ NI ∪ K ∪ Tags))"
        by (auto simp add: HNI HI HK intro: validI)
    next
      from HK HI HNI 
      show "(UNIV - broken K) ∩ 
            broken (parts (
              implSecureSet (UNIV - broken K) payload ∪
              (extractable K I ∪ NI ∪ K ∪ Tags)) ∩ range LtK)  = {}"
        by (auto simp add: LtKeys_parts 
               LtKeys_parts_implSecureSet_elt [where Ag="- broken K", simplified])
    qed (auto)
  also have "... ⊆ synth (analz (extractable K I ∪ NI ∪ K ∪ Tags)) ∪ -payload"
    proof (rule Un_least, rule synth_idem_payload)
      show "analz (implSecureSet (UNIV - broken K) payload ∪ 
                   (extractable K I ∪ NI ∪ K ∪ Tags))
            ⊆ synth (analz (extractable K I ∪ NI ∪ K ∪ Tags)) ∪ -payload"
        proof (rule analz_Un_implSecureSet_2)
          show "Enc_keys_clean (extractable K I ∪ NI ∪ K ∪ Tags)"
            using HNI HK HI by auto
        next  
          from HI HK HNI 
          show "(UNIV - broken K) ∩ 
                broken (parts (extractable K I ∪ NI ∪ K ∪ Tags) ∩ range LtK) = {}"
          by (auto simp add: LtKeys_parts)
        qed (auto)
    next
      show "-payload ⊆ synth (analz (extractable K I ∪ NI ∪ K ∪ Tags)) ∪ -payload"
        by auto
    qed
  also have "... ⊆ synth (analz (NI ∪ extractable K I ∪ K ∪ Tags)) ∪ -payload"
    by (simp add: sup.left_commute sup_commute)
  finally show ?thesis .
qed


subsubsection ‹Only keep the extracted messages (instead of extractable)›
(**************************************************************************************************)

lemma analz_NI_EI_K_synth_analz_NI_E_K:
assumes HNI: "NI ⊆ payload"
    and HK: "K ⊆ range LtK"
    and HI: "I ⊆ valid"
    and Hbad: "Keys_bad K Bad"
shows "analz (NI ∪ extractable K I ∪ K ∪ Tags)
    ⊆ synth (analz (extr Bad NI (abs I) ∪ K ∪ Tags)) ∪ -payload"
proof -
  from HNI HI Hbad
  have "analz (NI ∪ extractable K I ∪ K ∪ Tags) ⊆ 
        analz (NI ∪ (implInsecSet (extr Bad NI (abs I)) ∪
                     implConfidSet UNIV (extr Bad NI (abs I)) ∪
                     implAuthSet (extr Bad NI (abs I)) ∪
                     implSecureSet UNIV (extr Bad NI (abs I))) ∪
                    K ∪ Tags)"
    by (intro analz_mono Un_mono extractable_partition) (auto)

  also have "... ⊆ analz (implInsecSet (extr Bad NI (abs I)) ∪
                     (implConfidSet UNIV (extr Bad NI (abs I)) ∪
                     (implAuthSet (extr Bad NI (abs I)) ∪
                     (implSecureSet UNIV (extr Bad NI (abs I)) ∪
                     (NI ∪ K ∪ Tags)))))"
    by (auto)
  also have "... ⊆ synth (analz (extr Bad NI (abs I) ∪
                   (implConfidSet UNIV (extr Bad NI (abs I)) ∪
                   (implAuthSet (extr Bad NI (abs I)) ∪
                   (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags)))))) 
                 ∪ -payload"
    by (rule analz_Un_implInsecSet)
       (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb, 
        auto simp add: HNI HK HI intro!: validI)
  also have "... ⊆ synth (analz (extr Bad NI (abs I) ∪
                   (implAuthSet (extr Bad NI (abs I)) ∪
                   (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags))))) 
                 ∪ -payload"
    proof (rule Un_least, rule synth_idem_payload)
      have "analz (implConfidSet UNIV (extr Bad NI (abs I)) ∪
                   (implAuthSet (extr Bad NI (abs I)) ∪
                   (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                   (NI ∪ (K ∪ extr Bad NI (abs I) ∪ Tags)))))
            ⊆ synth (analz (extr Bad NI (abs I) ∪
                           (implAuthSet (extr Bad NI (abs I)) ∪
                           (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                           (NI ∪ (K ∪ extr Bad NI (abs I) ∪ Tags)))))) 
              ∪ -payload"
        by (rule analz_Un_implConfidSet)
           (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb,
            auto simp add: HK HI HNI  intro!: validI)
      then show "analz (extr Bad NI (abs I) ∪
                        (implConfidSet UNIV (extr Bad NI (abs I)) ∪
                        (implAuthSet (extr Bad NI (abs I)) ∪
                        (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags)))))
                 ⊆ synth (analz (extr Bad NI (abs I) ∪
                         (implAuthSet (extr Bad NI (abs I)) ∪
                         (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                         (NI ∪ K ∪ Tags))))) 
                   ∪ -payload"
        by (simp add: inf_sup_aci(6) inf_sup_aci(7))
    next
      show "-payload
            ⊆ synth (analz (extr Bad NI (abs I) ∪
                           (implAuthSet (extr Bad NI (abs I)) ∪
                           (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags))))) 
              ∪ -payload"
        by blast
    qed
  also have "... ⊆ synth (analz (extr Bad NI (abs I) ∪
                   (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags)))) 
                 ∪ -payload"
    proof (rule Un_least, rule synth_idem_payload)
      have "analz (implAuthSet (extr Bad NI (abs I)) ∪
                   (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                   (NI ∪ (K ∪ (extr Bad NI (abs I) ∪ Tags)))))
            ⊆ synth (analz (extr Bad NI (abs I) ∪
                           (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                           (NI ∪ (K ∪ (extr Bad NI (abs I) ∪ Tags)))))) 
              ∪ -payload"
        by (rule analz_Un_implAuthSet)
           (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb,
            auto simp add: HI HNI HK intro!: validI)
      then show "analz (extr Bad NI (abs I) ∪
                        (implAuthSet (extr Bad NI (abs I)) ∪
                        (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags))))
                 ⊆ synth (analz (extr Bad NI (abs I) ∪
                         (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                         (NI ∪ K ∪ Tags)))) 
                   ∪ -payload"
        by (simp add: inf_sup_aci(6) inf_sup_aci(7))
    next
      show "-payload
            ⊆ synth (analz (extr Bad NI (abs I) ∪
                           (implSecureSet UNIV (extr Bad NI (abs I)) 
                            ∪ (NI ∪ K ∪ Tags))))  
              ∪ -payload"
        by blast
    qed
  also have "... ⊆ synth (analz (extr Bad NI (abs I) ∪ (NI ∪ K ∪ Tags))) 
                 ∪ -payload"
    proof (rule Un_least, rule synth_idem_payload)
      have "analz (implSecureSet UNIV (extr Bad NI (abs I)) ∪ 
                   (NI ∪ (K ∪ (extr Bad NI (abs I) ∪ Tags))))
            ⊆ synth (analz (extr Bad NI (abs I) ∪
                           (NI ∪ (K ∪ (extr Bad NI (abs I) ∪ Tags))))) 
               ∪ -payload"
        by (rule analz_Un_implSecureSet)
           (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb,
            auto simp add: HI HNI HK intro!: validI)
      then show "analz (extr Bad NI (abs I) ∪
                        (implSecureSet UNIV (extr Bad NI (abs I)) ∪ (NI ∪ K ∪ Tags)))
                 ⊆ synth (analz (extr Bad NI (abs I) ∪ (NI ∪ K ∪ Tags))) 
                   ∪ -payload"
        by (simp add: inf_sup_aci(6) inf_sup_aci(7))
    next
      show "-payload
            ⊆ synth (analz (extr Bad NI (abs I)∪ (NI ∪ K ∪ Tags))) 
              ∪ -payload"
        by blast
    qed
  also have "... ⊆ synth (analz (extr Bad NI (abs I) ∪ K ∪ Tags)) ∪ -payload"
    by (metis IK_subset_extr inf_sup_aci(6) set_eq_subset sup.absorb1)
  finally show ?thesis .
qed


subsubsection ‹Keys and Tags can be moved out of the @{term "analz"}›

lemma analz_LtKeys_Tag:
assumes "NI ⊆ payload" and "K ⊆ range LtK"
shows "analz (NI ∪ K ∪ Tags) ⊆ analz NI ∪ K ∪ Tags"
proof 
  fix X
  assume H: "X ∈ analz (NI ∪ K ∪ Tags) "
  thus "X ∈ analz NI ∪ K ∪ Tags" 
  proof (induction X rule: analz.induct)
    case (Dec X Y) 
    hence "Enc X Y ∈ payload" using assms by auto
    moreover
    from Dec.IH(2) have "Y ∈ synth (analz NI ∪ (K ∪ Tags))"
      by (auto simp add: Collect_disj_eq dest!: synth_Int2 )
    ultimately show ?case using Dec.IH(1) assms(2) 
      by (auto dest!: synth_payload [THEN [2] rev_subsetD])
  next
    case (Adec_lt X Y)
    hence "Aenc X (pubK Y) ∈ payload ∪ range LtK ∪ Tags" using assms
      by auto
    then show ?case by auto
  next
    case (Sign_getmsg X Y)
    hence "Sign X (priK Y) ∈ payload ∪ range LtK ∪ Tags" using assms by auto
    then show ?case by auto
  next
    case (Adec_eph X Y)
    then show ?case using assms by (auto dest!: EpriK_synth)
  qed (insert assms, auto)
qed

lemma analz_NI_E_K_analz_NI_E:
  "⟦ NI ⊆ payload; K ⊆ range LtK; I ⊆ valid ⟧ 
 ⟹ analz (extr Bad NI (abs I) ∪ K ∪ Tags) ⊆ analz (extr Bad NI (abs I)) ∪ K ∪ Tags"
by (rule analz_LtKeys_Tag) auto


subsubsection ‹Final lemmas, using all the previous ones›
(**************************************************************************************************)

lemma analz_NI_I_K_synth_analz_NI_E:
assumes
  Hbad: "Keys_bad K Bad" and 
  HNI: "NI ⊆ payload" and 
  HK:  "K ⊆ range LtK" and 
  HI: "I ⊆ valid"
shows 
  "analz (NI ∪ I ∪ K ∪ Tags) ⊆ synth (analz (extr Bad NI (abs I))) ∪ -payload"
proof -
  from HNI HK HI have "analz (NI ∪ I ∪ K ∪ Tags) ⊆
        synth (analz (NI ∪ extractable K I ∪ K ∪ Tags)) ∪ -payload"
    by (rule analz_NI_I_K_analz_NI_EI)
  also have "... ⊆ synth (analz (extr Bad NI (abs I) ∪ K ∪ Tags)) ∪ -payload"
    proof (rule Un_least, simp_all)
      from Hbad HNI HK HI have "analz (NI ∪ extractable K I ∪ K ∪ Tags) ⊆
            synth (analz (extr Bad NI (abs I) ∪ K ∪ Tags)) ∪ -payload"
        by (intro analz_NI_EI_K_synth_analz_NI_E_K)
      then show "synth (analz (NI ∪ extractable K I ∪ K ∪ Tags)) ⊆
                 synth (analz (extr Bad NI (abs I) ∪ K ∪ Tags)) ∪ -payload"
        by (rule synth_idem_payload)
    qed
  also have "... ⊆ synth (analz (extr Bad NI (abs I))) ∪ -payload"
    proof (rule Un_least, simp_all)
      from HNI HK HI have "analz (extr Bad NI (abs I) ∪ K ∪ Tags) ⊆
                           analz (extr Bad NI (abs I)) ∪ K ∪ Tags"
        by (rule analz_NI_E_K_analz_NI_E)
      also from HK have "... ⊆ analz (extr Bad NI (abs I)) ∪ -payload"
        by auto
      also have "... ⊆ synth (analz (extr Bad NI (abs I))) ∪ -payload"
        by auto
      finally show "synth (analz (extr Bad NI (abs I) ∪ K ∪ Tags)) ⊆
                  synth (analz (extr Bad NI (abs I))) ∪ -payload"
        by (rule synth_idem_payload)
    qed
  finally show ?thesis .
qed


text ‹Lemma actually used to prove the refinement.›
lemma synth_analz_NI_I_K_synth_analz_NI_E:
  "⟦ Keys_bad K Bad; NI ⊆ payload; K ⊆ range LtK; I ⊆ valid⟧
 ⟹ synth (analz (NI ∪ I ∪ K ∪ Tags)) 
   ⊆ synth (analz (extr Bad NI (abs I))) ∪ -payload"
by (intro synth_idem_payload analz_NI_I_K_synth_analz_NI_E) (assumption+)


subsubsection ‹Partitioning @{term "analz (ik)"}›
(**************************************************************************************************)
text ‹Two lemmas useful for proving the invariant
  @{term [display] "analz ik ⊆ synth (analz (ik ∩ payload ∪ ik ∩ valid ∪ ik ∩ range LtK ∪ Tags))"}
›

lemma analz_Un_partition:
  "analz S ⊆ synth (analz ((S ∩ payload) ∪ (S ∩ valid) ∪ (S ∩ range LtK) ∪ Tags)) ⟹
  H ⊆ payload ∪ valid ∪ range LtK ⟹
  analz (H ∪ S) ⊆
    synth (analz (((H ∪ S) ∩ payload) ∪ ((H ∪ S) ∩ valid) ∪ ((H ∪ S) ∩ range LtK) ∪ Tags))"
proof -
  assume "H ⊆ payload ∪ valid ∪ range LtK"
  then have HH:"H = (H ∩ payload) ∪ (H ∩ valid) ∪ (H ∩ range LtK)"
    by auto
  assume HA:
    "analz S ⊆ synth (analz ((S ∩ payload) ∪ (S ∩ valid) ∪ (S ∩ range LtK) ∪ Tags))"
  then have 
   "analz (H ∪ S) ⊆ 
    synth (analz (H ∪ ((S ∩ payload) ∪ (S ∩ valid) ∪ (S ∩ range LtK) ∪ Tags)))"
    by (rule analz_synth_subset_Un2)
  also with HH have 
    "... ⊆ synth (analz (((H ∩ payload) ∪ (H ∩ valid) ∪ (H ∩ range LtK)) ∪ 
                         ((S ∩ payload) ∪ (S ∩ valid) ∪ (S ∩ range LtK) ∪ Tags)))"
    by auto
  also have "... = synth (analz (((H ∪ S) ∩ payload) ∪ ((H ∪ S) ∩ valid) ∪ 
                                 ((H ∪ S) ∩ range LtK) ∪ Tags))"
    by (simp add: Un_left_commute sup.commute Int_Un_distrib2)
  finally show ?thesis .
qed

lemma analz_insert_partition:
  "analz S ⊆ synth (analz ((S ∩ payload) ∪ (S ∩ valid) ∪ (S ∩ range LtK) ∪ Tags)) ⟹
  x ∈ payload ∪ valid ∪ range LtK ⟹
  analz (insert x S) ⊆
    synth (analz (((insert x S) ∩ payload) ∪ ((insert x S) ∩ valid) ∪ 
                  ((insert x S) ∩ range LtK) ∪ Tags))"
by (simp only: insert_is_Un [of x S], erule analz_Un_partition, auto)

end
end