Theory SD_Incomplete

section ‹Secret Directed Unwinding Incompleteness example›

text ‹Demonstrating a counterexample which is secure but fails in the infinatary unwinding›
theory SD_Incomplete
  imports SD_Unwinding
begin


no_notation bot ("⊥")

(* This will be used for non-informative entities, e.g., a noninformative output: *)
abbreviation noninform ("⊥") where "⊥ ≡ undefined"


datatype State = s0 | s0' | s1 | s1' | s2 
type_synonym secret = "State"

fun transit::"State ⇒ State ⇒ bool"(infix "→I" 55) where 
  "transit s s' = 

      (if (s = s0 ∧ s' = s1) ∨
          (s = s1 ∧ s' = s2) ∨
          (s = s0' ∧ s' = s1') ∨
          (s = s1' ∧ s' = s2) then True 
      else False)"
(*s0 → s1 → s2*)
lemma transit_s0_s1:"s0 →I s1" by auto
lemma transit_s1_s2:"s1 →I s2" by auto


(*s0' → s1' → s2*)
lemma transit_s0'_s1':"s0' →I s1'" by auto
lemma transit_s1'_s2:"s1' →I s2" by auto

lemma transit_iff:"s →I s' ⟷ (s = s0 ∧ s' = s1) ∨
          (s = s1 ∧ s' = s2) ∨
          (s = s0' ∧ s' = s1') ∨
          (s = s1' ∧ s' = s2)" by auto

definition "final x ≡ ∀y. ¬ (→I) x y"

lemma final_s2[simp]:"final s2" unfolding final_def transit_iff by auto

lemma final_iff: "final s ⟷ s = s2" unfolding final_def transit_iff by (auto,metis State.exhaust)

text ‹Vanilla-semantics system model›
type_synonym stateV = State
fun validTransV where "validTransV (s,s') = s →I s'"

text ‹Secrets at initial states, interaction at everywhere besides final (i.e. s2)›
fun isIntV :: "stateV ⇒ bool" where "isIntV s = (s ≠ s2)"

(*need:
  1) getAct s0 = getAct s0' 
  2) getObs s0 ≠ getObs s0'
  3) getAct s1 ≠ getAct s1' *)
fun getIntV :: "stateV ⇒ nat × nat" where 
"getIntV s = 
 (case s of 
    s0  ⇒ (1, 0)
   |s0' ⇒ (1, 1)
   |s1  ⇒ (0, ⊥)
   |s1' ⇒ (1, ⊥)
   |_ ⇒ (⊥,⊥)
 )"

definition isSecV :: "stateV ⇒ bool" where "isSecV s = (s ∈ {s0, s0'})"
fun getSecV :: "stateV ⇒ secret" where "getSecV s = s"

lemma getSecV_neq: "getSecV s0 ≠ getSecV s0'" by auto

(* *)

text ‹The optimization-enhanced system model›

type_synonym stateO = State
fun validTransO where "validTransO (s,s') = s →I s'"

text ‹Secrets and interaction at initial states›
fun isIntO :: "stateO ⇒ bool" where "isIntO s = (s ∈ {s0, s0'})"


(*need:
  1) getAct s0 = getAct s0' 
  2) getObs s0 ≠ getObs s0'
  3) getAct s1 ≠ getAct s1' *)
fun getIntO :: "stateO ⇒ nat × nat" where 
"getIntO s = 
 (case s of 
    s0  ⇒ (1, 0)
   |s0' ⇒ (1, 1)
   |_ ⇒ (⊥,⊥)
 )"

definition isSecO :: "stateO ⇒ bool" where "isSecO s = (s ∈ {s0, s0'})"
lemma isSec0[simp]:"isSecO s0" unfolding isSecO_def by auto
lemma isSec1[simp]:"¬isSecO s1" unfolding isSecO_def by auto

lemma isSec0'[simp]:"isSecO s0'" unfolding isSecO_def by auto
lemma isSec1'[simp]:"¬isSecO s1'" unfolding isSecO_def by auto

fun getSecO :: "stateO ⇒ secret" where "getSecO s = s"

text ‹corrState›
fun corrState :: "stateV ⇒ stateO ⇒ bool" where 
"corrState cfgO cfgA = True"

interpretation Rel_Sec 
  where validTransV = validTransV and istateV = "λs. s = s0 ∨ s = s0'" 
  and finalV = final 
  and isSecV = isSecV and getSecV = getSecV
  and isIntV = isIntV and getIntV = getIntV
  (* *)
  and validTransO = validTransO and istateO = "λs. s = s0 ∨ s = s0'"
  and finalO = final
  and isSecO = isSecO  and getSecO = getSecO
  and isIntO = isIntO and getIntO = getIntO
  and corrState = corrState 
  apply(unfold_locales)
  subgoal by (auto simp: final_def)
  subgoal by (auto simp: final_iff)
  subgoal by (auto simp: final_iff isSecV_def)
  subgoal by (auto simp: final_def)
  subgoal by (auto simp: final_iff)
  subgoal by (auto simp: final_iff isSecO_def) .


lemma getAct0:"getActO s0 = getActO s0'" unfolding Opt.getAct_def by auto
lemma getObs0:"getObsO s0 ≠ getObsO s0'" unfolding Opt.getObs_def by auto


lemma getActV0:"getActV s0 = getActV s0'" unfolding Van.getAct_def by auto
lemma getObsV0:"getObsV s0 ≠ getObsV s0'" unfolding Van.getObs_def by auto


lemma getAct1:"getActV s1 ≠ getActV s1'" unfolding Van.getAct_def by auto

(*transition*)
lemma validFromO:"Opt.lvalidFromS s0 [[s0, s1, s2]]" unfolding Opt.lvalidFromS_def Opt.lvalidS_def apply clarsimp
  subgoal for i by(cases i, simp_all add: eSuc_def) .

lemma validFromO':"Opt.lvalidFromS s0' [[s0', s1', s2]]" unfolding Opt.lvalidFromS_def Opt.lvalidS_def apply clarsimp
  subgoal for i by(cases i, simp_all add: eSuc_def) .

lemma validTrFinite:"Van.lvalidFromS s0 tr1 ⟹ lfinite tr1"
  unfolding Van.lvalidFromS_def Van.lvalidS_def  
  by (auto,metis State.distinct enat_ord_code(4) idiff_infinity llength_eq_infty_conv_lfinite )


lemma validTrFinite':"Van.lvalidFromS s0' tr1 ⟹ lfinite tr1"
  unfolding Van.lvalidFromS_def Van.lvalidS_def 
  by (auto,metis State.distinct enat_ord_code(4) idiff_infinity llength_eq_infty_conv_lfinite )



lemma validOptTrFinite:"Opt.lvalidFromS s0 tr1 ⟹ lfinite tr1"
  unfolding Opt.lvalidFromS_def Opt.lvalidS_def
  by (auto,metis State.distinct enat_ord_code(4) idiff_infinity llength_eq_infty_conv_lfinite )



lemma validOptTrFinite':"Opt.lvalidFromS s0' tr1 ⟹ lfinite tr1"
  unfolding Opt.lvalidFromS_def Opt.lvalidS_def 
  by (auto,metis State.distinct enat_ord_code(4) idiff_infinity llength_eq_infty_conv_lfinite )



lemma enat_reduce: "enat i < enat x ⟹ i < x" by simp
(*infer traces*)
find_theorems lnth
lemma tr1_shape_s0_aux:"Van.lvalidFromS s0 tr1 ⟹ lcompletedFromO s0 tr1 ⟹ tr1 = [[s0, s1, s2]]"  
  unfolding Opt.lcompletedFrom_def apply(erule impE)
  subgoal by(simp add: validTrFinite)
  apply(frule validTrFinite)
  unfolding Van.lvalidFromS_def Van.lvalidS_def final_iff 
  apply(cases tr1, auto split: if_splits)
  subgoal for tr1' 
    apply(unfold nth_list_of[symmetric, of tr1'])
    apply(unfold nth_list_of[symmetric, of "(s0 $ tr1')", unfolded lfinite_LCons])
    apply(unfold length_list_of[symmetric])
    apply(cases tr1', simp)
    subgoal premises p 
      using p apply-apply(erule allE[of _ 0], simp split: if_splits)
      using p apply-apply(erule allE[of _ 1], simp split: if_splits)
      using p apply-apply(erule allE[of _ 2], simp split: if_splits)
    by (metis Suc_length_conv length_0_conv less_Suc0 lfinite.simps linorder_neqE_nat list.distinct(1) list.inject list_of_LCons list_of_LNil
          lnth_0) . .

lemma tr1_shape_s0:"s1 = s0 ⟹ Van.lvalidFromS s1 tr1 ⟹ lcompletedFromO s1 tr1 ⟹ tr1 = [[s0, s1, s2]]"  
  using tr1_shape_s0_aux by auto


lemma tr1_shape_s0'_aux:"Van.lvalidFromS s0' tr1 ⟹ lcompletedFromO s0' tr1 ⟹ tr1 = [[s0', s1', s2]]"  
  unfolding Opt.lcompletedFrom_def apply(erule impE)
  subgoal by(simp add: validTrFinite')
  apply(frule validTrFinite')
  unfolding Van.lvalidFromS_def Van.lvalidS_def final_iff
  apply(cases tr1, auto split: if_splits)
  subgoal for tr1' 
    apply(unfold nth_list_of[symmetric, of tr1'])
    apply(unfold nth_list_of[symmetric, of "(s0' $ tr1')", unfolded lfinite_LCons])
    apply(unfold length_list_of[symmetric])
    apply(cases tr1', simp)
    subgoal premises p 
      using p apply-apply(erule allE[of _ 0], simp split: if_splits)
      using p apply-apply(erule allE[of _ 1], simp split: if_splits)
      using p apply-apply(erule allE[of _ 2], simp split: if_splits)
    by (metis Suc_length_conv length_0_conv less_Suc0 lfinite.simps linorder_neqE_nat list.distinct(1) list.inject list_of_LCons list_of_LNil
          lnth_0) . .

lemma tr1_shape_s0':"s1 = s0' ⟹ Van.lvalidFromS s1 tr1 ⟹ lcompletedFromO s1 tr1 ⟹ tr1 = [[s0', s1', s2]]"  
  using tr1_shape_s0'_aux by auto

(*Systems are relatively insecure*)
proposition "¬lrsecure"
  unfolding lrsecure_def2 unfolding not_all not_imp
  apply(rule exI[of _ s0],rule exI[of _ "[[s0, s1, s2]]"])
  apply(rule exI[of _ s0'],rule exI[of _ "[[s0', s1', s2]]"])
  apply(intro conjI, simp_all add: validFromO validFromO' getAct0 getObs0)
  apply(intro allI)
  subgoal for sv1 apply(cases sv1, simp_all,intro allI impI)
     (*sv1 = s0*)
     subgoal for trv1 sv2 apply(cases sv2, simp_all, intro allI impI)
       (*sv2 = s0*)
       subgoal for trv2 
         apply(frule tr1_shape_s0[of _ trv1], simp_all)
         by(frule tr1_shape_s0[of _ trv2], simp_all)
       apply(intro allI impI)
       subgoal for trv2 
         apply(frule tr1_shape_s0[of _ trv1], simp_all)
         by(frule tr1_shape_s0'[of _ trv2], simp_all add: getAct1) .
     (*sv1 = s0' *)
     apply(intro allI impI)
     subgoal for trv1 sv2 apply(cases sv2, simp_all, intro allI impI)
       (*sv2 = s0*)
       subgoal for trv2 
         apply(frule tr1_shape_s0'[of _ trv1], simp_all)
         apply(frule tr1_shape_s0[of _ trv2], simp_all)
         using getAct1 by auto
       apply(intro allI impI)
       subgoal for trv2 
         apply(frule tr1_shape_s0'[of _ trv1], simp_all)
         by(frule tr1_shape_s0'[of _ trv2], simp_all add: getAct1) . . .



(*infer traces*)
lemma tr1_shape_s0_auxOpt:"Opt.lvalidFromS s0 tr1 ⟹ lcompletedFromO s0 tr1 ⟹ tr1 = [[s0, s1, s2]]"  
  unfolding Opt.lcompletedFrom_def apply(erule impE)
  subgoal by(simp add: validOptTrFinite)
  apply(frule validOptTrFinite)
  unfolding Opt.lvalidFromS_def Opt.lvalidS_def final_iff
  apply(cases tr1, auto split: if_splits)
  subgoal for tr1' 
    apply(unfold nth_list_of[symmetric, of tr1'])
    apply(unfold nth_list_of[symmetric, of "(s0 $ tr1')", unfolded lfinite_LCons])
    apply(unfold length_list_of[symmetric])
    apply(cases tr1', simp)
    subgoal premises p 
      using p apply-apply(erule allE[of _ 0], simp split: if_splits)
      using p apply-apply(erule allE[of _ 1], simp split: if_splits)
      using p apply-apply(erule allE[of _ 2], simp split: if_splits)
    by (metis Suc_length_conv length_0_conv less_Suc0 lfinite.simps linorder_neqE_nat list.distinct(1) list.inject list_of_LCons list_of_LNil
          lnth_0) . .

lemma tr1_shape_s0_Opt:"s1 = s0 ⟹ Opt.lvalidFromS s1 tr1 ⟹ lcompletedFromO s1 tr1 ⟹ tr1 = [[s0, s1, s2]]"  
  using tr1_shape_s0_auxOpt by auto


lemma tr1_shape_s0'_auxOpt:"Opt.lvalidFromS s0' tr1 ⟹ lcompletedFromO s0' tr1 ⟹ tr1 = [[s0', s1', s2]]"  
  unfolding Opt.lcompletedFrom_def apply(erule impE)
  subgoal by(simp add: validOptTrFinite')
  apply(frule validOptTrFinite')
  unfolding Opt.lvalidFromS_def Opt.lvalidS_def final_iff
  apply(cases tr1, auto split: if_splits)
  subgoal for tr1' 
    apply(unfold nth_list_of[symmetric, of tr1'])
    apply(unfold nth_list_of[symmetric, of "(s0' $ tr1')", unfolded lfinite_LCons])
    apply(unfold length_list_of[symmetric])
    apply(cases tr1', simp)
    subgoal premises p 
      using p apply-apply(erule allE[of _ 0], simp split: if_splits)
      using p apply-apply(erule allE[of _ 1], simp split: if_splits)
      using p apply-apply(erule allE[of _ 2], simp split: if_splits)
    by (metis Suc_length_conv length_0_conv less_Suc0 lfinite.simps linorder_neqE_nat list.distinct(1) list.inject list_of_LCons list_of_LNil
          lnth_0) . .

lemma tr1_shape_s0'_Opt:"s1 = s0' ⟹ Opt.lvalidFromS s1 tr1 ⟹ lcompletedFromO s1 tr1 ⟹ tr1 = [[s0', s1', s2]]"  
  using tr1_shape_s0'_auxOpt by auto

lemma OptS[simp]:"Opt.S [s0, s1, s2] = [s0]" unfolding Opt.S_def by auto
lemma OptS'[simp]:"Opt.S [s0', s1', s2] = [s0']" unfolding Opt.S_def by auto


lemma reachO0:"reachO s0" using Opt.reach.Istate by auto
lemma reachV0:"reachV s0" using Van.reach.Istate by auto
lemma reachO0':"reachO s0'" using Opt.reach.Istate by auto
lemma reachV0':"reachV s0'" using Van.reach.Istate by auto


(*incompleteness*)
lemma SD_incomplete:
  assumes
"s1 = s0 ∨ s1 = s0'"
"Opt.lvalidFromS s1 tr1"
"lcompletedFromO s1 tr1"
"s4 = s0 ∨ s4 = s0'"
"Opt.lvalidFromS s4 tr2"
"lcompletedFromO s4 tr2"
"Opt.lA tr1 = Opt.lA tr2"
"Opt.lO tr1 ≠ Opt.lO tr2" 
"⋀sv1 sv2.
    sv1 = s0 ∨ sv1 = s0' ⟹
    corrState sv1 s1 ⟹ sv2 = s0 ∨ sv2 = s0' ⟹ corrState sv2 s4 ⟹ Γ sv1 (Opt.lS tr1) sv2 (Opt.lS tr2)"
"lunwindSDCond Γ"
shows "False"
  using assms(9)[OF assms(1) _ assms(4), simplified] assms(1,4)
  apply-apply(elim disjE)
  subgoal using tr1_shape_s0_Opt[OF _ assms(2,3), simplified]
                tr1_shape_s0_Opt[OF _ assms(5,6), simplified]
                assms(7,8) by simp
  
  subgoal using tr1_shape_s0_Opt[OF _ assms(2,3), simplified]
                tr1_shape_s0'_Opt[OF _ assms(5,6), simplified]
                assms(7,8) apply simp
    using assms(10)[unfolded lunwindSDCond_def]
    apply-apply(erule allE[of _ "s0"], erule allE[of _ "[[s0]]"])   
    apply-apply(erule allE[of _ "s0'"], elim allE[of _ "[[s0']]"] impE)
    subgoal using reachV0' reachV0 by auto
    by (auto simp: getActV0 getObsV0)

  subgoal using tr1_shape_s0'_Opt[OF _ assms(2,3), simplified]
                tr1_shape_s0_Opt[OF _ assms(5,6), simplified]
                assms(7,8) apply simp
    using assms(10)[unfolded lunwindSDCond_def]
    apply-apply(erule allE[of _ "s0'"], erule allE[of _ "[[s0']]"])   
    apply-apply(erule allE[of _ "s0"], elim allE[of _ "[[s0]]"] impE)
    subgoal using reachV0' reachV0 by auto
    using getActV0 getObsV0 by auto
  subgoal using tr1_shape_s0'_Opt[OF _ assms(2,3), simplified]
                tr1_shape_s0'_Opt[OF _ assms(5,6), simplified]
                assms(7,8) by simp . 


end