Theory Paper_Aut_PC

theory Paper_Aut_PC
imports "../Observation_Setup" Paper_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsection ‹Confidentiality protection from users who are not the
paper's authors or PC members›

text ‹We verify the following property:

\ \\
A group of users UIDs
learns nothing about the various uploads of a paper PID
(save for the non-existence of any upload)
unless/until one of the following occurs:
\begin{itemize}
\item a user in UIDs becomes the paper's author or
\item a user in UIDs becomes a PC member in the paper's conference
and the conference moves to the bidding phase.
\end{itemize}
›

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

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_isAut_isPC_isChair:
assumes "reachNT s" and "uid ∈ UIDs"
shows
"¬ isAut s cid uid PID ∧
 (isPC s cid uid ⟶ ¬ PID ∈∈ paperIDs s cid ∨ phase s cid ≤ subPH) ∧
 (isChair s cid uid ⟶ ¬ PID ∈∈ paperIDs s cid ∨ phase s cid ≤ subPH)"
  using assms
  apply (cases rule: reachNT_state_cases)
   apply (auto simp: istate_def)[]
  apply clarsimp
    (* safety property used: isChair_isPC *)
  by (simp add: T.simps assms(1) isAUT_def isChair_isPC not_less_eq_eq reachNT_reach)


lemma P_φ_γ:
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_isAut_isPC_isChair[OF 1] 2 unfolding T.simps φ_def2
by (auto simp add: u_defs)

(* Note: the following alternative formulation is not always guaranteed to hold,
due to the trigger T speaking about s', not s:
lemma P_φ_γ:
assumes 1: "¬ T (Trans s a ou s')" and 2: "step s a = (ou,s')" "φ (Trans s a ou s')"
shows "¬ γ (Trans s a ou s')"
using 1 2 unfolding T.simps φ_def2
by (auto simp add: u_defs)
*)

text ‹major› lemma eqButPID_step_out:
assumes s's1': "eqButPID 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_isAut_isPC_isChair[OF sT UIDs]
  note eqs = eqButPID_imp[OF s's1']
  note eqs' = eqButPID_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 eqButPID_def eeqButPID_def eqButC
  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)
    with * show ?thesis
    proof (cases x4)
      case (rPaperC x61 x62 x63 x64)
      then show ?thesis using * Ract by (clarsimp; metis not_less_eq_eq)
    next
      case (rMyReview x81 x82 x83 x84)
      then show ?thesis using * Ract by (auto simp: getNthReview_def)
    next
      case (rReviews x91 x92 x93 x94)
      then show ?thesis using * Ract by (clarsimp; metis Suc_leD eqButPID_imp2 not_less_eq_eq s's1')
    qed auto
  next
    case (Lact x5)
    then show ?thesis using * by (cases x5; auto)
  qed
qed

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡ ¬ (∃cid. PID ∈∈ paperIDs s cid) ∧ s = s1 ∧ B vl vl1"

definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡
 ∃cid. PID ∈∈ paperIDs s cid ∧ phase s cid = subPH ∧ eqButPID s s1"

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

definition Δe :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δe s vl s1 vl1 ≡
 ∃cid. PID ∈∈ paperIDs s cid ∧ phase s cid > subPH ∧ vl ≠ []"

lemma istate_Δ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, goal_cases)
  case (1 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: "∀cid. PID ∉ set (paperIDs s cid)"
  using reachNT_reach unfolding Δ1_def B_def by auto
  show ?case (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof (rule, goal_cases)
      case (1 a ou s' 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"
        apply(cases a)
        subgoal by simp
        subgoal for x2 apply(cases x2) using step pid by(auto simp: u_defs)
        by simp_all
      hence vl': "vl' = vl" using c unfolding consume_def by auto
      show ?case (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 "disjAll {Δ1, Δ2, Δe} s' vl' s' vl1"
          proof (cases "∃cid. PID ∈∈ paperIDs s' cid")
            case False hence "Δ1 s' vl' s' vl1"
              by (simp add: Δ1_def B_def vl vl')
            thus ?thesis by simp
          next
            case True
            hence "Δ2 s' vl' s' vl1"
              using step pid
              apply (simp add: Δ2_def vl' vl)
              apply (erule exE)
              subgoal for cid apply (rule exI[of _ cid])
                apply (cases a)
                  subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
                  subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
                  subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
                  by simp_all
              done
            thus ?thesis by simp
          qed
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl by simp
  qed
qed

lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2,Δ3,Δe}"
proof(rule,goal_cases)
  case (1 s vl s1 vl1)
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ2 s vl s1 vl1"
  then obtain cid where rs: "reach s"
    and pid: "PID ∈∈ paperIDs s cid" and ss1: "eqButPID s s1"
    and ph: "phase s cid = subPH"
    using reachNT_reach unfolding Δ2_def by auto

  have cid: "cid ∈∈ confIDs s"
    by (metis paperIDs_confIDs pid rs)

  from pid ph cid have
    pid1: "PID ∈∈ paperIDs s1 cid"
    and ph1: "phase s1 cid = subPH"
    and cid1: "cid ∈∈ confIDs s1"
    by (auto simp add: eqButPID_imp[OF ss1])


  show ?case (is "?iact ∨ (_ ∧ ?react)")
  proof (cases vl1)
    case (Cons v vl1') note this[simp]
    obtain uid1 where aut1: "isAut s1 cid uid1 PID"
      thm paperID_ex_userID
      using paperID_ex_userID[OF rs1 pid1] by auto
    have uid1: "uid1 ∈∈ userIDs s1"
      by (metis roles_userIDs rs1 aut1)

    from aut1 have "isAut s cid uid1 PID"
      using ss1 aut1 by (simp add: eqButPID_imp[OF ss1])
    with reachNT_non_isAut_isPC_isChair[OF rsT] uid1 have uid1_ne: "uid1∉UIDs"
      by auto

    let ?a1 = "(Uact (uPaperC cid uid1 (pass s1 uid1) PID v))"
    obtain s1' where step: "step s1 ?a1 = (outOK,s1')" and s1's1: "eqButPID s1' s1"
      by (cases "paper s1 PID")
         (auto simp add: u_defs cid1 uid1 pid1 ph1 aut1 eqButPID_def eeqButPID_def)

    have "?iact"
    proof
      show "step s1 ?a1 = (outOK,s1')" using step .
      show "φ (Trans s1 ?a1 outOK s1')" by simp
      show "consume (Trans s1 ?a1 outOK s1') vl1 vl1'" by (simp add: consume_def)
      show "¬γ (Trans s1 ?a1 outOK s1')" by (simp add: uid1_ne)
      have "Δ2 s vl s1' vl1'" unfolding Δ2_def
        apply (rule exI[where x=cid])
        using ph pid
        apply clarsimp
        by (metis s1's1 eqButPID_sym eqButPID_trans ss1)
      thus "disjAll {Δ2, Δ3, Δe} s vl s1' vl1'" by simp
    qed
    thus ?thesis by simp
  next
    case Nil note this[simp]
    have "?react"
    proof (rule, goal_cases)
      case (1 a ou s' vl')
      assume STEP: "step s a = (ou, s')" and "¬ T (Trans s a ou s')"
        and CONSUME: "consume (Trans s a ou s') vl vl'"

      have ph': "phase s' cid ≥ subPH"
        by (smt (verit) STEP ph phase_increases)

      have pid': "PID ∈∈ paperIDs s' cid" using pid STEP
        by (metis paperIDs_mono)

      {
        fix s1 vl1
        assume "phase s' cid ≠ subPH" "vl'≠[]"
        hence "Δe s' vl' s1 vl1"
          unfolding Δe_def
          apply -
          apply(rule exI[of _ cid])
          using STEP CONSUME ph
          apply (cases a)
          subgoal for x1 apply (cases x1) apply(auto simp: c_defs) .
          subgoal for x2 apply (cases x2) apply(auto simp: u_defs consume_def pid) .
          subgoal for x3 apply (cases x3) apply(auto simp: uu_defs) .
          by simp_all
      } note Δe=this

      obtain s1' ou' where
        STEP': "step s1 a = (ou',s1')" and s's1': "eqButPID s' s1'"
        using eqButPID_step[OF ss1 STEP]
        by fastforce

      from eqButPID_step_φ[OF ss1 STEP STEP']
      have φ_eq: "φ (Trans s1 a ou' s1') = φ (Trans s a ou s')" by simp

      show ?case (is "?match ∨ ?ignore")
      proof (cases "φ (Trans s a ou s')")
        case True note φ=this

        then obtain cid' uid p where
          a[simp]: "a=Uact (uPaperC cid' uid p PID (hd vl))" "ou=outOK"
          using CONSUME
          by (cases "(Trans s a ou s')" rule: f.cases) (auto simp add: consume_def)

        from STEP pid have [simp]: "cid'=cid"
          by (simp add: u_defs paperIDs_equals[OF rs])

        from φ_step_eqButPID[OF φ STEP] have ss': "eqButPID s s'" .

        have nγ: "¬γ (Trans s a ou s')"
          using P_φ_γ[OF rsT STEP] by simp

        have ph': "phase s' cid = subPH"
          using STEP by (auto simp add: u_defs)

        have ?ignore
        proof
          show "¬ γ (Trans s a ou s')" by (rule nγ)
          have "Δ2 s' vl' s1 vl1"
            unfolding Δ2_def
            using ph' pid' eqButPID_trans[OF eqButPID_sym[OF ss'] ss1]
            by auto
          thus "disjAll {Δ2, Δ3, Δe} s' vl' s1 vl1" by simp
        qed
        thus ?thesis by simp
      next
        case False note φ=this
        with CONSUME have [simp]: "vl'=vl" by (simp add: consume_def)

        have ?match proof
          show "validTrans (Trans s1 a ou' s1')" using STEP' by simp
          show "consume (Trans s1 a ou' s1') vl1 vl1" using φ
            by (simp add: consume_def φ_eq)
          show "γ (Trans s a ou s') = γ (Trans s1 a ou' s1')" by simp
          show "γ (Trans s a ou s') ⟹ g (Trans s a ou s') = g (Trans s1 a ou' s1')"
            using eqButPID_step_out[OF ss1 STEP STEP' rsT rs1 pid]
            by simp
          show "disjAll {Δ2, Δ3, Δe} s' vl' s1' vl1"
          proof (cases "phase s' cid = subPH")
            case True
            hence "Δ2 s' vl' s1' vl1"
              unfolding Δ2_def
              using eqButPID_step[OF ss1 STEP STEP']
              using ph' pid' by auto
            thus ?thesis by simp
          next
            case False with ph' have ph': "subPH < phase s' cid" by simp
            show ?thesis proof (cases "vl'=[]")
              case False
              hence "Δe s' vl' s1' vl1" using Δe ph' by simp
              thus ?thesis by simp
            next
              case True
              hence "Δ3 s' vl' s1' vl1"
                unfolding Δ3_def
                apply(intro exI[of _ cid])
                using ph' pid' eqButPID_step[OF ss1 STEP STEP']
                by simp
              thus ?thesis by simp
            qed
          qed
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis by simp
  qed
qed

lemma unwind_cont_Δ3: "unwind_cont Δ3 {Δ3,Δe}"
proof (rule, goal_cases)
  case (1 s vl s1 vl1)
  assume rsT: "reachNT s" and rs1: "reach s1" and Δ: "Δ3 s vl s1 vl1"
  thm Δ3_def
  then obtain cid where ss1: "eqButPID s s1" and [simp]: "vl=[]" "vl1=[]"
    and pid: "PID ∈∈ paperIDs s cid" and ph: "subPH < phase s cid"
    unfolding Δ3_def by auto

  from rsT have rs: "reach s"
    by (metis reachNT_reach)

  from pid ph have
    pid1: "PID ∈∈ paperIDs s1 cid"
    and ph1: "subPH < phase s1 cid"
    using ss1
    by (auto simp add: eqButPID_imp)


  thus ?case (is "_ ∨ (_ ∧ ?react)")
  proof -
    have "?react"
    proof (rule, goal_cases)
      case (1 a ou s' vl')
      assume STEP: "step s a = (ou, s')" and NT: "¬ T (Trans s a ou s')" (is "¬T ?trn")
        and CONSUME: "consume (Trans s a ou s') vl vl'"

      show ?case (is "?match ∨ _")
      proof -

        have ph': "subPH < phase s' cid"
         using STEP ph phase_increases by (meson le_trans not_less)

        have [simp]: "vl'=[]" using CONSUME by (auto simp add: consume_def)

        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': "eqButPID s' s1'" using eqButPID_step[OF ss1 STEP STEP1] .

        from s's1' ph' have ph1': "subPH < phase s1' cid"
          by (simp add: eqButPID_imp)

        have φ: "¬ φ ?trn1"
          using STEP1 ph1' unfolding φ_def2 by (auto simp: u_defs paperIDs_equals[OF rs1 pid1])

        have ?match proof
          show "validTrans ?trn1" using STEP1 by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def using φ by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqButPID_step_out[OF ss1 STEP STEP1 rsT rs1 pid] by simp
        next
          have "Δ3 s' vl' s1' vl1" using ph' s's1' paperIDs_mono[OF STEP pid]
            unfolding Δ3_def by auto
          thus "disjAll {Δ3, Δe} s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?case by simp
  qed
qed


definition K1exit where
"K1exit s ≡ ∃cid. phase s cid > subPH ∧ PID ∈∈ paperIDs s cid"

lemma invarNT_K1exit: "invarNT K1exit"
  unfolding invarNT_def apply (safe dest!: reachNT_reach)
  subgoal for _ a apply(cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs K1exit_def) .
    subgoal for x2 apply (cases x2)
      apply(auto simp: u_defs K1exit_def paperIDs_equals)
      apply (metis less_nat_zero_code)
      apply (metis Suc_lessD) .
    subgoal for x3 apply (cases x3, auto simp: uu_defs K1exit_def) .
    by simp_all
  done

lemma noVal_K1exit: "noVal K1exit v"
  apply(rule noφ_noVal)
  unfolding noφ_def apply safe
  subgoal for _ a apply(cases a)
    subgoal by simp
    subgoal for x2
      apply(cases x2, auto simp add: u_defs K1exit_def) []
      apply (metis reachNT_reach less_not_refl paperIDs_equals) .
    by simp_all
  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
  hence "K1exit 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
    istate_Δ1
    unwind_cont_Δ1 unwind_cont_Δ2 unwind_cont_Δ3
    unwind_exit_Δe
  by auto

end