Theory Independent_Secrets

section ‹Combining independent secret sources›

text ‹This theory formalizes the discussion about considering
combined sources of secrets from \<^cite>‹‹Appendix E› in "cosmedis-SandP2017"›.
›

theory Independent_Secrets
imports Bounded_Deducibility_Security.BD_Security_TS
begin

locale Abstract_BD_Security_Two_Secrets =
  One: Abstract_BD_Security validSystemTrace V1 O1 B1 TT1
+ Two: Abstract_BD_Security validSystemTrace V2 O2 B2 TT2
for
  validSystemTrace :: "'traces ⇒ bool"
and
  V1 :: "'traces ⇒ 'values1"
and
  O1 :: "'traces ⇒ 'observations1"
and (* declassification bound: *)
  B1 :: "'values1 ⇒ 'values1 ⇒ bool"
and (* declassification trigger: *)
  TT1 :: "'traces ⇒ bool"
and
  V2 :: "'traces ⇒ 'values2"
and
  O2 :: "'traces ⇒ 'observations2"
and (* declassification bound: *)
  B2 :: "'values2 ⇒ 'values2 ⇒ bool"
and (* declassification trigger: *)
  TT2 :: "'traces ⇒ bool"
+
fixes
  O :: "'traces ⇒ 'observations"
assumes
  O1_O: "O1 tr = O1 tr' ⟹ validSystemTrace tr ⟹ validSystemTrace tr' ⟹ O tr = O tr'"
and
  O2_O: "O2 tr = O2 tr' ⟹ validSystemTrace tr ⟹ validSystemTrace tr' ⟹ O tr = O tr'"
and
  O1_V2: "O1 tr = O1 tr' ⟹ validSystemTrace tr ⟹ validSystemTrace tr' ⟹ B1 (V1 tr) (V1 tr') ⟹ V2 tr = V2 tr'"
and
  O2_V1: "O2 tr = O2 tr' ⟹ validSystemTrace tr ⟹ validSystemTrace tr' ⟹ B2 (V2 tr) (V2 tr') ⟹ V1 tr = V1 tr'"
and
  O1_TT2: "O1 tr = O1 tr' ⟹ validSystemTrace tr ⟹ validSystemTrace tr' ⟹ B1 (V1 tr) (V1 tr') ⟹ TT2 tr = TT2 tr'"
begin

definition "V tr = (V1 tr, V2 tr)"
definition "B vl vl' = (B1 (fst vl) (fst vl') ∧ B2 (snd vl) (snd vl'))"
definition "TT tr = (TT1 tr ∧ TT2 tr)"

sublocale Abstract_BD_Security validSystemTrace V O B TT .

theorem two_secure:
assumes "One.secure" and "Two.secure"
shows "secure"
unfolding secure_def
proof (intro allI impI, elim conjE)
  fix tr vl vl'
  assume tr: "validSystemTrace tr" and TT: "TT tr" and B: "B vl vl'" and V_tr: "V tr = vl"
  then obtain vl1' vl2' where vl: "vl = (V1 tr, V2 tr)" and vl': "vl' = (vl1', vl2')"
    by (cases vl, cases vl') (auto simp: V_def)
  obtain tr' where tr': "validSystemTrace tr'" and O1: "O1 tr' = O1 tr" and V1: "V1 tr' = vl1'"
    using assms(1) tr TT B by (auto elim: One.secureE simp: TT_def B_def V_def vl vl')
  then have O': "O tr' = O tr" and V2': "V2 tr = V2 tr'" and TT2': "TT2 tr = TT2 tr'"
    using B tr V1 by (auto intro: O1_O O1_V2 simp: O1_TT2 B_def vl vl')
  obtain tr'' where tr'': "validSystemTrace tr''" and O2: "O2 tr'' = O2 tr'" and V2: "V2 tr'' = vl2'"
    using assms(2) tr' TT2' TT B V2'
    by (elim Two.secureE[of tr' vl2']) (auto simp: TT_def B_def vl vl')
  moreover then have "O tr'' = O tr'" and "V1 tr' = V1 tr''"
    using B tr' V2 by (auto intro: O2_O O2_V1 simp: B_def V2' vl vl')
  ultimately show "∃tr1. validSystemTrace tr1 ∧ O tr1 = O tr ∧ V tr1 = vl'"
    unfolding V_def V1 vl' O' by auto
qed

end

locale BD_Security_TS_Two_Secrets =
  One: BD_Security_TS istate validTrans srcOf tgtOf φ1 f1 γ1 g1 T1 B1
+ Two: BD_Security_TS istate validTrans srcOf tgtOf φ2 f2 γ2 g2 T2 B2
for istate :: 'state and validTrans :: "'trans ⇒ bool"
and srcOf :: "'trans ⇒ 'state" and tgtOf :: "'trans ⇒ 'state"
and φ1 :: "'trans ⇒ bool" and f1 :: "'trans ⇒ 'val1"
and γ1 :: "'trans ⇒ bool" and g1 :: "'trans ⇒ 'obs1"
and T1 :: "'trans ⇒ bool" and B1 :: "'val1 list ⇒ 'val1 list ⇒ bool"
and φ2 :: "'trans ⇒ bool" and f2 :: "'trans ⇒ 'val2"
and γ2 :: "'trans ⇒ bool" and g2 :: "'trans ⇒ 'obs2"
and T2 :: "'trans ⇒ bool" and B2 :: "'val2 list ⇒ 'val2 list ⇒ bool"
+
fixes γ :: "'trans ⇒ bool" and g :: "'trans ⇒ 'obs"
assumes γ_γ12: "⋀tr trn. One.validFrom istate (tr ## trn) ⟹ γ trn ⟹ γ1 trn ∧ γ2 trn"
and O1_γ: "⋀tr tr' trn trn'. One.O tr = One.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ1 trn ⟹ γ1 trn' ⟹ g1 trn = g1 trn' ⟹ γ trn = γ trn'"
and O1_g: "⋀tr tr' trn trn'. One.O tr = One.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ1 trn ⟹ γ1 trn' ⟹ g1 trn = g1 trn' ⟹ γ trn ⟹ γ trn' ⟹ g trn = g trn'"
and O2_γ: "⋀tr tr' trn trn'. Two.O tr = Two.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ2 trn ⟹ γ2 trn' ⟹ g2 trn = g2 trn' ⟹ γ trn = γ trn'"
and O2_g: "⋀tr tr' trn trn'. Two.O tr = Two.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ2 trn ⟹ γ2 trn' ⟹ g2 trn = g2 trn' ⟹ γ trn ⟹ γ trn' ⟹ g trn = g trn'"
and φ2_γ1: "⋀tr trn. One.validFrom istate (tr ## trn) ⟹ φ2 trn ⟹ γ1 trn"
and γ1_φ2: "⋀tr tr' trn trn'. One.O tr = One.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ1 trn ⟹ γ1 trn' ⟹ g1 trn = g1 trn' ⟹ φ2 trn = φ2 trn'"
and g1_f2: "⋀tr tr' trn trn'. One.O tr = One.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ1 trn ⟹ γ1 trn' ⟹ g1 trn = g1 trn' ⟹ φ2 trn ⟹ φ2 trn' ⟹ f2 trn = f2 trn'"
and φ1_γ2: "⋀tr trn. One.validFrom istate (tr ## trn) ⟹ φ1 trn ⟹ γ2 trn"
and γ2_φ1: "⋀tr tr' trn trn'. Two.O tr = Two.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ2 trn ⟹ γ2 trn' ⟹ g2 trn = g2 trn' ⟹ φ1 trn = φ1 trn'"
and g2_f1: "⋀tr tr' trn trn'. Two.O tr = Two.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ2 trn ⟹ γ2 trn' ⟹ g2 trn = g2 trn' ⟹ φ1 trn ⟹ φ1 trn' ⟹ f1 trn = f1 trn'"
and T2_γ1: "⋀tr trn. One.validFrom istate (tr ## trn) ⟹ never T2 tr ⟹ T2 trn ⟹ γ1 trn"
and γ1_T2: "⋀tr tr' trn trn'. One.O tr = One.O tr' ⟹ One.validFrom istate (tr ## trn) ⟹ One.validFrom istate (tr' ## trn') ⟹ γ1 trn ⟹ γ1 trn' ⟹ g1 trn = g1 trn' ⟹ T2 trn = T2 trn'"
begin

definition "O tr = map g (filter γ tr)"

lemma O_Nil_never: "O tr = [] ⟷ never γ tr" unfolding O_def by (induction tr) auto
lemma Nil_O_never: "[] = O tr ⟷ never γ tr" unfolding O_def by (induction tr) auto
lemma O_append: "O (tr @ tr') = O tr @ O tr'" unfolding O_def by auto

lemma never_γ12_never_γ: "One.validFrom istate (tr @ tr') ⟹ never γ1 tr' ∨ never γ2 tr' ⟹ never γ tr'"
proof (induction tr' rule: rev_induct)
  case (snoc trn tr')
  then show ?case using γ_γ12[of "tr @ tr'" trn] by (auto simp: One.validFrom_append)
qed auto

lemma never_γ1_never_φ2: "One.validFrom istate (tr @ tr') ⟹ never γ1 tr' ⟹ never φ2 tr'"
proof (induction tr' rule: rev_induct)
  case (snoc trn tr')
  then show ?case using φ2_γ1[of "tr @ tr'" trn] by (auto simp: One.validFrom_append)
qed auto

lemma never_γ2_never_φ1: "One.validFrom istate (tr @ tr') ⟹ never γ2 tr' ⟹ never φ1 tr'"
proof (induction tr' rule: rev_induct)
  case (snoc trn tr')
  then show ?case using φ1_γ2[of "tr @ tr'" trn] by (auto simp: One.validFrom_append)
qed auto

lemma never_γ1_never_T2: "One.validFrom istate (tr @ tr') ⟹ never T2 tr ⟹ never γ1 tr' ⟹ never T2 tr'"
proof (induction tr' rule: rev_induct)
  case (snoc trn tr')
  then show ?case using T2_γ1[of "tr @ tr'" trn] by (auto simp: One.validFrom_append)
qed auto

sublocale Abstract_BD_Security_Two_Secrets "One.validFrom istate" One.V One.O B1 "never T1" Two.V Two.O B2 "never T2" O
proof
  fix tr tr'
  assume "One.O tr = One.O tr'" "One.validFrom istate tr" "One.validFrom istate tr'"
  then show "O tr = O tr'"
  proof (induction "One.O tr" arbitrary: tr tr' rule: rev_induct)
    case (Nil tr tr')
    then have tr: "O tr = []" using never_γ12_never_γ[of "[]" tr] by (auto simp: O_Nil_never One.O_Nil_never)
    show "O tr = O tr'" using Nil never_γ12_never_γ[of "[]" tr'] by (auto simp: tr Nil_O_never One.Nil_O_never)
  next
    case (snoc obs obsl tr tr')
    obtain tr1 trn tr2 where tr: "tr = tr1 @ [trn] @ tr2" and trn: "γ1 trn" "g1 trn = obs"
                         and tr1: "One.O tr1 = obsl" and tr2: "never γ1 tr2"
      using snoc(2) One.O_eq_RCons[of tr obsl obs] by auto
    obtain tr1' trn' tr2' where tr': "tr' = tr1' @ [trn'] @ tr2'" and trn': "γ1 trn'" "g1 trn' = obs"
                          and tr1': "One.O tr1' = obsl" and tr2': "never γ1 tr2'"
      using snoc(2,3) One.O_eq_RCons[of tr' obsl obs] by auto
    have "O tr1 = O tr1'" using snoc(1)[of tr1 tr1'] tr1 tr1' snoc(4,5) unfolding tr tr'
      by (auto simp: One.validFrom_append)
    moreover have "O [trn] = O [trn']" using O1_γ[of tr1 tr1' trn trn'] O1_g[of tr1 tr1' trn trn']
      using snoc(4,5) tr1 tr1' trn trn' by (auto simp: tr tr' O_def One.validFrom_append One.validFrom_Cons)
    moreover have "O tr2 = []" and "O tr2' = []" using tr2 tr2'
      using never_γ12_never_γ[of "tr1 ## trn" tr2] never_γ12_never_γ[of "tr1' ## trn'" tr2']
      using snoc(4,5) unfolding tr tr' by (auto simp: O_Nil_never)
    ultimately show "O tr = O tr'" unfolding tr tr' O_append by auto
  qed
next
  fix tr tr'
  assume "Two.O tr = Two.O tr'" "One.validFrom istate tr" "One.validFrom istate tr'"
  then show "O tr = O tr'"
  proof (induction "Two.O tr" arbitrary: tr tr' rule: rev_induct)
    case (Nil tr tr')
    then have tr: "O tr = []" using never_γ12_never_γ[of "[]" tr] by (auto simp: O_Nil_never Two.O_Nil_never)
    show "O tr = O tr'" using Nil never_γ12_never_γ[of "[]" tr'] by (auto simp: tr Nil_O_never Two.Nil_O_never)
  next
    case (snoc obs obsl tr tr')
    obtain tr1 trn tr2 where tr: "tr = tr1 @ [trn] @ tr2" and trn: "γ2 trn" "g2 trn = obs"
                         and tr1: "Two.O tr1 = obsl" and tr2: "never γ2 tr2"
      using snoc(2) Two.O_eq_RCons[of tr obsl obs] by auto
    obtain tr1' trn' tr2' where tr': "tr' = tr1' @ [trn'] @ tr2'" and trn': "γ2 trn'" "g2 trn' = obs"
                          and tr1': "Two.O tr1' = obsl" and tr2': "never γ2 tr2'"
      using snoc(2,3) Two.O_eq_RCons[of tr' obsl obs] by auto
    have "O tr1 = O tr1'" using snoc(1)[of tr1 tr1'] tr1 tr1' snoc(4,5) unfolding tr tr'
      by (auto simp: One.validFrom_append)
    moreover have "O [trn] = O [trn']" using O2_γ[of tr1 tr1' trn trn'] O2_g[of tr1 tr1' trn trn']
      using snoc(4,5) tr1 tr1' trn trn' by (auto simp: tr tr' O_def One.validFrom_append One.validFrom_Cons)
    moreover have "O tr2 = []" and "O tr2' = []" using tr2 tr2'
      using never_γ12_never_γ[of "tr1 ## trn" tr2] never_γ12_never_γ[of "tr1' ## trn'" tr2']
      using snoc(4,5) unfolding tr tr' by (auto simp: O_Nil_never)
    ultimately show "O tr = O tr'" unfolding tr tr' O_append by auto
  qed
next
  fix tr tr'
  assume "One.O tr = One.O tr'" "One.validFrom istate tr" "One.validFrom istate tr'"
  then show "Two.V tr = Two.V tr'"
  proof (induction "One.O tr" arbitrary: tr tr' rule: rev_induct)
    case (Nil tr tr')
    then have tr: "Two.V tr = []" using never_γ1_never_φ2[of "[]" tr]
      unfolding Two.V_Nil_never One.Nil_O_never by auto
    show "Two.V tr = Two.V tr'" using never_γ1_never_φ2[of "[]" tr'] using Nil
      unfolding tr Two.Nil_V_never One.O_Nil_never[symmetric] by auto
  next
    case (snoc obs obsl tr tr')
    obtain tr1 trn tr2 where tr: "tr = tr1 @ [trn] @ tr2" and trn: "γ1 trn" "g1 trn = obs"
                         and tr1: "One.O tr1 = obsl" and tr2: "never γ1 tr2"
      using snoc(2) One.O_eq_RCons[of tr obsl obs] by auto
    obtain tr1' trn' tr2' where tr': "tr' = tr1' @ [trn'] @ tr2'" and trn': "γ1 trn'" "g1 trn' = obs"
                          and tr1': "One.O tr1' = obsl" and tr2': "never γ1 tr2'"
      using snoc(2,3) One.O_eq_RCons[of tr' obsl obs] by auto
    have "Two.V tr1 = Two.V tr1'" using snoc(1)[of tr1 tr1'] tr1 tr1' snoc(4,5) unfolding tr tr'
      by (auto simp: One.validFrom_append)
    moreover have "Two.V [trn] = Two.V [trn']" using γ1_φ2[of tr1 tr1' trn trn'] g1_f2[of tr1 tr1' trn trn']
      using snoc(4,5) tr1 tr1' trn trn' unfolding tr tr' Two.V_map_filter
      by (auto simp: One.validFrom_append One.validFrom_Cons)
    moreover have "Two.V tr2 = []" and "Two.V tr2' = []" using tr2 tr2'
      using never_γ1_never_φ2[of "tr1 ## trn" tr2] never_γ1_never_φ2[of "tr1' ## trn'" tr2']
      using snoc(4,5) unfolding tr tr' by (auto simp: Two.V_Nil_never)
    ultimately show "Two.V tr = Two.V tr'" unfolding tr tr' Two.V_append by auto
  qed
next
  fix tr tr'
  assume "Two.O tr = Two.O tr'" "One.validFrom istate tr" "One.validFrom istate tr'"
  then show "One.V tr = One.V tr'"
  proof (induction "Two.O tr" arbitrary: tr tr' rule: rev_induct)
    case (Nil tr tr')
    then have tr: "One.V tr = []" using never_γ2_never_φ1[of "[]" tr]
      unfolding One.V_Nil_never Two.Nil_O_never by auto
    show "One.V tr = One.V tr'" using never_γ2_never_φ1[of "[]" tr'] using Nil
      unfolding tr One.Nil_V_never Two.O_Nil_never[symmetric] by auto
  next
    case (snoc obs obsl tr tr')
    obtain tr1 trn tr2 where tr: "tr = tr1 @ [trn] @ tr2" and trn: "γ2 trn" "g2 trn = obs"
                         and tr1: "Two.O tr1 = obsl" and tr2: "never γ2 tr2"
      using snoc(2) Two.O_eq_RCons[of tr obsl obs] by auto
    obtain tr1' trn' tr2' where tr': "tr' = tr1' @ [trn'] @ tr2'" and trn': "γ2 trn'" "g2 trn' = obs"
                          and tr1': "Two.O tr1' = obsl" and tr2': "never γ2 tr2'"
      using snoc(2,3) Two.O_eq_RCons[of tr' obsl obs] by auto
    have "One.V tr1 = One.V tr1'" using snoc(1)[of tr1 tr1'] tr1 tr1' snoc(4,5) unfolding tr tr'
      by (auto simp: One.validFrom_append)
    moreover have "One.V [trn] = One.V [trn']" using γ2_φ1[of tr1 tr1' trn trn'] g2_f1[of tr1 tr1' trn trn']
      using snoc(4,5) tr1 tr1' trn trn' unfolding tr tr' Two.V_map_filter
      by (auto simp: One.validFrom_append One.validFrom_Cons)
    moreover have "One.V tr2 = []" and "One.V tr2' = []" using tr2 tr2'
      using never_γ2_never_φ1[of "tr1 ## trn" tr2] never_γ2_never_φ1[of "tr1' ## trn'" tr2']
      using snoc(4,5) unfolding tr tr' by (auto simp: One.V_Nil_never)
    ultimately show "One.V tr = One.V tr'" unfolding tr tr' One.V_append by auto
  qed
next
  fix tr tr'
  assume "One.O tr = One.O tr'" "One.validFrom istate tr" "One.validFrom istate tr'"
  then show "never T2 tr = never T2 tr'"
  proof (induction "One.O tr" arbitrary: tr tr' rule: rev_induct)
    case (Nil tr tr')
    then have tr: "never T2 tr" using never_γ1_never_T2[of "[]" tr]
      unfolding Two.V_Nil_never One.Nil_O_never by auto
    then show "never T2 tr = never T2 tr'" using never_γ1_never_T2[of "[]" tr'] using Nil
      unfolding tr Two.Nil_V_never One.O_Nil_never[symmetric] by auto
  next
    case (snoc obs obsl tr tr')
    obtain tr1 trn tr2 where tr: "tr = tr1 @ [trn] @ tr2" and trn: "γ1 trn" "g1 trn = obs"
                         and tr1: "One.O tr1 = obsl" and tr2: "never γ1 tr2"
      using snoc(2) One.O_eq_RCons[of tr obsl obs] by auto
    obtain tr1' trn' tr2' where tr': "tr' = tr1' @ [trn'] @ tr2'" and trn': "γ1 trn'" "g1 trn' = obs"
                          and tr1': "One.O tr1' = obsl" and tr2': "never γ1 tr2'"
      using snoc(2,3) One.O_eq_RCons[of tr' obsl obs] by auto
    have "never T2 tr1 = never T2 tr1'" using snoc(1)[of tr1 tr1'] tr1 tr1' snoc(4,5) unfolding tr tr'
      by (auto simp: One.validFrom_append)
    moreover have "T2 trn = T2 trn'" using γ1_T2[of tr1 tr1' trn trn']
      using snoc(4,5) tr1 tr1' trn trn' unfolding tr tr' Two.V_map_filter
      by (auto simp: One.validFrom_append One.validFrom_Cons)
    moreover have "never T2 (tr1 ## trn) ⟶ never T2 tr2"
              and "never T2 (tr1' ## trn') ⟶ never T2 tr2'"
      using never_γ1_never_T2[of "tr1 ## trn" tr2] never_γ1_never_T2[of "tr1' ## trn'" tr2']
      using tr2 tr2' snoc(4,5) unfolding tr tr' by (auto simp: Two.V_Nil_never)
    ultimately show "never T2 tr = never T2 tr'" unfolding tr tr' by auto
  qed
qed

end

end