Theory Discussion_NCPC

theory Discussion_NCPC
imports "../Observation_Setup" Discussion_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsection ‹Confidentiality protection from non-PC-members›

text ‹We verify the following property:

\ \\
A group of users UIDs learn
nothing about the various updates of a paper's discussion
(i.e., about the comments being posted on a paper by the PC members)
(save for the non-existence of any edit)
unless/until a user in UIDs becomes a PC member in the paper's conference having no conflict with that paper
and the conference moves to the discussion phase.

\ \\
›

fun T :: "(state,act,out) trans ⇒ bool" where
"T (Trans _ _ ou s') =
 (∃ uid ∈ UIDs. ∃ cid.
    PID ∈∈ paperIDs s' cid ∧ isPC s' cid uid ∧ pref s' uid PID ≠ Conflict ∧ phase s' cid ≥ disPH
 )"

declare T.simps [simp del]

definition B :: "value list ⇒ value list ⇒ bool" where
"B vl vl1 ≡ vl ≠ []"

interpretation BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done

lemma reachNT_non_isPC_isChair:
assumes "reachNT s" and "uid ∈ UIDs"
shows
"(PID ∈∈ paperIDs s cid ∧ isPC s cid uid ∧ phase s cid ≥ disPH ⟶ pref s uid PID = Conflict) ∧
 (PID ∈∈ paperIDs s cid ∧ isChair s cid uid ∧ phase s cid ≥ disPH ⟶ pref s uid PID = Conflict)"
  using assms
  apply induct
   apply (auto simp: istate_def)[]
  apply(intro conjI)
  subgoal for trn apply(cases trn, auto simp: T.simps reachNT_reach)[] .
  by (metis T.elims(3) isChair_isPC reachNT_reach reach.Step tgtOf_simps)


lemma T_φ_γ:
assumes 1: "reachNT s" and 2: "step s a = (ou,s')" "φ (Trans s a ou s')"
shows "¬ γ (Trans s a ou s')"
using reachNT_non_isPC_isChair[OF 1] 2 unfolding φ_def2
by (fastforce simp add: uu_defs)

(* major *) lemma eqExcPID_step_out:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and sT: "reachNT s" and s1: "reach s1"
and PID: "PID ∈∈ paperIDs s cid"
and UIDs: "userOfA a ∈ UIDs"
shows "ou = ou1"
proof-
  note Inv = reachNT_non_isPC_isChair[OF sT UIDs]
  note eqs = eqExcPID_imp[OF s's1']
  note eqs' = eqExcPID_imp1[OF s's1']
  note s = reachNT_reach[OF sT]

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def eeqExcPID_def eqExcD
  note * = step step1 eqs eqs' s s1 PID UIDs paperIDs_equals[OF s] Inv

  show ?thesis
  proof (cases a)
    case (Cact x1)
    then show ?thesis using * by (cases x1) auto
  next
    case (Uact x2)
    then show ?thesis using * by (cases x2) auto
  next
    case (UUact x3)
    then show ?thesis using * by (cases x3) auto
  next
    case (Ract x4)
    show ?thesis
    proof (cases x4)
      case (rMyReview x81 x82 x83 x84)
      then show ?thesis using * Ract by (auto simp add: getNthReview_def)
    next
      case (rReviews x91 x92 x93 x94)
      then show ?thesis using * Ract by (clarsimp; metis eqExcPID_imp2 s's1')
    next
      case (rDis x111 x112 x113 x114)
      then show ?thesis using * Ract by (clarsimp; metis discussion.inject)
    qed (use * Ract in auto)
  next
    case (Lact x5)
    then show ?thesis using * by (cases x5; auto; presburger)
  qed
qed

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
 (∀ cid. PID ∈∈ paperIDs s cid ⟶ phase s cid < disPH) ∧ s = s1 ∧ B vl vl1"

(* main difference from the Paper_Confidentiality/Aut_PC: need to assume
that there are means to produce vl1 via iaction when disPH has been reached;
if not, this yields and exit *)
definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡
 ∃ cid uid.
    PID ∈∈ paperIDs s cid ∧ phase s cid = disPH ∧
    isPC s cid uid ∧ pref s uid PID ≠ Conflict
    ∧ eqExcPID s s1"

definition Δ3 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ3 s vl s1 vl1 ≡
 ∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid > disPH ∧ eqExcPID s s1 ∧ vl1 = []"

definition Δe :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δe s vl s1 vl1 ≡
 vl ≠ [] ∧
 (∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid ≥ disPH ∧
         ¬ (∃ uid. isPC s cid uid ∧ pref s uid PID ≠ Conflict)
 )"

lemma init_Δ1:
assumes B: "B vl vl1"
shows "Δ1 istate vl istate vl1"
using B unfolding Δ1_def B_def istate_def by auto

lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1,Δ2,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨ Δ2 s vl s1 vl1 ∨ Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ1 s vl s1 vl1"
  hence rs: "reach s" and ss1: "s1 = s" and vl: "vl ≠ []"
  and PID_ph: "⋀ cid. PID ∈∈ paperIDs s cid ⟹ phase s cid < disPH"
  using reachNT_reach unfolding Δ1_def B_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have φ: "¬ φ ?trn"
      proof (cases a)
        case (UUact x3)
        then show ?thesis
          using step PID_ph
          by (cases x3; fastforce simp: uu_defs)
      qed auto
      hence vl': "vl' = vl" using c unfolding consume_def by auto
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have ?match proof
          show "validTrans ?trn1" unfolding ss1 using step by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def ss1 using φ by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
        next
          show "?Δ s' vl' s' vl1"
          proof(cases "∃ cid. PID ∈∈ paperIDs s cid")
            case False note PID = False
            have ph_PID': "⋀ cid. PID ∈∈ paperIDs s' cid ⟹ phase s' cid < disPH" using PID step rs
            subgoal apply(cases a)
              subgoal for x1 apply(cases x1) apply(fastforce simp: c_defs)+ .
              subgoal for x2 apply(cases x2) apply(fastforce simp: u_defs)+ .
              subgoal for x3 apply(cases x3) apply(fastforce simp: uu_defs)+ .
              by auto
            done
            hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using ph_PID' vl by auto
            thus ?thesis by auto
          next
            case True then obtain CID where PID: "PID ∈∈ paperIDs s CID" by auto
            hence ph: "phase s CID < disPH" (is "?ph < _") using PID_ph by auto
            show ?thesis
            proof(cases "phase s' CID < disPH")
              case True note ph' = True
              show ?thesis proof(cases "PID ∈∈ paperIDs s' CID")
                case False
                hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using vl ph' apply auto
                by (metis PID paperIDs_mono step)(* safety crucially used *)
                thus ?thesis by auto
              next
                case True
                hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using vl ph' apply auto
                by (metis reach_PairI paperIDs_equals rs step) (* safety crucially used *)
                thus ?thesis by auto
              qed
            next
              case False
              hence ph': "phase s' CID = disPH ∧ PID ∈∈ paperIDs s' CID"
              using PID ph step rs
              subgoal apply(cases a)
                subgoal for x1 apply(cases x1) apply(fastforce simp: c_defs)+ .
                subgoal for x2 apply(cases x2) apply(fastforce simp: u_defs)+ .
                subgoal for x3 apply(cases x3) apply(fastforce simp: uu_defs)+ .
              by auto
            done
              show ?thesis
              proof(cases "∃uid. isPC s' CID uid ∧ pref s' uid PID ≠ Conflict")
                case True
                hence "Δ2 s' vl' s' vl1" unfolding Δ2_def vl' using vl ph' by auto
                thus ?thesis by auto
              next
                case False
                hence "Δe s' vl' s' vl1" unfolding Δe_def vl' using vl ph' by auto
                thus ?thesis by auto
              qed
            qed
          qed
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl by auto
  qed
qed

lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2,Δ3,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ2 s vl s1 vl1 ∨ Δ3 s vl s1 vl1 ∨ Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ2 s vl s1 vl1"
  then obtain CID uid where uid: "isPC s CID uid" "pref s uid PID ≠ Conflict"
  and rs: "reach s" and ph: "phase s CID = disPH" (is "?ph = _")
  and PID: "PID ∈∈ paperIDs s CID" and ss1: "eqExcPID s s1"
  using reachNT_reach unfolding Δ2_def by auto
  hence uid_notin: "uid ∉ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] by force
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases vl1)
    case (Cons v1 vl1') note vl1 = Cons
    have uid1: "isPC s1 CID uid" "pref s1 uid PID ≠ Conflict"
    using ss1 uid unfolding eqExcPID_def by auto
    define a1 where "a1 ≡ UUact (uuDis CID uid (pass s uid) PID v1)"
    obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')" by (metis prod.exhaust)
    let ?trn1 = "Trans s1 a1 ou1 s1'"
    have s1s1': "eqExcPID s1 s1'" using a1_def step1 UUact_uuDis_step_eqExcPID by auto
    have ss1': "eqExcPID s s1'" using eqExcPID_trans[OF ss1 s1s1'] .
    hence many_s1': "PID ∈∈ paperIDs s1' CID" "isPC s1' CID uid"
    "pref s1' uid PID ≠ Conflict" "phase s1' CID = disPH"
    "pass s1' uid = pass s uid"
    using uid PID ph unfolding eqExcPID_def by auto
    hence more_s1': "uid ∈∈ userIDs s1'" "CID ∈∈ confIDs s1'"
    by (metis paperIDs_confIDs reach_PairI roles_userIDs rs1 step1 many_s1'(1))+
    have f: "f ?trn1 = v1" unfolding a1_def by simp
    have rs1': "reach s1'" using rs1 step1 by (auto intro: reach_PairI)
    have ou1: "ou1 = outOK"
    using step1 uid1 ph unfolding a1_def by (auto simp add: uu_defs many_s1' more_s1')
    have ?iact proof
      show "step s1 a1 = (ou1,s1')" by fact
    next
      show φ: "φ ?trn1" using ou1 unfolding a1_def by simp
      thus "consume ?trn1 vl1 vl1'" using f unfolding consume_def vl1 by simp
    next
      show "¬ γ ?trn1" by (simp add: a1_def uid_notin)
    next
      have "Δ2 s vl s1' vl1'" unfolding Δ2_def using ph PID ss1' uid by auto
      thus "?Δ s vl s1' vl1'" by simp
    qed
    thus ?thesis by auto
  next
    case Nil note vl1 = Nil
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      let ?ph' = "phase s' CID"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ paperIDs s' CID" using PID rs by (metis paperIDs_mono step)
      have uid': "isPC s' CID uid ∧ pref s' uid PID ≠ Conflict"
      using uid step rs ph PID pref_Conflict_disPH isPC_persistent by auto
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof(cases "φ ?trn")
        case False note φ = False
        have vl: "vl' = vl" using c φ unfolding consume_def by (cases vl) auto
        obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
        let ?trn1 = "Trans s1 a ou1 s1'"
        have s's1': "eqExcPID s' s1'" using eqExcPID_step[OF ss1 step step1] .
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID_step_φ[OF ss1 step step1] .
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def using φ1 by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqExcPID_step_out[OF ss1 step step1 rsT rs1 PID] by simp
        next
          show "?Δ s' vl' s1' vl1"
          proof(cases "?ph' = disPH")
            case True
            hence "Δ2 s' vl' s1' vl1" using PID' s's1' uid' unfolding Δ2_def by auto
            thus ?thesis by auto
          next
            case False hence "?ph' > disPH"
            using ph rs step by (metis le_less phase_increases)
            hence "Δ3 s' vl' s1' vl1" using s's1' PID' unfolding Δ3_def vl1 by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by simp
      next
        case True note φ = True
        have s's: "eqExcPID s' s" using eqExcPID_sym[OF φ_step_eqExcPID[OF φ step]] .
        have s's1: "eqExcPID s' s1" using eqExcPID_trans[OF s's ss1] .
        have ?ignore proof
          show "¬ γ ?trn" using T_φ_γ φ rsT step by auto
        next
          show "?Δ s' vl' s1 vl1"
          proof(cases "?ph' = disPH")
            case True
            hence "Δ2 s' vl' s1 vl1" using s's1 PID' uid' unfolding Δ2_def by auto
            thus ?thesis by auto
          next
            case False hence "?ph' > disPH"
            using ph rs step by (metis le_less phase_increases)
            hence "Δ3 s' vl' s1 vl1" using s's1 PID' unfolding Δ3_def vl1 by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by auto
      qed
    qed
    thus ?thesis using vl1 by auto
  qed
qed

lemma unwind_cont_Δ3: "unwind_cont Δ3 {Δ3,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ3 s vl s1 vl1 ∨ Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ3 s vl s1 vl1"
  then obtain CID where rs: "reach s" and ph: "phase s CID > disPH" (is "?ph < _")
  and PID: "PID ∈∈ paperIDs s CID"
  and ss1: "eqExcPID s s1" and vl1: "vl1 = []"
  using reachNT_reach unfolding Δ3_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have "?react"
    proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      let ?ph' = "phase s' CID"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ paperIDs s' CID" using PID rs by (metis paperIDs_mono step)
      have ph': "phase s' CID > disPH" using ph rs by (meson less_le_trans local.step phase_increases)
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have φ: "¬ φ ?trn" using ph step unfolding φ_def2 apply (auto simp: uu_defs)
        using PID less_not_refl2 paperIDs_equals rs by blast (* safety crucialy used *)
        have vl: "vl' = vl" using c φ unfolding consume_def by (cases vl) auto
        obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
        let ?trn1 = "Trans s1 a ou1 s1'"
        have s's1': "eqExcPID s' s1'" using eqExcPID_step[OF ss1 step step1] .
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID_step_φ[OF ss1 step step1] .
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def using φ1 by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqExcPID_step_out[OF ss1 step step1 rsT rs1 PID] by simp
        next
          have "Δ3 s' vl' s1' vl1" using ph' PID' s's1' unfolding Δ3_def vl1 by auto
          thus "?Δ s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl1 by simp
  qed
qed

(* Exit arguments: *)
definition K1exit where
"K1exit cid s ≡
 (PID ∈∈ paperIDs s cid ∧ phase s cid ≥ disPH ∧
  ¬ (∃ uid. isPC s cid uid ∧ pref s uid PID ≠ Conflict))"

lemma invarNT_K1exit: "invarNT (K1exit cid)"
unfolding invarNT_def apply (safe dest!: reachNT_reach)
  subgoal for _ a apply(cases a)
    subgoal for x1 apply(cases x1) apply (fastforce simp add: c_defs K1exit_def geq_noPH_confIDs)+ .
    subgoal for x2
      apply(cases x2)
            apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
           apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
          apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
         apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
        apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
        subgoal for x61 apply(cases "x61 = cid")
           apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+ .
        apply (fastforce simp add: u_defs K1exit_def paperIDs_equals) .
    subgoal for x3 apply(cases x3) apply (fastforce simp add: uu_defs K1exit_def)+ .
    by auto
  done

lemma noVal_K1exit: "noVal (K1exit cid) v"
apply(rule noφ_noVal)
unfolding noφ_def apply safe
  subgoal for _ a apply(cases a)
        apply (fastforce simp add: c_defs K1exit_def)
       apply (fastforce simp add: c_defs K1exit_def)
    subgoal for x3
      apply(cases x3) apply (auto simp add: uu_defs K1exit_def)
      apply (metis paperIDs_equals reachNT_reach) (* crucial use of safety *) .
    by auto
  done

lemma unwind_exit_Δe: "unwind_exit Δe"
proof
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and Δe: "Δe s vl s1 vl1"
  hence vl: "vl ≠ []" using reachNT_reach unfolding Δe_def by auto
  then obtain CID where "K1exit CID s" using Δe unfolding K1exit_def Δe_def by auto
  thus "vl ≠ [] ∧ exit s (hd vl)" apply(simp add: vl)
  by (metis rsT exitI2 invarNT_K1exit noVal_K1exit)
qed

theorem secure: secure
apply(rule unwind_decomp3_secure[of Δ1 Δ2 Δe Δ3])
using
init_Δ1
unwind_cont_Δ1 unwind_cont_Δ2 unwind_cont_Δ3
unwind_exit_Δe
by auto

end