Theory Decision_NCPC_Aut

theory Decision_NCPC_Aut
imports "../Observation_Setup" Decision_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

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

text ‹We verify the following property:

A group of users UIDs learn
nothing about the various updates of a paper's decision
(save for the non-existence of any update)
unless/until one of the following happens:
\begin{itemize}
\item 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,
or
\item a user in UIDs becomes a PC member in the paper's conference or an author of the paper,
and the conference moves to the notification phase
\end{itemize}
›

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)
    ∨
    (∃ cid. PID ∈∈ paperIDs s' cid ∧ isPC s' cid uid ∧ phase s' cid ≥ notifPH)
    ∨
    isAUT s' uid PID ∧ (∃ cid. PID ∈∈ paperIDs s' cid ∧ phase s' cid ≥ notifPH)
 )"

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 ∧ phase s cid < notifPH) ∧
 (PID ∈∈ paperIDs s cid ∧ isChair s cid uid ∧ phase s cid ≥ disPH
     ⟶ pref s uid PID = Conflict ∧ phase s cid < notifPH) ∧
 (isAut s cid uid PID ⟶ phase s cid < notifPH)"
  using assms
  apply induct
   apply (auto simp: istate_def)[]
  apply(intro conjI)
  subgoal for trn apply(cases trn, fastforce simp: T.simps)[] .
  subgoal
    using T.simps isChair_isPC[OF reachNT_reach] not_less
      reach_PairI[OF reachNT_reach] validTrans validTrans_Trans_srcOf_actOf_tgtOf
    by (metis (no_types, opaque_lifting) isChair_isPC)
  by (metis T.elims(3) reach.Step[OF reachNT_reach] isAUT_def isAut_paperIDs not_le_imp_less 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 T.simps φ_def2
by (force 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 (rDecs x101 x102 x103 x104)
      then show ?thesis using * Ract by (clarsimp; metis)
    next
      case (rFinalDec x131 x132 x133 x134)
      then show ?thesis using * Ract by (clarsimp; metis Suc_leD Suc_leI not_less_eq_eq)
    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"

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 ∧
   isChair 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)
  ∨
  (∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid ≥ disPH ∧
          ¬ (∃ uid. isChair s cid uid ∧ pref s uid PID ≠ Conflict))
 )"

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, 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 PID_ph': "⋀ cid. PID ∈∈ paperIDs s' cid ⟹ phase s' cid < disPH" using PID step rs
              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
            hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using PID_ph' 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" using PID_ph by auto
            have PID': "PID ∈∈ paperIDs s' CID" by (metis PID paperIDs_mono step)
            show ?thesis
            proof(cases "phase s' CID < disPH")
              case True note ph' = True
              hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using vl ph' PID' apply auto
              by (metis reach_PairI paperIDs_equals rs step)
              thus ?thesis by auto
            next
              case False note ph' = False
              hence ph': "phase s' CID = disPH" using ph PID step rs
                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
              show ?thesis
              proof(cases "∃uid. isChair s' CID uid ∧ pref s' uid PID ≠ Conflict")
                case True
                hence "Δ2 s' vl' s' vl1" unfolding Δ2_def vl' using vl ph' PID' by auto
                thus ?thesis by auto
              next
                case False
                hence "Δe s' vl' s' vl1" unfolding Δe_def vl' using vl ph' PID' 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: "isChair 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: "isChair s1 CID uid" "pref s1 uid PID ≠ Conflict" using ss1 uid unfolding eqExcPID_def by auto
    define a1 where "a1 ≡ UUact (uuDec 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_uuDec_step_eqExcPID by auto
    have ss1': "eqExcPID s s1'" using eqExcPID_trans[OF ss1 s1s1'] .
    hence many_s1': "PID ∈∈ paperIDs s1' CID" "isChair 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': "isChair s' CID uid ∧ pref s' uid PID ≠ Conflict"
      using uid step rs ph PID pref_Conflict_disPH isChair_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: "Δ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 ph': "?ph' > disPH" using ph step by (metis less_le_trans phase_increases)
      have PID': "PID ∈∈ paperIDs s' CID" using PID step by (metis paperIDs_mono)

      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
        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 _] ph 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. isChair 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)+ .
     apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+ .
  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) .
    by auto
  done

definition K2exit where
"K2exit cid s ≡ PID ∈∈ paperIDs s cid ∧ phase s cid > disPH"

lemma invarNT_K2exit: "invarNT (K2exit 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 K2exit_def geq_noPH_confIDs)+ .
    subgoal for x2 apply(cases x2)
      apply (fastforce simp add: u_defs K2exit_def paperIDs_equals)+ .
    subgoal for x3 apply(cases x3)
         apply (fastforce simp add: uu_defs K2exit_def)+ .
    by auto
  done

lemma noVal_K2exit: "noVal (K2exit cid) v"
apply(rule noφ_noVal)
unfolding noφ_def apply safe
  subgoal for _ a apply(cases a)
        apply (fastforce simp add: c_defs K2exit_def)
       apply (fastforce simp add: c_defs K2exit_def)
    subgoal for x3 apply(cases x3)
      apply (auto simp add: uu_defs K2exit_def)
      apply (metis less_not_refl paperIDs_equals reachNT_reach) .
    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 ∨ K2exit CID s" using Δe unfolding K1exit_def K2exit_def Δe_def by auto
  thus "vl ≠ [] ∧ exit s (hd vl)" apply(simp add: vl)
  by (metis rsT exitI2 invarNT_K1exit noVal_K1exit invarNT_K2exit noVal_K2exit)
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