(*****************************************************************************
 * 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 ExplicitModel
imports
  HOL_ext
  Hints
  Protocol
  ExecMessage
begin



chapter{* Security Proofs *}

section{* Explicit Execution Model *}

datatype rawevent = 
    Step "tid \<times> rolestep"
  | Learns "execmsg set"
  | LKReveal id


datatype reveal =  
  RCompr notetype tid
| RLKR execmsg

type_synonym explicit_trace = "rawevent list"
type_synonym execstep = "tid \<times> rolestep"
type_synonym threadpool = "tid \<rightharpoonup> (rolestep list \<times> rolestep list \<times> rolestep set)"

fun knows :: "explicit_trace \<Rightarrow> execmsg set"
where
  "knows [] = {}"
| "knows (Learns M # t) = M \<union> knows t"
| "knows (Step estep # t) = knows t"
| "knows (LKReveal a # t) = knows t"

fun steps :: "explicit_trace \<Rightarrow> execstep set"
where
  "steps [] = {}"
| "steps (Learns M # t) = steps t"
| "steps (Step estep # t) = insert estep (steps t)"
| "steps (LKReveal a # t) = steps t"

fun reveals :: "explicit_trace \<Rightarrow> reveal set"
where
  "reveals (Step (i, s) # xs)  = 
     (if (noteStep s) then
        insert (RCompr (noteType s) i) (reveals xs)
      else
        reveals xs)"
| "reveals (Learns m # xs) = reveals xs"
| "reveals (LKReveal a # xs) =  insert (RLKR (Lit (EAgent a))) (reveals xs)"
| "reveals [] = {}"

fun lkreveals :: "explicit_trace \<Rightarrow> execmsg set"
where
  "lkreveals [] = {}"
| "lkreveals (Learns M # t) = lkreveals t"
| "lkreveals (Step estep # t) = lkreveals t"
| "lkreveals (LKReveal a # t) = insert (Lit (EAgent a)) (lkreveals t)"

definition longTermKeys :: "id \<Rightarrow> execmsg set"
where
  "longTermKeys a =  { SK (Lit (EAgent a)) } \<union>
                     { K (Lit (EAgent a)) b | b. b \<in> Agent } \<union> 
                     { K b (Lit (EAgent a)) | b. b \<in> Agent } \<union> 
                     { KShr A | A. a \<in> A }"
                    
lemma SK_in_longTermKeys [iff]:
  "(SK x \<in>  longTermKeys a) = (x = (Lit (EAgent a)))"
  by (auto simp: longTermKeys_def)

lemma K_in_longTermKeys [iff]:
  "(K x y \<in> longTermKeys a) = 
   ( (x = (Lit (EAgent a)) \<and> y \<in> Agent) \<or> 
     (y = (Lit (EAgent a)) \<and> x \<in> Agent) 
   )"
  by (auto simp: longTermKeys_def)

lemma KShr_in_longTermKeys [iff]:
  "(KShr A \<in> longTermKeys a) = (a \<in> A)"
  by (auto simp: longTermKeys_def)

lemma notin_longTermKeys [iff]:
  "Hash m \<notin> longTermKeys a"
  "Tup x y \<notin> longTermKeys a"
  "Enc m k \<notin> longTermKeys a"
by (auto simp: longTermKeys_def)

lemma longTermKeys_conv: 
  "(m \<in> longTermKeys a) = 
   ( (m = SK (Lit (EAgent a))) \<or> 
     (\<exists> b \<in> Agent. m = K (Lit (EAgent a)) b \<or> 
                   m = K b (Lit (EAgent a))
     ) \<or> 
     (\<exists> A. m = KShr A \<and> a \<in> A)
   )"
  by (auto simp: longTermKeys_def)


type_synonym state = "explicit_trace \<times> threadpool \<times> store"

inductive_set 
  reachable :: "proto \<Rightarrow> state set" 
  for P     :: "proto"
where
  init:  "\<lbrakk> \<forall> i done todo skipped. r i = Some (done,todo,skipped) \<longrightarrow>  done = [] \<and> skipped = {} \<and> todo \<in> P;
            \<forall> a i. s (AVar a, i) \<in> Agent
          \<rbrakk>
          \<Longrightarrow> ([Learns IK0], r, s) \<in> reachable P"
 
| compr: "\<lbrakk> (t, r, s) \<in> reachable P;
            r i = Some (done, Note l ty pt # todo, skipped);
            Some m = inst s i pt
          \<rbrakk>
          \<Longrightarrow> (t @ [Step (i,Note l ty pt), Learns (pairParts m - knows t)], r(i \<mapsto> (done @ [Note l ty pt], todo, skipped)), s) \<in> reachable P"

| skip:  "\<lbrakk> (t, r, s) \<in> reachable P;
            r i = Some (done, Note l ty pt # todo, skipped)
          \<rbrakk> 
          \<Longrightarrow> (t,  r(i \<mapsto> (done @ [Note l ty pt], todo, insert (Note l ty pt) skipped)), s) \<in> reachable P"

| lkr:   "\<lbrakk> (t, r, s) \<in> reachable P;
            LKReveal a \<notin> set t
          \<rbrakk>
          \<Longrightarrow> (t @ [LKReveal a, Learns (longTermKeys a - knows t)], r, s) \<in> reachable P"

| send:  "\<lbrakk> (t, r, s) \<in> reachable P;
            r i = Some (done, Send l pt # todo, skipped);
            Some m = inst s i pt
          \<rbrakk>
          \<Longrightarrow> (t @ [Step (i, Send l pt), Learns (pairParts m - knows t)], r(i \<mapsto> (done @ [Send l pt], todo, skipped)), s) \<in> reachable P"
            
| recv:  "\<lbrakk> (t, r, s) \<in> reachable P;
            r i = Some (done, Recv l pt # todo, skipped);
            Some m = inst s i pt;
            m \<in> knows t
          \<rbrakk>
          \<Longrightarrow> (t @ [Step (i, Recv l pt)], r(i \<mapsto> (done @ [Recv l pt], todo, skipped)), s) \<in> reachable P"

| hash:  "\<lbrakk> (t, r, s) \<in> reachable P;
            m \<in> knows t;
            Hash m \<notin> knows t
          \<rbrakk>
          \<Longrightarrow> (t @ [Learns {Hash m}], r, s) \<in> reachable P"

| tuple: "\<lbrakk> (t, r, s) \<in> reachable P;
            x \<in> knows t;
            y \<in> knows t;
            Tup x y \<notin> knows t
          \<rbrakk>
          \<Longrightarrow> (t @ [Learns {Tup x y}], r, s) \<in> reachable P"

| encr:  "\<lbrakk> (t, r, s) \<in> reachable P;
            m \<in> knows t;
            k \<in> knows t;
            Enc m k \<notin> knows t
          \<rbrakk>
          \<Longrightarrow> (t @ [Learns {Enc m k}], r, s) \<in> reachable P"


| decr:  "\<lbrakk> (t, r, s) \<in> reachable P;
            Enc m k \<in> knows t;
            inv k \<in> knows t
          \<rbrakk>
          \<Longrightarrow> (t @ [Learns (pairParts m - knows t)], r, s) \<in> reachable P"

locale reachable_state =  wf_proto +
  fixes t :: explicit_trace
  and   r :: threadpool
  and   s :: store
  assumes reachable [simp,intro!]: "(t,r,s) \<in> reachable P"
begin
  text{* A local variant of the induction rule of @{term "reachable"}. *}
  lemmas reachable_induct = reachable.induct
    [ OF reachable
    , rule_format
    , consumes 0
    , case_names init compr skip lkr send recv hash tuple encr decr
    ]
end

text{* An extension of the reachable state locale denoting
       an individual thread and its state. *}

locale reachable_thread = reachable_state +
  fixes i       :: "tid"
    and "done"  :: "rolestep list"
    and todo    :: "rolestep list"
    and skipped :: "rolestep set" 
  assumes thread_exists: "r i = Some (done, todo, skipped)"
begin

text{* The thread state is built such that @{term "done @ todo"} is
         always a role of @{term P}. *}

lemma role_in_P:  "done @ todo \<in> P"
using thread_exists
proof (induct arbitrary: i "done" todo skipped rule: reachable_induct)
qed (fastforce split: if_splits)+

end

text{* Importing all lemmas of the wellformed role locale for
the term @{term "done @ todo"}. *}
sublocale reachable_thread \<subseteq> wf_role "done @ todo"
  by (rule wf_roles[OF role_in_P])



subsection{* Basic Properties *}

lemma knowsI: "\<lbrakk> Learns M \<in> set t; m \<in> M \<rbrakk> \<Longrightarrow> m \<in> knows t"
  by(induct t rule: knows.induct, auto)

lemma knowsD: "m \<in> knows t \<Longrightarrow> \<exists> M. Learns M \<in> set t \<and> m \<in> M"
  by(induct t rule: steps.induct, auto)

lemma knows_append [simp]: 
  "knows (xs@ys) = knows xs \<union> knows ys"
  by(induct xs rule: knows.induct, auto)

lemma stepsI: "Step estep \<in> set t \<Longrightarrow> estep \<in> steps t"
  by(induct t rule: steps.induct, auto)

lemma stepsD: "estep \<in> steps t \<Longrightarrow> Step estep \<in> set t"
  by(induct t rule: steps.induct, auto)

lemma Step_in_set_conv [simp]: 
  "(Step estep \<in> set t) = (estep \<in> steps t)"
  by(auto intro!: stepsI stepsD)

lemma steps_append [simp]: 
  "steps (t@t') = steps t \<union> steps t'"
  by(induct t rule: steps.induct, auto)

lemma lkrevealsI: "LKReveal a \<in> set t \<Longrightarrow> (Lit (EAgent a)) \<in> lkreveals t"
  by(induct t rule: lkreveals.induct, auto)

lemma lkrevealsD: "(Lit (EAgent a)) \<in> lkreveals t \<Longrightarrow> LKReveal a \<in> set t"
  by(induct t rule: lkreveals.induct, auto)

lemma Lkr_in_set_conv [simp]: 
  "(LKReveal a \<in> set t) = ((Lit (EAgent a)) \<in> lkreveals t)"
  by(auto intro!: lkrevealsI lkrevealsD)

lemma lkreveals_append [simp]: 
  "lkreveals (t@t') = lkreveals t \<union> lkreveals t'"
  by(induct t rule: lkreveals.induct, auto)

lemma lkreveals_agent: 
  "a \<in> lkreveals t \<Longrightarrow> \<exists> b. a = (Lit (EAgent b))"
  by(induct t rule: lkreveals.induct, auto)

subsection{* Thread Execution *}

lemma (in reachable_state) step_in_dom: 
  "(i, step) \<in> steps t \<Longrightarrow> i \<in> dom r"
proof (induct rule: reachable_induct) qed auto

lemma reveals_Nil[dest!]:
  "a \<in> reveals [] \<Longrightarrow> False"
by (auto)

lemma reveals_append [simp]:
  "reveals (xs@ys) = reveals xs \<union> reveals ys"
by(induct xs rule: reveals.induct, auto)

lemma RLKR_lkreveals_conv:
  "(RLKR a \<in> reveals t) = (a \<in> lkreveals t)"
proof(induct t rule: reveals.induct)
  case (1 i s xs)
  thus ?case by force
qed auto

lemma steps_to_reveals:
  "(i, Note l ty pt) \<in> steps t \<Longrightarrow> RCompr ty i \<in> reveals t"
by(induct t rule: reveals.induct) (auto)

lemma reveals_to_steps:
  "RCompr ty i \<in> reveals t \<Longrightarrow> \<exists> l pt. (i, Note l ty pt) \<in> steps t"
proof(induct t rule: reveals.induct)
  case (1 i' s xs)
  thus ?case by (cases s) auto
qed auto

lemma RCompr_steps_conv:
  "RCompr ty i \<in> reveals t = (\<exists> l pt. (i, Note l ty pt) \<in> steps t)"
by (fastforce intro: reveals_to_steps steps_to_reveals)

context reachable_thread
begin

lemma in_dom_r [iff]: "i \<in> dom r" 
  by (auto intro!: thread_exists)

lemma distinct_done [iff]: "distinct done"
  using distinct by auto

lemma skipped_in_done: 
  "step \<in> skipped \<Longrightarrow> step \<in> set done"
using thread_exists
proof (induct arbitrary: i "done" skipped todo rule: reachable_induct)
qed (auto split: if_splits)+

lemma distinct_todo [iff]: "distinct todo"
using distinct by auto


(*
 
 Proofs of the relationship between steps, skipped and done 

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

lemma note_in_skipped: 
  "\<lbrakk> step \<in> skipped \<rbrakk> \<Longrightarrow> 
   \<exists> l ty pt. (step = (Note l ty pt))"
using thread_exists
proof(induct arbitrary: i "done" todo skipped rule: reachable_induct)
  case init
  thus "?case" by fastforce
qed( auto split: if_splits)


lemma send_notin_skipped [iff]: 
  "Send l pt \<notin> skipped"
 by (auto dest!: note_in_skipped)

lemma recv_notin_skipped [iff]: 
  "Recv l pt \<notin> skipped"
 by (auto dest!: note_in_skipped)

lemma in_steps_conv_done_skipped:
  "(i, step) \<in> steps t = 
   (step \<in> set done \<and> step \<notin> skipped)"
using thread_exists
using distinct
proof(induct arbitrary: i "done" todo skipped rule: reachable_induct)
  case init thus ?case by fastforce
next 
  case (send t r s i "done" l pt todo skipped m i' done' todo' skipped')
  thus ?case
  proof(cases "i = i'")
    case True
    then interpret thread: 
      reachable_thread P t r s i "done" "Send l pt # todo" skipped'
      using send by unfold_locales auto
    show ?thesis 
      using send `i = i'` by fastforce 
  qed auto
next
  case (recv t r s i "done" l pt todo skipped m i' done' todo' skipped')
  thus ?case
  proof(cases "i = i'")
    case True
    then interpret thread: 
      reachable_thread P t r s i "done" "Recv l pt # todo" skipped'
      using recv by unfold_locales auto
    show ?thesis 
      using recv `i = i'` by fastforce
  qed auto
next
  case (compr t r s i "done" l ty pt todo skipped m i' done' todo' skipped')  
  thus ?case
  proof(cases "i = i'")
    case True
    thus ?thesis using compr `i = i'`
    proof(cases "step = Note l ty pt")
       case True
      interpret thread:
        reachable_thread P t r s i "done" "Note l ty pt # todo" skipped'
        using compr  `i = i'` by unfold_locales auto
      show ?thesis using compr  `i = i'` `step = Note l ty pt` by (fastforce dest: thread.skipped_in_done )
    qed fastforce
  qed auto
next
  case(skip t r s i "done" l ty pt todo skipped i' done' todo' skipped')
  thus ?case
  proof(cases "i = i'")
    case True
    thus ?thesis using skip `i = i'`
    proof(cases "step = Note l ty pt")
      case True
      interpret thread:
        reachable_thread P t r s i "done" "Note l ty pt # todo" skipped
        using skip  `i = i'` by unfold_locales auto
      show ?thesis using skip  `i = i'` `step = Note l ty pt` by fastforce
    qed fastforce
 qed auto
qed auto

lemma in_steps_recv:
  "((Recv l pt) \<in> set done) = ((i,Recv l pt) \<in> steps t)"
using thread_exists
proof(induct arbitrary: i "done" todo skipped rule rule: reachable_induct)
  case init
    thus "?case" by fastforce
qed ((unfold map_upd_Some_unfold)?, auto)+

lemma in_steps_send:
  "((Send l pt) \<in> set done) = ((i,Send l pt) \<in> steps t)"
using thread_exists
proof(induct arbitrary: i "done" todo skipped rule rule: reachable_induct)
  case init
    thus "?case" by fastforce
qed ((unfold map_upd_Some_unfold)?, auto)+

lemmas send_steps_in_done [elim!] = iffD1[OF in_steps_send, rule_format]
lemmas send_done_in_steps [elim!] = iffD2[OF in_steps_send, rule_format]
lemmas recv_steps_in_done [elim!] = iffD1[OF in_steps_recv, rule_format]
lemmas recv_done_in_steps [elim!] = iffD2[OF in_steps_recv, rule_format]


lemma in_steps_eq_in_done:
  "step \<notin> skipped \<Longrightarrow> ((i, step) \<in> steps t) = (step \<in> set done)" 
using thread_exists
by(auto simp add: in_steps_conv_done_skipped)

lemma todo_notin_doneD:
  "step \<in> set todo \<Longrightarrow> step \<notin> set done"
using distinct
using role_in_P
by(auto)

lemma done_notin_todoD:
  "step \<in> set done \<Longrightarrow> step \<notin> set todo"
using distinct
using role_in_P
by(auto)

lemma todo_notin_skippedD:
  "step \<in> set todo \<Longrightarrow> step \<notin> skipped"
using distinct
using role_in_P
by(fastforce dest: skipped_in_done)

lemma skipped_notin_todoD:
  "step \<in> skipped \<Longrightarrow> step \<notin> set todo"
using distinct
using role_in_P
by(fastforce dest: skipped_in_done)

lemma notin_steps_notin_trace:
  "(i, step) \<notin> steps t \<Longrightarrow> (Step (i, step)) \<notin> set t"
by(auto)

lemma in_steps_in_done:
  assumes inSteps:
    "(i, step) \<in> steps t"
  shows 
    "step \<in> set done"
proof(cases step)
  case (Send l pt)
    thus ?thesis using inSteps by (fastforce dest: in_steps_send[THEN iffD2])
next
  case (Recv l pt)
    thus ?thesis using inSteps by (fastforce dest: in_steps_recv[THEN iffD2])
next
  case (Note l ty pt)
    thus ?thesis using inSteps by (fastforce simp add: in_steps_conv_done_skipped)
qed


lemma step_notin_skippedD [dest]:
  "\<lbrakk> step \<in> skipped; (i, step) \<in> steps t \<rbrakk> \<Longrightarrow> False"
by(auto simp add: in_steps_conv_done_skipped)

lemma notin_skipped_notin_steps [dest]:
  "\<lbrakk> step \<in> set done; (i, step) \<notin> steps t; step \<notin> skipped \<rbrakk> \<Longrightarrow> False"
by(auto simp add: in_steps_conv_done_skipped)

lemma[dest]:
  "\<lbrakk> step \<in> set todo; step \<in> set done \<rbrakk> \<Longrightarrow> False"
by(fastforce dest: todo_notin_doneD)

lemma[dest]:
  "\<lbrakk> step \<in> set todo; step \<in> skipped \<rbrakk> \<Longrightarrow> False"
by(auto dest: todo_notin_skippedD)

lemma[dest]:
  "\<lbrakk> (i, step) \<notin>  steps t; (Step (i, step)) \<in> set t \<rbrakk> \<Longrightarrow> False"
by(auto)

lemma[dest]:
  "\<lbrakk> (i, step) \<in> steps t; (Step (i, step)) \<notin> set t \<rbrakk> \<Longrightarrow> False"
by(auto)

lemma listOrd_done_imp_listOrd_trace:
  assumes facts:
    "listOrd done prev step"
    "prev \<notin> skipped"
    "step \<notin> skipped" 
  shows stepOrd:
    "listOrd t (Step (i, prev)) (Step (i, step))"
using thread_exists
using facts
proof(induct arbitrary: i "done" todo skipped rule: reachable_induct)
  case (init r s i "done" todo) 
  thus ?case
    by fastforce
next
  case (send t r s i "done" l msg todo skipped m i' done' todo' skipped')
  thus ?case using send 
 proof(cases "i = i'")
    case True
      interpret this_thread:
          reachable_thread P t r s i' "done" "Send l msg # todo'" skipped'
          using send `i = i'` by unfold_locales auto
       show?thesis using send `i = i'`
          by fastforce
  qed fastforce
next
  case (recv t r s i "done" l msg todo skipped m i' done' todo' skipped')
  from recv show ?case 
  proof(cases "i = i'")
    case True
      interpret this_thread:
          reachable_thread P t r s i' "done" "Recv l msg # todo'" skipped'
          using recv `i = i'` by unfold_locales auto
       show ?thesis using recv `i = i'`
          by fastforce
  qed fastforce
next
  case (compr t r s i "done" l ty msg todo skipped m i' done' todo' skipped')
  from compr show ?case 
  proof(cases "i = i'")
    case True
      interpret this_thread:
          reachable_thread P t r s i' "done" "Note l ty msg # todo'" skipped'
          using compr `i = i'` by unfold_locales auto
       show ?thesis using compr `i = i'`
          by fastforce
  qed fastforce
next
  case (skip t r s i "done" l ty msg todo skipped i' done' todo' skipped') 
  from skip show ?case 
  proof(cases "i = i'")
    case True
    then interpret this_thread:
      reachable_thread P t r s i "done" "Note l ty msg # todo" skipped
      using skip `i = i'` by unfold_locales auto
    show ?thesis using skip `i = i'`
      by fastforce
  qed fastforce
qed auto

lemma listOrd_recv_role_imp_listOrd_trace:
  assumes facts:
    "(i, step) \<in> steps t"
    "listOrd (done @ todo) (Recv l pt) step"
  shows rtOrd:
    "listOrd t (Step (i, Recv l pt)) (Step (i, step))" 
using distinct
using facts
by(auto dest: in_set_listOrd1 todo_notin_doneD listOrd_done_imp_listOrd_trace in_set_listOrd2  listOrd_append[THEN iffD1] in_steps_conv_done_skipped[THEN iffD1])

lemma listOrd_send_role_imp_listOrd_trace:
  assumes facts:
    "(i, step) \<in> steps t"
    "listOrd (done @ todo) (Send l pt) step"
  shows stOrd:
    "listOrd t (Step (i, Send l pt)) (Step (i, step))" 
using distinct
using facts
by(auto dest: in_set_listOrd1 todo_notin_doneD listOrd_done_imp_listOrd_trace in_set_listOrd2  listOrd_append[THEN iffD1] in_steps_conv_done_skipped[THEN iffD1])

lemma roleOrd_notSkipped_imp_listOrd_trace:
  assumes facts:
    "(i, step) \<in> steps t"
    "step' \<notin> skipped"
    "listOrd (done @ todo)  step' step"
  shows
    "listOrd t (Step (i, step')) (Step  (i, step))"
using distinct
using facts
by(auto dest: in_set_listOrd1 todo_notin_doneD listOrd_done_imp_listOrd_trace in_set_listOrd2  listOrd_append[THEN iffD1] in_steps_conv_done_skipped[THEN iffD1])

end


subsection{* Variable Substitutions *}

context reachable_state
begin

lemma inst_AVar_cases: 
  "s (AVar v, i) \<in> Agent"
 by (induct rule: reachable_induct, auto)

lemma inst_AVar_in_IK0: 
 "s (AVar v, i) \<in> IK0"
using inst_AVar_cases[of v i] 
by (auto simp: IK0_def Agent_def)

lemma knows_IK0: "m \<in> IK0 \<Longrightarrow> m \<in> knows t"
 by(induct rule: reachable_induct, auto)

lemma inst_AVar_in_knows [iff]:
  "s (AVar a, i) \<in> knows t"
  by (rule knows_IK0[OF inst_AVar_in_IK0])

end (* reachable_state *)

lemma (in reachable_state) send_step_FV:
  assumes thread_exists: "r i = Some (done, Send l msg # todo, skipped)"
  and FV: "MVar n \<in> FV msg"
  shows "\<exists> l' msg'. (i, Recv l' msg') \<in> steps t \<and>  MVar n \<in> FV msg'"
proof -
  interpret this_thread: reachable_thread P t r s i "done" "Send l msg # todo" skipped
    using thread_exists by unfold_locales auto
  let ?role = "done @ Send l msg # todo"
  have "Send l msg \<in> set ?role" by simp
  then obtain l' msg' 
    where "listOrd ?role (Recv l' msg') (Send l msg)"
    and "MVar n \<in> FV msg'"
    using FV by(fast dest!: this_thread.Send_FV)
  thus ?thesis using this_thread.distinct
    by(auto dest: in_set_listOrd1 in_set_listOrd2)
qed

lemma (in reachable_state) note_step_FV:
  assumes thread_exists: "r i = Some (done, Note l ty msg # todo, skipped)"
  and FV: "MVar n \<in> FV msg"
  shows "\<exists> l' msg'. (i, Recv l'  msg') \<in> steps t \<and>  MVar n \<in> FV msg'"
proof -
  interpret this_thread: reachable_thread P t r s i "done" "Note l ty msg # todo" skipped
    using thread_exists by unfold_locales auto
  let ?role = "done @ Note l ty msg # todo"
  have "Note l ty msg \<in> set ?role" by simp
  then obtain l' msg' 
    where "listOrd ?role (Recv l' msg') (Note l ty msg)"
    and "MVar n \<in> FV msg'"
    using FV by(fast dest!: this_thread.Note_FV)
  thus ?thesis using this_thread.distinct
    by(auto dest: in_set_listOrd1 in_set_listOrd2)
qed


subsubsection{* The Effect of a Step on the Intruder Knowledge *}


context reachable_state
begin

lemma SendD: 
  "(i, Send lbl pt) \<in> steps t \<Longrightarrow> 
   (\<exists> m. Some m = inst s i pt \<and> m \<in> knows t)"
proof(induct rule: reachable_induct)
qed auto

end


subsection{* Almost Distinct Traces *}

fun distinct' :: "explicit_trace \<Rightarrow> bool"
where
  "distinct' [] = True"
| "distinct' (Learns M # t) =
     ((\<forall> m \<in> M. m \<notin> knows t) \<and> distinct' t)"
| "distinct' (Step estep # t) =
     ((estep \<notin> steps t) \<and> distinct' t)"
| "distinct' (LKReveal a # t) =
     (((Lit (EAgent a)) \<notin> lkreveals t) \<and> distinct' t)"


lemma distinct'_append [simp]:
  "distinct' (t@t') = 
   (distinct' t \<and> distinct' t' \<and> 
    (knows t \<inter> knows t' = {}) \<and> (steps t \<inter> steps t' = {}) \<and>
      (lkreveals t \<inter> lkreveals t') = {})"
proof (induct t rule: distinct'.induct)
qed (auto intro!: knowsI)

lemma distinct'_singleton [iff]: "distinct' [x]"
by (cases x) auto

lemma (in reachable_state) distinct'_trace [iff]:
  "distinct' t"
proof(induct arbitrary: i "done" todo skipped rule: reachable_induct)
  case (recv t r s i "done" l msg todo skipped)
  then interpret this_thread: 
    reachable_thread P t r s i "done" "Recv l msg # todo" skipped
    by unfold_locales auto
  show ?case using  `distinct' t` this_thread.distinct
    by(fastforce dest: this_thread.in_steps_in_done)
next
  case (send t r s i "done" l msg todo skipped m)
  then interpret this_thread: 
    reachable_thread P t r s i "done" "Send l msg # todo" skipped
    by unfold_locales auto
  show ?case using `distinct' t` and this_thread.distinct
    by(fastforce dest: this_thread.in_steps_in_done)
next
  case (compr t r s i "done" l ty msg todo skipped m)
  then interpret this_thread: 
     reachable_thread P t r s i "done" "Note l ty msg # todo" skipped
     by unfold_locales auto
  show ?case using `distinct' t` and this_thread.distinct
     by(fastforce dest: this_thread.in_steps_in_done)
next
  case (skip t r s i "done" l ty msg todo skipped)
  then interpret this_thread: 
     reachable_thread P t r s i "done" "Note l ty msg # todo" skipped
     by unfold_locales auto
  show ?case using `distinct' t` and this_thread.distinct
    by(auto)
qed auto


subsection{* Happens-Before Order *}

datatype event = St "tid \<times> rolestep" | Ln execmsg | LKR execmsg

fun predOrd :: "explicit_trace \<Rightarrow> event \<Rightarrow> event \<Rightarrow> bool"
where
  "predOrd []             x y = False"
| "predOrd (Learns M # xs) x y =
     ((x \<in> Ln ` M \<and> (y \<in> Ln ` knows xs \<or> y \<in> St ` steps xs \<or> y \<in> LKR ` lkreveals xs)) \<or>
      predOrd xs x y)"
| "predOrd (Step estep # xs) x y =
     ((x = St estep \<and> (y \<in> Ln ` knows xs \<or> y \<in> St ` steps xs \<or> y \<in> LKR ` lkreveals xs)) \<or>
      predOrd xs x y)"
| "predOrd (LKReveal a # xs) x y = 
     ((x = LKR (Lit (EAgent a)) \<and> (y \<in> Ln ` knows xs \<or> y \<in> St ` steps xs \<or> y \<in> LKR ` lkreveals xs)) \<or>
      predOrd xs x y)"

definition predEqOrd :: "explicit_trace \<Rightarrow> event \<Rightarrow> event \<Rightarrow> bool"
where "predEqOrd t x y = ((x = y) \<or> predOrd t x y)"


lemma predOrd_singleton [simp]: "\<not> predOrd [a] x y"
by (cases a) auto

lemma in_knows_predOrd1: "predOrd t (Ln x) y \<Longrightarrow> x \<in> knows t"
proof (induct t)
  case (Cons e t) thus ?case by (cases e) auto
qed auto

lemma in_knows_predOrd2: "predOrd t x (Ln y) \<Longrightarrow> y \<in> knows t"
proof (induct t)
  case (Cons e t) thus ?case by (cases e) auto
qed auto

lemma in_steps_predOrd1: "predOrd t (St x) y \<Longrightarrow> x \<in> steps t"
proof (induct t)
  case (Cons e t) thus ?case by (cases e) auto
qed auto

lemma in_steps_predOrd2: "predOrd t x (St y) \<Longrightarrow> y \<in> steps t"
proof (induct t)
  case (Cons e t) thus ?case by (cases e) auto
qed auto

lemma in_lkreveals_predOrd1: "predOrd t (LKR x) y \<Longrightarrow> x \<in> lkreveals t"
proof (induct t)
  case (Cons e t) thus ?case by (cases e) auto
qed auto

lemma in_lkreveals_predOrd2: "predOrd t x (LKR y) \<Longrightarrow> y \<in> lkreveals t"
proof (induct t)
  case (Cons e t) thus ?case by (cases e) auto
qed auto

lemma in_reveals_predOrd1:
  assumes facts: "predOrd t (St (i, st)) e"
                 "noteStep st"
  shows "RCompr (noteType st) i \<in> reveals t"
using facts
by(force dest: noteStepD intro: RCompr_steps_conv[THEN iffD2] in_steps_predOrd1)

lemma in_reveals_predOrd2:
  assumes facts: "predOrd t e (St (i, st))"
                 "noteStep st"
  shows "RCompr (noteType st) i \<in> reveals t"
using facts
by(force dest: noteStepD intro: RCompr_steps_conv[THEN iffD2] in_steps_predOrd2)

lemma note_in_reveals_predOrd1:
  assumes facts: "predOrd t (St (i, Note l ty pt)) e"
  shows "RCompr ty i \<in> reveals t"
using facts
by(force dest: noteStepD intro: RCompr_steps_conv[THEN iffD2] in_steps_predOrd1)

lemma note_in_reveals_predOrd2:
  assumes facts: "predOrd t e (St (i, Note l ty pt))"
  shows "RCompr ty i \<in> reveals t"
using facts
by(force dest: noteStepD intro: RCompr_steps_conv[THEN iffD2] in_steps_predOrd2)

lemma lkr_in_reveals_predOrd1:
  "predOrd t (LKR a) e \<Longrightarrow> RLKR a \<in> reveals t"
by(force intro: RLKR_lkreveals_conv[THEN iffD2] in_lkreveals_predOrd1)

lemma lkr_in_reveals_predOrd2:
  "predOrd t e (LKR a) \<Longrightarrow> RLKR a \<in> reveals t"
by(force intro: RLKR_lkreveals_conv[THEN iffD2] in_lkreveals_predOrd2)


lemmas event_predOrdI = 
  in_knows_predOrd1 in_knows_predOrd2 
  in_steps_predOrd1 in_steps_predOrd2

lemmas compr_predOrdI =
  lkr_in_reveals_predOrd1 lkr_in_reveals_predOrd2 
  note_in_reveals_predOrd1 note_in_reveals_predOrd2

lemma event_predOrdE:
  "\<lbrakk>predOrd t (Ln x) (Ln y);    \<lbrakk> x \<in> knows t; y \<in> knows t         \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (Ln x) (St b);    \<lbrakk> x \<in> knows t; b \<in> steps t         \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (St a) (Ln y);    \<lbrakk> a \<in> steps t; y \<in> knows t         \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (St a) (St b);    \<lbrakk> a \<in> steps t; b \<in> steps t         \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (LKR c) (Ln y);   \<lbrakk> RLKR c \<in> reveals t; y \<in> knows t     \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (LKR c) (St b);   \<lbrakk> RLKR c \<in> reveals t; b \<in> steps t     \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (St a) (LKR d);   \<lbrakk> a \<in> steps t; RLKR d \<in> reveals t     \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (Ln x) (LKR d);   \<lbrakk> x \<in> knows t; RLKR d \<in> reveals t     \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>predOrd t (LKR c) (LKR d);  \<lbrakk> RLKR c \<in> reveals t; RLKR d \<in> reveals t \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  by(fastforce intro: event_predOrdI compr_predOrdI)+


lemma predOrd_LKR_agent1:
  "predOrd t (LKR a) b \<Longrightarrow>  \<exists> c. a = (Lit (EAgent c))"
by(auto dest!: lkreveals_agent  RLKR_lkreveals_conv[THEN iffD1] dest: compr_predOrdI )

lemma predOrd_LKR_agent2:
  "predOrd t b (LKR a) \<Longrightarrow> \<exists> c. a = (Lit (EAgent c))"
by(auto dest!: lkreveals_agent  RLKR_lkreveals_conv[THEN iffD1] dest: compr_predOrdI )

lemma in_set_predOrd1: 
  "predOrd t x y \<Longrightarrow> x \<in> Ln ` knows t \<or> x \<in> St ` steps t \<or> x \<in> LKR ` lkreveals t"
by (induct t x y rule: predOrd.induct) auto

lemma in_set_predOrd2: 
  "predOrd t x y \<Longrightarrow> y \<in> Ln ` knows t \<or> y \<in> St ` steps t \<or> y \<in> LKR ` lkreveals t"
by (induct t x y rule: predOrd.induct) auto

lemma listOrd_imp_predOrd:
  "listOrd t (Step e) (Step e') \<Longrightarrow> predOrd t (St e) (St e')"
by (induct t rule: steps.induct) (auto dest!: stepsI)

lemma predOrd_append [simp]:
  "predOrd (xs@ys) x y = 
   (predOrd xs x y \<or> predOrd ys x y \<or>
   ((x \<in> Ln ` knows xs \<or> x \<in> St ` steps xs \<or> x \<in> LKR ` lkreveals xs) \<and> 
    (y \<in> Ln ` knows ys \<or> y \<in> St ` steps ys \<or> y \<in> LKR ` lkreveals ys)))"
  apply(induct xs x y rule: predOrd.induct)
  apply(simp_all)
  apply(blast+)
  done

lemma predOrd_distinct'_irr [simp]: 
  "distinct' t \<Longrightarrow> \<not>predOrd t x x"
  apply(induct t, auto)
  apply(case_tac x, auto)
  apply(case_tac a, auto)
  apply(case_tac a, auto)
  apply(case_tac a, auto)
  done

lemma predOrd_distinct'_trans: 
  "\<lbrakk> predOrd t x y; predOrd t y z; distinct' t \<rbrakk> 
   \<Longrightarrow> predOrd t x z"
  apply(induct t x y rule: predOrd.induct)
  apply(auto dest: in_set_predOrd1 in_set_predOrd2)
  done

lemma predOrd_distinct'_asymD: 
  "\<lbrakk> predOrd t x y; distinct' t \<rbrakk> \<Longrightarrow> \<not> predOrd t y x"
  apply(induct t x y rule: predOrd.induct)
  apply(auto dest: in_set_predOrd1 in_set_predOrd2)
  done


sublocale reachable_state \<subseteq> beforeOrd: order "predEqOrd t" "predOrd t"
  apply(unfold_locales)
  apply(auto simp: predEqOrd_def
          dest: predOrd_distinct'_asymD 
         intro: predOrd_distinct'_trans)
  done

abbreviation (in reachable_state)
  "pred'"   (infixl "\<prec>" 50) where "pred' \<equiv> predOrd t"

abbreviation (in reachable_state) 
  "predEq'" (infixl "\<preceq>" 50) where "predEq' \<equiv>  predEqOrd t"

lemma predOrd_conv:
  "predOrd xs x y = 
  (\<exists> ys zs. xs = ys @ zs \<and> 
            (x \<in> Ln ` knows ys \<or> x \<in> St ` steps ys \<or> x \<in> LKR ` lkreveals ys) \<and>
            (y \<in> Ln ` knows zs \<or> y \<in> St ` steps zs \<or> y \<in> LKR ` lkreveals zs))"
  (is "?pred xs = (\<exists> ys zs. ?decomp xs ys zs)")
proof -
  { assume "?pred xs"
    hence "\<exists> ys zs. ?decomp xs ys zs"
    proof (induct xs)
      case Nil thus ?case by simp
    next
      case (Cons e xs) thus ?case
      proof(cases e)
	case (Step st) thus ?thesis
	proof(cases "x = St st")
	  case True hence "?decomp (e#xs) [e] xs" 
	    using Step Cons by auto
	  thus ?thesis by blast
	next
	  case False
	  hence "predOrd xs x y"
	    using Step Cons by auto
	  then obtain ys zs where "?decomp xs ys zs"
	    using Cons by blast
	  hence "?decomp (e#xs) (e#ys) zs"
	    using Step Cons by auto
	  thus ?thesis by blast
	qed
      next
	case (Learns M) thus ?thesis
	proof(cases "\<exists> m \<in> M. x = Ln m")
	  case True 
	  then obtain m where "m \<in> M" and "x = Ln m"
	    by auto
	  hence "?decomp (e#xs) [e] xs" 
	    using Learns Cons by auto
	  thus ?thesis by blast
	next
	  case False
	  hence "predOrd xs x y"
	    using Learns Cons by auto
	  then obtain ys zs where "?decomp xs ys zs"
	    using Cons by blast
	  hence "?decomp (e#xs) (e#ys) zs"
	    using Learns Cons by auto
	  thus ?thesis by blast
	qed
      next
        case (LKReveal a) thus ?thesis
        proof(cases "x = LKR (Lit (EAgent a))")
          case True hence "?decomp (e#xs) [e] xs"
            using LKReveal Cons by auto
          thus ?thesis by blast
        next
          case False hence "predOrd xs x y"
            using LKReveal Cons by auto
          then obtain ys zs where "?decomp xs ys zs"
             using Cons by blast
          hence "?decomp (e#xs) (e#ys) zs"
             using LKReveal Cons by auto
          thus ?thesis by blast
        qed
      qed
    qed
  }
  moreover
  { assume "\<exists> ys zs. ?decomp xs ys zs"
    hence "?pred xs"
    proof (induct xs)
      case Nil thus ?case by simp
    next
      case (Cons e xs)
      then obtain ys zs where decomp1: "?decomp (e#xs) ys zs"
	by blast
      hence "ys = [] \<and> e # xs = zs \<or> (\<exists>ys'. e # ys' = ys \<and> xs = ys' @ zs)"
	(is "?nil \<or> ?non_nil")
	by (simp add: Cons_eq_append_conv)
      moreover
      { assume ?nil hence ?case using decomp1 by auto }
      moreover
      { assume ?non_nil
	then obtain ys' where decomp2: "ys = e # ys'" and "xs = ys' @ zs"
	  by auto
	hence ?case
	proof(cases e)
	  case (Step st) thus ?thesis
	  proof(cases "x = St st")
	    case True thus ?thesis
	      using Step decomp1 decomp2 by auto
	  next
	    case False
	    hence "?decomp xs ys' zs"
	      using Step decomp1 decomp2 by auto
	    hence "predOrd xs x y"
	      using Cons by auto
	    thus ?thesis
	      using Step by auto
	  qed
	next
	  case (Learns M) thus ?thesis
	  proof(cases "\<exists> m \<in> M. x = Ln m")
	    case True thus ?thesis
	      using Learns decomp1 decomp2 by auto
	  next
	    case False
	    hence "?decomp xs ys' zs"
	      using Learns decomp1 decomp2 by auto
	    hence "predOrd xs x y"
	      using Cons by auto
	    thus ?thesis
	      using Learns by auto
	  qed
        next
          case (LKReveal a) thus ?thesis
          proof(cases "x = LKR (Lit (EAgent a))")
            case True thus ?thesis
              using LKReveal decomp1 decomp2 by auto
          next
            case False
            hence "?decomp xs ys' zs"
              using LKReveal decomp1 decomp2 by auto
            hence "predOrd xs x y"
              using Cons by auto
            thus ?thesis 
              using LKReveal by auto
          qed
	qed
      }
      ultimately show ?case by fast
    qed
  }
  ultimately show ?thesis by fast
qed


subsection{* Input Terms *}


context reachable_state
begin

lemma knows_pairParts_closed:
  "m \<in> knows t \<Longrightarrow> pairParts m \<subseteq> knows t"
proof(induct arbitrary: m rule: reachable_induct)
  case init thus ?case by(auto simp: IK0_def) 
next
  case send thus ?case by(auto dest: pairParts_idemD)
next
  case decr thus ?case by(auto dest: pairParts_idemD)
next
  case tuple thus ?case by fastforce
next
  case lkr thus ?case by(auto simp: longTermKeys_def)
next
  case compr thus ?case by(auto dest: pairParts_idemD)
qed auto


lemmas knows_pairParts_closedD =
  subsetD[OF knows_pairParts_closed, rule_format]

lemmas rev_knows_pairParts_closedD =
  rev_subsetD[OF _ knows_pairParts_closed, rule_format]


lemma pairParts_before:
  "\<lbrakk> predOrd t (Ln m) y; m' \<in> pairParts m \<rbrakk> \<Longrightarrow>
   predOrd t (Ln m') y"
proof(induct rule: reachable_induct)
  case (hash t r s msg)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from hash show ?case
    by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (encr t r s msg key)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from encr show ?case
    by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (tuple t r s msg1 msg2)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from tuple show ?case
    by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (decr t r s msg key)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from decr show ?case
    by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (send t r s i "done" l msg todo msg)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from send show ?case
    by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (recv t r s i "done" l msg todo)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from recv show ?case
    by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (init r s) thus ?case by simp
next
  case (lkr t r s a)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from lkr show ?case
   by (fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (skip t r s i "done" l ty pt todo)
  then interpret s1: reachable_state P t r s 
    by unfold_locales
  from skip show ?case
    by(fastforce dest: s1.rev_knows_pairParts_closedD)
next
  case (compr t r s i "done" l ty pt todo skipped m)
  then interpret s1: reachable_state P t r s
    by unfold_locales
  from compr show ?case
    by(fastforce dest: s1.rev_knows_pairParts_closedD)
qed

lemma Ln_before_inp:
  "(i, Recv l pt) \<in> steps t \<Longrightarrow> 
   \<exists> m. Some m = inst s i pt \<and> Ln m \<prec> St (i, Recv l pt)"
  by (induct arbitrary: i l pt rule: reachable_induct) fastforce+

lemma Ln_before_inpE:
  "\<lbrakk> (i, Recv l pt) \<in> steps t;
     \<And> m. \<lbrakk> Some m = inst s i pt; Ln m \<prec> St (i, Recv l pt) \<rbrakk>
           \<Longrightarrow> Q
   \<rbrakk> \<Longrightarrow> Q"
  by (auto dest!: Ln_before_inp)

(*
lemmas knows_inp = in_knows_predOrd1[OF Ln_before_inp, rule_format]
*)

text{* Three of the lemmas for the reasoning technique. *}
lemmas Input = Ln_before_inp

lemma split_before:
  "Ln (Tup m m') \<prec> y \<Longrightarrow> Ln m \<prec> y \<and> Ln m' \<prec> y"
  by (fastforce intro: pairParts_before)

lemma split_knows:
  "Tup m m' \<in> knows t \<Longrightarrow> m \<in> knows t \<and> m' \<in> knows t"
  by (fastforce intro: knows_pairParts_closedD)
end

subsection{* Case Distinction on Learning Messages *}

text{* Note that the hints are logically equal to true. Thus they have no logical
  content. However they are placed here to track the individual cases when 
  computing the decryption chains for a concrete message and protocol.
*}

fun decrChain :: "string \<Rightarrow> explicit_trace \<Rightarrow> event set \<Rightarrow> execmsg \<Rightarrow> execmsg \<Rightarrow> bool"
where
  "decrChain path t from (Enc msg key) m = 
   ( ( m = Enc msg key \<and> (\<forall> f \<in> from. predOrd t f (Ln m)) \<and> 
       hint ''decrChainPath'' path
     ) \<or>
     ( (\<forall> f \<in> from. predOrd t f (Ln (Enc msg key))) \<and> 
       decrChain (path@''E'') t {Ln (Enc msg key), Ln (inv key)} msg m  )
   )"
| "decrChain path t from (Tup x y) m = 
   ( ( m = Tup x y \<and> (\<forall> f \<in> from. predOrd t f (Ln m)) \<and>
       hint ''decrChainPath'' path
     ) \<or>
     decrChain (path@''L'') t from x m \<or>
     decrChain (path@''R'') t from y m
   )"
| "decrChain path t from msg m =
   ( m = msg \<and> (\<forall> f \<in> from. predOrd t f (Ln m)) \<and>
     hint ''decrChainPath'' path
   )"

lemma decrChain_append:
  "decrChain path t from msg m \<Longrightarrow> decrChain path (t@t') from msg m"
  by (induct path t "from" msg m rule: decrChain.induct) auto

lemma decrChain_unpair:
  "\<lbrakk> m' \<in> pairParts m; m' \<in> M;
     \<forall> f \<in> from. f \<in> Ln ` knows t \<or> f \<in> St ` steps t
   \<rbrakk> \<Longrightarrow> decrChain path (t@[Learns M]) from m m'"
by (induct m arbitrary: path M) (auto simp: remove_hints)

lemma decrChain_decrypt:
  "\<lbrakk> decrChain path t from msg (Enc m k);
     Enc m k \<in> knows t; inv k \<in> knows t;
     m' \<in> pairParts m; m' \<notin> knows t \<rbrakk> \<Longrightarrow>
   decrChain path' (t @ [Learns (pairParts m - knows t)]) from msg m'"
proof(induct msg arbitrary: path path' "from")
  case (Enc msg key)
  hence from_before [simp]: 
    "\<forall>f\<in>from. predOrd t f (Ln (Enc msg key))" by auto
  have "m = msg \<and> k = key \<or> 
    decrChain (path@''E'') t {Ln (Enc msg key), Ln (inv key)} msg (Enc m k)"
    (is "?here \<or> ?nested")
    using Enc by auto
  moreover
  { assume "?here"
    hence "?case"
    proof(cases "m' = Enc m k")
      case True thus ?thesis
	using `?here` Enc by fastforce
    next
      case False thus ?thesis
	using `?here` Enc
	by(auto intro!: decrChain_unpair)
    qed
  }
  moreover
  { assume "?nested"
    hence "?case" using Enc
      by (fastforce dest!: Enc(2))
  }
  ultimately show ?case by fast
qed auto


lemma (in reachable_state) knows_cases_raw:
  assumes knows: "m' \<in> knows t"
  shows 
   "(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 (Lit (EAgent a)) \<prec> Ln m')
   "
  (is "?cases m' t r s")
proof -
  --{* Prove cases transfer lemma for trace extension *}
  { fix m' t t' r s
    let ?thesis = "?cases m' (t@t') r s"
    assume "?cases m' t r s" 
    (is "?ik0 \<or> ?hash \<or> ?enc \<or> ?tup \<or> ?chain t r s \<or> ?note t r s \<or> ?keys")
    moreover
    { assume "?ik0"  hence "?thesis" by blast }    moreover
    { assume "?hash" hence "?thesis" by fastforce } moreover
    { assume "?enc"  hence "?thesis" by fastforce } moreover
    { assume "?tup"  hence "?thesis" by fastforce } moreover
    { assume "?chain t r s"
      hence "?chain (t@t') r s" 
	by (fastforce intro!: decrChain_append)
      hence "?thesis" by blast
    } moreover
    { assume "?note t r s"
      hence "?note (t@t') r s" 
	by (fastforce intro!: decrChain_append)
      hence "?thesis" by blast
    } moreover
    { assume "?keys" hence "?thesis" by auto }
    ultimately have ?thesis by fast
  }
  note cases_appendI_trace = this

  --{* Prove actual thesis *}
  from knows show ?thesis
  proof (induct arbitrary: m' rule: reachable_induct)
    case init thus ?case by simp
  next
    case (hash t r s m)
    let ?t' = "t @ [Learns {Hash m}]"
    note IH = hash(2)
    have "m' \<in> knows t \<or> m' = Hash m" (is "?old \<or> ?new")
      using hash by fastforce
    moreover
    { assume "?new" hence ?case 
	using `m \<in> knows t` by fastforce 
    }
    moreover
    { assume "?old" 
      hence ?case by (fastforce intro!: IH cases_appendI_trace)
    }
    ultimately show ?case by fast
  next
    case (encr t r s m k)
    let ?t' = "t @ [Learns {Enc m k}]"
    note IH = encr(2)
    have "m' \<in> knows t \<or> m' = Enc m k" (is "?old \<or> ?new")
      using encr by fastforce
    moreover
    { assume "?new" hence ?case 
	using `m \<in> knows t` and `k \<in> knows t` by fastforce 
    }
    moreover
    { assume "?old" 
      hence ?case by (fast intro!: IH cases_appendI_trace)
    }
    ultimately show ?case by fast
  next
    case (tuple t r s x y)
    let ?t' = "t @ [Learns {Tup x y}]"
    note IH = tuple(2)
    have "m' \<in> knows t \<or> m' = Tup x y" (is "?old \<or> ?new")
      using tuple by fastforce
    moreover
    { assume "?new" hence ?case 
	using `x \<in> knows t` and `y \<in> knows t` by fastforce 
    }
    moreover
    { assume "?old" 
      hence ?case by (fast intro!: IH cases_appendI_trace)
    }
    ultimately show ?case by fast
  next
    case (recv t r s i "done" l pt todo skipped)
    hence "?cases m' t r s" 
      (is "?ik0 \<or> ?hash \<or> ?enc \<or> ?tup \<or> ?chain t r s \<or> ?note t r s \<or> ?keys")
      by clarsimp
    moreover
    { assume "?ik0"   hence "?case" by blast    } moreover
    { assume "?hash"  hence "?case" by fastforce } moreover
    { assume "?enc"   hence "?case" by fastforce } moreover
    { assume "?keys"  hence "?case" by fastforce } moreover
    { assume "?tup"   hence "?case" by fastforce } moreover
    { let ?t' = "t@[Step (i, Recv l pt)]"
      and ?r' = "r(i \<mapsto> (done @ [Recv l pt], todo, skipped))"
      assume "?chain t r s" then
      obtain i' done' todo' l' pt' skipped' m
        where thread': "r i' = Some (done', todo', skipped')"
        and send: "Send l' pt' \<in> set done'"
        and msg:  "Some m = inst s i' pt'"
        and chain:"decrChain [] t {St (i', Send l' pt')} m m'"
        by auto
      then interpret th1: reachable_thread P t r s i' done' todo' skipped'
        using recv by unfold_locales auto
        obtain done'' todo'' skipped''
        where "Send l' pt' \<in> set done''"
        and "?r' i' = Some (done'', todo'', skipped'')"
        using `r i = Some (done, Recv l pt # todo, skipped)` thread' send
        by (cases "i = i'") (fastforce+)
      hence "?chain ?t' ?r' s"
        using chain msg
        by (fast intro!: decrChain_append)
      hence "?case" by auto
    } moreover
    { let ?t' = "t@[Step (i, Recv l pt)]"
      and ?r' = "r(i \<mapsto> (done @ [Recv l pt], todo, skipped))"
      assume "?note t r s" then
      obtain i' done' todo' skipped' l' ty' pt' m
        where thread': "r i' = Some (done', todo', skipped')"
        and inDone: "Note l' ty' pt' \<in> set done'"
        and notSkipped: "Note l' ty' pt' \<notin> skipped'"
        and msg: "Some m = inst s i' pt'"
        and chain: "decrChain [] t {St (i', Note l' ty' pt')} m m'"
        by auto
      then interpret th1: reachable_thread P t r s i' done' todo' skipped'
        using recv by unfold_locales auto
      obtain done'' todo'' skipped''
        where "Note l' ty' pt' \<in> set done''"
        and "Note l' ty' pt' \<notin> skipped'' "
        and "?r' i' = Some (done'', todo'', skipped'')"
        using `r i = Some (done, Recv l pt # todo, skipped)` thread' inDone notSkipped
        by (cases "i = i'") (fastforce+)
      hence "?note ?t' ?r' s" using msg chain notSkipped inDone
        by (fast intro!: decrChain_append)
      hence "?case" by auto
    }
    ultimately show ?case by fastforce
  next
    case (send t r s i "done" l pt todo skipped m)
    then interpret th1: 
      reachable_thread P t r s i "done" "Send l pt # todo" skipped
      by unfold_locales
    let ?r' = "r(i \<mapsto> (done @ [Send l pt], todo, skipped))"
    let ?t' = "(t @ [Step (i, Send l pt)]) @ [Learns (pairParts m - knows t)]"
    have "m' \<in> knows t \<or> m' \<in> pairParts m \<and> m' \<notin> knows t \<and> Some m = inst s i pt" 
      (is "?old \<or> ?new")
      using send by fastforce
    moreover
    { assume "?new"
      hence "decrChain [] ?t' {St (i, Send l pt)} m m'"
	by (fastforce intro!: decrChain_unpair)
      moreover
      have "?r' i = Some (done @ [Send l pt], todo, skipped)"
	using th1.thread_exists by auto
      ultimately
      have ?case using `Some m = inst s i pt`
        apply-
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI1)
        apply(fastforce)
	done
    }
    moreover
    { assume "?old" 
      hence "?cases m' t r s" 
        (is "?ik0 \<or> ?hash \<or> ?enc \<or> ?tup \<or> ?chain t r s \<or> ?note t r s \<or> ?keys")
	using send by clarsimp
      moreover
      { assume "?ik0"   hence "?case" by blast    } moreover
      { assume "?hash"  hence "?case" by fastforce } moreover
      { assume "?enc"   hence "?case" by fastforce } moreover
      { assume "?keys"  hence "?case" by fastforce } moreover
      { assume "?tup"   hence "?case" by fastforce } moreover
      { assume "?chain t r s" then
	obtain i' done' todo' l' pt' skipped' m
	  where thread': "r i' = Some (done', todo',skipped')"
	  and send: "Send l' pt' \<in> set done'"
          and msg:  "Some m = inst s i' pt'"
	  and chain: "decrChain [] t {St (i', Send l' pt')} m m'"
	  by auto
	obtain done'' todo'' skipped''
	  where "Send l' pt' \<in> set done''"
	  and "(r(i \<mapsto> (done @ [Send l pt], todo, skipped))) i' = Some (done'', todo'',skipped'')"
	  using `r i = Some (done, Send l pt # todo, skipped)` thread' send
	  by (cases "i = i'") (fastforce+)
	hence "?chain ?t' ?r' s"
	  using chain msg
          by (fast intro!: decrChain_append)
	hence "?case" by auto
      } moreover
      { assume "?note t r s" then
        obtain i' done' todo' skipped' l' ty' pt' m
	  where thread': "r i' = Some (done', todo', skipped')"
	  and inDone: "Note l' ty' pt' \<in> set done'"
          and notSkipped: "Note l' ty' pt' \<notin> skipped'"
          and msg: "Some m = inst s i' pt'"
	  and chain: "decrChain [] t {St (i', Note l' ty' pt')} m m'"
          by auto
        obtain done'' todo'' skipped''
	  where "Note l' ty' pt' \<in> set done''"
          and "Note l' ty' pt' \<notin> skipped'' "
	  and "?r' i' = Some (done'', todo'', skipped'')"
	  using `r i = Some (done, Send l pt # todo, skipped)` thread' inDone notSkipped
	  by (cases "i = i'") (fastforce+)
        hence "?note ?t' ?r' s" using chain notSkipped inDone msg
 	  by(fast intro!: decrChain_append)
        hence "?case" by auto
       }
      ultimately have ?case by fast
    }
    ultimately show ?case by fast
  next
    case (decr t r s m k)
    then interpret s1: reachable_state P t r s
      by unfold_locales
    let ?t' = "t @ [Learns (pairParts m - knows t)]"
    note IH = decr(2)
    have "m' \<in> knows t \<or> m' \<in> pairParts m \<and> m' \<notin> knows t" 
      (is "?old \<or> ?new")
      using decr by fastforce
    moreover
    { assume "?new"
      hence "m' \<in> pairParts m" and "m' \<notin> knows t" by auto
      hence 
	"(predOrd t (Ln m) (Ln (Enc m k)) \<and> predOrd t (Ln k) (Ln (Enc m k))) \<or>
         ((\<exists>i done todo skipped. r i = Some (done, todo,skipped) \<and>
          (\<exists>l pt ms. Send l pt \<in> set done \<and> Some ms = inst s i pt \<and> 
                    decrChain [] t {St (i, Send l pt)} ms (Enc m k)))) \<or>
         ((\<exists>i done todo skipped. r i = Some (done, todo,skipped) \<and>
          (\<exists>l ty pt ms. Note l ty pt \<in> set done \<and> Note l ty pt \<notin> skipped \<and>
                       Some ms = inst s i pt \<and> 
                  decrChain [] t {St (i, Note l ty pt)} ms (Enc m k))))"
	(is "?fake_enc \<or> ?decchain t (Enc m k) \<or> ?notechain t (Enc m k)")
	using IH[OF `Enc m k \<in> knows t`] by auto
      moreover
      { assume "?fake_enc"
	hence "?case" using `?new`
	  by (auto dest!: in_knows_predOrd1 s1.rev_knows_pairParts_closedD)
      }
      moreover
      { assume "?decchain t (Enc m k)" then
	obtain i' done' todo' l' pt' skipped' ms
	  where thread': "r i' = Some (done', todo',skipped')"
	  and send: "Send l' pt' \<in> set done'"
          and msg:  "Some ms = inst s i' pt'"
	  and chain: "decrChain [] t {St (i', Send l' pt')} ms (Enc m k)"
	  by auto
	moreover
	hence "decrChain [] ?t' {St (i', Send l' pt')} ms m'"
	  using `?new` `Enc m k \<in> knows t` `inv k \<in> knows t`
	  by (fastforce intro!: decrChain_decrypt)
	ultimately
	have "?decchain ?t' m'" by fastforce
	hence "?case" by blast
      }
      moreover
      { assume "?notechain t (Enc m k)" then
	obtain i' done' todo' l' ty' pt' skipped' ms
	  where thread': "r i' = Some (done', todo',skipped')"
	  and inDone: "Note l' ty' pt' \<in> set done'"
          and notSkipped: "Note l' ty' pt' \<notin>  skipped'"
          and msg:   "Some ms = inst s i' pt'"
	  and chain: "decrChain [] t {St (i', Note l' ty' pt')} ms (Enc m k)"
	  by auto
	moreover
	hence "decrChain [] ?t' {St (i', Note l' ty' pt')} ms m'"
	  using `?new` `Enc m k \<in> knows t` `inv k \<in> knows t`
	  by (fastforce intro!: decrChain_decrypt)
	ultimately
	have "?notechain ?t' m'" by fastforce
	hence "?case" by blast
      }
      ultimately have ?case by fast
    }
    moreover
    { assume "?old" 
      hence ?case by (fast intro!: IH cases_appendI_trace)
    }
    ultimately show ?case by fast thm decr
  next
    case(lkr t r s a)
    then interpret s1: reachable_state P t r s
      by unfold_locales
    let ?t' = "t @ [ LKReveal a, Learns (longTermKeys a - knows t)]"
    note IH = lkr(2)
    have "m' \<in> knows t \<or> m' \<in> longTermKeys a \<and> m' \<notin> knows t" 
      (is "?old \<or> ?new")
    using lkr by fastforce
    moreover 
    {
      assume "?old"
      hence "?case" by (fast intro!: IH cases_appendI_trace)
    }
    moreover
    {
      assume "?new"
      hence ?case by (auto simp: longTermKeys_def)
    }
    ultimately show "?case" by fast
  next
   case (skip t r s i "done" l ty pt todo skipped)
   then interpret this_thread:  reachable_thread P t r s i "done" "Note l ty pt # todo" skipped  by unfold_locales
   let ?r' = "r(i \<mapsto> (done @ [Note l ty pt], todo, insert (Note l ty pt) skipped))"
   have "m' \<in> knows t" using skip by fastforce
   hence "?cases m' t r s" 
     (is "?ik0 \<or> ?hash \<or> ?enc \<or> ?tup \<or> ?chain t r s \<or> ?note t r s \<or> ?keys")
     using skip by clarsimp
   moreover
   { assume "?ik0"   hence "?case" by blast    } moreover
   { assume "?hash"  hence "?case" by fastforce } moreover
   { assume "?enc"   hence "?case" by fastforce } moreover
   { assume "?keys"  hence "?case" by fastforce } moreover
   { assume "?tup"   hence "?case" by fastforce } moreover
   { assume "?chain t r s" then
     obtain i' done' todo' l' pt' skipped' m
       where thread': "r i' = Some (done', todo',skipped')"
       and send: "Send l' pt' \<in> set done'"
       and msg: "Some m = inst s i' pt'"
       and chain: "decrChain [] t {St (i', Send l' pt')} m m'"
       by auto
     obtain done'' todo'' skipped''
       where "Send l' pt' \<in> set done''"
       and "?r' i' = Some (done'', todo'',skipped'')"
       using skip(3) thread' send
       by (cases "i = i'") (fastforce+)
     hence "?chain t ?r'  s"
       using chain msg by fast
     hence "?case" by auto
   }
   moreover
   { assume "?note t r s" then
     obtain i' done' todo' skipped' l' ty' pt' m
       where thread': "r i' = Some (done', todo', skipped')"
       and inDone: "Note l' ty' pt' \<in> set done'"
       and notSkipped: "Note l' ty' pt' \<notin> skipped'"
       and msg:   "Some m = inst s i' pt'"
       and chain: "decrChain [] t {St (i', Note l' ty' pt')} m m'"
       by auto
      obtain done'' todo'' skipped''
       where "Note l' ty' pt' \<in> set done''"
       and "Note l' ty' pt' \<notin> skipped'' "
       and "?r' i' = Some (done'', todo'', skipped'')"
       using `r i = Some (done, Note l ty pt # todo, skipped)` thread' inDone notSkipped
       by (cases "i = i'") (force dest: this_thread.done_notin_todoD)+
     hence "?note t ?r' s" 
       using chain notSkipped inDone msg
       by fast
     hence "?case" by auto
   } moreover
   { assume "?keys" hence "?case" by fastforce }
   ultimately  
   show  "?case" by fastforce
  next
   case(compr t r s i "done" l ty pt todo skipped m m')
   then interpret th1: 
      reachable_thread P t r s i "done" "Note l ty pt # todo" skipped
      by unfold_locales
    let ?r' = "r(i \<mapsto> (done @ [Note l ty pt], todo, skipped))"
    let ?t' = "(t @ [Step (i, Note l ty pt)]) @ [Learns (pairParts m - knows t)]"
    have "m' \<in> knows t \<or> m' \<in> pairParts m \<and> m' \<notin> knows t \<and> Some m = inst s i pt" 
      (is "?old \<or> ?new")
      using compr by fastforce
    moreover
    { assume "?new"
  (*
        hence "m' \<in> pairParts (inst s i pt)" and "m' \<notin> knows t" using `m = inst s i pt` 
      by auto
*)
        hence "decrChain [] ?t' {St (i, Note l ty pt)} m m'" 
          by (fastforce intro!: decrChain_unpair)
      moreover
        have "?r' i = Some (done @ [Note l ty pt], todo, skipped)" 
          using th1.thread_exists by auto
      moreover
        have "Note l ty pt \<in> set (Note l ty pt # todo)" 
          using th1.thread_exists by auto
        hence "Note l ty pt \<notin> skipped" 
          by (fastforce dest: th1.todo_notin_skippedD)
      ultimately
      have ?case using `Some m = inst s i pt`
	apply-
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI2)
        apply(rule disjI1)
        by force
    }
    moreover
    { assume "?old" 
      hence "?cases m' t r s" 
        (is "?ik0 \<or> ?hash \<or> ?enc \<or> ?tup \<or> ?chain t r s \<or> ?note t r s \<or> ?keys")
	using compr by clarsimp
      moreover
      { assume "?ik0"   hence "?case" by blast    } moreover
      { assume "?hash"  hence "?case" by fastforce } moreover
      { assume "?enc"   hence "?case" by fastforce } moreover
      { assume "?keys"  hence "?case" by fastforce } moreover
      { assume "?tup"   hence "?case" by fastforce } moreover
      { assume "?chain t r s" then
	obtain i' done' todo' l' pt' skipped' m
	  where thread': "r i' = Some (done', todo',skipped')"
	  and send: "Send l' pt' \<in> set done'"
          and msg:  "Some m = inst s i' pt'"
	  and chain: "decrChain [] t {St (i', Send l' pt')} m m'"
	  by auto
	obtain done'' todo'' skipped''
	  where "Send l' pt' \<in> set done''"
	  and "(r(i \<mapsto> (done @ [Note l ty pt], todo, skipped))) i' = Some (done'', todo'',skipped'')"
	  using compr(3) thread' send
	  by (cases "i = i'") (fastforce+)
	hence "?chain ?t' ?r' s" using chain msg
          by(fast intro!: decrChain_append)
	hence "?case"  by auto
      } moreover
      { assume "?note t r s" then
        obtain i' done' todo' skipped' l' ty' pt' m
	  where thread': "r i' = Some (done', todo', skipped')"
	  and inDone: "Note l' ty' pt' \<in> set done'"
          and notSkipped: "Note l' ty' pt' \<notin> skipped'"
          and msg:   "Some m = inst s i' pt'"
	  and chain: "decrChain [] t {St (i', Note l' ty' pt')} m m'"
          by auto
        obtain done'' todo'' skipped''
	  where "Note l' ty' pt' \<in> set done''"
          and "Note l' ty' pt' \<notin> skipped'' "
	  and "?r' i' = Some (done'', todo'', skipped'')"
	  using `r i = Some (done, Note l ty pt # todo, skipped)` thread' inDone notSkipped
	  by (cases "i = i'") (fastforce+)
        hence "?note ?t' ?r' s"
          using chain notSkipped inDone msg
          by(fast intro!: decrChain_append)
        hence "?case" by auto
       }
      ultimately have ?case by fast
    }
    ultimately show ?case by fast
  qed
qed

end