(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2018

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      TLSExample.thy
    Author:     Andreas Viktor Hess, DTU
*)

(* Note:
   There is a minor mistake in the article; prf is applied both to a single term and to two terms.
   More specifically, the term
      finished(prf(clientFinished(prf(masterForm(PMS, R\<^sub>A, R\<^sub>B)), R\<^sub>A, R\<^sub>B), hash(HSMsgs)))
   from the article should actually have one of the parenthesis moved:
      finished(prf(clientFinished(prf(masterForm(PMS, R\<^sub>A, R\<^sub>B)), R\<^sub>A, R\<^sub>B, hash(HSMsgs))))
   so that hash(HSMsgs) is a parameter of the clientFinished function and not the prf function.
*)

section {* Theory: Proving Type-Flaw Resistance of the TLS Handshake Protocol *}
theory TLSExample
imports TypedModel "~~/src/HOL/Eisbach/Eisbach_Tools"
begin

subsection {* Alternative definition for SMP *}
context typed_model
begin
inductive_set wt_subst_closure::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms" for M where
  WtSubst: "\<lbrakk>t \<in> M; wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>; \<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)\<rbrakk> \<Longrightarrow> t \<cdot> \<delta> \<in> wt_subst_closure M"

lemma SMP_eq_subterm_wt_subst_closure:
  assumes "\<And>t K M. Ana t = (K, M) \<Longrightarrow> K \<union> M \<subset> subterms t"
  shows
  "SMP\<^sub>s\<^sub>t M = \<Union>(subterms ` wt_subst_closure M)" (is "?A M = ?B M")
  "\<And>t. t \<in> SMP\<^sub>s\<^sub>t M \<Longrightarrow> t \<in> \<Union>(subterms ` wt_subst_closure M)" (is "\<And>t. ?C t M \<Longrightarrow> ?D t M")
  "\<And>t. t \<in> \<Union>(subterms ` wt_subst_closure M) \<Longrightarrow> t \<in> SMP\<^sub>s\<^sub>t M" (is "\<And>t. ?D t M \<Longrightarrow> ?C t M")
proof -
  { fix x assume "x \<in> ?A M" hence "x \<in> ?B M"
    proof (induct x rule: SMP\<^sub>s\<^sub>t.induct)
      case (MP t)
      moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
      ultimately show ?case using WtSubst[of t M Var] unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by force
    next
      case (Subterm t t')
      then obtain s where s: "s \<in> wt_subst_closure M" "t \<sqsubseteq> s" by blast
      hence "t' \<sqsubseteq> s" by (meson Subterm.hyps(3) subterm_def subtermeq_trans)
      thus ?case using s by auto
    next
      case (Substitution t \<delta>)
      then obtain s where s: "s \<in> wt_subst_closure M" "t \<sqsubseteq> s" by blast
      then obtain s' \<theta> where \<theta>: "s' \<in> M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "s = s' \<cdot> \<theta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
        using wt_subst_closure.cases by blast
      moreover have "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<delta>) v)"
        using \<open>\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)\<close> \<open>\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)\<close> unfolding subst_compose_def
        by (simp add: wf_trm_subst) 
      ultimately have "s \<cdot> \<delta> \<in> wt_subst_closure M"
        using wt_subst_compose[OF \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>] subst_comp 
        by (metis (no_types, lifting) wt_subst_closure.simps)
      moreover have "t \<cdot> \<delta> \<sqsubseteq> s \<cdot> \<delta>" using \<open>t \<sqsubseteq> s\<close> subst_mono by auto
      ultimately show ?case by auto
    next
      case (Ana t K T t')
      hence "t' \<in> subterms t" using assms(1) by auto
      thus ?case by (meson contra_subsetD in_subterms_subset_Union Ana.hyps(2)) 
    qed
  }
  thus "\<And>t. ?C t M \<Longrightarrow> ?D t M" .
  moreover
  { fix x assume "x \<in> ?B M"
    then obtain y where "y \<in> wt_subst_closure M" "x \<sqsubseteq> y" by blast
    hence "x \<in> ?A M"
    proof (induct y rule: wt_subst_closure.induct)
      case (WtSubst t \<delta>) thus ?case
        using Substitution[OF MP[OF \<open>t \<in> M\<close>] \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>] Subterm[of "t \<cdot> \<delta>" M x]
        by (cases "x = t \<cdot> \<delta>") auto
    qed
  }
  thus "\<And>t. ?D t M \<Longrightarrow> ?C t M" .
  ultimately show "?A M = ?B M" by blast
qed

lemma SMP_D:
  assumes "t \<in> SMP\<^sub>s\<^sub>t M" and "\<And>t K M. Ana t = (K, M) \<Longrightarrow> K \<union> M \<subset> subterms t"
  obtains \<delta> s where "s \<in> M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV s" "t \<sqsubseteq> s \<cdot> \<delta>"
proof -
  obtain \<theta> s where \<theta>s: "s \<in> M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)" "t \<sqsubseteq> s \<cdot> \<theta>"
    using SMP_eq_subterm_wt_subst_closure(2)[OF assms(2,1)] wt_subst_closure.cases[of _ M]
    by moura
  
  { fix \<delta> assume \<delta>: "\<delta> = rm_vars (\<V> - FV s) \<theta>"
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV s" "s \<cdot> \<theta> = s \<cdot> \<delta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
      using rm_vars_dom[of "\<V> - FV s" \<theta>] \<theta>s(2,3)
      unfolding \<V>_def wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def wf\<^sub>t\<^sub>r\<^sub>m_def
      by (blast, simp_all add: subst_agreement)
  }
  then obtain \<delta> where \<delta>: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV s" "t \<sqsubseteq> s \<cdot> \<delta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
    using \<theta>s(4) by fastforce
  thus ?thesis by (metis that \<theta>s(1))
qed

lemma SMP_Var_subterm_type:
  assumes "Var v \<in> SMP\<^sub>s\<^sub>t M" "\<And>m. m \<in> M \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m m"
  and "\<And>t K M. Ana t = (K, M) \<Longrightarrow> K \<union> M \<subset> subterms t"
  obtains w where "w \<in> FV\<^sub>s\<^sub>e\<^sub>t M" "\<Gamma> (Var v) \<sqsubseteq> \<Gamma> (Var w)"
proof -
  obtain t \<delta> where t\<delta>: "t \<in> M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV t" "Var v \<sqsubseteq> t \<cdot> \<delta>"
    using SMP_D[OF assms(1,3)] by moura
  then obtain w where w: "w \<in> FV t" "Var v \<sqsubseteq> \<delta> w"
    by (metis (no_types, hide_lams) contra_subsetD elim_dest elim_intro'
            no_var_subterm subst_apply_img_var subst_apply_term.simps(1)
            var_not_in_subst_dom vars_iff_subterm_or_eq vars_iff_subtermeq) 
  have "\<Gamma> (Var v) \<sqsubseteq> \<Gamma> (\<delta> w)"
    using subtermeq_imp_subtermtypeeq[OF _ w(2)] assms(2)[OF t\<delta>(1)] t\<delta>(3)
    by metis
  moreover have "\<Gamma> (\<delta> w) = \<Gamma> (Var w)" using t\<delta>(2) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  ultimately show ?thesis using that t\<delta> w by auto
qed
end

context intruder_model
begin

lemma ideduct_ground:
  assumes "intruder_deduct M t" "ground M"
  shows "FV t = {}"
using assms
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K T t\<^sub>i)
  hence "FV t = {}" "t\<^sub>i \<sqsubseteq> t" using Ana_subterm[OF Decompose.hyps(2)] Decompose.hyps(4) by auto
  thus ?case using subtermeq_vars_subset by auto 
qed auto

end



subsection {* TLS example: Datatypes and functions setup *}
datatype tls_atom = PrivKey | SymKey | PubConst | Agent | Nonce

datatype tls_fun =
  clientHello | clientKeyExchange | clientFinished
| serverHello | serverCert | serverHelloDone
| finished | changeCipher | x509 | prfun | master | pmsForm
| sign | hash | crypt | pub
| pubconst tls_atom nat | privkey nat
| concat

datatype tls_var =
  T\<^sub>1 | T\<^sub>2 | R\<^sub>A | R\<^sub>B | S | Cipher | Comp | Pr\<^sub>c\<^sub>a | B | P\<^sub>B | PMS | HSMsgs | V tls_atom nat

type_synonym tls_type = "(tls_fun, tls_atom) term_type"

instance tls_atom::countable by countable_datatype
instance tls_fun::countable by countable_datatype
instance tls_var::countable by countable_datatype


instance tls_atom::finite
proof
  let ?S = "UNIV::tls_atom set"
  have "?S = {PrivKey, SymKey, PubConst, Agent, Nonce}" by (auto intro: tls_atom.exhaust)
  thus "finite ?S" by (metis finite.emptyI finite.insertI) 
qed

type_synonym tls_term = "(tls_fun, tls_var) term"
type_synonym tls_terms = "(tls_fun, tls_var) terms"

primrec arity::"tls_fun \<Rightarrow> nat" where
  "arity changeCipher = 0"
| "arity clientFinished = 4"
| "arity clientHello = 5"
| "arity clientKeyExchange = 1"
| "arity concat = 5"
| "arity crypt = 2"
| "arity finished = 1"
| "arity hash = 1"
| "arity master = 3"
| "arity pmsForm = 1"
| "arity prfun = 1"
| "arity (privkey _) = 0"
| "arity pub = 1"
| "arity (pubconst _ _) = 0"
| "arity serverCert = 1"
| "arity serverHello = 5"
| "arity serverHelloDone = 0"
| "arity sign = 2"
| "arity x509 = 2"

abbreviation \<Gamma>\<^sub>v_HSMsgs where
  "\<Gamma>\<^sub>v_HSMsgs \<equiv> TComp concat [
    TComp clientHello [TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce],
    TComp serverHello [TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce],
    TComp serverCert [TComp sign [
      TAtom PrivKey,
      TComp x509 [TAtom Agent, TComp pub [TAtom PrivKey]]]],
    TAtom PubConst,
    TComp clientKeyExchange [TComp crypt [
      TComp pub [TAtom PrivKey],
      TComp pmsForm [TAtom SymKey]]]]"

fun \<Gamma>\<^sub>v::"tls_var \<Rightarrow> tls_type" where
  "\<Gamma>\<^sub>v T\<^sub>1 = TAtom Nonce"
| "\<Gamma>\<^sub>v T\<^sub>2 = TAtom Nonce"
| "\<Gamma>\<^sub>v R\<^sub>A = TAtom Nonce"
| "\<Gamma>\<^sub>v R\<^sub>B = TAtom Nonce"
| "\<Gamma>\<^sub>v S = TAtom Nonce"
| "\<Gamma>\<^sub>v Cipher = TAtom Nonce"
| "\<Gamma>\<^sub>v Comp = TAtom Nonce"
| "\<Gamma>\<^sub>v Pr\<^sub>c\<^sub>a = TAtom PrivKey"
| "\<Gamma>\<^sub>v B = TAtom Agent"
| "\<Gamma>\<^sub>v P\<^sub>B = TComp pub [TAtom PrivKey]"
| "\<Gamma>\<^sub>v PMS = TAtom SymKey"
| "\<Gamma>\<^sub>v HSMsgs = \<Gamma>\<^sub>v_HSMsgs"
| "\<Gamma>\<^sub>v (V \<tau> _) = TAtom \<tau>"

fun \<Gamma>::"tls_term \<Rightarrow> tls_type" where
  "\<Gamma> (Var X) = \<Gamma>\<^sub>v X"
| "\<Gamma> (Fun (privkey _) _) = TAtom PrivKey"
| "\<Gamma> (Fun (pubconst \<tau> _) _) = TAtom \<tau>"
| "\<Gamma> (Fun changeCipher _) = TAtom PubConst"
| "\<Gamma> (Fun serverHelloDone _) = TAtom PubConst"
| "\<Gamma> (Fun f T) = TComp f (map \<Gamma> T)"

fun public::"tls_fun \<Rightarrow> bool" where "public f = (case f of (privkey _) \<Rightarrow> False | _ \<Rightarrow> True)"

fun Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t::"tls_term list \<Rightarrow> (tls_terms \<times> tls_terms)" where
  "Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t [Fun pub [k],m] = ({k}, {m})"
| "Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t _ = ({}, {})"

lemma Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold:
  assumes "Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t T = (K, M)"
  shows "(K = {} \<and> M = {}) \<or> (\<exists>k m. T = [Fun pub [k], m] \<and> K = {k} \<and> M = {m})"
using assms by (auto elim!: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t.elims)

fun Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n::"tls_term list \<Rightarrow> (tls_terms \<times> tls_terms)" where
  "Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n [k,m] = ({}, {m})"
| "Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n _ = ({}, {})"

lemma Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold:
  assumes "Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n T = (K, M)"
  shows "(K = {} \<and> M = {}) \<or> (\<exists>k m. T = [k,m] \<and> K = {} \<and> M = {m})"
using assms by (auto elim!: Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n.elims)

fun Ana::"tls_term \<Rightarrow> (tls_terms \<times> tls_terms)" where
  "Ana (Fun crypt T) = Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t T"
| "Ana (Fun finished T) = ({}, set T)"
| "Ana (Fun master T) = ({}, set T)"
| "Ana (Fun pmsForm T) = ({}, set T)"
| "Ana (Fun serverCert T) = ({}, set T)"
| "Ana (Fun serverHello T) = ({}, set T)"
| "Ana (Fun serverHelloDone T) = ({}, set T)"
| "Ana (Fun sign T) = Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n T"
| "Ana (Fun x509 T) = ({}, set T)"
| "Ana _ = ({}, {})"


subsection {* TLS example: Locale interpretation *}
lemma assm01: "Ana t = (K, M) \<Longrightarrow> FV\<^sub>s\<^sub>e\<^sub>t K \<subseteq> FV t"
by (induct t rule: Ana.induct) (auto dest: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold)

lemma assm02: "Ana t = (K,T) \<Longrightarrow> finite K"
by (induct t rule: Ana.induct) (auto dest: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold)

lemma assm03: "Ana t = (K,T) \<Longrightarrow> (\<And>g S'. Fun g S' \<sqsubseteq> t \<Longrightarrow> length S' = arity g)
                \<Longrightarrow> k \<in> K \<Longrightarrow> Fun f T' \<sqsubseteq> k \<Longrightarrow> length T' = arity f"
by (induct t rule: Ana.induct) (auto dest: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold)

lemma assm1: "Ana t = (K, M) \<Longrightarrow> K \<union> M \<subset> subterms t"
proof (induction t rule: Ana.induct)
  case (1 T)
  hence "K = {} \<and> M = {} \<or> (\<exists>k m. T = [Fun pub [k], m] \<and> K = {k} \<and> M = {m})"
    using Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold[of T K M] Ana.simps(1)[of T] by simp
  thus ?case
  proof
    assume "\<exists>k m. T = [Fun pub [k], m] \<and> K = {k} \<and> M = {m}"
    then obtain k m where *: "T = [Fun pub [k], m]" "K = {k}" "M = {m}" by moura
    hence "k \<sqsubset> Fun crypt T" "m \<sqsubset> Fun crypt T"
      using Fun_subterm_inside_params in_subterms_refl by fastforce+ 
    thus ?thesis using *(2,3) by fastforce
  qed auto
next
  case (8 T)
  hence "K = {} \<and> M = {} \<or> (\<exists>k m. T = [k,m] \<and> K = {} \<and> M = {m})"
    using Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold[of T K M] Ana.simps(9)[of T] by simp
  thus ?case
  proof
    assume "\<exists>k m. T = [k,m] \<and> K = {} \<and> M = {m}"
    then obtain k m where *: "T = [k, m]" "K = {}" "M = {m}" by moura
    hence "k \<sqsubset> Fun crypt T" "m \<sqsubset> Fun crypt T"
      using Fun_subterm_inside_params by fastforce+ 
    thus ?thesis using * by fastforce
  qed auto
qed auto

lemma assm2: "Ana (Fun f T) = (K, M) \<Longrightarrow> M \<subseteq> set T"
apply (induction "Fun f T" rule: Ana.induct)
by (fastforce dest!: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold)+

lemma assm3: "Ana t = (K,M) \<Longrightarrow> K \<noteq> {} \<or> M \<noteq> {} \<Longrightarrow> Ana (t \<cdot> \<delta>) = (K \<cdot>set \<delta>, M \<cdot>set \<delta>)"
apply (induction t rule: Ana.induct)
by (fastforce dest!: Ana\<^sub>c\<^sub>r\<^sub>y\<^sub>p\<^sub>t_unfold Ana\<^sub>s\<^sub>i\<^sub>g\<^sub>n_unfold)+

lemma assm4: "infinite (UNIV::tls_var set)"
proof -
  let ?\<tau> = "PubConst"
  let ?T = "(range (V ?\<tau>))::tls_var set"
  have *:
       "\<And>x y::nat. x \<in> UNIV \<Longrightarrow> y \<in> UNIV \<Longrightarrow> (V ?\<tau> x = V ?\<tau> y) = (x = y)"
       "\<And>x::nat. x \<in> UNIV \<Longrightarrow> V ?\<tau> x \<in> ?T"
       "\<And>y::tls_var. y \<in> ?T \<Longrightarrow> \<exists>x \<in> UNIV. y = V ?\<tau> x"
    by auto
  have "?T \<subseteq> (UNIV::tls_var set)" by simp
  moreover have "\<exists>f::nat \<Rightarrow> tls_var. bij_betw f UNIV ?T"
    using bij_betwI'[OF *] by blast
  hence "infinite ?T" by (metis nat_not_finite bij_betw_finite)
  ultimately show ?thesis using infinite_super by blast
qed

lemma assm5: "infinite {c. public c \<and> arity c = 0}"
proof -
  let ?\<tau> = "PubConst"
  let ?T = "(range (pubconst ?\<tau>))::tls_fun set"
  have *:
       "\<And>x y::nat. x \<in> UNIV \<Longrightarrow> y \<in> UNIV \<Longrightarrow> (pubconst ?\<tau> x = pubconst ?\<tau> y) = (x = y)"
       "\<And>x::nat. x \<in> UNIV \<Longrightarrow> pubconst ?\<tau> x \<in> ?T"
       "\<And>y::tls_fun. y \<in> ?T \<Longrightarrow> \<exists>x \<in> UNIV. y = pubconst ?\<tau> x"
    by auto
  have "?T \<subseteq> {c. public c \<and> arity c = 0}" by auto
  moreover have "\<exists>f::nat \<Rightarrow> tls_fun. bij_betw f UNIV ?T"
    using bij_betwI'[OF *] by blast
  hence "infinite ?T" by (metis nat_not_finite bij_betw_finite)
  ultimately show ?thesis using infinite_super by blast
qed

lemma assm6: "0 < arity f \<Longrightarrow> public f" by (cases f) simp_all

lemma assm7: "arity c = 0 \<Longrightarrow> \<exists>a. \<forall>X. \<Gamma> (Fun c X) = TAtom a" by (cases c) simp_all

lemma assm8: "0 < arity f \<Longrightarrow> \<Gamma> (Fun f X) = TComp f (map \<Gamma> X)" by (cases f) simp_all

lemma assm9: "infinite {c. \<Gamma> (Fun c []) = TAtom a \<and> public c}"
proof -
  let ?T = "(range (pubconst a))::tls_fun set"
  have *:
       "\<And>x y::nat. x \<in> UNIV \<Longrightarrow> y \<in> UNIV \<Longrightarrow> (pubconst a x = pubconst a y) = (x = y)"
       "\<And>x::nat. x \<in> UNIV \<Longrightarrow> pubconst a x \<in> ?T"
       "\<And>y::tls_fun. y \<in> ?T \<Longrightarrow> \<exists>x \<in> UNIV. y = pubconst a x"
    by auto
  have "?T \<subseteq> {c. \<Gamma> (Fun c []) = TAtom a \<and> public c}" by auto
  moreover have "\<exists>f::nat \<Rightarrow> tls_fun. bij_betw f UNIV ?T"
    using bij_betwI'[OF *] by blast
  hence "infinite ?T" by (metis nat_not_finite bij_betw_finite)
  ultimately show ?thesis using infinite_super by blast
qed

interpretation intruder_model arity public Ana
apply standard
by (metis assm01, metis assm02, metis assm03, rule Ana.simps(10),
    metis assm2, metis assm3, metis assm4, metis assm5, metis assm6)

lemma assm10: "TComp f T \<sqsubseteq> \<Gamma> t \<Longrightarrow> arity f > 0"
proof (induction rule: \<Gamma>.induct)
  case (1 x)
  hence "Fun f T \<sqsubseteq> \<Gamma>\<^sub>v x" by simp
  thus ?case by (induction rule: \<Gamma>\<^sub>v.induct) auto
qed auto

lemma assm11: "wf\<^sub>t\<^sub>r\<^sub>m (\<Gamma> (Var x))"
proof -
  have "wf\<^sub>t\<^sub>r\<^sub>m (\<Gamma>\<^sub>v x)" by (induction rule: \<Gamma>\<^sub>v.cases[of x]) force+
  thus ?thesis by simp
qed

interpretation typed_model arity public Ana \<Gamma>
by standard (metis assm7, metis assm8, metis assm9, metis assm10, metis assm11)


subsection {* TLS example: Proving type-flaw resistance *}
subsubsection {* Defining the over-approximation set *}
abbreviation clientHello\<^sub>t\<^sub>r\<^sub>m where
  "clientHello\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun clientHello [Var T\<^sub>1, Var R\<^sub>A, Var S, Var Cipher, Var Comp]"

abbreviation serverHello\<^sub>t\<^sub>r\<^sub>m where
  "serverHello\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun serverHello [Var T\<^sub>2, Var R\<^sub>B, Var S, Var Cipher, Var Comp]"

abbreviation serverCert\<^sub>t\<^sub>r\<^sub>m where
  "serverCert\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun serverCert [Fun sign [Var Pr\<^sub>c\<^sub>a, Fun x509 [Var B, Var P\<^sub>B]]]"

abbreviation serverHelloDone\<^sub>t\<^sub>r\<^sub>m where
  "serverHelloDone\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun serverHelloDone []"

abbreviation clientKeyExchange\<^sub>t\<^sub>r\<^sub>m where
  "clientKeyExchange\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun clientKeyExchange [Fun crypt [Var P\<^sub>B, Fun pmsForm [Var PMS]]]"

abbreviation changeCipher\<^sub>t\<^sub>r\<^sub>m where
  "changeCipher\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun changeCipher []"

abbreviation finished\<^sub>t\<^sub>r\<^sub>m where
  "finished\<^sub>t\<^sub>r\<^sub>m \<equiv> Fun finished [Fun prfun [
      Fun clientFinished [
          Fun prfun [Fun master [Var PMS, Var R\<^sub>A, Var R\<^sub>B]],
          Var R\<^sub>A, Var R\<^sub>B, Fun hash [Var HSMsgs]
      ]
  ]]"

abbreviation M\<^sub>T\<^sub>L\<^sub>S::"tls_terms" where
  "M\<^sub>T\<^sub>L\<^sub>S \<equiv> {
      clientHello\<^sub>t\<^sub>r\<^sub>m,
      serverHello\<^sub>t\<^sub>r\<^sub>m,
      serverCert\<^sub>t\<^sub>r\<^sub>m,
      serverHelloDone\<^sub>t\<^sub>r\<^sub>m,
      clientKeyExchange\<^sub>t\<^sub>r\<^sub>m,
      changeCipher\<^sub>t\<^sub>r\<^sub>m,
      finished\<^sub>t\<^sub>r\<^sub>m
}"

lemma M\<^sub>T\<^sub>L\<^sub>S_wf_trm: "m \<in> M\<^sub>T\<^sub>L\<^sub>S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m m" by (auto simp add: wf\<^sub>t\<^sub>r\<^sub>m_def)

lemma M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm: "t \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t" by (metis M\<^sub>T\<^sub>L\<^sub>S_wf_trm SMP_wf_trm)


subsubsection {* Shape predicates for the function symbols occurring in the over-approximation set *}
definition clientHello_shape where
   "clientHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<equiv> (t = Fun clientHello [t\<^sub>1,t\<^sub>2,t\<^sub>3,t\<^sub>4,t\<^sub>5]
            \<and> \<Gamma> t\<^sub>1 = TAtom Nonce \<and> \<Gamma> t\<^sub>2 = TAtom Nonce \<and> \<Gamma> t\<^sub>3 = TAtom Nonce
            \<and> \<Gamma> t\<^sub>4 = TAtom Nonce \<and> \<Gamma> t\<^sub>5 = TAtom Nonce)"
declare clientHello_shape_def[simp]

definition serverHello_shape where
   "serverHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<equiv> (t = Fun serverHello [t\<^sub>1,t\<^sub>2,t\<^sub>3,t\<^sub>4,t\<^sub>5]
            \<and> \<Gamma> t\<^sub>1 = TAtom Nonce \<and> \<Gamma> t\<^sub>2 = TAtom Nonce \<and> \<Gamma> t\<^sub>3 = TAtom Nonce
            \<and> \<Gamma> t\<^sub>4 = TAtom Nonce \<and> \<Gamma> t\<^sub>5 = TAtom Nonce)"
declare serverHello_shape_def[simp]

definition serverCert_shape where
   "serverCert_shape t t\<^sub>1 \<equiv> (t = Fun serverCert [t\<^sub>1]
            \<and> \<Gamma> t\<^sub>1 = TComp sign [TAtom PrivKey,
                                 TComp x509 [TAtom Agent, TComp pub [TAtom PrivKey]]])"
declare serverCert_shape_def[simp]

definition sign_shape where
   "sign_shape t t\<^sub>1 t\<^sub>2 \<equiv> (t = Fun sign [t\<^sub>1,t\<^sub>2] \<and> \<Gamma> t\<^sub>1 = TAtom PrivKey
            \<and> \<Gamma> t\<^sub>2 = TComp x509 [TAtom Agent, TComp pub [TAtom PrivKey]])"
declare sign_shape_def[simp]

definition x509_shape where
   "x509_shape t t\<^sub>1 t\<^sub>2 \<equiv> (t = Fun x509 [t\<^sub>1,t\<^sub>2] \<and> \<Gamma> t\<^sub>1 = TAtom Agent
            \<and> \<Gamma> t\<^sub>2 = TComp pub [TAtom PrivKey])"
declare x509_shape_def[simp]

definition pub_shape where
   "pub_shape t t\<^sub>1 \<equiv> (t = Fun pub [t\<^sub>1] \<and> \<Gamma> t\<^sub>1 = TAtom PrivKey)"
declare pub_shape_def[simp]

definition clientKeyExchange_shape where
   "clientKeyExchange_shape t t\<^sub>1 \<equiv> (t = Fun clientKeyExchange [t\<^sub>1]
            \<and> \<Gamma> t\<^sub>1 = TComp crypt [TComp pub [TAtom PrivKey], TComp pmsForm [TAtom SymKey]])"
declare clientKeyExchange_shape_def[simp]

definition crypt_shape where
   "crypt_shape t t\<^sub>1 t\<^sub>2 \<equiv> (t = Fun crypt [t\<^sub>1,t\<^sub>2] \<and> \<Gamma> t\<^sub>1 = TComp pub [TAtom PrivKey]
            \<and> \<Gamma> t\<^sub>2 = TComp pmsForm [TAtom SymKey])"
declare crypt_shape_def[simp]

definition pmsForm_shape where
   "pmsForm_shape t t\<^sub>1 \<equiv> (t = Fun pmsForm [t\<^sub>1] \<and> \<Gamma> t\<^sub>1 = TAtom SymKey)"
declare pmsForm_shape_def[simp]

definition finished_shape where
   "finished_shape t t\<^sub>1 \<equiv> (t = Fun finished [t\<^sub>1]
            \<and> \<Gamma> t\<^sub>1 = TComp prfun [
                TComp clientFinished [
                  TComp prfun [TComp master [TAtom SymKey, TAtom Nonce, TAtom Nonce]],
                  TAtom Nonce, TAtom Nonce, TComp hash [\<Gamma>\<^sub>v_HSMsgs]
            ]])"
declare finished_shape_def[simp]

definition prf_shape1 where
   "prf_shape1 t t\<^sub>1 \<equiv> (t = Fun prfun [t\<^sub>1]
            \<and> \<Gamma> t\<^sub>1 = TComp clientFinished [
                TComp prfun [TComp master [TAtom SymKey, TAtom Nonce, TAtom Nonce]],
                TAtom Nonce, TAtom Nonce, TComp hash [\<Gamma>\<^sub>v_HSMsgs]])"
declare prf_shape1_def[simp]

definition prf_shape2 where
   "prf_shape2 t t\<^sub>1 \<equiv> (t = Fun prfun [t\<^sub>1]
            \<and> \<Gamma> t\<^sub>1 = TComp master [TAtom SymKey, TAtom Nonce, TAtom Nonce])"
declare prf_shape2_def[simp]

definition clientFinished_shape where
   "clientFinished_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 \<equiv> (t = Fun clientFinished [t\<^sub>1,t\<^sub>2,t\<^sub>3,t\<^sub>4]
            \<and> \<Gamma> t\<^sub>1 = TComp prfun [TComp master [TAtom SymKey, TAtom Nonce, TAtom Nonce]]
            \<and> \<Gamma> t\<^sub>2 = TAtom Nonce \<and> \<Gamma> t\<^sub>3 = TAtom Nonce \<and> \<Gamma> t\<^sub>4 = TComp hash [\<Gamma>\<^sub>v_HSMsgs])"
declare clientFinished_shape_def[simp]

definition master_shape where
   "master_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 \<equiv> (t = Fun master [t\<^sub>1,t\<^sub>2,t\<^sub>3] \<and> \<Gamma> t\<^sub>1 = TAtom SymKey
            \<and> \<Gamma> t\<^sub>2 = TAtom Nonce \<and> \<Gamma> t\<^sub>3 = TAtom Nonce)"
declare master_shape_def[simp]

definition hash_shape where
   "hash_shape t t\<^sub>1 \<equiv> (t = Fun hash [t\<^sub>1] \<and> \<Gamma> t\<^sub>1 = \<Gamma>\<^sub>v_HSMsgs)"
declare hash_shape_def[simp]

definition concat_shape where
   "concat_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<equiv> (t = Fun concat [t\<^sub>1,t\<^sub>2,t\<^sub>3,t\<^sub>4,t\<^sub>5]
            \<and> \<Gamma> t\<^sub>1 = TComp clientHello [TAtom Nonce, TAtom Nonce, TAtom Nonce,
                                        TAtom Nonce, TAtom Nonce]
            \<and> \<Gamma> t\<^sub>2 = TComp serverHello [TAtom Nonce, TAtom Nonce, TAtom Nonce,
                                        TAtom Nonce, TAtom Nonce]
            \<and> \<Gamma> t\<^sub>3 = TComp serverCert [TComp sign [TAtom PrivKey,
                                       TComp x509 [TAtom Agent, TComp pub [TAtom PrivKey]]]]
            \<and> \<Gamma> t\<^sub>4 = TAtom PubConst
            \<and> \<Gamma> t\<^sub>5 = TComp clientKeyExchange [TComp crypt [TComp pub [TAtom PrivKey],
                                              TComp pmsForm [TAtom SymKey]]])"
declare concat_shape_def[simp]

lemmas all_shape_defs =
  clientHello_shape_def serverHello_shape_def serverCert_shape_def sign_shape_def x509_shape_def
  pub_shape_def clientKeyExchange_shape_def crypt_shape_def pmsForm_shape_def finished_shape_def
  prf_shape1_def clientFinished_shape_def prf_shape2_def master_shape_def hash_shape_def
  concat_shape_def

definition M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes where
  "M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t \<equiv> (\<exists>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5. clientHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5. serverHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5) \<or>
         (\<exists>t\<^sub>1. serverCert_shape t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2. sign_shape t t\<^sub>1 t\<^sub>2) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2. x509_shape t t\<^sub>1 t\<^sub>2) \<or>
         (\<exists>t\<^sub>1. pub_shape t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1. clientKeyExchange_shape t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2. crypt_shape t t\<^sub>1 t\<^sub>2) \<or>
         (\<exists>t\<^sub>1. pmsForm_shape t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1. finished_shape t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1. prf_shape1 t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4. clientFinished_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4) \<or>
         (\<exists>t\<^sub>1. prf_shape2 t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2 t\<^sub>3. master_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3) \<or>
         (\<exists>t\<^sub>1. hash_shape t t\<^sub>1) \<or>
         (\<exists>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5. concat_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5)"

lemma M\<^sub>T\<^sub>L\<^sub>S_SMP_shapesI:
  shows "clientHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "serverHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "serverCert_shape t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "sign_shape t t\<^sub>1 t\<^sub>2 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "x509_shape t t\<^sub>1 t\<^sub>2 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "pub_shape t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "clientKeyExchange_shape t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "crypt_shape t t\<^sub>1 t\<^sub>2 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "pmsForm_shape t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "finished_shape t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "prf_shape1 t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "clientFinished_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "prf_shape2 t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "master_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "hash_shape t t\<^sub>1 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
        "concat_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<Longrightarrow> M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
unfolding M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_def by auto

lemma M\<^sub>T\<^sub>L\<^sub>S_member_cases[consumes 1]:
  assumes "t \<in> M\<^sub>T\<^sub>L\<^sub>S"
  and "t = clientHello\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  and "t = serverHello\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  and "t = serverCert\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  and "t = serverHelloDone\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  and "t = clientKeyExchange\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  and "t = changeCipher\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  and "t = finished\<^sub>t\<^sub>r\<^sub>m \<Longrightarrow> P"
  shows "P"
using assms by blast

lemma M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_cases[
    case_names clientHello serverHello serverCert sign x509 pub clientKeyExchange crypt pmsForm
               finished prf1 clientFinished prf2 master hash concat,
    consumes 1]:
  assumes "M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes t"
  and "\<And>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5. clientHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5. serverHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. serverCert_shape t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2. sign_shape t t\<^sub>1 t\<^sub>2 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2. x509_shape t t\<^sub>1 t\<^sub>2 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. pub_shape t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. clientKeyExchange_shape t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2. crypt_shape t t\<^sub>1 t\<^sub>2 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. pmsForm_shape t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. finished_shape t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. prf_shape1 t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4. clientFinished_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. prf_shape2 t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2 t\<^sub>3. master_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 \<Longrightarrow> P"
  and "\<And>t\<^sub>1. hash_shape t t\<^sub>1 \<Longrightarrow> P"
  and "\<And>t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5. concat_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5 \<Longrightarrow> P"
  shows "P"
using assms unfolding M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_def by auto


subsubsection {* Custom proof methods for better proof automation *}
method params_shape_subst uses shape wf =
  (match shape in "?t = Fun ?f ?T" \<Rightarrow> \<open>succeed\<close>)
| (match shape in I: "?Q \<and> \<Gamma> s = TComp ?g ?S" for s
   \<Rightarrow> \<open>insert TComp_term_cases[OF wf_trm_subtermeq, of _ s, OF wf _ conjunct2[OF I]]\<close>)
| (match shape in I: "?Q \<and> \<Gamma> s = TComp ?g ?S \<and> ?P" for s
   \<Rightarrow> \<open>insert TComp_term_cases[OF wf_trm_subtermeq, of _ s, OF wf _ conjunct1[OF conjunct2[OF I]]];
       params_shape_subst wf: wf shape: conjI[OF conjunct1[OF I] conjunct2[OF conjunct2[OF I]]]\<close>)
| (match shape in I: "?Q \<and> \<Gamma> s = TAtom \<tau>" for s \<tau>
   \<Rightarrow> \<open>insert TAtom_term_cases[OF wf_trm_subtermeq[OF wf] conjunct2[OF I]]\<close>)
| (match shape in I: "?Q \<and> \<Gamma> s = TAtom \<tau> \<and> ?P" for s \<tau>
   \<Rightarrow> \<open>insert TAtom_term_cases[OF wf_trm_subtermeq[OF wf] conjunct1[OF conjunct2[OF I]]];
       params_shape_subst wf: wf shape: conjI[OF conjunct1[OF I] conjunct2[OF conjunct2[OF I]]]\<close>)
| (params_shape_subst wf: wf shape: conjunct2[OF shape])

method params_shape_solve uses shape wf =
  (params_shape_subst wf: wf shape: shape, auto simp add: shape)

method subterms_shape_solve_single
  for s t::tls_term uses shape param_shapes wf subterm_shapes
= (match shape[unfolded all_shape_defs] in "?t = Fun f T \<and> ?P" for f and T::"tls_term list" \<Rightarrow>
    \<open>insert shape[unfolded all_shape_defs] wf_trm_subterm[OF wf]
            param_shapes[OF wf shape] subterm_shapes,
     metis (full_types) subtermI'[of t T f] subtermeq_Var_const[of s t] insertCI list.simps(15)\<close>)

method subterms_shape_solve_single2
  for s t::tls_term and T::"tls_term list" and f::tls_fun
= (cases "s \<sqsubseteq> t",
   metis (full_types) subtermI'[of t T f] subtermeq_Var_const[of s t] insertCI list.simps(15))

method subterms_shape_solve_aux
  for s::tls_term and T::"tls_term list" and f::tls_fun
  uses shape_rest
= (match shape_rest in "\<Gamma> t = ?\<tau>" for t \<Rightarrow>
    \<open>subterms_shape_solve_single2 s t T f\<close>)
| (match shape_rest in I: "\<Gamma> t = ?\<tau> \<and> ?P" for t \<Rightarrow>
    \<open>subterms_shape_solve_single2 s t T f,
     subterms_shape_solve_aux s T f shape_rest: conjunct2[OF I]\<close>)

method subterms_shape_solve
  for s::tls_term uses shape param_shapes wf subterm_shapes subterm
= (match shape[unfolded all_shape_defs] in I: "?t = Fun f T \<and> ?P" for f and T::"tls_term list" \<Rightarrow>
    \<open>insert shape[unfolded all_shape_defs] wf_trm_subterm[OF wf]
            param_shapes[OF wf shape] subterm_shapes,
     subterms_shape_solve_aux s T f shape_rest: conjunct2[OF I],
     insert subterm, clarsimp\<close>)



subsubsection {* Characterizing the parameters of each shape *}
lemma clientHello_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "clientHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
  shows "((\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>f. t\<^sub>1 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>2 = Var v) \<or> (\<exists>f. t\<^sub>2 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>3 = Var v) \<or> (\<exists>f. t\<^sub>3 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>4 = Var v) \<or> (\<exists>f. t\<^sub>4 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>5 = Var v) \<or> (\<exists>f. t\<^sub>5 = Fun f []))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma serverHello_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "serverHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
  shows "((\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>f. t\<^sub>1 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>2 = Var v) \<or> (\<exists>f. t\<^sub>2 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>3 = Var v) \<or> (\<exists>f. t\<^sub>3 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>4 = Var v) \<or> (\<exists>f. t\<^sub>4 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>5 = Var v) \<or> (\<exists>f. t\<^sub>5 = Fun f []))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma serverCert_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "serverCert_shape t s"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2)"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma sign_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "sign_shape t s\<^sub>1 s\<^sub>2"
  shows "((\<exists>v. s\<^sub>1 = Var v) \<or> (\<exists>f. s\<^sub>1 = Fun f []))
        \<and> ((\<exists>v. s\<^sub>2 = Var v) \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s\<^sub>2 u\<^sub>1 u\<^sub>2))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma x509_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "x509_shape t s\<^sub>1 s\<^sub>2"
  shows "((\<exists>v. s\<^sub>1 = Var v) \<or> (\<exists>f. s\<^sub>1 = Fun f []))
        \<and> ((\<exists>v. s\<^sub>2 = Var v) \<or> (\<exists>u. pub_shape s\<^sub>2 u))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma pub_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "pub_shape t s"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma pmsForm_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "pmsForm_shape t s"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma crypt_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "crypt_shape t s\<^sub>1 s\<^sub>2"
  shows "((\<exists>v. s\<^sub>1 = Var v) \<or> (\<exists>u. pub_shape s\<^sub>1 u))
        \<and> ((\<exists>v. s\<^sub>2 = Var v) \<or> (\<exists>u. pmsForm_shape s\<^sub>2 u))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma clientKeyExchange_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "clientKeyExchange_shape t s"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2)"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma master_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "master_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3"
  shows "((\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>f. t\<^sub>1 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>2 = Var v) \<or> (\<exists>f. t\<^sub>2 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>3 = Var v) \<or> (\<exists>f. t\<^sub>3 = Fun f []))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma prf_params_shape2:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "prf_shape2 t t\<^sub>1"
  shows "((\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3. master_shape t\<^sub>1 s\<^sub>1 s\<^sub>2 s\<^sub>3))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma concat_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "concat_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
  shows "((\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. clientHello_shape t\<^sub>1 s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5))
        \<and> ((\<exists>v. t\<^sub>2 = Var v) \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. serverHello_shape t\<^sub>2 s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5))
        \<and> ((\<exists>v. t\<^sub>3 = Var v) \<or> (\<exists>s\<^sub>1. serverCert_shape t\<^sub>3 s\<^sub>1))
        \<and> ((\<exists>v. t\<^sub>4 = Var v) \<or> (\<exists>f. t\<^sub>4 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>5 = Var v) \<or> (\<exists>s\<^sub>1. clientKeyExchange_shape t\<^sub>5 s\<^sub>1))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma hash_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "hash_shape t s"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5. concat_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5)"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma clientFinished_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "clientFinished_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4"
  shows "((\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>s\<^sub>1. prf_shape2 t\<^sub>1 s\<^sub>1)) 
        \<and> ((\<exists>v. t\<^sub>2 = Var v) \<or> (\<exists>f. t\<^sub>2 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>3 = Var v) \<or> (\<exists>f. t\<^sub>3 = Fun f []))
        \<and> ((\<exists>v. t\<^sub>4 = Var v) \<or> (\<exists>s\<^sub>1. hash_shape t\<^sub>4 s\<^sub>1))"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma prf_params_shape1:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "prf_shape1 t t\<^sub>1"
  shows "(\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4. clientFinished_shape t\<^sub>1 s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4)"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])

lemma finished_params_shape:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "finished_shape t t\<^sub>1"
  shows "(\<exists>v. t\<^sub>1 = Var v) \<or> (\<exists>s\<^sub>1. prf_shape1 t\<^sub>1 s\<^sub>1)"
by (params_shape_solve wf: assms(1) shape: assms(2)[unfolded all_shape_defs])


subsubsection {* Characterizing the subterms of each shape *}
lemma clientHello_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "clientHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> clientHello_shape s t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: clientHello_params_shape)

lemma serverHello_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "serverHello_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> serverHello_shape s t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: serverHello_params_shape)

lemma pub_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "pub_shape t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> pub_shape s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: pub_params_shape)

lemma x509_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "x509_shape t t\<^sub>1 t\<^sub>2"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> (\<exists>u. pub_shape s u) \<or> x509_shape s t\<^sub>1 t\<^sub>2"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: x509_params_shape
      subterm_shapes: pub_subterms_shape[of _ s])

lemma sign_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "sign_shape t t\<^sub>1 t\<^sub>2"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> (\<exists>u. pub_shape s u) \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2)
        \<or> sign_shape s t\<^sub>1 t\<^sub>2"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: sign_params_shape
      subterm_shapes: x509_subterms_shape[of _ s] pub_subterms_shape[of _ s])

lemma serverCert_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "serverCert_shape t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2) \<or> (\<exists>u. pub_shape s u) \<or> serverCert_shape s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: serverCert_params_shape
      subterm_shapes: x509_subterms_shape[of _ s] pub_subterms_shape[of _ s]
                      sign_subterms_shape[of _ s])

lemma pmsForm_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "pmsForm_shape t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> pmsForm_shape s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: pmsForm_params_shape)

lemma crypt_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "crypt_shape t t\<^sub>1 t\<^sub>2"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> (\<exists>u. pub_shape s u) \<or> (\<exists>u. pmsForm_shape s u)
        \<or> crypt_shape s t\<^sub>1 t\<^sub>2"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: crypt_params_shape
      subterm_shapes: pub_subterms_shape[of _ s] pmsForm_subterms_shape[of _ s])

lemma clientKeyExchange_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "clientKeyExchange_shape t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pub_shape s u) \<or> (\<exists>u. pmsForm_shape s u) \<or> clientKeyExchange_shape s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: clientKeyExchange_params_shape
      subterm_shapes: crypt_subterms_shape[of _ s] pub_subterms_shape[of _ s]
                      pmsForm_subterms_shape[of _ s])

lemma master_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "master_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f []) \<or> master_shape s t\<^sub>1 t\<^sub>2 t\<^sub>3"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2) param_shapes: master_params_shape)

lemma prf_subterms_shape2:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "prf_shape2 t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3. master_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3) \<or> prf_shape2 s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: prf_params_shape2
      subterm_shapes: master_subterms_shape[of _ s])

lemma concat_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "concat_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. clientHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. serverHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1. serverCert_shape s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. clientKeyExchange_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2) \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2) \<or> (\<exists>u. pub_shape s u)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2) \<or> (\<exists>u. pmsForm_shape s u)
        \<or> concat_shape s t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4 t\<^sub>5"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: concat_params_shape
      subterm_shapes: clientHello_subterms_shape[of _ s] clientKeyExchange_subterms_shape[of _ s]
                      serverCert_subterms_shape[of _ s] serverHello_subterms_shape[of _ s])

lemma hash_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "hash_shape t t\<^sub>1"
  shows "(\<exists>v. s = Var v)
        \<or> (\<exists>f. s = Fun f [])
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. clientHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. serverHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1. serverCert_shape s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. clientKeyExchange_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pub_shape s u) \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2) \<or> (\<exists>u. pmsForm_shape s u)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5. concat_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5) \<or> hash_shape s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: hash_params_shape
      subterm_shapes: concat_subterms_shape[of _ s])

lemma clientFinished_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "clientFinished_shape t t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])
        \<or> (\<exists>s\<^sub>1. prf_shape2 s s\<^sub>1) \<or> (\<exists>s\<^sub>1. hash_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3. master_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. clientHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. serverHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1. serverCert_shape s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. clientKeyExchange_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pub_shape s u)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pmsForm_shape s u) \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5. concat_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5)
        \<or> clientFinished_shape s t\<^sub>1 t\<^sub>2 t\<^sub>3 t\<^sub>4"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: clientFinished_params_shape
      subterm_shapes: prf_subterms_shape2[of _ s] hash_subterms_shape[of _ s])

lemma prf_subterms_shape1:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "prf_shape1 t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])
        \<or> (\<exists>s\<^sub>1. prf_shape2 s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. hash_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3. master_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. clientHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. serverHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1. serverCert_shape s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. clientKeyExchange_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pub_shape s u)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pmsForm_shape s u) \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5. concat_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4. clientFinished_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4)
        \<or> prf_shape1 s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: prf_params_shape1
      subterm_shapes: clientFinished_subterms_shape[of _ s])

lemma finished_subterms_shape:
  assumes a: "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t" "finished_shape t t\<^sub>1"
  shows "(\<exists>v. s = Var v) \<or> (\<exists>f. s = Fun f [])
        \<or> (\<exists>s\<^sub>1. prf_shape1 s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. prf_shape2 s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4. clientFinished_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4)
        \<or> (\<exists>s\<^sub>1. hash_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3. master_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. clientHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5. serverHello_shape s s\<^sub>1 s\<^sub>2 s\<^sub>3 s\<^sub>4 s\<^sub>5)
        \<or> (\<exists>s\<^sub>1. serverCert_shape s s\<^sub>1)
        \<or> (\<exists>s\<^sub>1. clientKeyExchange_shape s s\<^sub>1)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. sign_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. x509_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pub_shape s u)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2. crypt_shape s u\<^sub>1 u\<^sub>2)
        \<or> (\<exists>u. pmsForm_shape s u)
        \<or> (\<exists>u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5. concat_shape s u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4 u\<^sub>5)
        \<or> finished_shape s t\<^sub>1"
by (subterms_shape_solve s shape: a(3) wf: a(1) subterm: a(2)
      param_shapes: finished_params_shape
      subterm_shapes: prf_subterms_shape1[of _ s])


subsubsection {* The sub-message patterns satisfy the shapes-predicate *}
lemma M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes:
  assumes "Fun f T \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "\<Gamma> (Fun f T) = TComp f (map \<Gamma> T)"
  shows "M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes (Fun f T)"
proof -
  obtain s \<delta> where s\<delta>: "s \<in> M\<^sub>T\<^sub>L\<^sub>S" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)" "Fun f T \<sqsubseteq> s \<cdot> \<delta>"
    by (metis SMP_D[OF assms(1) assm1])
  hence len: "length T > 0" and wf: "wf\<^sub>t\<^sub>r\<^sub>m (s \<cdot> \<delta>)"
    using M\<^sub>T\<^sub>L\<^sub>S_wf_trm[OF s\<delta>(1)] M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm[OF assms(1)]
          wf_trm_subst[OF s\<delta>(3), of s]
          fun_type_inv[OF assms(2)] fun_type_inv_wf[OF assms(2)]
    by auto

  from s\<delta>(1) have "M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes (s \<cdot> \<delta>)"
    using s\<delta>(2,4) \<Gamma>\<^sub>v.simps assms(2) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
    by (induct rule: M\<^sub>T\<^sub>L\<^sub>S_member_cases) (auto intro: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapesI[unfolded all_shape_defs])
  thus ?thesis
    using s\<delta>(1) (* Needed for the cases that cannot occur *)
    using len (* Needed for all the other cases *)
    using clientHello_subterms_shape[OF wf s\<delta>(4)] (* Subterm lemmas for the cases that can occur *)
          serverHello_subterms_shape[OF wf s\<delta>(4)]
          serverCert_subterms_shape[OF wf s\<delta>(4)]
          clientKeyExchange_subterms_shape[OF wf s\<delta>(4)]
          finished_subterms_shape[OF wf s\<delta>(4)] 
  by (induct rule: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_cases) (fastforce simp add: len intro: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapesI)+
qed


subsubsection {* Sub-message patterns with the same outermost function symbol
  (just prf in this example) are only unifiable if they have the same type *}
lemma prf_subterm_only: "prfun \<notin> \<Union>(funs_term ` \<Gamma>\<^sub>v ` FV\<^sub>s\<^sub>e\<^sub>t M\<^sub>T\<^sub>L\<^sub>S)"
by auto

lemma prf_nonvar_params:
  assumes "t \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "prf_shape1 t t\<^sub>1 \<or> prf_shape2 t t\<^sub>1"
  shows "is_Fun t\<^sub>1"
proof -
  { fix t assume "t \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" hence "\<not>(\<exists>v. Fun prfun [Var v] \<sqsubseteq> t)"
    proof (induction t rule: SMP\<^sub>s\<^sub>t.induct)
      case (MP t) thus ?case by auto
    next
      case (Subterm t s)
      { fix v assume "Fun prfun [Var v] \<sqsubseteq> s" hence "Fun prfun [Var v] \<sqsubseteq> t"
          using subtermeq_subterm_trans[OF _ \<open>s \<sqsubset> t\<close>] unfolding subterm_def by metis
      }
      thus ?case using Subterm.IH by blast
    next
      case (Substitution t \<delta>) thus ?case
      proof (induction t rule: term.induct)
        case (Var v)
        have "\<exists>w. w \<in> FV\<^sub>s\<^sub>e\<^sub>t M\<^sub>T\<^sub>L\<^sub>S \<and> \<Gamma> (Var v) \<sqsubseteq> \<Gamma> (Var w)"
          using SMP_Var_subterm_type[OF \<open>Var v \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S\<close> M\<^sub>T\<^sub>L\<^sub>S_wf_trm assm1] by metis
        hence "\<exists>w. w \<in> FV\<^sub>s\<^sub>e\<^sub>t M\<^sub>T\<^sub>L\<^sub>S \<and> \<Gamma> (\<delta> v) \<sqsubseteq> \<Gamma> (Var w)"
          using wt_subst_trm[of "Var v" \<delta>] \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def FV\<^sub>s\<^sub>e\<^sub>t_def
          by metis
        then obtain w' where w': "w' \<in> FV\<^sub>s\<^sub>e\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "funs_term (\<Gamma> (\<delta> v)) \<subseteq> funs_term (\<Gamma> (Var w'))"
          using wt_subst_trm subtermeq_imp_funs_term_subset[of "\<Gamma> (\<delta> v)"] by blast
    
        { fix w assume w: "Fun prfun [Var w] \<sqsubseteq> \<delta> v"
          { fix f T assume "Fun f T \<sqsubseteq> Fun prfun [Var w]"
            hence "Fun f T = Fun prfun [Var w]" "length T = arity prfun" by auto
          }
          hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun prfun [Var w])" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
          hence "\<Gamma> (Fun prfun [Var w]) = TComp prfun (map \<Gamma> [Var w])" by auto
          hence "prfun \<in> funs_term (\<Gamma> (\<delta> v))"
            using subterm_funs_term_in_type[OF _ w] Var.prems(3) by metis
          hence False using prf_subterm_only w'(1) w'(2) by auto
        }
        thus ?case by auto
      next
        case (Fun f T)
        have "\<And>x. x \<in> set T \<Longrightarrow> x \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" using SMP\<^sub>s\<^sub>t.Subterm[OF Fun.prems(1)] by blast
        moreover have "\<And>x. x \<in> set T \<Longrightarrow> \<not>(\<exists>v. Fun prfun [Var v] \<sqsubseteq> x)" using Fun.prems(4) by auto
        ultimately have "\<And>x. x \<in> set T \<Longrightarrow> \<not>(\<exists>v. Fun prfun [Var v] \<sqsubseteq> x \<cdot> \<delta>)"
          by (metis Fun.IH Fun.prems(2,3))
        moreover { fix v assume v: "Fun prfun [Var v] = Fun f T \<cdot> \<delta>"
          then obtain x where x: "Fun f T = Fun prfun [x]" by auto
          hence x\<delta>: "x \<cdot> \<delta> = Var v" using v by fastforce
          then obtain w where "x = Var w" by (cases x) auto
          hence False using Fun.prems(4) v x x\<delta> by fastforce
        }
        hence "\<not>(\<exists>v. Fun prfun [Var v] = Fun f T \<cdot> \<delta>)" by metis
        ultimately show ?case by auto
      qed
    next
      case (Ana t K M s)
      have "s \<sqsubseteq> t" using assm1[OF Ana.hyps(2)] Ana.hyps(3) by blast
      { fix v assume "Fun prfun [Var v] \<sqsubseteq> s" hence "Fun prfun [Var v] \<sqsubseteq> t"
          using subtermeq_trans[OF _ \<open>s \<sqsubseteq> t\<close>] unfolding subterm_def by metis
      }
      thus ?case using Ana.IH by blast
    qed
  }
  thus ?thesis using assms unfolding prf_shape1_def prf_shape2_def by blast
qed

lemma prf_SMP_wt_unif:
  assumes "Fun f T \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "Fun f' T' \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S"
          "f = prfun" "f' = prfun"
          "Unifier \<delta> (Fun f T) (Fun f' T')"
  shows "\<Gamma> (Fun f T) = \<Gamma> (Fun f' T')"
proof -
  from assms have in_SMP: "Fun f T \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "Fun f' T' \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S"
    and types: "\<Gamma> (Fun f T) = TComp f (map \<Gamma> T)" "\<Gamma> (Fun f' T') = TComp f' (map \<Gamma> T')"
    by auto

  have S: "\<exists>S. prf_shape1 (Fun f T) (Fun clientFinished S)
              \<or> prf_shape2 (Fun f T) (Fun master S)"
  using M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes[OF in_SMP(1) types(1)]
  proof (induct rule: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_cases)
    case prf1 thus ?case
      using prf_nonvar_params[OF assms(1)] assms(3) prf_params_shape1
      unfolding prf_shape1_def prf_shape2_def clientFinished_shape_def
      by (metis M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm in_SMP(1) is_VarI)
  next
    case prf2 thus ?case
      using prf_nonvar_params[OF assms(1)] assms(3) prf_params_shape2
      unfolding prf_shape1_def prf_shape2_def master_shape_def
      by (metis M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm in_SMP(1) is_VarI)
  qed (simp_all add: assms)

  have S': "\<exists>S'. prf_shape1 (Fun prfun T') (Fun clientFinished S')
                \<or> prf_shape2 (Fun prfun T') (Fun master S')"
  using M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes[OF in_SMP(2) types(2)]
  proof (induct rule: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_cases)
    case prf1 thus ?case
      using prf_nonvar_params[OF assms(2)] assms(4) prf_params_shape1
      unfolding prf_shape1_def prf_shape2_def clientFinished_shape_def
      by (metis M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm in_SMP(2) is_VarI)
  next
    case prf2 thus ?case
      using prf_nonvar_params[OF assms(2)] assms(4) prf_params_shape2
      unfolding prf_shape1_def prf_shape2_def master_shape_def
      by (metis M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm in_SMP(2) is_VarI)
  qed (simp_all add: assms)

  show ?thesis using assms S S' by auto
qed


subsubsection {* Theorem: The over-approximation set is type-flaw resistant *}
theorem M\<^sub>T\<^sub>L\<^sub>S_tfr: "tfr\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S"
proof
  show "\<forall>x \<in> M\<^sub>T\<^sub>L\<^sub>S. wf\<^sub>t\<^sub>r\<^sub>m x" using M\<^sub>T\<^sub>L\<^sub>S_wf_trm by metis

  let ?prems = "\<lambda>f S g T \<delta>. Fun f S \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S
                          \<and> Fun g T \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S
                          \<and> Unifier \<delta> (Fun f S) (Fun g T)"
  let ?prems_comp = "\<lambda>f S g T \<delta> f\<tau> S\<tau> g\<tau> T\<tau>. ?prems f S g T \<delta>
                          \<and> \<Gamma> (Fun f S) = TComp f\<tau> S\<tau>
                          \<and> \<Gamma> (Fun g T) = TComp g\<tau> T\<tau>"
  let ?prems_atom = "\<lambda>f S g T \<delta> \<tau>1 \<tau>2. ?prems f S g T \<delta>
                          \<and> \<Gamma> (Fun f S) = TAtom \<tau>1
                          \<and> \<Gamma> (Fun g T) = TAtom \<tau>2"

  { fix f S g T \<delta> f\<tau> S\<tau> g\<tau> T\<tau>
    assume SMP_funs: "Fun f S \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "Fun g T \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S"
      and nonatomic: "\<Gamma> (Fun f S) = TComp f\<tau> S\<tau>" "\<Gamma> (Fun g T) = TComp g\<tau> T\<tau>"
      and unif: "Unifier \<delta> (Fun f S) (Fun g T)"
    hence fg_eqs[simp]: "f = g" "f = f\<tau>" "g = g\<tau>"
      and fun_shapes: "M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes (Fun f S)" "M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes (Fun g T)"
      using fun_type_id_eq apply (simp, simp, simp)
      using nonatomic M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes[OF SMP_funs(1)] M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes[OF SMP_funs(2)]
      by (metis fun_type fun_type_id_eq fun_type_inv(1))+

    from unif prf_SMP_wt_unif[OF SMP_funs] nonatomic
    have "\<Gamma> (Fun f S) = \<Gamma> (Fun g T)"
      apply (induct rule: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_cases[OF fun_shapes(1)])
      by (induct rule: M\<^sub>T\<^sub>L\<^sub>S_SMP_shapes_cases[OF fun_shapes(2)]; simp_all; blast+)+
  }
  hence 1: "\<And>f S g T \<delta> f\<tau> S\<tau> g\<tau> T\<tau>. ?prems_comp f S g T \<delta> f\<tau> S\<tau> g\<tau> T\<tau> \<Longrightarrow> \<Gamma> (Fun f S) = \<Gamma> (Fun g T)"
    by metis

  { fix f S g T \<delta> \<tau>1 \<tau>2
    assume *: "Fun f S \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S" "Fun g T \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S"
    and **: "\<Gamma> (Fun f S) = TAtom \<tau>1" "\<Gamma> (Fun g T) = TAtom \<tau>2" "Unifier \<delta> (Fun f S) (Fun g T)"
    hence "f = g" by simp
    hence "S = []" "T = []"
        using const_type_inv[OF **(1)]
              M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm[OF *(1)] M\<^sub>T\<^sub>L\<^sub>S_SMP_wf_trm[OF *(2)]
              subtermeq_refl[of "Fun f S"] subtermeq_refl[of "Fun f T"]
        unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
    hence "Fun f S = Fun g T" by (metis \<open>f = g\<close>)
  }
  hence 2: "\<And>f S g T \<delta> \<tau>1 \<tau>2. ?prems_atom f S g T \<delta> \<tau>1 \<tau>2 \<Longrightarrow> Fun f S = Fun g T" by metis

  { fix s t assume *: "s \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S - Var`\<V>" "t \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S - Var`\<V>"
    then obtain f S g T where **: "s = Fun f S" "t = Fun g T" unfolding \<V>_def
      by (cases s, (simp_all; fail), cases t, (simp_all; fail))
    have "(\<exists>\<delta>. Unifier \<delta> s t) \<Longrightarrow> \<Gamma> s = \<Gamma> t"
    proof (erule exE)
      fix \<delta> assume ***: "Unifier \<delta> s t"
      hence "f = g" using ** by simp
      { fix f\<tau> S\<tau> g\<tau> T\<tau> assume "\<Gamma> (Fun f S) = TComp f\<tau> S\<tau>" "\<Gamma> (Fun g T) = TComp g\<tau> T\<tau>"
        hence ?thesis using * ** *** 1[of f S g T \<delta> f\<tau> S\<tau> g\<tau> T\<tau>] by simp }
      moreover
      { fix \<tau>1 \<tau>2 assume "\<Gamma> (Fun f S) = TAtom \<tau>1" "\<Gamma> (Fun g T) = TAtom \<tau>1"
        hence ?thesis using * ** *** 2[of f S g T \<delta> \<tau>1 \<tau>2] by simp }
      ultimately show ?thesis by (metis "term.exhaust" \<open>f = g\<close> const_type const_type_inv)
    qed
  }
  thus "\<forall>s \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S - Var`\<V>. \<forall>t \<in> SMP\<^sub>s\<^sub>t M\<^sub>T\<^sub>L\<^sub>S - Var`\<V>. (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t"
    by metis
qed






subsection {* Instantiation of the abstract over-approximation set preserves type-flaw resistance *}
context typed_model
begin
lemma tfr_preservation_subset:
  assumes "tfr\<^sub>s\<^sub>t M" "SMP\<^sub>s\<^sub>t M' \<subseteq> SMP\<^sub>s\<^sub>t M"
  shows "tfr\<^sub>s\<^sub>t M'"
proof -
  { fix s t u::"('fun, 'var) Term.term" and \<delta>::"('fun, 'var) subst"
    have "SMP\<^sub>s\<^sub>t M' \<union> (SMP\<^sub>s\<^sub>t M - SMP\<^sub>s\<^sub>t M') = SMP\<^sub>s\<^sub>t M" by (meson assms(2) Diff_partition)
    hence "((t \<in> SMP\<^sub>s\<^sub>t M'-Var`\<V> \<and> s \<in> SMP\<^sub>s\<^sub>t M'-Var`\<V> \<and> Unifier \<delta> t s) \<longrightarrow> \<Gamma> t = \<Gamma> s)
            \<and> (u \<in> M' \<longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m u)"
      by (metis (no_types) assms(1) Un_Diff Un_iff SMP\<^sub>s\<^sub>t.MP SMP_wf_trm)
  }
  thus ?thesis by blast
qed

lemma tfr_preservation_concretization:
  fixes M::"('fun,'var) terms" and \<gamma>::"('fun,'var) term \<Rightarrow> ('fun,'var) terms"
  assumes tfr_M: "tfr\<^sub>s\<^sub>t M"
  and \<gamma>_wt_instances: "\<forall>m \<in> M. \<forall>t \<in> \<gamma> m. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> (\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)) \<and> t = m \<cdot> \<delta>"
  and "\<And>t K M. Ana t = (K, M) \<Longrightarrow> K \<union> M \<subset> subterms t"
  shows "tfr\<^sub>s\<^sub>t (\<Union>m \<in> M. \<gamma> m)"
proof -
  { fix t assume "t \<in> SMP\<^sub>s\<^sub>t (\<Union>m \<in> M. \<gamma> m)"
    then obtain m \<theta> \<delta> where *:
        "m \<in> M" "t \<sqsubseteq> m \<cdot> (\<delta> \<circ>\<^sub>s \<theta>)" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> " "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
      by (metis (no_types) SMP_D[OF _ assms(3), of t "\<Union>m\<in>M. \<gamma> m"] UN_iff \<gamma>_wt_instances subst_comp)
    have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<delta> \<circ>\<^sub>s \<theta>)" by (simp_all add: * wt_subst_compose)
    moreover have "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m ((\<delta> \<circ>\<^sub>s \<theta>) v)" by (simp_all add: * wf_trm_subst subst_compose_def)
    ultimately have "t \<in> SMP\<^sub>s\<^sub>t M" by (metis SMP_I[OF *(1)] *(2))
  }
  thus ?thesis using tfr_preservation_subset[OF tfr_M] by blast
qed

end

end