Theory Implem_asymmetric

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Implem_asymmetric.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Implem_asymmetric.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>
  
  Asymmetric channel implementation (local interpretation) using
  public-key encryption and signatures.

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

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

section ‹Asymmetric Implementation of Channel Messages›

theory Implem_asymmetric
imports Implem
begin

(**************************************************************************************************)
subsection ‹Implementation of channel messages›
(**************************************************************************************************)

fun implem_asym :: "chan ⇒ msg" where
  "implem_asym (Insec A B M) = ⟨InsecTag, Agent A, Agent B, M⟩"
 |"implem_asym (Confid A B M) = Aenc ⟨Agent A, M⟩ (pubK B)"
 |"implem_asym (Auth A B M) = Sign ⟨Agent B, M⟩ (priK A)"
 |"implem_asym (Secure A B M) = Sign (Aenc ⟨SecureTag, Agent A, M⟩ (pubK B)) (priK A)"


text ‹
First step: @{locale "basic_implem"}. 
Trivial as there are no assumption, this locale just defines some useful abbreviations and valid.
›
interpretation asym: basic_implem implem_asym
done


text ‹Second step: @{locale "semivalid_implem"}.
Here we prove some basic properties such as injectivity and some properties about the 
interaction of sets of implementation messages with @{term analz}; these properties are 
proved as separate lemmas as the proofs are more complex. 
›

text ‹Auxiliary: simpler definitions of the ‹implSets› for the proofs, using the 
‹msgSet› definitions. 
›

abbreviation implInsecSet_aux :: "msg set ⇒ msg set"
where "implInsecSet_aux G ≡ PairSet Tags (PairSet AgentSet (PairSet AgentSet G))"

abbreviation implAuthSet_aux :: "msg set ⇒ msg set"
where "implAuthSet_aux G ≡ SignSet (PairSet AgentSet G) (range priK)"

abbreviation implConfidSet_aux :: "(agent * agent) set ⇒ msg set ⇒ msg set"
where "implConfidSet_aux Ag G ≡ AencSet (PairSet AgentSet G) (pubK` (Ag `` UNIV))"

abbreviation implSecureSet_aux :: "(agent * agent) set ⇒ msg set ⇒ msg set"
where "implSecureSet_aux Ag G ≡
  SignSet (AencSet (PairSet Tags (PairSet AgentSet G)) (pubK` (Ag `` UNIV))) (range priK)"

text ‹These auxiliary definitions are overapproximations.›

lemma implInsecSet_implInsecSet_aux: "asym.implInsecSet G ⊆ implInsecSet_aux G"
by auto

lemma implAuthSet_implAuthSet_aux: "asym.implAuthSet G ⊆ implAuthSet_aux G"
by auto

lemma implConfidSet_implConfidSet_aux: "asym.implConfidSet Ag G ⊆ implConfidSet_aux Ag G"
by (auto, blast)

lemma implSecureSet_implSecureSet_aux: "asym.implSecureSet Ag G ⊆ implSecureSet_aux Ag G"
by (auto, blast)

lemmas implSet_implSet_aux =
  implInsecSet_implInsecSet_aux implAuthSet_implAuthSet_aux
  implConfidSet_implConfidSet_aux implSecureSet_implSecureSet_aux

declare Enc_keys_clean_msgSet_Un [intro]


(**************************************************************************************************)
subsection ‹Lemmas to pull implementation sets out of @{term analz}›
(**************************************************************************************************)

text ‹
All these proofs are similar:
\begin{enumerate}
\item prove the lemma for the @{term "implSet_aux"} and with the set added outside of  
  @{term analz} given explicitly,
\item prove the lemma for the @{term "implSet_aux"} but with payload, and
\item prove the lemma for the @{term "implSet"}.
\end{enumerate}
There  are two cases for the confidential and secure messages:
the general case (the payloads stay in @{term  analz}) and the case where the key is unknown
(the messages cannot be opened and are completely removed from the @{term analz}).
›


subsubsection ‹Pull @{term PairAgentSet} out of ‹analz››
(**************************************************************************************************)

lemma analz_Un_PairAgentSet:
shows
  "analz (PairSet AgentSet G ∪ H) ⊆ PairSet AgentSet G ∪ AgentSet ∪ analz (G ∪ H)"
proof -
  have "analz (PairSet AgentSet G ∪ H) ⊆ PairSet AgentSet G ∪ analz (AgentSet ∪ G ∪ H)"
    by (rule analz_Un_PairSet)
  also have "... ⊆ PairSet AgentSet G ∪ AgentSet ∪ analz (G ∪ H)"
    apply (simp only: Un_assoc)
    apply (intro Un_mono analz_Un_AgentSet, fast)
    done 
  finally show ?thesis .
qed


subsubsection ‹Pull @{term implInsecSet} out of @{term analz}›
(**************************************************************************************************)

lemma analz_Un_implInsecSet_aux_aux:
assumes "Enc_keys_clean (G ∪ H)"
shows "analz (implInsecSet_aux G ∪ H) ⊆ implInsecSet_aux G ∪ Tags ∪ synth (analz (G ∪ H))"
proof -
   have "analz (implInsecSet_aux G ∪ H) ⊆ 
         implInsecSet_aux G ∪ analz (Tags ∪ PairSet AgentSet (PairSet AgentSet G) ∪ H)"
     by (rule analz_Un_PairSet)
   also have "... ⊆ implInsecSet_aux G ∪ Tags ∪ analz (PairSet AgentSet (PairSet AgentSet G) ∪ H)"
     using assms
     apply - 
     apply (simp only: Un_assoc, rule Un_mono, fast)
     apply (rule analz_Un_Tag, blast)
     done
   also have "... ⊆ implInsecSet_aux G ∪ Tags ∪ PairSet AgentSet (PairSet AgentSet G) ∪ AgentSet 
                     ∪ analz (PairSet AgentSet G ∪ H)"
     apply -
     apply (simp only: Un_assoc, (rule Un_mono, fast)+)
     apply (simp only: Un_assoc [symmetric], rule analz_Un_PairAgentSet)
     done
   also have 
     "... ⊆ implInsecSet_aux G ∪ Tags ∪ PairSet AgentSet (PairSet AgentSet G) ∪ AgentSet 
            ∪ PairSet AgentSet G ∪ AgentSet ∪ analz (G ∪ H)"
     apply -
     apply (simp only: Un_assoc, (rule Un_mono, fast)+)
     apply (simp only: Un_assoc [symmetric], rule analz_Un_PairAgentSet)
     done
   also have "... ⊆ implInsecSet_aux G ∪ Tags ∪ synth (analz (G ∪ H))"
     apply - 
     apply (simp only: Un_assoc, (rule Un_mono, fast)+, auto)
     done
   finally show ?thesis .
qed

lemma analz_Un_implInsecSet_aux:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (implInsecSet_aux G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implInsecSet_aux_aux], auto)

lemma analz_Un_implInsecSet:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (asym.implInsecSet G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implInsecSet_aux G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
apply (blast dest: analz_Un_implInsecSet_aux)
done


subsection ‹Pull @{term implConfidSet} out of @{term analz}›
(**************************************************************************************************)

lemma analz_Un_implConfidSet_aux_aux:
  "Enc_keys_clean (G ∪ H) ⟹
  analz (implConfidSet_aux Ag G ∪ H) ⊆ 
  implConfidSet_aux Ag G ∪ PairSet AgentSet G ∪
  synth (analz (G ∪ H))"
apply (rule subset_trans [OF analz_Un_AencSet], blast, blast)
apply (simp only: Un_assoc, rule Un_mono, simp)
apply (rule subset_trans [OF analz_Un_PairAgentSet], blast)
done

lemma analz_Un_implConfidSet_aux:
  "Enc_keys_clean (G ∪ H) ⟹
  analz (implConfidSet_aux Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implConfidSet_aux_aux], auto)

lemma analz_Un_implConfidSet:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (asym.implConfidSet Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implConfidSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implConfidSet_aux apply blast
done

text ‹Pull @{term implConfidSet} out of @{term analz}, 2nd case where the agents are honest.›

lemma analz_Un_implConfidSet_aux_aux_2:
  "Enc_keys_clean H ⟹
   Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
   analz (implConfidSet_aux Ag G ∪ H) ⊆ implConfidSet_aux Ag G ∪ synth (analz H)"
apply (rule subset_trans [OF analz_Un_AencSet2], simp)
apply (auto dest:analz_into_parts)
done

lemma analz_Un_implConfidSet_aux_2:
  "Enc_keys_clean H ⟹
   Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
   analz (implConfidSet_aux Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
by (rule subset_trans [OF analz_Un_implConfidSet_aux_aux_2], auto)

lemma analz_Un_implConfidSet_2:
  "Enc_keys_clean H ⟹
   Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
   analz (asym.implConfidSet Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
apply (rule subset_trans [of _ "analz (implConfidSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implConfidSet_aux_2 apply auto
done


subsection ‹Pull @{term implAuthSet} out of @{term analz}›
(**************************************************************************************************)

lemma analz_Un_implAuthSet_aux_aux:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (implAuthSet_aux G ∪ H) ⊆ implAuthSet_aux G ∪ synth (analz (G ∪ H))"
apply (rule subset_trans [OF analz_Un_SignSet], blast, blast)
apply (rule Un_mono, blast)
apply (rule subset_trans [OF analz_Un_PairAgentSet], blast)
done

lemma analz_Un_implAuthSet_aux:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (implAuthSet_aux G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implAuthSet_aux_aux], auto)

lemma analz_Un_implAuthSet:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (asym.implAuthSet G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implAuthSet_aux G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implAuthSet_aux apply blast
done


subsection ‹Pull @{term implSecureSet} out of @{term analz}›
(**************************************************************************************************)

lemma analz_Un_implSecureSet_aux_aux:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (implSecureSet_aux Ag G ∪ H) ⊆
   implSecureSet_aux Ag G ∪ AencSet (PairSet Tags (PairSet AgentSet G)) (pubK` (Ag`` UNIV)) ∪ 
   PairSet Tags (PairSet AgentSet G) ∪ Tags ∪ PairSet AgentSet G ∪
   synth (analz (G ∪ H))"
apply (rule subset_trans [OF analz_Un_SignSet], blast, blast)
apply (simp only:Un_assoc, rule Un_mono, simp)
apply (rule subset_trans [OF analz_Un_AencSet], blast, blast)
apply (rule Un_mono, simp)
apply (rule subset_trans [OF analz_Un_PairSet], rule Un_mono, simp, simp only: Un_assoc)
apply (rule subset_trans [OF analz_Un_Tag], blast)
apply (rule Un_mono, simp)
apply (rule subset_trans [OF analz_Un_PairAgentSet], blast)
done

lemma analz_Un_implSecureSet_aux:
  "Enc_keys_clean (G ∪ H) ⟹
  analz (implSecureSet_aux Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implSecureSet_aux_aux], auto)

lemma analz_Un_implSecureSet:
  "Enc_keys_clean (G ∪ H) ⟹
   analz (asym.implSecureSet Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implSecureSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implSecureSet_aux apply blast
done

text ‹
Pull @{term implSecureSet} out of @{term analz}, 2nd case, where the agents are honest. 
›
lemma analz_Un_implSecureSet_aux_aux_2:
  "Enc_keys_clean (G ∪ H) ⟹
   Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
   analz (implSecureSet_aux Ag G ∪ H) ⊆ 
   implSecureSet_aux Ag G ∪ AencSet (PairSet Tags (PairSet AgentSet G)) (pubK` (Ag`` UNIV)) ∪
   synth (analz H)"
apply (rule subset_trans [OF analz_Un_SignSet], blast, blast)
apply (simp only: Un_assoc, rule Un_mono, simp)
apply (rule subset_trans [OF analz_Un_AencSet2], simp)
apply (auto dest: analz_into_parts)
done

lemma analz_Un_implSecureSet_aux_2:
  "Enc_keys_clean (G ∪ H) ⟹
   Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
   analz (implSecureSet_aux Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
by (rule subset_trans [OF analz_Un_implSecureSet_aux_aux_2], auto)

lemma analz_Un_implSecureSet_2:
  "Enc_keys_clean (G ∪ H) ⟹
   Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
   analz (asym.implSecureSet Ag G ∪ H) ⊆
   synth (analz H) ∪ -payload"
apply (rule subset_trans [of _ "analz (implSecureSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implSecureSet_aux_2 apply auto
done

declare Enc_keys_clean_msgSet_Un [rule del]


subsection ‹Locale interpretations›
(**************************************************************************************************)

interpretation asym: semivalid_implem implem_asym
proof (unfold_locales)
  fix x A B M x' A' B' M'
  show "implem_asym (Chan x A B M) = implem_asym (Chan x' A' B' M') ⟷
        x = x' ∧ A = A' ∧ B = B' ∧ M = M'"
    by (cases x, (cases x', auto)+)
next
  fix M' M x x' A A' B B'
  assume "M' ∈ payload" "implem_asym (Chan x A B M) ∈ parts {implem_asym (Chan x' A' B' M')}"
  then show "x = x' ∧ A = A' ∧ B = B' ∧ M = M'"
    by (cases "x", auto,(cases x', auto)+)
next
  fix I
  assume "I ⊆ asym.valid"
  then show "Enc_keys_clean I"
    proof (simp add: Enc_keys_clean_def, intro allI impI)
      fix X Y
      assume "Enc X Y ∈ parts I"
      obtain x A B M where "M ∈ payload" and "Enc X Y ∈ parts {implem_asym (Chan x A B M)}"
      using parts_singleton [OF ‹Enc X Y ∈ parts I›] ‹I ⊆ asym.valid›
        by (auto elim!: asym.validE)
      then show "Y ∈ range LtK ∨ Y ∈ payload" by (cases x, auto)
    qed
next
  fix Z
  show "composed (implem_asym Z)"
    proof (cases Z, simp)
      fix x A B M
      show "composed (implem_asym (Chan x A B M))" by (cases x, auto)
    qed
next
  fix x A B M
  show "implem_asym (Chan x A B M) ∉ payload"
    by (cases x, auto)
next
  fix X K
  assume "X ∈ asym.valid"
  then obtain x A B M where "M ∈ payload" "X = implem_asym (Chan x A B M)" 
    by (auto elim: asym.validE)
  then show "LtK K ∉ parts {X}"
  by (cases x, auto)
next
  fix G H
  assume "G ⊆ payload" "Enc_keys_clean H"
  hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
  then show "analz ({implem_asym (Insec A B M) |A B M. M ∈ G} ∪ H) ⊆ 
               synth (analz (G ∪ H)) ∪ - payload"
    by (rule analz_Un_implInsecSet)
next
  fix G H
  assume "G ⊆ payload" "Enc_keys_clean H"
  hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
  then show "analz ({implem_asym (Auth A B M) |A B M. M ∈ G} ∪ H) ⊆ 
               synth (analz (G ∪ H)) ∪ - payload"
    by (rule analz_Un_implAuthSet)
next
  fix G H Ag
  assume "G ⊆ payload" "Enc_keys_clean H"
  hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
  then show "analz ({implem_asym (Confid A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆ 
               synth (analz (G ∪ H)) ∪ - payload"
    by (rule analz_Un_implConfidSet)
next
  fix G H Ag
  assume "G ⊆ payload" "Enc_keys_clean H"
  hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
  then show "analz ({implem_asym (Secure A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆ 
               synth (analz (G ∪ H)) ∪ - payload"
    by (rule analz_Un_implSecureSet)
next
  fix G H Ag
  assume "G ⊆ payload" (*unused*)
  assume "Enc_keys_clean H"
  moreover assume "Ag ∩ broken (parts H ∩ range LtK) = {}"
  ultimately show "analz ({implem_asym (Confid A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆ 
               synth (analz H) ∪ - payload"
    by (rule analz_Un_implConfidSet_2)
next
  fix G H Ag
  assume "G ⊆ payload" "Enc_keys_clean H"
  hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
  moreover assume "Ag ∩ broken (parts H ∩ range LtK) = {}"
  ultimately 
    show "analz ({implem_asym (Secure A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆ 
          synth (analz H) ∪ - payload"
    by (rule analz_Un_implSecureSet_2)
qed


text ‹
Third step: @{locale "valid_implem"}. The lemmas giving conditions on $M$, $A$ and $B$ for 
@{prop [display] "implXXX A B M ∈ synth (analz Z)"}.
›

lemma implInsec_synth_analz:
  "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags ⟹
   asym.implInsec A B M ∈ synth (analz H) ⟹
   asym.implInsec A B M ∈ I ∨ M ∈ synth (analz H)"
apply (erule synth.cases, auto)
done

lemma implConfid_synth_analz:
  "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags ⟹
   asym.implConfid A B M ∈ synth (analz H) ⟹
   asym.implConfid A B M ∈ H ∨ M ∈ synth (analz H)"
apply (erule synth.cases, auto)
apply (frule asym.analz_valid [where x=confid], auto)
done

lemma implAuth_synth_analz:
  "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags ⟹
   asym.implAuth A B M ∈ synth (analz H) ⟹
   asym.implAuth A B M ∈ H ∨ (M ∈ synth (analz H) ∧ (A, B) ∈ broken H)"
apply (erule synth.cases, auto)
apply (frule asym.analz_valid [where x=auth], auto)
apply (frule asym.analz_valid [where x=auth], auto)
apply (blast dest: asym.analz_LtKeys)
done

lemma implSecure_synth_analz:
  "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags ⟹
   asym.implSecure A B M ∈ synth (analz H) ⟹
   asym.implSecure A B M ∈ H ∨ (M ∈ synth (analz H) ∧ (A, B) ∈ broken H)"
using [[simproc del: defined_all]] proof (erule synth.cases, simp_all)
  fix X
  assume H:"H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags"
  assume H':"Sign (Aenc ⟨SecureTag, Agent A, M⟩ (pubK B)) (priK A) = X"
            " X ∈ analz H"
  hence "asym.implSecure A B M ∈ analz H" by auto
  with H have "asym.implSecure A B M ∈ H" by (rule asym.analz_valid)
  with H' show "X ∈ H ∨ M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
    by auto
next
  fix X Y
  assume H:"H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags"
  assume H':"Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) = X ∧ priK A = Y"
            "X ∈ synth (analz H)" "Y ∈ synth (analz H)"
  hence "priK A ∈ analz H" by auto
  with H have HAgents:"(A, B) ∈ broken H " by (auto dest: asym.analz_LtKeys)
  from H' have "Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) ∈ synth (analz H)" by auto
  then have "Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) ∈ analz H ∨ 
             M ∈ synth (analz H)"
    by (rule synth.cases, auto)
  then show "Sign X Y ∈ H ∨ M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
    proof
      assume "M ∈ synth (analz H)"
      with HAgents show ?thesis by auto
    next
      assume "Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) ∈ analz H"
      hence "Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) ∈ parts H" by (rule analz_into_parts)
      from H obtain Z where 
        "Z ∈ H" and H'':"Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) ∈ parts {Z}"
        using parts_singleton [OF ‹Aenc ⟨SecureTag, Agent A, M⟩ (pubK B) ∈ parts H›] 
        by blast
      moreover with H have "Z ∈ asym.valid" by (auto dest!: subsetD)
      moreover with H'' have "Z = asym.implSecure A B M"
        by (auto) (erule asym.valid_cases, auto)
      ultimately have "asym.implSecure A B M ∈ H" by auto
      with H' show ?thesis by auto
    qed
qed



interpretation asym: valid_implem implem_asym
proof (unfold_locales)
  fix H A B M
  assume "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags"
         "implem_asym (Insec A B M) ∈ synth (analz H)"
  then show "implem_asym (Insec A B M) ∈ H ∨ M ∈ synth (analz H)"
    by (rule implInsec_synth_analz)
next
  fix H A B M
  assume "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags"
         "implem_asym (Confid A B M) ∈ synth (analz H)"
  then show "implem_asym (Confid A B M) ∈ H ∨ M ∈ synth (analz H)"
    by (rule implConfid_synth_analz)
next
  fix H A B M
  assume "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags"
         "implem_asym (Auth A B M) ∈ synth (analz H)"
  then show "implem_asym (Auth A B M) ∈ H ∨ 
             M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
    by (rule implAuth_synth_analz)
next
  fix H A B M
  assume "H ⊆ payload ∪ asym.valid ∪ range LtK ∪ Tags"
         "implem_asym (Secure A B M) ∈ synth (analz H)"
  then show "implem_asym (Secure A B M) ∈ H ∨ 
             M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
    by (rule implSecure_synth_analz)
qed

end