(*****************************************************************************
 * ESPL --- an embedded security protocol logic
 *          http://people.inf.ethz.ch/meiersi/espl/
 *
 *   Copyright (c) 2009-2011, Simon Meier, ETH Zurich, Switzerland
 *
 * Extension to compromising adversaries:
 *
 *   Copyright (c) 2010-2011, Martin Schaub, ETH Zurich, Switzerland
 *
 * All rights reserved. See file LICENCE for more information.
 ******************************************************************************)
theory WeakTyping
imports
  InferenceRules
  Syntax
begin

section{* A Shallow Embedding of a Message Type System *}

subsection{* Introduction *}

text{*
  The goal of this theory is to develop a simple way for specifying
  type invariants for the message variables of a protocol. A message
  type is a set of messages that depends on the thread and the 
  system state that this message type is interpreted relative to.
  
  A typing is then a function assigning to each combination of a
  role and an identifier of a message variable in this role a 
  message type. 

  Each typing approximates the set of states where all instantiated
  message variables are instantiated with a message corresponding 
  to their type.
*}

type_synonym msgtype = "tid \<Rightarrow> state \<Rightarrow> execmsg set"

type_synonym typing = "(role \<times> id) \<Rightarrow> msgtype"

definition approx :: "typing \<Rightarrow> state set"
where "approx typing \<equiv> {q. case q of (t,r,s) \<Rightarrow>
  \<forall> (i,step) \<in> steps t. 
    \<forall> R. roleMap r i = Some R \<longrightarrow>
      (\<forall> n. MVar n \<in> FV_rolestep step \<longrightarrow>
         s (MVar n, i) \<in> typing (R, n) i (t,r,s)
      )}"

locale typed_state = reachable_state+
  fixes typing :: "typing"
  assumes approximates: "(t,r,s) \<in> approx typing"

locale typed_thread = reachable_thread+
  fixes typing :: "typing"
  assumes approximates: "(t,r,s) \<in> approx typing"

sublocale typed_thread \<subseteq> typed_state
  using approximates by unfold_locales


lemma approx_unfold:
  "((t,r,s) \<in> approx typing) = 
   (\<forall> (i,step) \<in> steps t. 
      \<forall> R. roleMap r i = Some R \<longrightarrow>
        (\<forall> n. MVar n \<in> FV_rolestep step \<longrightarrow>
           s (MVar n, i) \<in> typing (R, n) i (t,r,s)))"
by (auto simp: approx_def)

lemma in_approxI:
  assumes all_vars:
    "\<And> i step R n.
     \<lbrakk> (i,step) \<in> steps t;
       roleMap r i = Some R;
       MVar n \<in> FV_rolestep step
     \<rbrakk>
       \<Longrightarrow> s (MV n i) \<in> typing (R, n) i (t,r,s)"
  shows "(t,r,s) \<in> approx typing"
by (auto simp: approx_unfold dest!: all_vars)

lemma in_approxD:
  assumes approx: "(t,r,s) \<in> approx typing"
  and asms: "(i,step) \<in> steps t"
            "roleMap r i = Some R"
            "MVar n \<in> FV_rolestep step"
  shows "s (MV n i) \<in> typing (R, n) i (t,r,s)"
using approx asms
by (auto simp: approx_unfold)


subsection{* A Combinator Language for Message Types *}

subsubsection{* Structural Types *}

text{*
  Structural message types specify the structure of a message.
  Their interpretation is independent of the thread that they
  are interpreted in. All of them except the type for nonces of
  a specific role are also independent of the state that they
  are interpreted in.
*}

definition ConstT :: "id \<Rightarrow> msgtype"
where "ConstT c i q \<equiv> { LC c }"

definition AgentT :: msgtype
where "AgentT i q \<equiv>  Agent"

declare AgentT_def [simp]

definition NonceT :: "role \<Rightarrow> id \<Rightarrow> msgtype"
where "NonceT R n i q  \<equiv> case q of 
         (t,r,s) \<Rightarrow> { LN n i' | i'. roleMap r i' = Some R }"

definition HashT :: "msgtype \<Rightarrow> msgtype"
where "HashT ty  i q \<equiv> { Hash m | m. m \<in> ty i q }"

definition TupT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "TupT ty1 ty2 i q \<equiv> 
         { \<lbrace>x, y\<rbrace> | x y. x \<in> ty1 i q \<and> y \<in> ty2 i q }"

definition EncT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "EncT tym tyk i q \<equiv> 
         { Enc m k | m k. m \<in> tym i q \<and> k \<in> tyk i q }"

definition PKT :: "msgtype \<Rightarrow> msgtype"
where "PKT ty  i q \<equiv> { PK m | m. m \<in> ty i q }"

definition SKT :: "msgtype \<Rightarrow> msgtype"
where "SKT ty  i q \<equiv> { SK m | m. m \<in> ty i q }"

definition KT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "KT ty1 ty2 i q \<equiv> 
         { K m1 m2 | m1 m2. m1 \<in> ty1 i q \<and> m2 \<in> ty2 i q }"

definition KShrT :: "msgtype"
where "KShrT i q \<equiv> { KShr A | A. True }" 


text{* TODO: Make this syntax abbreviation work. *}
syntax
  "@TTuple"      :: "['a, args] => 'a * 'b"       ("(2{$_,/ _$})")

syntax (xsymbols)
  "@TTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>$_,/ _$\<rbrace>)")

translations
  "{$x, y, z$}"   == "{$x, {$y, z$}$}" 
  "{$x, y$}"      == "WeakTyping.TupT x y"


subsubsection{* Special Types *}

text{* 
  The empty type denotes that a variable is never instantiated.
  The sum type denotes the union of two message types, while
  the intersection type denotes the intersection of the two 
  message types.
*}

definition EmptyT :: "msgtype"
where "EmptyT i q \<equiv> {}"

declare EmptyT_def [simp]

definition SumT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "SumT ty1 ty2 i q \<equiv> ty1 i q \<union> ty2 i q"

definition InterT :: "msgtype \<Rightarrow> msgtype \<Rightarrow> msgtype"
where "InterT ty1 ty2 i q \<equiv> ty1 i q \<inter> ty2 i q"


text{*
  The known before a specific role step type captures the
  interaction of the intruder with the execution of a protocol.
  If the intruder fakes a message being received, then the
  variables are instantiated with messages known to the intruder
  \emph{before} the receive step was executed.
*}

definition KnownT :: "rolestep \<Rightarrow> msgtype"
where "KnownT step i q \<equiv> case q of  (t,r,s) \<Rightarrow> 
  { m | m. predOrd t (Ln m) (St (i,step)) }"


subsubsection{* Constructing Type Invariants *}

text{*
  The following function converts a list of type assignments to a
  typing. It will be used to specify the type invariants of specific
  protocols.
*}

definition mk_typing :: "((role \<times> id) \<times> msgtype) list \<Rightarrow> typing"
where "mk_typing tyeqs \<equiv> 
         foldr (\<lambda>(x, ty) typing. typing(x:=ty)) tyeqs (\<lambda>x. EmptyT)"


subsection{* Proving Well-Typedness *}

text{*
  A protocol is well-typed with respect to a typing iff
  all its reachable state are approximated by the typing.

  We specialize the induction scheme that we get from the definition
  of the set of reachable states to a ``type checking'' induction
  scheme. It works for message typings that are monotoneous with
  respect to state updates.
*}

definition monoTyp :: "typing \<Rightarrow> bool" 
where "monoTyp typ \<equiv> 
  (\<forall> x i t r s t' r'.
      roleMap r \<subseteq>\<^sub>m roleMap r' \<longrightarrow>
      typ x i (t,r,s) \<subseteq> typ x i (t@t',r',s)
  )"

lemma monoTypI:
  "\<lbrakk> \<And> x i t r s t' r' s' m. 
     \<lbrakk> roleMap r \<subseteq>\<^sub>m roleMap r'; m \<in> typ x i (t,r,s) \<rbrakk>
     \<Longrightarrow> m \<in> typ x i (t@t',r',s)
   \<rbrakk> \<Longrightarrow> monoTyp typ"
  by(auto simp: monoTyp_def)

lemma monoTypD:
  "\<lbrakk> monoTyp typ;
     m \<in> typ x i (t,r,s);
     roleMap r \<subseteq>\<^sub>m roleMap r'
   \<rbrakk> \<Longrightarrow>
   m \<in> typ x i (t@t',r',s)"
  unfolding monoTyp_def by blast

lemma monoTyp_freeD:
  "\<lbrakk> monoTyp typ;
     m \<in> typ x i (t,r,s);
     roleMap r \<subseteq>\<^sub>m roleMap r';
     t' = t@t''
   \<rbrakk> \<Longrightarrow>
   m \<in> typ x i (t',r',s)"
  unfolding monoTyp_def by blast

lemma monoTyp_appendD:
  "\<lbrakk> monoTyp typ;
     m \<in> typ x i (t,r,s)
   \<rbrakk> \<Longrightarrow>
   m \<in> typ x i (t@t',r,s)"
  by (rule monoTyp_freeD) auto


lemma (in reachable_thread) step_done_typing:
  assumes typ_rule:
    "\<And> step.
     \<lbrakk> (i, step) \<in> steps t;
       MVar v \<in> FV_rolestep step
     \<rbrakk> \<Longrightarrow> s (MV v i) \<in> typing (done @ todo, v) i (t, r, s)"
  and step_done: "step \<in> set done"
  and step_var: "MVar v \<in> FV_rolestep step"
  shows "s (MV v i) \<in> typing (done @ todo, v) i (t, r, s)"
proof (cases "step \<in> skipped")
  case False
  thus ?thesis using assms by auto
next
  case True
  note inSkipped = this
  then obtain l ty pt
    where noteEq: "(Note l ty pt) = step"
    by(auto dest!: note_in_skipped)
  hence "\<exists> step'. listOrd (done@todo) step' (Note l ty pt) \<and> v \<in> sourced_vars step'"
    using inSkipped step_done step_var
    apply -
    apply(subgoal_tac "v \<in> used_vars step")
      apply(subgoal_tac "Note l ty pt \<in> set (done@todo)")
        apply(drule source_use_ord)
    by auto
  then obtain step'
    where roleBefore: "listOrd (done@todo) step' (Note l ty pt)"
    and varSourced: "v \<in> sourced_vars step'"
    by auto
  have notNote: "\<not> noteStep step'" using varSourced by auto
  have "step' \<in> set done" 
    using roleBefore step_done noteEq
    apply -
    apply(drule listOrd_append[THEN iffD1])
    apply(case_tac "listOrd done step' (Note l ty pt)")
      apply(fastforce dest: in_set_listOrd1)
    apply(case_tac "listOrd todo step' (Note l ty pt)")
      apply(fastforce dest: in_set_listOrd2 done_notin_todoD)
    apply(case_tac "step' \<in> set done \<and> Note l ty pt \<in> set todo")
    by(auto dest: done_notin_todoD)
  hence "(i, step') \<in> steps t" using notNote by (cases step', auto)
  thus ?thesis
    using varSourced by (auto intro!: typ_rule thread_exists)
qed


lemma (in reachable_state) reachable_in_approxI:
  assumes monoTyp: "monoTyp typing"
  and source_case:
    "\<And> t r s i done todo skipped m R step n.
     \<lbrakk> R \<in> P; 
       roleMap r i = Some R;
       (done, step # todo) \<in> set (splits R);
       \<not> sendStep step; \<not> noteStep step;
       n \<in> sourced_vars step;
       \<forall> step' \<in> set done. MVar n \<notin> FV_rolestep step';
       hint ''completenessCase'' (step, n);
       
       (t,r,s) \<in> reachable P;
       (t,r,s) \<in> approx typing;
       r i = Some (done, step # todo, skipped);
       
       recvStep step \<Longrightarrow> Some m = inst s i (stepPat step) \<and> m \<in> knows t;
       matchEqStep step \<Longrightarrow> exec_match s i (matchVar step) (stepPat step)
     \<rbrakk> \<Longrightarrow> 
        s (MV n i) \<in> typing (R, n) i (t @ [Step (i, step)], r(i \<mapsto> (done @ [step], todo, skipped)), s)"
  shows "(t,r,s) \<in> approx typing"
proof -
  { fix i step "done" todo skipped n
    have
     "\<lbrakk> r i = Some (done, todo, skipped);
        (i,step) \<in> steps t;
        MVar n \<in> FV_rolestep step
      \<rbrakk> \<Longrightarrow> s (MV n i) \<in> typing (done@todo, n) i (t,r,s)"
    proof(induct arbitrary: i "done" todo step n skipped rule: reachable_induct)
      case (send t r s i "done" l pt todo skipped m i' done' todo' step n skipped')
      then interpret th1: 
        reachable_thread P t r s i "done" "Send l pt # todo" skipped
        by unfold_locales auto
      from send 
      have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Send l pt"
        (is "?old \<or> ?new") by auto
      moreover
      { assume ?old
        hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
          using send by (auto split: if_splits)
        hence ?case
        proof(rule monoTyp_freeD[OF monoTyp])
        qed (auto simp: th1.thread_exists)
      }
      moreover
      { let ?role = "done @ Send l pt # todo"
        note IH = send(2)
        assume "?new"
        moreover hence "n \<in> used_vars step" using send by auto
        ultimately obtain step' 
          where "(i, step') \<in> steps t" 
                "n \<in> sourced_vars step'"   
          by (fastforce dest!: th1.source_step[OF th1.thread_exists])
        hence typed: "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
          by (auto dest: IH[OF th1.thread_exists])
        have "done'@todo' = ?role"
          using send `?new` by auto
        hence ?case using `?new`
          apply -
          apply(rule monoTyp_freeD[OF monoTyp])
          by (auto intro!: typed simp: th1.thread_exists)
      }
      ultimately show ?case by fast
    next
      case (recv t r s i "done" l pt todo skipped m i' done' todo' step n skipped') then
      interpret th1: 
        reachable_thread P t r s i "done" "Recv l pt # todo" skipped
        by unfold_locales auto
      from recv
      have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Recv l pt"
        (is "?old \<or> ?new") by auto
      moreover
      { assume ?old
        hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
          using recv by (auto split: if_splits)
        hence ?case using `?old`
          apply -
          apply(rule monoTyp_freeD[OF monoTyp])
          apply(auto simp: th1.thread_exists)
          done
      }
      moreover
      { let ?role = "done @ Recv l pt # todo"
        note IH = recv(2)
        assume "?new"
        hence cur_thread: "?role = done' @ todo'" "i = i'" 
          using recv by auto
        have ?case
        proof(cases "\<exists> step' \<in> set done. MVar n \<in> FV_rolestep step'")
          case True
          with recv
          obtain step'
            where FV: "MVar n \<in> FV_rolestep step'" 
            and step': "step' \<in> set done"
            by auto
          hence "s (MV n i) \<in> typing (done'@todo', n) i (t, r, s)"
            using th1.thread_exists cur_thread IH
            by (metis th1.step_done_typing)
          thus ?thesis using `?new`
            apply -
            apply(rule monoTyp_freeD[OF monoTyp])
            apply(auto simp: th1.thread_exists)
            done
        next
          case False
            moreover have "(t, r, s) \<in> approx typing"
              by (auto simp: approx_unfold dest!: IH roleMap_SomeD)
            moreover note `?new`
            moreover note `MVar n \<in> FV_rolestep step`
            moreover note `Some m = inst s i pt`
            moreover note `m \<in> knows t`
            moreover note cur_thread[symmetric]
          
            ultimately show ?thesis
              apply -
              apply(clarsimp simp del: fun_upd_apply)
              apply(rule source_case)
              apply(simp_all add: th1.role_in_P th1.roleMap th1.thread_exists 
                                  in_set_splits_conv remove_hints)
              done
         qed
      }
      ultimately show ?case by fastforce
    next
      case (compr t r s i "done" l ty pt todo skipped m i' done' todo' step n skipped')
      then interpret th1: 
        reachable_thread P t r s i "done" "Note l ty pt # todo" skipped
        by unfold_locales auto
      from compr
      have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Note l ty pt"
        (is "?old \<or> ?new") by auto
      moreover
      { assume ?old
        hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
          using compr by (auto split: if_splits)
        hence ?case
        proof(rule monoTyp_freeD[OF monoTyp])
        qed (auto simp: th1.thread_exists)
      }
      moreover
      { let ?role = "done @ Note l ty pt # todo"
        note IH = compr(2)
        assume "?new"
        hence "n \<in> used_vars (Note l ty pt)"
          using compr by auto
        then obtain step' 
          where "(i, step') \<in> steps t" 
                "n \<in> sourced_vars step'"
          by (fastforce dest!: th1.source_step[OF th1.thread_exists])
        moreover hence "MVar n \<in> FV_rolestep step'" by auto
        ultimately have typed: "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
          by (auto dest: IH[OF th1.thread_exists])
        have "done'@todo' = ?role"
          using compr `?new` by auto
        hence ?case using `?new`
          apply -
          apply(rule monoTyp_freeD[OF monoTyp])
          by (auto intro!: typed simp: th1.thread_exists)
      }
      ultimately show ?case by fast
    next
      case (skip t r s i "done" l ty pt todo skipped i' done' todo' step n skipped')
      then interpret th1: 
        reachable_thread P t r s i "done" "Note l ty pt # todo" skipped
        by unfold_locales auto
      from skip
      have "(i', step) \<in> steps t" (is "?old") by auto
      hence "s(MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
        using skip by (auto split: if_splits)
      thus ?case
      proof(rule monoTyp_freeD[OF monoTyp])
      qed (auto simp: th1.thread_exists)
    next
      case (match t r s i "done" l eq mv pt todo skipped i' done' todo' step n skipped') then
      interpret th1:
        reachable_thread P t r s i "done" "Match l eq mv pt # todo" skipped
        by unfold_locales auto
      from match
      have "(i', step) \<in> steps t \<or> (i' = i) \<and> step = Match l eq mv pt"
        (is "?old \<or> ?new") by auto
      moreover
      { assume ?old
        hence "s (MV n i') \<in> typing (done'@todo', n) i' (t,r,s)"
          using match by (auto split: if_splits)
        hence ?case
        proof (rule monoTyp_freeD[OF monoTyp])
        qed (auto simp: th1.thread_exists)
      }
      moreover
      { let ?role = "done @ Match l eq mv pt # todo"
        note IH = match(2)
        assume "?new"
        have ?case proof (cases eq)
          case True
          note eq_case = this
          hence cur_thread: "?role = done' @ todo'" "i = i'" and
                match_FV: "n \<in> used_vars step \<or> n \<in> sourced_vars step"
          using `?new` match by auto
          from match_FV show ?thesis proof
            assume "n \<in> used_vars step"
            with `?new` obtain step'
              where "(i, step') \<in> steps t"
                    "n \<in> sourced_vars step'"
              by (fastforce dest!: th1.source_step[OF th1.thread_exists])
            hence typed: "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
              by (auto dest: IH[OF th1.thread_exists])
            thus ?thesis using `?new` cur_thread(1)
              apply -
              apply(rule monoTyp_freeD[OF monoTyp])
              by (auto intro!: typed simp: th1.thread_exists)
          next
            assume "n \<in> sourced_vars step"
            thus ?thesis
            proof (cases "\<exists> step' \<in> set done. MVar n \<in> FV_rolestep step'")
              case True
              with match
              obtain step'
                where FV: "MVar n \<in> FV_rolestep step'"
                and step': "step' \<in> set done"
                by auto
              hence "s (MV n i) \<in> typing (done'@todo', n) i (t, r, s)"
                using th1.thread_exists cur_thread IH
                by (metis th1.step_done_typing)
              thus ?thesis using `?new`
                apply -
                apply(rule monoTyp_freeD[OF monoTyp])
                apply(auto simp: th1.thread_exists)
                done
            next
              case False
                moreover have "(t, r, s) \<in> approx typing"
                  by (auto simp: approx_unfold dest!: IH roleMap_SomeD)
                moreover note `?new`
                moreover note `n \<in> sourced_vars step`
                moreover have "exec_match s i mv pt"
                  using match eq_case by simp
                moreover note cur_thread[symmetric]

                ultimately show ?thesis
                  apply -
                  apply(clarsimp simp del: fun_upd_apply)
                  apply(rule source_case)
                  apply(simp_all add: th1.role_in_P th1.roleMap th1.thread_exists
                                      in_set_splits_conv remove_hints)
                  done
            qed
          qed

        next
          case False note notMatch = this
          moreover note `?new`
          moreover hence "n \<in> used_vars step" using match notMatch by auto
          ultimately obtain step'
            where "(i, step') \<in> steps t" 
                  "n \<in> sourced_vars step'"   
            by (fastforce dest!: th1.source_step[OF th1.thread_exists])
          hence typed: "s (MV n i) \<in> typing (?role, n) i (t, r, s)"
            by (auto dest: IH[OF th1.thread_exists])
          have "done'@todo' = ?role" using match `?new` by auto
          thus ?thesis using `?new`
            apply -
            apply(rule monoTyp_freeD[OF monoTyp])
            by (auto intro!: typed simp: th1.thread_exists)
        qed
      }
      ultimately show ?case by fastforce

    qed (auto intro: monoTyp_appendD[OF monoTyp])
  }
  thus ?thesis unfolding approx_unfold by(auto elim!: roleMap_SomeE)
qed

text{*
  We prove a variant of the above lemma, which is suitable for
  automation. The difference is the description of the variables
  that need to be checked. Here, it is done such that Isabelle's
  simplifier gets a finite set that it can rewrite into normal
  form.
*}
lemma (in reachable_state) reachable_in_approxI_ext:
  assumes monoTyp: "monoTyp typing"
  and source_case:
    "\<And> t r s i done todo skipped m R step n.
     \<lbrakk> R \<in> P; 
       roleMap r i = Some R;
       (done, step # todo) \<in> set (splits R);
       \<not> sendStep step; \<not> noteStep step;
       n \<in> foldl (\<lambda> fv step'. fv - sourced_vars step') (sourced_vars step) done;
       hint ''completenessCase'' (step, n);
       
       (t,r,s) \<in> reachable P;
       (t,r,s) \<in> approx typing;
       r i = Some (done, step # todo, skipped);
       \<forall> st'. st' \<in> set done \<longrightarrow> \<not> noteStep st' \<longrightarrow> (i, st') \<in> steps t;

       recvStep step \<Longrightarrow> Some m = inst s i (stepPat step) \<and> m \<in> knows t;
       matchEqStep step \<Longrightarrow> exec_match s i (matchVar step) (stepPat step)
     \<rbrakk> \<Longrightarrow>
        s (MV n i) \<in> typing (R, n) i ( t @ [Step (i, step)], r(i \<mapsto> (done @ [step], todo, skipped)), s)"
  shows "(t,r,s) \<in> approx typing"
proof(induct rule: reachable_in_approxI[OF monoTyp])
  case (1 t r s i "done" todo skipped m R step n)
  { fix v V
    assume "v \<in> V"
      and "\<forall>step'\<in>set done. MVar v \<notin> FV_rolestep step'"
    hence "v \<in> foldl (\<lambda> fv step'. fv - sourced_vars step') V done"
      by (induct "done" arbitrary: V) (auto intro!: sourced_imp_FV)
  }
  hence "n \<in> foldl (\<lambda> fv step'. fv - sourced_vars step') (sourced_vars step) done"
    using 1 by auto
  moreover {
    interpret thread: reachable_thread P t r s i "done" "(step # todo)" skipped
      using 1 by unfold_locales auto
    fix st'
    assume "st' \<in> set done" and "\<not> noteStep st'"
    hence "(i, st') \<in> steps t" by (auto intro: thread.not_note_done_in_steps)
  }
  ultimately show ?case using 1
    apply(subgoal_tac "True")
    apply(clarsimp)
    apply(rule source_case)
    by(assumption | simp add: remove_hints)+
qed

text{* Proving typing monotonicity *}

subsubsection{* Monotonicity Proofs *}

definition monoMsgTyp :: "msgtype \<Rightarrow> bool"
where "monoMsgTyp ty \<equiv>
         (\<forall>i t r s t' r'.
            roleMap r \<subseteq>\<^sub>m roleMap r' \<longrightarrow>
            ty i (t, r, s) \<subseteq> ty i (t @ t', r', s))"

lemma monoMsgTypD:
  "\<lbrakk> monoMsgTyp ty;
     m \<in> ty i (t,r,s);
     roleMap r \<subseteq>\<^sub>m roleMap r'
   \<rbrakk> \<Longrightarrow>
   m \<in> ty  i (t@t',r',s)"
  unfolding monoMsgTyp_def by blast


lemma monoMsgTyp_SumTI[intro!]:
  assumes ty1: "monoMsgTyp ty1"
  and     ty2: "monoMsgTyp ty2"
  shows "monoMsgTyp (SumT ty1 ty2)"
  by(auto simp: monoMsgTyp_def SumT_def 
          dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])

lemma monoMsgTyp_InterTI[intro!]:
  assumes ty1: "monoMsgTyp ty1"
  and     ty2: "monoMsgTyp ty2"
  shows "monoMsgTyp (InterT ty1 ty2)"
  by(auto simp: monoMsgTyp_def InterT_def 
          dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])

lemma monoMsgTyp_KnownTI[iff]:
  shows "monoMsgTyp (KnownT step)"
  by(auto simp: monoMsgTyp_def KnownT_def )
      
lemma monoMsgTyp_NonceTI[iff]:
  shows "monoMsgTyp (NonceT R n)"
  by(auto simp: monoMsgTyp_def NonceT_def dest: map_leD)

lemma monoMsgTyp_ConstTI[iff]:
  shows "monoMsgTyp (ConstT c)"
  by(auto simp: monoMsgTyp_def ConstT_def dest: map_leD)

lemma monoMsgTyp_AgentTI[iff]:
  shows "monoMsgTyp AgentT"
  by(auto simp: monoMsgTyp_def AgentT_def dest: map_leD)

lemma monoMsgTyp_EncTI[intro!]:
  assumes ty1: "monoMsgTyp ty1"
  and     ty2: "monoMsgTyp ty2"
  shows "monoMsgTyp (EncT ty1 ty2)"
  by(auto simp: monoMsgTyp_def EncT_def 
          dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])

lemma monoMsgTyp_KTI[intro!]:
  assumes ty1: "monoMsgTyp ty1"
  and     ty2: "monoMsgTyp ty2"
  shows "monoMsgTyp (KT ty1 ty2)"
  by(auto simp: monoMsgTyp_def KT_def 
          dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])

lemma monoMsgTyp_KShrTI[intro!]:
  shows "monoMsgTyp KShrT"
  by(auto simp: monoMsgTyp_def KShrT_def)

lemma monoMsgTyp_TupTI[intro!]:
  assumes ty1: "monoMsgTyp ty1"
  and     ty2: "monoMsgTyp ty2"
  shows "monoMsgTyp (TupT ty1 ty2)"
  by(auto simp: monoMsgTyp_def TupT_def 
          dest: monoMsgTypD[OF ty1] monoMsgTypD[OF ty2])

lemma monoMsgTyp_HashTI[intro!]:
  assumes ty: "monoMsgTyp ty"
  shows "monoMsgTyp (HashT ty)"
  by(auto simp: monoMsgTyp_def HashT_def 
          dest: monoMsgTypD[OF ty])

lemma monoMsgTyp_PKTI[intro!]:
  assumes ty: "monoMsgTyp ty"
  shows "monoMsgTyp (PKT ty)"
  by(auto simp: monoMsgTyp_def PKT_def 
          dest: monoMsgTypD[OF ty])

lemma monoMsgTyp_SKTI[intro!]:
  assumes ty: "monoMsgTyp ty"
  shows "monoMsgTyp (SKT ty)"
  by(auto simp: monoMsgTyp_def SKT_def 
          dest: monoMsgTypD[OF ty])

lemma monoTyp_mk_typing[intro!]:
  assumes monoMsgTyp: 
     "\<And> pos ty. (pos, ty) \<in> set tyeqs \<Longrightarrow> monoMsgTyp ty"
  shows "monoTyp (mk_typing tyeqs)"
using monoMsgTyp
proof(induct tyeqs)
  case Nil thus ?case
    by(auto intro!: monoTypI simp: mk_typing_def EmptyT_def)
next
  case (Cons tyeq tyeqs) 
  thus ?case
    proof(cases tyeq)
      case (Pair pos' ty') 
      have mk_typing_Cons [simp]:
        "mk_typing ((pos',ty')#tyeqs) = (mk_typing tyeqs)(pos' := ty')"
        by (simp add: mk_typing_def)
      with Pair show ?thesis
        apply(auto intro!: monoTypI)
        apply(auto intro: monoTypD[OF Cons(1), OF Cons(2)]
                          monoMsgTypD[OF Cons(2)]
                   simp: Pair)
        done
    qed
qed

subsection{* Automation *}

text{*
The automation of the welltypedness proofs is rather fragile.
As a general rule of operation we try to unfold type information
as late as possible. This allows to guide the automation tools
by matching on the structure of the types. However, it also
implies that more rules are necessary. Moreover the current set
of rules is not guaranteed to be complete.
*}

subsubsection{* ACI of Sum and Intersection Types *}

lemma SumT_absorb [simp]: "SumT ty ty = ty"
  by (rule ext, rule ext) (auto simp: SumT_def)

lemma SumT_left_absorb: "SumT ty1 (SumT ty1 ty2) = SumT ty1 ty2"
  by (rule ext, rule ext) (auto simp: SumT_def)

lemma SumT_commute: "SumT ty1 ty2 = SumT ty1 ty2"
  by (rule ext, rule ext) (auto simp: SumT_def)

lemma SumT_left_commute: "SumT ty1 (SumT ty2 ty3) = SumT ty2 (SumT ty1 ty3)"
  by (rule ext, rule ext) (auto simp: SumT_def)

lemma SumT_assoc: "SumT (SumT ty1 ty2) ty3  = SumT ty1 (SumT ty2 ty3)"
  by (rule ext, rule ext) (auto simp: SumT_def)

lemmas SumT_ac = SumT_assoc SumT_left_absorb SumT_commute SumT_left_commute
  -- {* Type sum is an AC-operator *}

lemma InterT_absorb [simp]: "InterT ty ty = ty"
  by (rule ext, rule ext) (auto simp: InterT_def)

lemma InterT_left_absorb: "InterT ty1 (InterT ty1 ty2) = InterT ty1 ty2"
  by (rule ext, rule ext) (auto simp: InterT_def)

lemma InterT_commute: "InterT ty1 ty2 = InterT ty1 ty2"
  by (rule ext, rule ext) (auto simp: InterT_def)

lemma InterT_left_commute: "InterT ty1 (InterT ty2 ty3) = InterT ty2 (InterT ty1 ty3)"
  by (rule ext, rule ext) (auto simp: InterT_def)

lemma InterT_assoc: "InterT (InterT ty1 ty2) ty3  = InterT ty1 (InterT ty2 ty3)"
  by (rule ext, rule ext) (auto simp: InterT_def)


lemmas InterT_ac = InterT_assoc InterT_left_absorb InterT_commute InterT_left_commute
  -- {* Type intersection is an AC-operator *}


subsubsection{* Type Membership *}


text{* Special types *}

text{* The rules for SumT are special, as their usage currently
depends on the combination of SumT and KnownT.
*}
lemma in_SumTE:
  "\<lbrakk> m \<in> SumT ty1 ty2 i q; m \<in> ty1 i q \<Longrightarrow> R; m \<in> ty2 i q \<Longrightarrow> R 
   \<rbrakk> \<Longrightarrow> R"
  by(auto simp: SumT_def)

lemma notin_SumTE [elim!]: 
  "\<lbrakk> m \<notin> SumT ty1 ty2 i q; 
     \<lbrakk> m \<notin> ty1 i q; m \<notin> ty2 i q \<rbrakk> \<Longrightarrow> R
   \<rbrakk> \<Longrightarrow> R"
  by(auto simp: SumT_def)

lemma notin_KnownT_append_StepE [dest!]:
  "m \<notin> KnownT step i (t@ [Step (i, step)], r, s) \<Longrightarrow>
   m \<notin> knows t"
  by(auto simp: KnownT_def)

lemma in_SumT_NonceT_NonceTE [elim!]:
  "\<lbrakk> m \<in> SumT (NonceT Ro n) (NonceT Ro' n') i q; 
     m \<in> NonceT Ro n i q \<Longrightarrow> R; 
     m \<in> NonceT Ro' n' i q \<Longrightarrow> R 
   \<rbrakk> \<Longrightarrow> R"
  by(auto simp: SumT_def)

(* TODO: Add more of the restricted SumT unfoldings analogous to the ones above.
   We don't unfold SumT eagerly, as this would result in too many branches being created.
   The above lemma is a hack to get triple types of the form SumT KnownT (SumT NonceT NonceT)
   to work. The proper way would be to only expand types of variables that are being analyzed
   by the decrChain function.
*)

text{* Direct unfoldings *}

lemma in_ConstT_simp [iff]:
  "(m \<in> ConstT c i q) = (m = LC c)"
  by(auto simp: ConstT_def)

lemma in_KnownTD [dest!]:
  "(x \<in> KnownT step i (t,r,s)) \<Longrightarrow> (predOrd t (Ln x) (St (i, step)))"
  by(simp add: KnownT_def)


text{* To be used together with if\_splits in a well-typedness
proof *}
lemma in_NonceT [simp]: 
  "(LN n i \<in> NonceT R n i' (t,r,s)) = (roleMap r i = Some R)"
  by(simp add: NonceT_def)

lemma in_NonceTE [elim!]:
  "\<lbrakk> m \<in> NonceT R n i (t,r,s); 
    \<And> nTid. \<lbrakk> m = LN n nTid; roleMap r nTid = Some R \<rbrakk> \<Longrightarrow> Q 
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: NonceT_def)

lemma notin_NonceT_thenonceE [elim!]:
  "\<lbrakk> LN n nTid \<notin> NonceT nR n i (t, r(i \<mapsto> (done,todo,skipped)), s);
     nTid = i \<Longrightarrow> Q;
     \<lbrakk> nTid \<noteq> i; roleMap r nTid \<noteq> Some nR \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: NonceT_def split: if_splits)


text{* These rules ensure that type information is exploited
when a match impossible without intruder activity happening.
*}
lemma Tup_in_SumT_KnownT_NonceTD [dest!]:
  "Tup x y \<in> SumT (KnownT step) (NonceT R n) i (t, r, s)
   \<Longrightarrow> predOrd t (Ln (Tup x y)) (St (i, step))"
  by(auto simp: KnownT_def SumT_def)

lemma Hash_in_SumT_KnownT_NonceTD [dest!]:
  "Hash x \<in> SumT (KnownT step) (NonceT R n) i (t, r, s)
   \<Longrightarrow> predOrd t (Ln (Hash x)) (St (i, step))"
  by(auto simp: KnownT_def SumT_def)

lemma Enc_in_SumT_KnownT_NonceTD [dest!]:
  "Enc x y \<in> SumT (KnownT step) (NonceT R n) i (t, r, s)
   \<Longrightarrow> predOrd t (Ln (Enc x y)) (St (i, step))"
  by(auto simp: KnownT_def SumT_def)

text{* TODO: Extend these lemmas for further combinations. This requires
some more thinking. However, for a well-designed protocols the message
structure is not required for disambiguation because the encryptions
contain tags that identify them.
*}

text{* Structural types *}

text{* The following rules are used in well-typedness proofs *}
lemma Hash_in_HashT [simp]: 
  "(Hash x \<in> HashT ty i q) = (x \<in> ty i q)"
  by (simp add: HashT_def)

lemma Tup_in_TupT [simp]: 
  "(Tup x y \<in> TupT ty1 ty2 i q) = (x \<in> ty1 i q \<and> y \<in> ty2 i q)"
  by (simp add: TupT_def)

lemma Enc_in_EncT [simp]: 
  "(Enc x y \<in> EncT ty1 ty2 i q) = (x \<in> ty1 i q \<and> y \<in> ty2 i q)"
  by (simp add: EncT_def)

lemma PK_in_PKT [simp]: "(PK x \<in> PKT ty i q) = (x \<in> ty i q)"
  by (simp add: PKT_def)

lemma SK_in_SKT [simp]: "(SK x \<in> SKT ty i q) = (x \<in> ty i q)"
  by (simp add: SKT_def)

lemma K_in_KT [simp]: 
  "(K x y \<in> KT ty1 ty2 i q) = (x \<in> ty1 i q \<and> y \<in> ty2 i q)"
  by (simp add: KT_def)



text{* The following rules ensure that messages are expanded
automatically in when applying the sources rule.
*}

lemma in_HashTE [elim!]:
  "\<lbrakk> m \<in> HashT ty i q;
     \<And> x. \<lbrakk> m = Hash x; x \<in> ty i q \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: HashT_def)

lemma in_EncTE [elim!]:
  "\<lbrakk> m \<in> EncT ty1 ty2 i q;
     \<And> x k. \<lbrakk> m = Enc x k; x \<in> ty1 i q; k \<in> ty2 i q \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: EncT_def)

lemma in_TupTE [elim!]:
  "\<lbrakk> m \<in> TupT ty1 ty2 i q;
     \<And> x y. \<lbrakk> m = \<lbrace> x, y \<rbrace>; x \<in> ty1 i q; y \<in> ty2 i q \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: TupT_def)

lemma in_KTE [elim!]:
  "\<lbrakk> m \<in> KT ty1 ty2 i q;
     \<And> x y. \<lbrakk> m = K x y; x \<in> ty1 i q; y \<in> ty2 i q \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: KT_def)

lemma in_PKTE [elim!]:
  "\<lbrakk> m \<in> PKT ty i q;
     \<And> x. \<lbrakk> m = PK x; x \<in> ty i q \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: PKT_def)

lemma in_SKTE [elim!]:
  "\<lbrakk> m \<in> SKT ty i q;
     \<And> x. \<lbrakk> m = SK x; x \<in> ty i q \<rbrakk> \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by(auto simp: SKT_def)


subsection{* Specialization of the Chain Rule *}

text{* We prove the case distinction on messages known to the
  intruder with respect to an typed state, because we need
  a sufficiently precise invariant when reasoning about the
  contents of a variable.
*}
lemma (in typed_state) knows_cases:
  assumes known: "m' \<in> knows t"
  shows "
   (m' \<in> IK0 \<and> 
    hint ''case_name'' ''ik0''
   ) \<or>
   (\<exists> m. m' = Hash m \<and> Ln m \<prec> Ln (Hash m) \<and>
         hint ''case_name'' ''fake''
   ) \<or>
   (\<exists> m k. m' = Enc m k \<and> 
           Ln m \<prec> Ln (Enc m k) \<and> Ln k \<prec> Ln (Enc m k) \<and>
           hint ''case_name'' ''fake''
   ) \<or>
   (\<exists> x y. m' = Tup x y \<and> 
           Ln x \<prec> Ln (Tup x y) \<and> Ln y \<prec> Ln (Tup x y) \<and>
           hint ''case_name'' ''fake''
   ) \<or>
   (\<exists> R \<in> P. \<exists> i. roleMap r i = Some R \<and> 
      (\<exists> step \<in> set R.
         (sendStep step \<or> noteStep step) \<and>
         (\<exists> m. Some m = inst s i (stepPat step) \<and> decrChain [] t {St (i, step)} m m') \<and>
         prefixClose s t R step i \<and>
         (\<forall> v \<in> FV (stepPat step). \<forall> n. v = MVar n \<longrightarrow> 
            s (MVar n, i) \<in> typing (R, n) i (t,r,s) \<and>
            hint ''case_name_subst'' n) \<and>
         hint ''decrChainFrom'' (i, R, step) \<and>
         hint ''case_name'' ''decrypt''
      )

   ) \<or>
   (\<exists> a. m' = SK a \<and> LKR a \<prec> Ln m' \<and> hint ''case_name'' ''asym_lkr'') \<or>
   (\<exists> a b. m' = K a b \<and> LKR a \<prec> Ln m' \<and> hint ''case_name'' ''sym_lkr1'') \<or>
   (\<exists> a b. m' = K a b \<and> LKR b \<prec> Ln m' \<and> hint ''case_name'' ''sym_lkr2'') \<or>
   (\<exists> A. \<exists> a \<in> A. m' = KShr A \<and> LKR (LAg a) \<prec> Ln m' \<and> hint ''case_name'' ''shr_lkr'')
   "
  (is "?ik0 \<or> ?hash \<or> ?encr \<or> ?tup \<or> ?decr \<or> ?keys")
proof -
  from known have
   "(m' \<in> IK0) \<or>
    (\<exists> m.   m' = Hash m   \<and> Ln m \<prec> Ln (Hash m)) \<or>
    (\<exists> m k. m' = Enc  m k \<and> Ln m \<prec> Ln (Enc m k) \<and> Ln k \<prec> Ln (Enc m k)) \<or>
    (\<exists> x y. m' = Tup  x y \<and> Ln x \<prec> Ln (Tup x y) \<and> Ln y \<prec> Ln (Tup x y)) \<or>
    (\<exists> i done todo skipped. r i = Some (done, todo, skipped) \<and> 
       (\<exists> l pt m. 
          Send l pt \<in> set done \<and> Some m = inst s i pt \<and> 
          decrChain [] t {St (i, Send l pt)} m m'
       )
    ) \<or>
    (\<exists> i done todo skipped. r i = Some (done, todo, skipped) \<and> 
       (\<exists> l ty pt m. 
          Note l ty pt \<in> set done \<and> Note l ty pt \<notin> skipped \<and> 
          Some m = inst s i pt \<and> 
          decrChain [] t {St (i, Note l ty pt)} m m'
       )
    ) \<or>
   (\<exists> a. m' = SK a \<and> LKR a \<prec> Ln m') \<or>
   (\<exists> a b. m' = K a b \<and> LKR a \<prec> Ln m') \<or>
   (\<exists> a b. m' = K a b \<and> LKR b \<prec> Ln m') \<or> 
   (\<exists> A. \<exists> a \<in> A. m' = KShr A \<and> LKR (LAg a) \<prec> Ln m')
   "
    (is "?ik0_raw \<or> ?hash_raw \<or> ?encr_raw \<or> ?tup_raw \<or> ?decr_raw \<or> ?note_raw \<or> ?keys_raw")
    by (rule knows_cases_raw)
  moreover 
  {
    assume "?ik0_raw" 
    hence ?thesis by( simp add: remove_hints)
  }
  moreover 
  {
    assume "?hash_raw" 
    hence ?thesis by( simp add: remove_hints)
  }
  moreover 
  {
    assume "?encr_raw" 
    hence ?thesis by( simp add: remove_hints)
  }
  moreover 
  {
    assume "?tup_raw" 
    hence ?thesis by( simp add: remove_hints)
  }
  moreover 
  {
    assume "?keys_raw" 
    hence ?thesis by( simp add: remove_hints)
  }
  moreover
  { assume ?decr_raw then
    obtain i "done" todo l msg skipped m
      where thread_exists: "r i = Some (done, todo,skipped)"
      and send_done: "Send l msg \<in> set done"
      and msg:       "Some m = inst s i msg"
      and decrChain: "decrChain [] t {St (i, Send l msg)} m m'"
      by fast
    then interpret th1: typed_thread P t r s i "done" todo skipped "typing"
      using approximates by unfold_locales
    from send_done have send_step: "(i, Send l msg) \<in> steps t" 
      by (rule th1.in_steps_send[THEN iffD1])
    moreover
    have "prefixClose s t (done@todo) (Send l msg) i" using send_step
      by(auto intro!: prefixCloseI th1.roleMap)
    moreover
    have send_in_role: "Send l msg \<in> set (done @ todo)"
      using send_done by simp
    moreover
    note in_approxD[OF th1.approximates send_step th1.roleMap, simplified]
    ultimately
    have ?decr using decrChain msg
      apply -
      apply(rule bexI[OF _ th1.role_in_P])
      apply(rule exI)
      apply(rule conjI[OF th1.roleMap])
      apply(rule bexI[OF _ send_in_role])
      by(auto simp: remove_hints)
    hence ?thesis by blast 
  }
  moreover
  {
    assume ?note_raw
    then obtain i "done" todo skipped l ty pt m
      where thread_exists: "r i = Some (done, todo,skipped)"
      and inDone: "Note l ty pt \<in> set done"
      and notinSkipped:  "Note l ty pt \<notin> skipped"
      and msg:       "Some m = inst s i pt"
      and decrChain: "decrChain [] t {St (i, Note l ty pt)} m m'"
      by fast
    then interpret th1: typed_thread P t r s i "done" todo skipped "typing"
      using approximates by unfold_locales
    from inDone and notinSkipped have note_step: "(i, Note l ty pt) \<in> steps t" 
      by (fastforce dest!: th1.in_steps_eq_in_done)
    moreover
    have "prefixClose s t (done@todo) (Note l ty pt) i" using note_step
      by(auto intro!: prefixCloseI th1.roleMap)
    moreover
    have note_in_role: "Note l ty pt \<in> set (done @ todo)"
      using inDone by simp
    moreover
    note in_approxD[OF th1.approximates note_step th1.roleMap, simplified]
    ultimately
    have ?decr using decrChain msg
      apply -
      apply(rule bexI[OF _ th1.role_in_P])
      apply(rule exI)+
      apply(rule conjI[OF th1.roleMap])
      apply(rule bexI[OF _ note_in_role])
      by(auto simp: remove_hints)
    hence ?thesis by blast 
  }
  ultimately
  show ?thesis by fastforce
qed


lemma (in reachable_state) decrChain_AgentE:
  assumes decrChain: "decrChain path t from m m'"
  and         Agent: "m \<in> Agent"
  and      nonempty: "from = {} \<Longrightarrow> Q"
  shows "Q"
  using decrChain Agent nonempty
  by (auto simp: Agent_def)

(*
lemma (in reachable_state) decrChain_AgentTE:
  assumes decrChain: "decrChain path t from m m'"
  and        AgentT: "m \<in> AgentT i (t,r,s)" 
  and          elim: "m = m' \<Longrightarrow> Q"
  shows "Q"
  using decrChain AgentT elim
  by (auto simp: AgentT_def)
*)

lemma (in reachable_state) decrChain_imp_predOrd:
  "\<lbrakk> decrChain path t from m m' \<rbrakk> \<Longrightarrow>
  \<exists> im \<in> pairParts m. (\<forall> f \<in> from. f \<prec> Ln im) \<and> Ln im \<preceq> Ln m'"
proof(induct m arbitrary: path "from")
  case (Tup x y) thus ?case
    apply(simp)
    apply(erule disjE)
    apply(clarsimp)
    apply(rule disjI2)
    apply(fastforce intro: less_le_trans)
    done
qed fastforce+

lemma (in reachable_state) decrChain_KnownT:
  assumes decrChain: "decrChain path t from m m'"
  and        KnownT: "predOrd t (Ln m) (St (i, step))"
  shows "\<exists> im \<in> pairParts m. 
           (\<forall> f \<in> from. f \<prec> Ln im) \<and> Ln im \<prec> St (i, step)"
proof -
  obtain im
    where "im \<in> pairParts m" and "\<forall>f \<in> from. f \<prec> Ln im"
    using decrChain by (fast dest!: decrChain_imp_predOrd)
  with KnownT show ?thesis
    by (fastforce intro: pairParts_before)
qed

lemma (in reachable_state) decrChain_KnownTE:
  assumes decrChain: "decrChain path t from m m'"
  and        KnownT: "predOrd t (Ln m) (St (i, step))"
  and elim: "\<And> im. \<lbrakk> im \<in> pairParts m; 
                      \<forall> f \<in> from. f \<prec> Ln im;
                      Ln im \<prec> St (i, step)
                    \<rbrakk> \<Longrightarrow> Q"
  shows "Q"
  using decrChain KnownT
  by(auto dest!: decrChain_KnownT elim)

lemma (in reachable_state) decrChain_SumT_KnownTE:
  assumes KnownT: "m \<in> SumT (KnownT step) ty i (t,r,s)" 
  and  decrChain: "decrChain path t from m m'"
  and elimK: "\<And> im. \<lbrakk> im \<in> pairParts m; 
                       \<forall> f \<in> from. f \<prec> Ln im;
                       Ln im \<prec> St (i, step)
                     \<rbrakk> \<Longrightarrow> Q"
  and elimTy: "m \<in> ty i (t,r,s) \<Longrightarrow> Q"
  shows "Q"
  using decrChain KnownT elimK elimTy
  by(auto elim!: in_SumTE decrChain_KnownTE)


lemma (in reachable_state) AV_in_Agent [iff]: 
  "s (AV a aTid) \<in> Agent"
using inst_AVar_cases 
by (auto simp: Agent_def)


end

(* TODO: 
    - Remove agent variables from protocol model by 
      replacing them with type annotations. 

      [General version will require us to reintroduce create event.
       But composition becomes nicer, as we can now model protocols, which
       use parameters that are secret values and so on.
      ]


    - Put decryption chain case into recursion of chain
      predicate to make more information available locally.
*)


