Theory Stateful_Protocol_Model

(*  Title:      Stateful_Protocol_Model.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, University of Exeter
    Author:     Anders Schlichtkrull, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section‹Stateful Protocol Model›
theory Stateful_Protocol_Model
  imports Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
          Transactions Term_Abstraction
begin

subsection ‹Locale Setup›
locale stateful_protocol_model =
  fixes arityf::"'fun ⇒ nat"
    and aritys::"'sets ⇒ nat"
    and publicf::"'fun ⇒ bool"
    and Anaf::"'fun ⇒ ((('fun,'atom::finite,'sets,'lbl) prot_fun, nat) term list × nat list)"
    and Γf::"'fun ⇒ 'atom option"
    and label_witness1::"'lbl"
    and label_witness2::"'lbl"
  assumes Anaf_assm1: "∀f. let (K, M) = Anaf f in (∀k ∈ subtermsset (set K).
      is_Fun k ⟶ (is_Fu (the_Fun k)) ∧ length (args k) = arityf (the_Fu (the_Fun k)))"
    and Anaf_assm2: "∀f. let (K, M) = Anaf f in ∀i ∈ fvset (set K) ∪ set M. i < arityf f"
    and publicf_assm: "∀f. arityf f > (0::nat) ⟶ publicf f"
    and Γf_assm: "∀f. arityf f = (0::nat) ⟶ Γf f ≠ None"
    and label_witness_assm: "label_witness1 ≠ label_witness2"
begin

lemma Anaf_assm1_alt: 
  assumes "Anaf f = (K,M)" "k ∈ subtermsset (set K)"
  shows "(∃x. k = Var x) ∨ (∃h T. k = Fun (Fu h) T ∧ length T = arityf h)"
proof (cases k)
  case (Fun g T)
  let ?P = "λk. is_Fun k ⟶ is_Fu (the_Fun k) ∧ length (args k) = arityf (the_Fu (the_Fun k))"
  let ?Q = "λK M. ∀k ∈ subtermsset (set K). ?P k"

  have "?Q (fst (Anaf f)) (snd (Anaf f))" using Anaf_assm1 split_beta[of ?Q "Anaf f"] by meson
  hence "?Q K M" using assms(1) by simp
  hence "?P k" using assms(2) by blast
  thus ?thesis using Fun by (cases g) auto
qed simp

lemma Anaf_assm2_alt:
  assumes "Anaf f = (K,M)" "i ∈ fvset (set K) ∪ set M"
  shows "i < arityf f"
using Anaf_assm2 assms by fastforce


subsection ‹Definitions›
fun arity where
  "arity (Fu f) = arityf f"
| "arity (Set s) = aritys s"
| "arity (Val _) = 0"
| "arity (Abs _) = 0"
| "arity Pair = 2"
| "arity (Attack _) = 0"
| "arity OccursFact = 2"
| "arity OccursSec = 0"
| "arity (PubConst _ _) = 0"

fun public where
  "public (Fu f) = publicf f"
| "public (Set s) = (aritys s > 0)"
| "public (Val n) = False"
| "public (Abs _) = False"
| "public Pair = True"
| "public (Attack _) = False"
| "public OccursFact = True"
| "public OccursSec = False"
| "public (PubConst _ _) = True"

fun Ana where
  "Ana (Fun (Fu f) T) = (
    if arityf f = length T ∧ arityf f > 0
    then let (K,M) = Anaf f in (K ⋅list (!) T, map ((!) T) M)
    else ([], []))"
| "Ana _ = ([], [])"

definition Γv where
  "Γv v ≡ (
    if (∀t ∈ subterms (fst v).
          case t of (TComp f T) ⇒ arity f > 0 ∧ arity f = length T | _ ⇒ True)
    then fst v
    else TAtom Bottom)"

fun Γ where
  "Γ (Var v) = Γv v"
| "Γ (Fun f T) = (
    if arity f = 0
    then case f of
      (Fu g) ⇒ TAtom (case Γf g of Some a ⇒ Atom a | None ⇒ Bottom)
    | (Val _) ⇒ TAtom Value
    | (Abs _) ⇒ TAtom AbsValue
    | (Set _) ⇒ TAtom SetType
    | (Attack _) ⇒ TAtom AttackType
    | OccursSec ⇒ TAtom OccursSecType
    | (PubConst a _) ⇒ TAtom a
    | _ ⇒ TAtom Bottom
    else TComp f (map Γ T))"

lemma Γ_consts_simps[simp]:
  "arityf g = 0 ⟹ Γ (Fun (Fu g) []::('fun,'atom,'sets,'lbl) prot_term)
                    = TAtom (case Γf g of Some a ⇒ Atom a | None ⇒ Bottom)"
  "Γ (Fun (Val n) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom Value"
  "Γ (Fun (Abs b) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom AbsValue"
  "aritys s = 0 ⟹ Γ (Fun (Set s) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom SetType"
  "Γ (Fun (Attack x) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom AttackType"
  "Γ (Fun OccursSec []::('fun,'atom,'sets,'lbl) prot_term) = TAtom OccursSecType"
  "Γ (Fun (PubConst a t) []::('fun,'atom,'sets,'lbl) prot_term) = TAtom a"
by simp+

lemma Γ_Fu_simps[simp]:
  "arityf f ≠ 0 ⟹ Γ (Fun (Fu f) T) = TComp (Fu f) (map Γ T)" (is "?A1 ⟹ ?A2")
  "arityf f = 0 ⟹ Γf f = Some a ⟹ Γ (Fun (Fu f) T) = TAtom (Atom a)" (is "?B1 ⟹ ?B2 ⟹ ?B3")
  "arityf f = 0 ⟹ Γf f = None ⟹ Γ (Fun (Fu f) T) = TAtom Bottom" (is "?C1 ⟹ ?C2 ⟹ ?C3")
  "Γ (Fun (Fu f) T) ≠ TAtom Value" (is ?D)
  "Γ (Fun (Fu f) T) ≠ TAtom AttackType" (is ?E)
  "Γ (Fun (Fu f) T) ≠ TAtom OccursSecType" (is ?F)
proof -
  show "?A1 ⟹ ?A2" by simp
  show "?B1 ⟹ ?B2 ⟹ ?B3" by simp
  show "?C1 ⟹ ?C2 ⟹ ?C3" by simp
  show ?D by (cases "Γf f") simp_all
  show ?E by (cases "Γf f") simp_all
  show ?F by (cases "Γf f") simp_all
qed

lemma Γ_Set_simps[simp]:
  "aritys s ≠ 0 ⟹ Γ (Fun (Set s) T) = TComp (Set s) (map Γ T)"
  "Γ (Fun (Set s) T) = TAtom SetType ∨ Γ (Fun (Set s) T) = TComp (Set s) (map Γ T)"
  "Γ (Fun (Set s) T) ≠ TAtom Value"
  "Γ (Fun (Set s) T) ≠ TAtom (Atom a)"
  "Γ (Fun (Set s) T) ≠ TAtom AttackType"
  "Γ (Fun (Set s) T) ≠ TAtom OccursSecType"
  "Γ (Fun (Set s) T) ≠ TAtom Bottom"
by auto


subsection ‹Locale Interpretations›
lemma Ana_Fu_cases:
  assumes "Ana (Fun f T) = (K,M)"
    and "f = Fu g"
    and "Anaf g = (K',M')"
  shows "(K,M) = (if arityf g = length T ∧ arityf g > 0
                  then (K' ⋅list (!) T, map ((!) T) M')
                  else ([],[]))" (is ?A)
    and "(K,M) = (K' ⋅list (!) T, map ((!) T) M') ∨ (K,M) = ([],[])" (is ?B)
proof -
  show ?A using assms by (cases "arityf g = length T ∧ arityf g > 0") auto
  thus ?B by metis
qed

lemma Ana_Fu_intro:
  assumes "arityf f = length T" "arityf f > 0"
    and "Anaf f = (K',M')"
  shows "Ana (Fun (Fu f) T) = (K' ⋅list (!) T, map ((!) T) M')"
using assms by simp

lemma Ana_Fu_elim:
  assumes "Ana (Fun f T) = (K,M)"
    and "f = Fu g"
    and "Anaf g = (K',M')"
    and "(K,M) ≠ ([],[])"
  shows "arityf g = length T" (is ?A)
    and "(K,M) = (K' ⋅list (!) T, map ((!) T) M')" (is ?B)
proof -
  show ?A using assms by force
  moreover have "arityf g > 0" using assms by force
  ultimately show ?B using assms by auto
qed

lemma Ana_nonempty_inv:
  assumes "Ana t ≠ ([],[])"
  shows "∃f T. t = Fun (Fu f) T ∧ arityf f = length T ∧ arityf f > 0 ∧
               (∃K M. Anaf f = (K, M) ∧ Ana t = (K ⋅list (!) T, map ((!) T) M))"
using assms
proof (induction t rule: Ana.induct)
  case (1 f T)
  hence *: "arityf f = length T" "0 < arityf f"
           "Ana (Fun (Fu f) T) = (case Anaf f of (K, M) ⇒ (K ⋅list (!) T, map ((!) T) M))"
    using Ana.simps(1)[of f T] unfolding Let_def by metis+

  obtain K M where **: "Anaf f = (K, M)" by (metis surj_pair)
  hence "Ana (Fun (Fu f) T) = (K ⋅list (!) T, map ((!) T) M)" using *(3) by simp
  thus ?case using ** *(1,2) by blast
qed simp_all

lemma assm1:
  assumes "Ana t = (K,M)"
  shows "fvset (set K) ⊆ fv t"
using assms
proof (induction t rule: term.induct)
  case (Fun f T)
  have aux: "fvset (set K ⋅set (!) T) ⊆ fvset (set T)"
    when K: "∀i ∈ fvset (set K). i < length T"
    for K::"(('fun,'atom,'sets,'lbl) prot_fun, nat) term list"
  proof
    fix x assume "x ∈ fvset (set K ⋅set (!) T)"
    then obtain k where k: "k ∈ set K" "x ∈ fv (k ⋅ (!) T)" by moura
    have "∀i ∈ fv k. i < length T" using K k(1) by simp
    thus "x ∈ fvset (set T)"
      by (metis (no_types, lifting) k(2) contra_subsetD fv_set_mono image_subsetI nth_mem
                                    subst_apply_fv_unfold)
  qed

  { fix g assume f: "f = Fu g" and K: "K ≠ []"
    obtain K' M' where *: "Anaf g = (K',M')" by moura
    have "(K, M) ≠ ([], [])" using K by simp
    hence "(K, M) = (K' ⋅list (!) T, map ((!) T) M')" "arityf g = length T"
      using Ana_Fu_cases(1)[OF Fun.prems f *]
      by presburger+
    hence ?case using aux[of K'] Anaf_assm2_alt[OF *] by auto
  } thus ?case using Fun by (cases f) fastforce+
qed simp

lemma assm2:
  assumes "Ana t = (K,M)"
  and "⋀g S'. Fun g S' ⊑ t ⟹ length S' = arity g"
  and "k ∈ set K"
  and "Fun f T' ⊑ k"
  shows "length T' = arity f"
using assms
proof (induction t rule: term.induct)
  case (Fun g T)
  obtain h where 2: "g = Fu h"
    using Fun.prems(1,3) by (cases g) auto
  obtain K' M' where 1: "Anaf h = (K',M')" by moura
  have "(K,M) ≠ ([],[])" using Fun.prems(3) by auto
  hence "(K,M) = (K' ⋅list (!) T, map ((!) T) M')"
        "⋀i. i ∈ fvset (set K') ∪ set M' ⟹ i < length T"
    using Ana_Fu_cases(1)[OF Fun.prems(1) 2 1] Anaf_assm2_alt[OF 1]
    by presburger+
  hence "K = K' ⋅list (!) T" and 3: "∀i∈fvset (set K'). i < length T" by simp_all
  then obtain k' where k': "k' ∈ set K'" "k = k' ⋅ (!) T" using Fun.prems(3) by moura
  hence 4: "Fun f T' ∈ subterms (k' ⋅ (!) T)" "fv k' ⊆ fvset (set K')"
    using Fun.prems(4) by auto
  show ?case
  proof (cases "∃i ∈ fv k'. Fun f T' ∈ subterms (T ! i)")
    case True
    hence "Fun f T' ∈ subtermsset (set T)" using k' Fun.prems(4) 3 by auto
    thus ?thesis using Fun.prems(2) by auto
  next
    case False
    then obtain S where "Fun f S ∈ subterms k'" "Fun f T' = Fun f S ⋅ (!) T"
      using k'(2) Fun.prems(4) subterm_subst_not_img_subterm by force
    thus ?thesis using Anaf_assm1_alt[OF 1, of "Fun f S"] k'(1) by (cases f) auto
  qed
qed simp

lemma assm4:
  assumes "Ana (Fun f T) = (K, M)"
  shows "set M ⊆ set T"
using assms
proof (cases f)
  case (Fu g)
  obtain K' M' where *: "Anaf g = (K',M')" by moura
  have "M = [] ∨ (arityf g = length T ∧ M = map ((!) T) M')"
    using Ana_Fu_cases(1)[OF assms Fu *]
    by (meson prod.inject)
  thus ?thesis using Anaf_assm2_alt[OF *] by auto
qed auto

lemma assm5: "Ana t = (K,M) ⟹ K ≠ [] ∨ M ≠ [] ⟹ Ana (t ⋅ δ) = (K ⋅list δ, M ⋅list δ)"
proof (induction t rule: term.induct)
  case (Fun f T) thus ?case
  proof (cases f)
    case (Fu g)
    obtain K' M' where *: "Anaf g = (K',M')" by moura
    have **: "K = K' ⋅list (!) T" "M = map ((!) T) M'"
             "arityf g = length T" "∀i ∈ fvset (set K') ∪ set M'. i < arityf g" "0 < arityf g"
      using Fun.prems(2) Ana_Fu_cases(1)[OF Fun.prems(1) Fu *] Anaf_assm2_alt[OF *]
      by (meson prod.inject)+

    have ***: "∀i ∈ fvset (set K'). i < length T" "∀i ∈ set M'. i < length T" using **(3,4) by auto
    
    have "K ⋅list δ = K' ⋅list (!) (map (λt. t ⋅ δ) T)"
         "M ⋅list δ = map ((!) (map (λt. t ⋅ δ) T)) M'"
      using subst_idx_map[OF ***(2), of δ]
            subst_idx_map'[OF ***(1), of δ]
            **(1,2)
      by fast+
    thus ?thesis using Fu * **(3,5) by auto
  qed auto
qed simp

sublocale intruder_model arity public Ana
apply unfold_locales
by (metis assm1, metis assm2, rule Ana.simps, metis assm4, metis assm5)

adhoc_overloading INTRUDER_SYNTH intruder_synth
adhoc_overloading INTRUDER_DEDUCT intruder_deduct

lemma assm6: "arity c = 0 ⟹ ∃a. ∀X. Γ (Fun c X) = TAtom a" by (cases c) auto

lemma assm7: "0 < arity f ⟹ Γ (Fun f T) = TComp f (map Γ T)" by auto

lemma assm8: "infinite {c. Γ (Fun c []::('fun,'atom,'sets,'lbl) prot_term) = TAtom a ∧ public c}"
  (is "?P a")
proof -
  let ?T = "λf. (range f)::('fun,'atom,'sets,'lbl) prot_fun set"
  let ?A = "λf. ∀x::nat ∈ UNIV. ∀y::nat ∈ UNIV. (f x = f y) = (x = y)"
  let ?B = "λf. ∀x::nat ∈ UNIV. f x ∈ ?T f"
  let ?C = "λf. ∀y::('fun,'atom,'sets,'lbl) prot_fun ∈ ?T f. ∃x ∈ UNIV. y = f x"
  let ?D = "λf b. ?T f ⊆ {c. Γ (Fun c []::('fun,'atom,'sets,'lbl) prot_term) = TAtom b ∧ public c}"

  have sub_lmm: "?P b" when "?A f" "?C f" "?C f" "?D f b" for b f
  proof -
    have "∃g::nat ⇒ ('fun,'atom,'sets,'lbl) prot_fun. bij_betw g UNIV (?T f)"
      using bij_betwI'[of UNIV f "?T f"] that(1,2,3) by blast
    hence "infinite (?T f)" by (metis nat_not_finite bij_betw_finite)
    thus ?thesis using infinite_super[OF that(4)] by blast
  qed

  show ?thesis
  proof (cases a)
    case (Atom b) thus ?thesis using sub_lmm[of "PubConst (Atom b)" a] by force
  next
    case Value thus ?thesis using sub_lmm[of "PubConst Value" a] by force
  next
    case SetType thus ?thesis using sub_lmm[of "PubConst SetType" a] by fastforce
  next
    case AttackType thus ?thesis using sub_lmm[of "PubConst AttackType" a] by fastforce
  next
    case Bottom thus ?thesis using sub_lmm[of "PubConst Bottom" a] by fastforce
  next
    case OccursSecType thus ?thesis using sub_lmm[of "PubConst OccursSecType" a] by fastforce
  next
    case AbsValue thus ?thesis using sub_lmm[of "PubConst AbsValue" a] by force
  qed
qed

lemma assm9: "TComp f T ⊑ Γ t ⟹ arity f > 0"
proof (induction t rule: term.induct)
  case (Var x)
  hence "Γ (Var x) ≠ TAtom Bottom" by force
  hence "∀t ∈ subterms (fst x). case t of
            TComp f T ⇒ arity f > 0 ∧ arity f = length T
          | _ ⇒ True"
    using Var Γ.simps(1)[of x] unfolding Γv_def by meson
  thus ?case using Var by (fastforce simp add: Γv_def)
next
  case (Fun g S)
  have "arity g ≠ 0" using Fun.prems Var_subtermeq assm6 by force
  thus ?case using Fun by (cases "TComp f T = TComp g (map Γ S)") auto
qed

lemma assm10: "wftrm (Γ (Var x))"
unfolding wftrm_def by (auto simp add: Γv_def)

lemma assm11: "arity f > 0 ⟹ public f" using publicf_assm by (cases f) auto

lemma assm12: "Γ (Var (τ, n)) = Γ (Var (τ, m))" by (simp add: Γv_def)

lemma assm13: "arity c = 0 ⟹ Ana (Fun c T) = ([],[])" by (cases c) simp_all

lemma assm14:
  assumes "Ana (Fun f T) = (K,M)"
  shows "Ana (Fun f T ⋅ δ) = (K ⋅list δ, M ⋅list δ)"
proof -
  show ?thesis
  proof (cases "(K, M) = ([],[])")
    case True
    { fix g assume f: "f = Fu g"
      obtain K' M' where "Anaf g = (K',M')" by moura
      hence ?thesis using assms f True by auto
    } thus ?thesis using True assms by (cases f) auto
  next
    case False
    then obtain g where **: "f = Fu g" using assms by (cases f) auto
    obtain K' M' where *: "Anaf g = (K',M')" by moura
    have ***: "K = K' ⋅list (!) T" "M = map ((!) T) M'" "arityf g = length T"
              "∀i ∈ fvset (set K') ∪ set M'. i < arityf g"
      using Ana_Fu_cases(1)[OF assms ** *] False Anaf_assm2_alt[OF *]
      by (meson prod.inject)+
    have ****: "∀i∈fvset (set K'). i < length T" "∀i∈set M'. i < length T" using ***(3,4) by auto
    have "K ⋅list δ = K' ⋅list (!) (map (λt. t ⋅ δ) T)"
         "M ⋅list δ = map ((!) (map (λt. t ⋅ δ) T)) M'"
      using subst_idx_map[OF ****(2), of δ]
            subst_idx_map'[OF ****(1), of δ]
            ***(1,2)
      by auto
    thus ?thesis using assms * ** ***(3) by auto
  qed
qed

sublocale labeled_stateful_typing' arity public Ana Γ Pair label_witness1 label_witness2
  apply unfold_locales
  subgoal by (metis assm6)
  subgoal by (metis assm7)
  subgoal by (metis assm9)
  subgoal by (rule assm10)
  subgoal by (metis assm12)
  subgoal by (metis assm13)
  subgoal by (metis assm14)
  subgoal by (rule label_witness_assm)
  subgoal by (rule arity.simps(5))
  subgoal by (metis assm14)
  subgoal by (metis assm8)
  subgoal by (metis assm11)
  done


subsection ‹The Protocol Transition System, Defined in Terms of the Reachable Constraints›
definition transaction_decl_subst where
  "transaction_decl_subst (ξ::('fun,'atom,'sets,'lbl) prot_subst) T ≡
    subst_domain ξ = fst ` set (transaction_decl T ()) ∧
    (∀(x,cs) ∈ set (transaction_decl T ()). ∃c ∈ cs.
      ξ x = Fun (Fu c) [] ∧
      arity (Fu c::('fun,'atom,'sets,'lbl) prot_fun) = 0) ∧
    wtsubst ξ"

definition transaction_fresh_subst where
  "transaction_fresh_subst σ T 𝒜 ≡
    subst_domain σ = set (transaction_fresh T) ∧
    (∀t ∈ subst_range σ. ∃c. t = Fun c [] ∧ ¬public c ∧ arity c = 0) ∧
    (∀t ∈ subst_range σ. t ∉ subtermsset (trmslsst 𝒜)) ∧
    (∀t ∈ subst_range σ. t ∉ subtermsset (trms_transaction T)) ∧
    wtsubst σ ∧ inj_on σ (subst_domain σ)"

(* NB: We need the protocol P as a parameter for this definition---even though we will only apply α
       to a single transaction T of P---because we have to ensure that α(fv(T)) is disjoint from
       the bound variables of P and 𝒜. *)
definition transaction_renaming_subst where
  "transaction_renaming_subst α P 𝒜 ≡
    ∃n ≥ max_var_set (⋃(vars_transaction ` set P) ∪ varslsst 𝒜). α = var_rename n"

definition (in intruder_model) constraint_model where
  "constraint_model ℐ 𝒜 ≡ 
    constr_sem_stateful ℐ (unlabel 𝒜) ∧
    interpretationsubst ℐ ∧
    wftrms (subst_range ℐ)"

definition (in typed_model) welltyped_constraint_model where
  "welltyped_constraint_model ℐ 𝒜 ≡  wtsubst ℐ ∧ constraint_model ℐ 𝒜"

text ‹
  The set of symbolic constraints reachable in any symbolic run of the protocol ‹P›.
  
  ‹ξ› instantiates the "declared variables" of transaction ‹T› with ground terms.
  ‹σ› instantiates the fresh variables of transaction ‹T› with fresh terms.
  ‹α› is a variable-renaming whose range consists of fresh variables.
›
inductive_set reachable_constraints::
  "('fun,'atom,'sets,'lbl) prot ⇒ ('fun,'atom,'sets,'lbl) prot_constr set"
  for P::"('fun,'atom,'sets,'lbl) prot"
where
  init[simp]:
  "[] ∈ reachable_constraints P"
| step:
  "⟦𝒜 ∈ reachable_constraints P;
    T ∈ set P;
    transaction_decl_subst ξ T;
    transaction_fresh_subst σ T 𝒜;
    transaction_renaming_subst α P 𝒜
   ⟧ ⟹ 𝒜@duallsst (transaction_strand T ⋅lsst ξ ∘s σ ∘s α) ∈ reachable_constraints P"


subsection ‹Minor Lemmata›
lemma Γv_TAtom[simp]: "Γv (TAtom a, n) = TAtom a"
unfolding Γv_def by simp

lemma Γv_TAtom':
  assumes "a ≠ Bottom"
  shows "Γv (τ, n) = TAtom a ⟷ τ = TAtom a"
proof
  assume "Γv (τ, n) = TAtom a"
  thus "τ = TAtom a" by (metis (no_types, lifting) assms Γv_def fst_conv term.inject(1)) 
qed simp

lemma Γv_TAtom_inv:
  "Γv x = TAtom (Atom a) ⟹ ∃m. x = (TAtom (Atom a), m)"
  "Γv x = TAtom Value ⟹ ∃m. x = (TAtom Value, m)"
  "Γv x = TAtom SetType ⟹ ∃m. x = (TAtom SetType, m)"
  "Γv x = TAtom AttackType ⟹ ∃m. x = (TAtom AttackType, m)"
  "Γv x = TAtom OccursSecType ⟹ ∃m. x = (TAtom OccursSecType, m)"
by (metis Γv_TAtom' surj_pair prot_atom.distinct(7),
    metis Γv_TAtom' surj_pair prot_atom.distinct(18),
    metis Γv_TAtom' surj_pair prot_atom.distinct(26),
    metis Γv_TAtom' surj_pair prot_atom.distinct(32),
    metis Γv_TAtom' surj_pair prot_atom.distinct(38))

lemma Γv_TAtom'':
  "(fst x = TAtom (Atom a)) = (Γv x = TAtom (Atom a))" (is "?A = ?A'")
  "(fst x = TAtom Value) = (Γv x = TAtom Value)" (is "?B = ?B'")
  "(fst x = TAtom SetType) = (Γv x = TAtom SetType)" (is "?C = ?C'")
  "(fst x = TAtom AttackType) = (Γv x = TAtom AttackType)" (is "?D = ?D'")
  "(fst x = TAtom OccursSecType) = (Γv x = TAtom OccursSecType)" (is "?E = ?E'")
proof -
  have 1: "?A ⟹ ?A'" "?B ⟹ ?B'" "?C ⟹ ?C'" "?D ⟹ ?D'" "?E ⟹ ?E'"
    by (metis Γv_TAtom prod.collapse)+

  have 2: "?A' ⟹ ?A" "?B' ⟹ ?B" "?C' ⟹ ?C" "?D' ⟹ ?D" "?E' ⟹ ?E"
    using Γv_TAtom Γv_TAtom_inv(1) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(2) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(3) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(4) apply fastforce
    using Γv_TAtom Γv_TAtom_inv(5) by fastforce

  show "?A = ?A'" "?B = ?B'" "?C = ?C'" "?D = ?D'" "?E = ?E'"
    using 1 2 by metis+
qed

lemma Γv_Var_image:
  "Γv ` X = Γ ` Var ` X"
by force

lemma Γ_Fu_const:
  assumes "arityf g = 0"
  shows "∃a. Γ (Fun (Fu g) T) = TAtom (Atom a)"
proof -
  have "Γf g ≠ None" using assms Γf_assm by blast
  thus ?thesis using assms by force
qed

lemma Fun_Value_type_inv:
  fixes T::"('fun,'atom,'sets,'lbl) prot_term list"
  assumes "Γ (Fun f T) = TAtom Value"
  shows "(∃n. f = Val n) ∨ (∃bs. f = Abs bs) ∨ (∃n. f = PubConst Value n)"
proof -
  have *: "arity f = 0" by (metis const_type_inv assms) 
  show ?thesis  using assms
  proof (cases f)
    case (Fu g)
    hence "arityf g = 0" using * by simp
    hence False using Fu Γ_Fu_const[of g T] assms by auto
    thus ?thesis by metis
  next
    case (Set s)
    hence "aritys s = 0" using * by simp
    hence False using Set assms by auto
    thus ?thesis by metis
  qed simp_all
qed

lemma Anaf_keys_not_val_terms:
  assumes "Anaf f = (K, T)"
    and "k ∈ set K"
    and "g ∈ funs_term k"
  shows "¬is_Val g"
    and "¬is_PubConstValue g"
    and "¬is_Abs g"
proof -
  { assume "is_Val g"
    then obtain n S where *: "Fun (Val n) S ∈ subtermsset (set K)"
      using assms(2) funs_term_Fun_subterm[OF assms(3)]
      by (cases g) auto
    hence False using Anaf_assm1_alt[OF assms(1) *] by simp
  } moreover {
    assume "is_PubConstValue g"
    then obtain n S where *: "Fun (PubConst Value n) S ∈ subtermsset (set K)"
      using assms(2) funs_term_Fun_subterm[OF assms(3)]
      unfolding is_PubConstValue_def by (cases g) auto
    hence False using Anaf_assm1_alt[OF assms(1) *] by simp
  } moreover {
    assume "is_Abs g"
    then obtain a S where *: "Fun (Abs a) S ∈ subtermsset (set K)"
      using assms(2) funs_term_Fun_subterm[OF assms(3)]
      by (cases g) auto
    hence False using Anaf_assm1_alt[OF assms(1) *] by simp
  } ultimately show "¬is_Val g" "¬is_PubConstValue g" "¬is_Abs g" by metis+
qed

lemma Anaf_keys_not_pairs:
  assumes "Anaf f = (K, T)"
    and "k ∈ set K"
    and "g ∈ funs_term k"
  shows "g ≠ Pair"
proof
  assume "g = Pair"
  then obtain S where *: "Fun Pair S ∈ subtermsset (set K)"
    using assms(2) funs_term_Fun_subterm[OF assms(3)]
    by (cases g) auto
  show False using Anaf_assm1_alt[OF assms(1) *] by simp
qed

lemma Ana_Fu_keys_funs_term_subset:
  fixes K::"('fun,'atom,'sets,'lbl) prot_term list"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
  shows "⋃(funs_term ` set K) ⊆ ⋃(funs_term ` set K') ∪ funs_term (Fun (Fu f) S)"
proof -
  { fix k assume k: "k ∈ set K"
    then obtain k' where k':
        "k' ∈ set K'" "k = k' ⋅ (!) S" "arityf f = length S"
        "subterms k' ⊆ subtermsset (set K')"
      using assms Ana_Fu_elim[OF assms(1) _ assms(2)] by fastforce

    have 1: "funs_term k' ⊆ ⋃(funs_term ` set K')" using k'(1) by auto

    have "i < length S" when "i ∈ fv k'" for i
      using that Anaf_assm2_alt[OF assms(2), of i] k'(1,3)
      by auto
    hence 2: "funs_term (S ! i) ⊆ funs_term (Fun (Fu f) S)" when "i ∈ fv k'" for i
      using that by force
  
    have "funs_term k ⊆ ⋃(funs_term ` set K') ∪ funs_term (Fun (Fu f) S)"
      using funs_term_subst[of k' "(!) S"] k'(2) 1 2 by fast
  } thus ?thesis by blast
qed

lemma Ana_Fu_keys_not_pubval_terms:
  fixes k::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
    and "k ∈ set K"
    and "∀g ∈ funs_term (Fun (Fu f) S). ¬is_PubConstValue g"
  shows "∀g ∈ funs_term k. ¬is_PubConstValue g"
using assms(3,4) Anaf_keys_not_val_terms(1,2)[OF assms(2)]
      Ana_Fu_keys_funs_term_subset[OF assms(1,2)]
by blast

lemma Ana_Fu_keys_not_abs_terms:
  fixes k::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
    and "k ∈ set K"
    and "∀g ∈ funs_term (Fun (Fu f) S). ¬is_Abs g"
  shows "∀g ∈ funs_term k. ¬is_Abs g"
using assms(3,4) Anaf_keys_not_val_terms(3)[OF assms(2)]
      Ana_Fu_keys_funs_term_subset[OF assms(1,2)]
by blast

lemma Ana_Fu_keys_not_pairs:
  fixes k::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "Ana (Fun (Fu f) S) = (K, T)"
    and "Anaf f = (K', T')"
    and "k ∈ set K"
    and "∀g ∈ funs_term (Fun (Fu f) S). g ≠ Pair"
  shows "∀g ∈ funs_term k. g ≠ Pair"
using assms(3,4) Anaf_keys_not_pairs[OF assms(2)]
      Ana_Fu_keys_funs_term_subset[OF assms(1,2)]
by blast

lemma Ana_Fu_keys_length_eq:
  assumes "length T = length S"
  shows "length (fst (Ana (Fun (Fu f) T))) = length (fst (Ana (Fun (Fu f) S)))"
proof (cases "arityf f = length T ∧ arityf f > 0")
  case True thus ?thesis using assms by (cases "Anaf f") auto
next
  case False thus ?thesis using assms by force
qed

lemma deduct_occurs_in_ik:
  fixes t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes t: "M ⊢ occurs t"
    and M: "∀s ∈ subtermsset M. OccursFact ∉ ⋃(funs_term ` set (snd (Ana s)))"
           "∀s ∈ subtermsset M. OccursSec ∉ ⋃(funs_term ` set (snd (Ana s)))"
           "Fun OccursSec [] ∉ M"
  shows "occurs t ∈ M"
using private_fun_deduct_in_ik''[of M OccursFact "[Fun OccursSec [], t]" OccursSec] t M 
by fastforce

lemma constraint_model_prefix:
  assumes "constraint_model I (A@B)"
  shows "constraint_model I A"
by (metis assms strand_sem_append_stateful unlabel_append constraint_model_def)

lemma welltyped_constraint_model_prefix:
  assumes "welltyped_constraint_model I (A@B)"
  shows "welltyped_constraint_model I A"
by (metis assms constraint_model_prefix welltyped_constraint_model_def)

lemma welltyped_constraint_model_deduct_append:
  assumes "welltyped_constraint_model I A"
    and "iklsst A ⋅set I ⊢ s ⋅ I"
  shows "welltyped_constraint_model I (A@[(l,send⟨[s]⟩)])"
using assms strand_sem_append_stateful[of "{}" "{}" "unlabel A" _ I]
unfolding welltyped_constraint_model_def constraint_model_def by simp

lemma welltyped_constraint_model_deduct_split:
  assumes "welltyped_constraint_model I (A@[(l,send⟨[s]⟩)])"
  shows "welltyped_constraint_model I A"
    and "iklsst A ⋅set I ⊢ s ⋅ I"
using assms strand_sem_append_stateful[of "{}" "{}" "unlabel A" _ I]
unfolding welltyped_constraint_model_def constraint_model_def by simp_all

lemma welltyped_constraint_model_deduct_iff:
  "welltyped_constraint_model I (A@[(l,send⟨[s]⟩)]) ⟷
    welltyped_constraint_model I A ∧ iklsst A ⋅set I ⊢ s ⋅ I"
by (metis welltyped_constraint_model_deduct_append welltyped_constraint_model_deduct_split)  

lemma constraint_model_Val_is_Value_term:
  assumes "welltyped_constraint_model I A"
    and "t ⋅ I = Fun (Val n) []"
  shows "t = Fun (Val n) [] ∨ (∃m. t = Var (TAtom Value, m))"
proof -
  have "wtsubst I" using assms(1) unfolding welltyped_constraint_model_def by simp
  moreover have "Γ (Fun (Val n) []) = TAtom Value" by auto
  ultimately have *: "Γ t = TAtom Value" by (metis (no_types) assms(2) wt_subst_trm'')

  show ?thesis
  proof (cases t)
    case (Var x)
    obtain τ m where x: "x = (τ, m)" by (metis surj_pair)
    have "Γv x = TAtom Value" using * Var by auto
    hence "τ = TAtom Value" using x Γv_TAtom'[of Value τ m] by simp
    thus ?thesis using x Var by metis
  next
    case (Fun f T) thus ?thesis using assms(2) by auto
  qed
qed

lemma wellformed_transaction_sem_receives:
  fixes T::"('fun,'atom,'sets,'lbl) prot_transaction"
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and s: "receive⟨ts⟩ ∈ set (unlabel (transaction_receive T ⋅lsst θ))"
  shows "∀t ∈ set ts. IK ⊢ t ⋅ ℐ"
proof -
  let ?R = "unlabel (duallsst (transaction_receive T ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)"

  obtain l B s where B:
      "(l,send⟨ts⟩) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (transaction_receive T ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(2)[of ts "transaction_receive T ⋅lsst θ"]
          duallsst_in_set_prefix_obtain_subst[of "send⟨ts⟩" "transaction_receive T" θ]
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[send⟨ts⟩]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps)

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[send⟨ts⟩]) ℐ"
    using B 1 unfolding prefix_def unlabel_def
    by (metis duallsst_def map_append strand_sem_append_stateful) 
  hence t_deduct: "∀t ∈ set ts. IK ∪ (iklsst (duallsst (B ⋅lsst θ)) ⋅set ℐ) ⊢ t ⋅ ℐ"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[send⟨ts⟩]" ℐ]
    by simp

  have "∀s ∈ set (unlabel (transaction_receive T)). ∃t. s = receive⟨t⟩"
    using T_valid wellformed_transaction_unlabel_cases(1)[OF T_valid] by auto
  moreover { fix A::"('fun,'atom,'sets,'lbl) prot_strand" and θ
    assume "∀s ∈ set (unlabel A). ∃t. s = receive⟨t⟩"
    hence "∀s ∈ set (unlabel (A ⋅lsst θ)). ∃t. s = receive⟨t⟩"
    proof (induction A)
      case (Cons a A) thus ?case using subst_lsst_cons[of a A θ] by (cases a) auto
    qed simp
    hence "∀s ∈ set (unlabel (A ⋅lsst θ)). ∃t. s = receive⟨t⟩"
      by (simp add: list.pred_set is_Receive_def)
    hence "∀s ∈ set (unlabel (duallsst (A ⋅lsst θ))). ∃t. s = send⟨t⟩"
      by (metis duallsst_memberD duallsstp_inv(2) unlabel_in unlabel_mem_has_label)
  }
  ultimately have "∀s ∈ set ?R. ∃ts. s = send⟨ts⟩" by simp
  hence "iksst ?R = {}" unfolding unlabel_def iksst_def by fast
  hence "iklsst (duallsst (B ⋅lsst θ)) = {}"
    using B(2) 1 iksst_append duallsst_append
    by (metis (no_types, lifting) Un_empty map_append prefix_def unlabel_def) 
  thus ?thesis using t_deduct by simp
qed

lemma wellformed_transaction_sem_pos_checks:
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and "⟨ac: t ∈ u⟩ ∈ set (unlabel (transaction_checks T ⋅lsst θ))"
  shows "(t ⋅ ℐ, u ⋅ ℐ) ∈ DB"
proof -
  let ?s = "⟨ac: t ∈ u⟩"
  let ?R = "transaction_receive T@transaction_checks T"
  let ?R' = "unlabel (duallsst (?R ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)@?S (transaction_checks T)"
  let ?P = "λa. is_Receive a ∨ is_Check_or_Assignment a"
  let ?Q = "λa. is_Send a ∨ is_Check_or_Assignment a"

  have s: "?s ∈ set (unlabel (?R ⋅lsst θ))"
    using assms(3) subst_lsst_append[of "transaction_receive T"]
          unlabel_append[of "transaction_receive T"]
    by auto

  obtain l B s where B:
      "(l,?s) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (?R ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(6)[of _ t u]
          duallsst_in_set_prefix_obtain_subst[of ?s ?R θ] 
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[?s]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps )

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[?s]) ℐ"
    using B 1 strand_sem_append_stateful subst_lsst_append
    unfolding prefix_def unlabel_def duallsst_def
    by (metis (no_types) map_append)
  hence in_db: "(t ⋅ ℐ, u ⋅ ℐ) ∈ dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[?s]" ℐ]
    by simp
  
  have "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ?Q a"
  proof
    fix a assume a: "a ∈ set (unlabel (duallsst (B ⋅lsst θ)))"

    have "?P a" when a: "a ∈ set (unlabel ?R)" for a
      using a wellformed_transaction_unlabel_cases(1,2)[OF T_valid]
      unfolding unlabel_def by fastforce
    hence "?P a" when a: "a ∈ set (unlabel (?R ⋅lsst θ))" for a
      using a stateful_strand_step_cases_subst(2,11)[of _ θ] subst_lsst_unlabel[of ?R θ]
      unfolding subst_apply_stateful_strand_def by auto
    hence B_P: "∀a ∈ set (unlabel (B ⋅lsst θ)). ?P a"
      using unlabel_mono[OF set_mono_prefix[OF append_prefixD[OF B(2)]]]
      by blast

    obtain l where "(l,a) ∈ set (duallsst (B ⋅lsst θ))"
      using a by (meson unlabel_mem_has_label)
    then obtain b where b: "(l,b) ∈ set (B ⋅lsst θ)" "duallsstp (l,b) = (l,a)"
      using duallsst_memberD by blast
    hence "?P b" using B_P unfolding unlabel_def by fastforce
    thus "?Q a" using duallsstp_inv[OF b(2)] by (cases b) auto
  qed
  hence "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ¬is_Insert a ∧ ¬is_Delete a" by fastforce
  thus ?thesis using dbupdsst_no_upd[of "unlabel (duallsst (B ⋅lsst θ))" ℐ DB] in_db by simp
qed

lemma wellformed_transaction_sem_neg_checks:
  assumes T_valid: "wellformed_transaction T"
    and ℐ: "strand_sem_stateful IK DB (unlabel (duallsst (transaction_strand T ⋅lsst θ))) ℐ"
    and "NegChecks X [] [(t,u)] ∈ set (unlabel (transaction_checks T ⋅lsst θ))"
  shows "∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ (t ⋅ δ ⋅ ℐ, u ⋅ δ ⋅ ℐ) ∉ DB" (is ?A)
    and "X = [] ⟹ (t ⋅ ℐ, u ⋅ ℐ) ∉ DB" (is "?B ⟹ ?B'")
proof -
  let ?s = "NegChecks X [] [(t,u)]"
  let ?R = "transaction_receive T@transaction_checks T"
  let ?R' = "unlabel (duallsst (?R ⋅lsst θ))"
  let ?S = "λA. unlabel (duallsst (A ⋅lsst θ))"
  let ?S' = "?S (transaction_receive T)@?S (transaction_checks T)"
  let ?P = "λa. is_Receive a ∨ is_Check_or_Assignment a"
  let ?Q = "λa. is_Send a ∨ is_Check_or_Assignment a"
  let ?U = "λδ. subst_domain δ = set X ∧ ground (subst_range δ)"

  have s: "?s ∈ set (unlabel (?R ⋅lsst θ))"
    using assms(3) subst_lsst_append[of "transaction_receive T"]
          unlabel_append[of "transaction_receive T"]
    by auto

  obtain l B s where B:
      "(l,?s) = duallsstp ((l,s) ⋅lsstp θ)"
      "prefix ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ]) (?R ⋅lsst θ)"
    using s duallsst_unlabel_steps_iff(7)[of X "[]" "[(t,u)]"]
          duallsst_in_set_prefix_obtain_subst[of ?s ?R θ]
    by blast

  have 1: "unlabel (duallsst ((B ⋅lsst θ)@[(l,s) ⋅lsstp θ])) = unlabel (duallsst (B ⋅lsst θ))@[?s]"
    using B(1) unlabel_append duallsstp_subst duallsst_subst singleton_lst_proj(4)
          duallsst_subst_snoc subst_lsst_append subst_lsst_singleton
    by (metis (no_types, lifting) subst_apply_labeled_stateful_strand_step.simps)

  have "strand_sem_stateful IK DB ?S' ℐ"
    using ℐ strand_sem_append_stateful[of IK DB _ _ ℐ] transaction_dual_subst_unfold[of T θ]
    by fastforce
  hence "strand_sem_stateful IK DB (unlabel (duallsst (B ⋅lsst θ))@[?s]) ℐ"
    using B 1 strand_sem_append_stateful subst_lsst_append
    unfolding prefix_def unlabel_def duallsst_def
    by (metis (no_types) map_append)
  hence "negchecks_model ℐ (dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB) X [] [(t,u)]"
    using strand_sem_append_stateful[of IK DB "unlabel (duallsst (B ⋅lsst θ))" "[?s]" ℐ]
    by fastforce
  hence in_db: "∀δ. ?U δ ⟶ (t ⋅ δ ⋅ ℐ, u ⋅ δ ⋅ ℐ) ∉ dbupdsst (unlabel (duallsst (B ⋅lsst θ))) ℐ DB"
    unfolding negchecks_model_def
    by simp

  have "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ?Q a"
  proof
    fix a assume a: "a ∈ set (unlabel (duallsst (B ⋅lsst θ)))"

    have "?P a" when a: "a ∈ set (unlabel ?R)" for a
      using a wellformed_transaction_unlabel_cases(1,2,3)[OF T_valid]
      unfolding unlabel_def by fastforce
    hence "?P a" when a: "a ∈ set (unlabel (?R ⋅lsst θ))" for a
      using a stateful_strand_step_cases_subst(2,11)[of _ θ] subst_lsst_unlabel[of ?R θ]
      unfolding subst_apply_stateful_strand_def by auto
    hence B_P: "∀a ∈ set (unlabel (B ⋅lsst θ)). ?P a"
      using unlabel_mono[OF set_mono_prefix[OF append_prefixD[OF B(2)]]]
      by blast

    obtain l where "(l,a) ∈ set (duallsst (B ⋅lsst θ))"
      using a by (meson unlabel_mem_has_label)
    then obtain b where b: "(l,b) ∈ set (B ⋅lsst θ)" "duallsstp (l,b) = (l,a)"
      using duallsst_memberD by blast
    hence "?P b" using B_P unfolding unlabel_def by fastforce
    thus "?Q a" using duallsstp_inv[OF b(2)] by (cases b) auto
  qed
  hence "∀a ∈ set (unlabel (duallsst (B ⋅lsst θ))). ¬is_Insert a ∧ ¬is_Delete a" by fastforce
  thus ?A using dbupdsst_no_upd[of "unlabel (duallsst (B ⋅lsst θ))" ℐ DB] in_db by simp
  moreover have "δ = Var" "t ⋅ δ = t"
    when "subst_domain δ = set []" for t and δ::"('fun, 'atom, 'sets, 'lbl) prot_subst"
    using that by auto
  moreover have "subst_domain Var = set []" "range_vars Var = {}"
    by simp_all
  ultimately show "?B ⟹ ?B'" unfolding range_vars_alt_def by metis
qed

lemma dual_transaction_ik_is_transaction_send'':
  fixes δ ℐ::"('a,'b,'c,'d) prot_subst"
  assumes "wellformed_transaction T"
  shows "(iksst (unlabel (duallsst (transaction_strand T ⋅lsst δ))) ⋅set ℐ) ⋅αset a =
         (trmssst (unlabel (transaction_send T)) ⋅set δ ⋅set ℐ) ⋅αset a" (is "?A = ?B")
using dual_transaction_ik_is_transaction_send[OF assms]
      subst_lsst_unlabel[of "duallsst (transaction_strand T)" δ]
      iksst_subst[of "unlabel (duallsst (transaction_strand T))" δ]
      duallsst_subst[of "transaction_strand T" δ]
by (auto simp add: abs_apply_terms_def)

lemma while_prot_terms_fun_mono:
  "mono (λM'. M ∪ ⋃(subterms ` M') ∪ ⋃((set ∘ fst ∘ Ana) ` M'))"
unfolding mono_def by fast

lemma while_prot_terms_SMP_overapprox:
  fixes M::"('fun,'atom,'sets,'lbl) prot_terms"
  assumes N_supset: "M ∪ ⋃(subterms ` N) ∪ ⋃((set ∘ fst ∘ Ana) ` N) ⊆ N"
    and Value_vars_only: "∀x ∈ fvset N. Γv x = TAtom Value"
  shows "SMP M ⊆ {a ⋅ δ | a δ. a ∈ N ∧ wtsubst δ ∧ wftrms (subst_range δ)}"
proof -
  define f where "f ≡ λM'. M ∪ ⋃(subterms ` M') ∪ ⋃((set ∘ fst ∘ Ana) ` M')"
  define S where "S ≡ {a ⋅ δ | a δ. a ∈ N ∧ wtsubst δ ∧ wftrms (subst_range δ)}"

  note 0 = Value_vars_only
  
  have "t ∈ S" when "t ∈ SMP M" for t
  using that
  proof (induction t rule: SMP.induct)
    case (MP t)
    hence "t ∈ N" "wtsubst Var" "wftrms (subst_range Var)" using N_supset by auto
    hence "t ⋅ Var ∈ S" unfolding S_def by blast
    thus ?case by simp
  next
    case (Subterm t t')
    then obtain δ a where a: "a ⋅ δ = t" "a ∈ N" "wtsubst δ" "wftrms (subst_range δ)"
      by (auto simp add: S_def)
    hence "∀x ∈ fv a. ∃τ. Γ (Var x) = TAtom τ" using 0 by auto
    hence *: "∀x ∈ fv a. (∃f. δ x = Fun f []) ∨ (∃y. δ x = Var y)"
      using a(3) TAtom_term_cases[OF wf_trm_subst_rangeD[OF a(4)]]
      by (metis wtsubst_def)
    obtain b where b: "b ⋅ δ = t'" "b ∈ subterms a"
      using subterms_subst_subterm[OF *, of t'] Subterm.hyps(2) a(1)
      by fast
    hence "b ∈ N" using N_supset a(2) by blast
    thus ?case using a b(1) unfolding S_def by blast
  next
    case (Substitution t θ)
    then obtain δ a where a: "a ⋅ δ = t" "a ∈ N" "wtsubst δ" "wftrms (subst_range δ)"
      by (auto simp add: S_def)
    have "wtsubst (δ ∘s θ)" "wftrms (subst_range (δ ∘s θ))"
      by (fact wt_subst_compose[OF a(3) Substitution.hyps(2)],
          fact wf_trms_subst_compose[OF a(4) Substitution.hyps(3)])
    moreover have "t ⋅ θ = a ⋅ δ ∘s θ" using a(1) subst_subst_compose[of a δ θ] by simp
    ultimately show ?case using a(2) unfolding S_def by blast
  next
    case (Ana t K T k)
    then obtain δ a where a: "a ⋅ δ = t" "a ∈ N" "wtsubst δ" "wftrms (subst_range δ)"
      by (auto simp add: S_def)
    obtain Ka Ta where a': "Ana a = (Ka,Ta)" by moura
    have *: "K = Ka ⋅list δ"
    proof (cases a)
      case (Var x)
      then obtain g U where gU: "t = Fun g U"
        using a(1) Ana.hyps(2,3) Ana_var
        by (cases t) simp_all
      have "Γ (Var x) = TAtom Value" using Var a(2) 0 by auto
      hence "Γ (Fun g U) = TAtom Value"
        using a(1,3) Var gU wt_subst_trm''[OF a(3), of a]
        by argo
      thus ?thesis using gU Fun_Value_type_inv Ana.hyps(2,3) by fastforce  
    next
      case (Fun g U) thus ?thesis using a(1) a' Ana.hyps(2) Ana_subst'[of g U] by simp
    qed
    then obtain ka where ka: "k = ka ⋅ δ" "ka ∈ set Ka" using Ana.hyps(3) by auto
    have "ka ∈ set ((fst ∘ Ana) a)" using ka(2) a' by simp
    hence "ka ∈ N" using a(2) N_supset by auto
    thus ?case using ka a(3,4) unfolding S_def by blast
  qed
  thus ?thesis unfolding S_def by blast
qed


subsection ‹Admissible Transactions›
definition admissible_transaction_checks where
  "admissible_transaction_checks T ≡
    ∀x ∈ set (unlabel (transaction_checks T)).
      (is_InSet x ⟶
          is_Var (the_elem_term x) ∧ is_Fun_Set (the_set_term x) ∧
          fst (the_Var (the_elem_term x)) = TAtom Value) ∧
      (is_NegChecks x ⟶
          bvarssstp x = [] ∧
          ((the_eqs x = [] ∧ length (the_ins x) = 1) ∨
           (the_ins x = [] ∧ length (the_eqs x) = 1))) ∧
      (is_NegChecks x ∧ the_eqs x = [] ⟶ (let h = hd (the_ins x) in
          is_Var (fst h) ∧ is_Fun_Set (snd h) ∧
          fst (the_Var (fst h)) = TAtom Value))"

definition admissible_transaction_updates where
  "admissible_transaction_updates T ≡
    ∀x ∈ set (unlabel (transaction_updates T)).
      is_Update x ∧ is_Var (the_elem_term x) ∧ is_Fun_Set (the_set_term x) ∧
      fst (the_Var (the_elem_term x)) = TAtom Value"

definition admissible_transaction_terms where
  "admissible_transaction_terms T ≡
    wftrms' arity (trmslsst (transaction_strand T)) ∧
    (∀f ∈ ⋃(funs_term ` trms_transaction T).
      ¬is_Val f ∧ ¬is_Abs f ∧ ¬is_PubConst f ∧ f ≠ Pair) ∧
    (∀r ∈ set (unlabel (transaction_strand T)).
      (∃f ∈ ⋃(funs_term ` (trmssstp r)). is_Attack f) ⟶
        is_Send r ∧ length (the_msgs r) = 1 ∧ is_Fun_Attack (hd (the_msgs r)))"

definition admissible_transaction_occurs_checks where
  "admissible_transaction_occurs_checks T ≡ (
    let occ_in = λx S. occurs (Var x) ∈ set (the_msgs (hd (unlabel S)));
        rcvs = transaction_receive T;
        snds = transaction_send T;
        frsh = transaction_fresh T;
        fvs = fv_transaction T
    in ((∃x ∈ fvs - set frsh. fst x = TAtom Value) ⟶ (
          rcvs ≠ [] ∧ is_Receive (hd (unlabel rcvs)) ∧
          (∀x ∈ fvs - set frsh. fst x = TAtom Value ⟶ occ_in x rcvs))) ∧
       (frsh ≠ [] ⟶ (
          snds ≠ [] ∧ is_Send (hd (unlabel snds)) ∧
          (∀x ∈ set frsh. occ_in x snds))) ∧
       (∀t ∈ trmslsst snds.
          OccursFact ∈ funs_term t ∨ OccursSec ∈ funs_term t ⟶
            (∃x ∈ set (transaction_fresh T). t = occurs (Var x)))
)"

definition admissible_transaction where
  "admissible_transaction T ≡ (
    wellformed_transaction T ∧
    transaction_decl T () = [] ∧
    list_all (λx. fst x = TAtom Value) (transaction_fresh T) ∧
    (∀x ∈ vars_transaction T. is_Var (fst x) ∧ (the_Var (fst x) = Value)) ∧
    bvarslsst (transaction_strand T) = {} ∧
    set (transaction_fresh T) ⊆
      fvlsst (filter (is_Insert ∘ snd) (transaction_updates T)) ∪ fvlsst (transaction_send T) ∧
    (∀x ∈ fv_transaction T - set (transaction_fresh T).
     ∀y ∈ fv_transaction T - set (transaction_fresh T).
      x ≠ y ⟶ ⟨Var x != Var y⟩ ∈ set (unlabel (transaction_checks T)) ∨
                ⟨Var y != Var x⟩ ∈ set (unlabel (transaction_checks T))) ∧
    fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T) - set (transaction_fresh T)
      ⊆ fvlsst (transaction_receive T) ∪ fvlsst (transaction_checks T) ∧
    (∀r ∈ set (unlabel (transaction_checks T)).
      is_Equality r ⟶ fv (the_rhs r) ⊆ fvlsst (transaction_receive T)) ∧
    fvlsst (transaction_checks T) ⊆
      fvlsst (transaction_receive T) ∪
      fvlsst (filter (λs. is_InSet (snd s) ∧ the_check (snd s) = Assign) (transaction_checks T)) ∧
    admissible_transaction_checks T ∧
    admissible_transaction_updates T ∧
    admissible_transaction_terms T ∧
    admissible_transaction_occurs_checks T
)"

lemma admissible_transactionE:
  assumes T: "admissible_transaction T"
  shows "transaction_decl T () = []" (is ?A)
    and "∀x ∈ set (transaction_fresh T). Γv x = TAtom Value" (is ?B)
    and "∀x ∈ varslsst (transaction_strand T). Γv x = TAtom Value" (is ?C)
    and "bvarslsst (transaction_strand T) = {}" (is ?D1)
    and "fv_transaction T ∩ bvars_transaction T = {}" (is ?D2)
    and "set (transaction_fresh T) ⊆
          fvlsst (filter (is_Insert ∘ snd) (transaction_updates T)) ∪ fvlsst (transaction_send T)"
      (is ?E)
    and "set (transaction_fresh T) ⊆ fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T)"
      (is ?F)
    and "∀x ∈ fv_transaction T - set (transaction_fresh T).
         ∀y ∈ fv_transaction T - set (transaction_fresh T).
          x ≠ y ⟶ ⟨Var x != Var y⟩ ∈ set (unlabel (transaction_checks T)) ∨
                    ⟨Var y != Var x⟩ ∈ set (unlabel (transaction_checks T))"
      (is ?G)
    and "∀x ∈ fvlsst (transaction_checks T).
          x ∈ fvlsst (transaction_receive T) ∨
          (∃t s. select⟨t,s⟩ ∈ set (unlabel (transaction_checks T)) ∧ x ∈ fv t ∪ fv s)"
      (is ?H)
    and "fvlsst (transaction_updates T) ∪ fvlsst (transaction_send T) - set (transaction_fresh T) ⊆
          fvlsst (transaction_receive T) ∪ fvlsst (transaction_checks T)"
      (is ?I)
    and "∀x ∈ set (unlabel (transaction_checks T)).
          is_Equality x ⟶ fv (the_rhs x) ⊆ fvlsst (transaction_receive T)"
      (is ?J)
    and "set (transaction_fresh T) ∩ fvlsst (transaction_receive T) = {}" (is ?K1)
    and "set (transaction_fresh T) ∩ fvlsst (transaction_checks T) = {}" (is ?K2)
    and "list_all (λx. fst x = Var Value) (transaction_fresh T)" (is ?K3)
    and "∀x ∈ vars_transaction T. ¬TAtom AttackType ⊑ Γv x" (is ?K4)
proof -
  show ?A ?D1 ?D2 ?G ?I ?J ?K3
    using T unfolding admissible_transaction_def
    by (blast, blast, blast, blast, blast, blast, blast)

  have "list_all (λx. fst x = Var Value) (transaction_fresh T)"
       "∀x∈vars_transaction T. is_Var (fst x) ∧ the_Var (fst x) = Value"
    using T unfolding admissible_transaction_def by (blast, blast)
  thus ?B ?C ?K4 using Γv_TAtom''(2) unfolding list_all_iff by (blast, force, force)

  show ?E using T unfolding admissible_transaction_def by argo
  thus ?F unfolding unlabel_def by auto

  show ?K1 ?K2
    using T unfolding admissible_transaction_def wellformed_transaction_def by (argo, argo)

  let ?selects = "filter (λs. is_InSet (snd s) ∧ the_check (snd s) = Assign) (transaction_checks T)"

  show ?H
  proof
    fix x assume "x ∈ fvlsst (transaction_checks T)"
    hence "x ∈ fvlsst (transaction_receive T) ∨ x ∈ fvlsst ?selects"
      using T unfolding admissible_transaction_def by blast
    thus "x ∈ fvlsst (transaction_receive T) ∨
          (∃t s. select⟨t,s⟩ ∈ set (unlabel (transaction_checks T)) ∧ x ∈ fv t ∪ fv s)"
    proof
      assume "x ∈ fvlsst ?selects"
      then obtain r where r: "x ∈ fvsstp r" "r ∈ set (unlabel (transaction_checks T))"
                             "is_InSet r" "the_check r = Assign"