Theory SD_Incomplete_fin

section ‹Secret Directed (Finatary) Unwinding Incompleteness example›

text ‹Demonstrating a counterexample which is secure but fails in the finatary unwinding›
theory SD_Incomplete_fin
  imports SD_Unwinding_fin
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.validFromS s0 [s0, s1, s2]" unfolding Opt.validFromS_def Opt.validS_def apply clarsimp
  by (metis less_Suc0 not_less_less_Suc_eq nth_Cons_0
      nth_Cons_Suc)

lemma validFromO':"Opt.validFromS s0' [s0', s1', s2]" unfolding Opt.validFromS_def Opt.validS_def apply clarsimp
  by (metis less_Suc0 not_less_less_Suc_eq nth_Cons_0
      nth_Cons_Suc)


(*infer traces*)
lemma tr1_shape_s0_aux:"Van.validFromS s0 tr1 ⟹ completedFromO s0 tr1 ⟹ tr1 = [s0, s1, s2]"  
  unfolding completedFromO_def apply(erule disjE)
  subgoal by(simp add: final_iff)
  unfolding Van.validFromS_def Van.validS_def final_iff 
  apply(cases tr1, auto split: if_splits) 
  subgoal for tr1' apply(cases tr1', auto split: if_splits, force+)
    subgoal premises p for a tr1''
      using p apply-apply(erule allE[of _ 0], auto)
      using p apply-apply(erule allE[of _ 1], auto)
      using p apply-apply(erule allE[of _ 2], auto)
      by (metis Suc_lessI gr0I length_0_conv length_Suc_conv nth_Cons_0) . .

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


lemma tr1_shape_s0'_aux:"Van.validFromS s0' tr1 ⟹ completedFromO s0' tr1 ⟹ tr1 = [s0', s1', s2]"  
  unfolding completedFromO_def apply(erule disjE)
  subgoal by(simp add: final_iff)
  unfolding Van.validFromS_def Van.validS_def final_iff
  apply(cases tr1, auto split: if_splits) 
  subgoal for tr1' apply(cases tr1', auto split: if_splits, force+)
    subgoal premises p for a tr1''
      using p apply-apply(erule allE[of _ 0], auto)
      using p apply-apply(erule allE[of _ 1], auto)
      using p apply-apply(erule allE[of _ 2], auto)
      by (metis Suc_lessI gr0I length_0_conv length_Suc_conv nth_Cons_0) . .

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

(*Systems are relatively insecure*)
proposition "¬rsecure"
  unfolding rsecure_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) . . .


 thm unwindSD_rsecure





(*infer traces*)
lemma tr1_shape_s0_auxOpt:"Opt.validFromS s0 tr1 ⟹ completedFromO s0 tr1 ⟹ tr1 = [s0, s1, s2]"  
  unfolding completedFromO_def apply(erule disjE)
  subgoal by(simp add: final_iff)
  unfolding Opt.validFromS_def Opt.validS_def final_iff
  apply(cases tr1, auto split: if_splits) 
  subgoal for tr1' apply(cases tr1', auto split: if_splits, force+)
    subgoal premises p for a tr1''
      using p apply-apply(erule allE[of _ 0], auto)
      using p apply-apply(erule allE[of _ 1], auto)
      using p apply-apply(erule allE[of _ 2], auto)
      by (metis Suc_lessI gr0I length_0_conv length_Suc_conv nth_Cons_0) . .

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


lemma tr1_shape_s0'_auxOpt:"Opt.validFromS s0' tr1 ⟹ completedFromO s0' tr1 ⟹ tr1 = [s0', s1', s2]"  
  unfolding completedFromO_def apply(erule disjE)
  subgoal by(simp add: final_iff)
  unfolding Opt.validFromS_def Opt.validS_def final_iff
  apply(cases tr1, auto split: if_splits) 
  subgoal for tr1' apply(cases tr1', auto split: if_splits, force+)
    subgoal premises p for a tr1''
      using p apply-apply(erule allE[of _ 0], auto)
      using p apply-apply(erule allE[of _ 1], auto)
      using p apply-apply(erule allE[of _ 2], auto)
      by (metis Suc_lessI gr0I length_0_conv length_Suc_conv nth_Cons_0) . .

lemma tr1_shape_s0'_Opt:"s1 = s0' ⟹ Opt.validFromS s1 tr1 ⟹ completedFromO 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.validFromS s1 tr1"
"completedFromO s1 tr1"
"s4 = s0 ∨ s4 = s0'"
"Opt.validFromS s4 tr2"
"completedFromO s4 tr2"
"Opt.A tr1 = Opt.A tr2"
"Opt.O tr1 ≠ Opt.O tr2" 
"⋀sv1 sv2.
    sv1 = s0 ∨ sv1 = s0' ⟹
    corrState sv1 s1 ⟹ sv2 = s0 ∨ sv2 = s0' ⟹ corrState sv2 s4 ⟹ Γ sv1 (Opt.S tr1) sv2 (Opt.S tr2)"
"unwindSDCond Γ"
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 unwindSDCond_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 unwindSDCond_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