Theory Reviewer_Assignment_NCPC_Aut

theory Reviewer_Assignment_NCPC_Aut
imports "../Observation_Setup" Reviewer_Assignment_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 reviewers assigned to a paper PID
except for the fact that they are PC members having no conflict with that paper
unless/until one of the following occurs:
\begin{itemize}
\item the user becomes a PC member in the paper's conference having no conflict
     with that paper and the conference moves to the reviewing phase,
or
\item the user becomes 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 ≥ revPH)
    ∨
    (∃ cid. PID ∈∈ paperIDs s' cid ∧ isAut s' cid uid PID ∧ phase s' cid ≥ notifPH)
 )"


declare T.simps [simp del]

(*
The bound says that a sequence of values vl,
i.e., a sequence of pairs [(uid_1,Uids_1),...,(uid_n,Uids_n)]
representing the users uid_i appointed as reviewers and the set
of PC members Uids_i not having conflict with paper ID at the time,
cannot be distinguished from a sequence of values
vl' = [(uid'_1,Uids'_1),...,(uid'_m,Uids'_m)] provided that
-- uid'_1,...,uid'_m are all distinct
-- Uids'_1 are all equal, and they are all equal to U
-- uid'_1 is in U

where U = Uids_1. Note actually that, because in the Reviewing phase
conflicts can no longer be changed, we actually have
U = Uids_1 = ... = Uids_n, which explains the above bound.

Thus, the second component of values (which turns out be constant)
is only collected in order to be able to express the following piece of information:
"the appointed reviewers are PC members having no conflict with paper".
*)

definition B :: "value list ⇒ value list ⇒ bool" where
"B vl vl1 ≡
 vl ≠ [] ∧
 distinct (map fst vl1) ∧ fst ` (set vl1) ⊆ snd (hd vl) ∧ snd ` (set vl1) = {snd (hd 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 ⟶ pref s uid PID = Conflict ∨ phase s cid < revPH)
 ∧
 (PID ∈∈ paperIDs s cid ∧ isChair s cid uid ⟶ pref s uid PID = Conflict ∨ phase s cid < revPH)
 ∧
 (PID ∈∈ paperIDs s cid ∧ isAut s cid uid PID ⟶
    phase s cid < notifPH)"
  using assms
  apply induct
  subgoal by (auto simp: istate_def)
  subgoal apply(intro conjI)
    subgoal by (metis (no_types, lifting) T.simps not_le_imp_less trans.collapse)
    subgoal by (metis (mono_tags, lifting) reachNT_reach T.simps isChair_isPC not_le_imp_less reach.Step trans.collapse)
    subgoal by (metis T.simps not_le_imp_less trans.collapse) .
  done

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 (fastforce simp: c_defs isRev_imp_isRevNth_getReviewIndex)

lemma T_φ_γ_stronger:
assumes s: "reach s" and 0: "PID ∈∈ paperIDs s cid"
and 2: "step s a = (ou,s')" "φ (Trans s a ou s')"
and 1:  "∀ uid ∈ UIDs. isChair s cid uid ⟶ pref s uid PID = Conflict ∨ phase s cid < revPH"
shows "¬ γ (Trans s a ou s')"
proof-
  have "¬ (∃ uid ∈ UIDs. ∃ cid. PID ∈∈ paperIDs s cid ∧
  isChair s cid uid ∧ pref s uid PID ≠ Conflict ∧ phase s cid ≥ revPH)"
  using 0 1 s by (metis not_le paperIDs_equals)
  thus ?thesis using assms unfolding T.simps φ_def2 by (force simp add: c_defs)
qed

lemma T_φ_γ_1:
assumes s: "reachNT s" and s1: "reach s1" and PID: "PID ∈∈ paperIDs s cid"
and ss1: "eqExcPID2 s s1"
and step1: "step s1 a = (ou1,s1')" and φ1: "φ (Trans s1 a ou1 s1')"
and φ: "¬ φ (Trans s a ou s')"
shows "¬ γ (Trans s1 a ou1 s1')"
proof-
  have "∀ uid ∈ UIDs. isChair s cid uid ⟶ pref s uid PID = Conflict ∨ phase s cid < revPH"
  using reachNT_non_isPC_isChair[OF s] PID by auto
  hence 1: "∀ uid ∈ UIDs. isChair s1 cid uid ⟶ pref s1 uid PID = Conflict ∨ phase s1 cid < revPH"
  using ss1 unfolding eqExcPID2_def using eqExcRLR_imp2 by fastforce
  have PID1: "PID ∈∈ paperIDs s1 cid" using PID ss1 eqExcPID2_imp by auto
  show ?thesis apply(rule T_φ_γ_stronger[OF s1 PID1 step1 φ1]) using 1 by auto
qed

lemma notInPaperIDs_eqExLRL_roles_eq:
assumes s: "reach s" and s1: "reach s1" and PID: "¬ PID ∈∈ paperIDs s cid"
and eq: "eqExcPID2 s s1"
shows "roles s cid uid = roles s1 cid uid"
proof-
  have "¬ PID ∈∈ paperIDs s1 cid" using PID eq unfolding eqExcPID2_def by auto
  hence "¬ isRev s cid uid PID ∧ ¬ isRev s1 cid uid PID" using s s1 PID by (metis isRev_paperIDs)
  thus ?thesis using eq unfolding eqExcPID2_def eqExcRLR_def
  by (metis Bex_set_list_ex filter_True isRev_def)
qed


(* major *) lemma eqExcPID2_step_out:
assumes ss1: "eqExcPID2 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 ph: "phase s cid ≥ revPH"
and φ: "¬ φ (Trans s a ou s')" and φ1: "¬ φ (Trans s1 a ou1 s1')"
and UIDs: "userOfA a ∈ UIDs"
shows "ou = ou1"
proof-
  note s = reachNT_reach[OF sT]
  have s': "reach s'" and s1': "reach s1'" by (metis reach_PairI s s1 step step1)+
  have s's1': "eqExcPID2 s' s1'" by (metis PID φ eqExcPID2_step ph s ss1 step step1)
  note Inv = reachNT_non_isPC_isChair[OF sT UIDs]
  note eqs = eqExcPID2_imp[OF ss1]
  note eqs' = eqExcPID2_imp1[OF ss1]

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID2_def
  note simps2[simp] = eqExcRLR_imp[of s _ _ _ s1, OF s] eqExcRLR_imp[of s' _ _ _ s1']
                eqExcRLR_imp[of s _ _ _ s1'] eqExcRLR_imp[of s' _ _ _ s1]
      eqExcRLR_imp2[of s _ _ s1] eqExcRLR_imp2[of s' _ _ s1']
                eqExcRLR_imp2[of s _ _ s1'] eqExcRLR_imp2[of s' _ _ s1]
      eqExcRLR_set[of "(roles s cid uid)" "(roles s1 cid uid)" for cid uid]
      eqExcRLR_set[of "(roles s cid uid)" "(roles s1' cid uid)" for cid uid]
      eqExcRLR_set[of "(roles s' cid uid)" "(roles s1 cid uid)" for cid uid]
      eqExcRLR_set[of "(roles s' cid uid)" "(roles s1' cid uid)" for cid uid]
      foo2 foo3
      eqExcRLR_imp_isRevRole_imp

  {fix cid uid p pid assume "a = Ract (rMyReview cid uid p pid)"
   hence ?thesis
   using step step1 eqs eqs' s s1 UIDs PID φ φ1 ph
    paperIDs_equals[OF s] Inv
   apply (auto simp add: isRev_getRevRole getRevRole_Some)[]
   apply (metis eqExcPID2_imp' isRev_isPC not_less option.inject pref_Conflict_isRev role.distinct role.inject ss1
                isRev_isPC not_less pref_Conflict_isRev simps2(1) simps2(8) isRev_getRevRole getRevRole_Some)+
   done
  } note this[simp]

  {fix cid uid p pid assume "a = Ract (rFinalDec cid uid p pid)"
   hence ?thesis
   apply(cases "pid = PID")
   using step step1 eqs eqs' s s1 UIDs PID φ φ1 ph
   paperIDs_equals[OF s] Inv using eeqExcPID_RDD by fastforce+
  } note this[simp]

  show ?thesis
    using step step1 eqs eqs' s s1 UIDs PID φ φ1 ph
    paperIDs_equals[OF s] Inv
    apply(cases a)
      subgoal for x1 by (cases x1; auto)
      subgoal for x2 apply(cases x2)
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal apply clarsimp
          subgoal by (metis eqExcPID2_imp' isRev_pref_notConflict_isPC nat_neq_iff simps2(7) ss1)
          subgoal by (metis isRev_pref_notConflict_isPC nat_neq_iff simps2(1)) . .
      subgoal for x3 apply(cases x3)
        subgoal by auto
        subgoal by auto
        subgoal apply clarsimp
          subgoal by (metis isRev_pref_notConflict_isPC le_antisym less_imp_le_nat n_not_Suc_n simps2(1) simps2(5))
          subgoal by (metis isRev_pref_notConflict_isPC le_antisym less_imp_le_nat n_not_Suc_n simps2(1)) .
        subgoal by auto .
      subgoal for x4 apply(cases x4)
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by clarsimp (metis eqExcPID2_RDD ss1)
        subgoal apply clarsimp
          subgoal by (metis eqExcPID2_RDD ss1)
          subgoal by auto .
        subgoal by auto
        subgoal by auto
        subgoal by clarsimp (metis eqExcPID2_imp2 less_imp_le_nat not_less_eq_eq ss1)
        subgoal by clarsimp (metis less_imp_le_nat not_less_eq_eq)
        subgoal by clarsimp (metis discussion.inject less_imp_le_nat not_less_eq_eq)
        subgoal by clarsimp (metis (mono_tags, lifting) Suc_le_lessD not_less_eq)
        subgoal by auto
        subgoal by clarsimp linarith .
      subgoal for x5 apply(cases x5)
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by clarsimp (metis (no_types, opaque_lifting) empty_iff list.set(1)
                           notInPaperIDs_eqExLRL_roles_eq notIsPC_eqExLRL_roles_eq simps2(5) ss1)
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by auto
        subgoal by clarsimp (smt (verit) Suc_le_lessD eqExcRLR_imp filter_cong isRev_pref_notConflict_isPC not_less_eq)
        subgoal by clarsimp (metis Suc_le_lessD eqExcPID2_imp' not_less_eq ss1) .
    done
qed

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
 (∀ cid. PID ∈∈ paperIDs s cid ⟶ phase s cid < revPH) ∧ 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 = revPH ∧
   isChair s cid uid ∧ pref s uid PID ≠ Conflict ∧
   eqExcPID2 s s1 ∧
   distinct (map fst vl1) ∧
   fst ` (set vl1) ⊆ {uid'. isPC s cid uid' ∧ pref s uid' PID ≠ Conflict} ∧
   fst ` (set vl1) ∩ {uid'. isRev s1 cid uid' PID} = {} ∧
   snd ` (set vl1) ⊆ {{uid'. isPC s cid uid' ∧ pref s uid' PID ≠ Conflict}}"

definition Δ3 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ3 s vl s1 vl1 ≡
 ∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid > revPH ∧ eqExcPID2 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 ≥ revPH ∧
          ¬ (∃ uid. isChair s cid uid ∧ pref s uid PID ≠ Conflict))
  ∨
  (∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid ≥ revPH ∧
          snd (hd vl) ≠ {uid'. isPC s cid uid' ∧ pref s uid' PID ≠ Conflict})
  ∨
  (∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid > revPH)
 )"

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 B: "B vl vl1"
  and c_d: "distinct (map fst vl1) ∧ fst ` (set vl1) ⊆ snd (hd vl) ∧ snd ` (set vl1) = {snd (hd vl)}"
  and vl: "vl ≠ []"
  and PID_ph: "⋀ cid. PID ∈∈ paperIDs s cid ⟹ phase s cid < revPH"
  using reachNT_reach unfolding Δ1_def B_def by auto
  have rv: "⋀ cid. ¬ (∃ uid'. isRev s cid uid' PID)" using rs PID_ph
  by (metis isRev_geq_revPH isRev_paperIDs less_Suc_eq_le not_less_eq_eq)
  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" 
        apply(cases a)
        subgoal for x1 apply(cases x1) using step PID_ph by (fastforce simp: c_defs)+
        by simp_all
      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 < revPH" 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' c_d 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 < revPH" using PID_ph by auto
            have PID': "PID ∈∈ paperIDs s' CID" by (metis PID paperIDs_mono step)
            show ?thesis
            proof(cases "phase s' CID < revPH")
              case True note ph' = True
              hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using vl c_d ph' PID' apply auto
              by (metis reach_PairI paperIDs_equals rs step)
              thus ?thesis by auto
            next
              case False
              hence ph_rv': "phase s' CID = revPH ∧ ¬ (∃ uid'. isRev s' CID uid' PID)"
              using ph PID step rs rv
                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 isRev_def2)+ .
                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) ∧
                           snd (hd vl) = {uid'. isPC s' CID uid' ∧ pref s' uid' PID ≠ Conflict}")
                case True
                hence "Δ2 s' vl' s' vl1"
                unfolding Δ2_def B_def vl' using c_d ph_rv' PID' by auto
                thus ?thesis by auto
              next
                case False
                hence "Δe s' vl' s' vl1"
                unfolding Δe_def vl' using vl c_d ph_rv' 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 = revPH" (is "?ph = _") and ss1: "eqExcPID2 s s1"
  and PID: "PID ∈∈ paperIDs s CID"
  and dis: "distinct (map fst vl1)"
  and fst_isPC: "fst ` (set vl1) ⊆ {uid'. isPC s CID uid' ∧ pref s uid' PID ≠ Conflict}"
  and fst_isRev: "fst ` (set vl1) ∩ {uid'. isRev s1 CID uid' PID} = {}"
  and snd_isPC: "snd ` (set vl1) ⊆ {{uid'. isPC s CID uid' ∧ pref s uid' PID ≠ Conflict}}"
  using reachNT_reach unfolding Δ2_def by auto
  hence uid_notin: "uid ∉ UIDs"
    using reachNT_non_isPC_isChair rsT by fastforce
  note vl1_all = dis fst_isPC fst_isRev snd_isPC
  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
    obtain uid' where v1: "v1 = (uid', {uid'. isPC s CID uid' ∧ pref s uid' PID ≠ Conflict})"
    using snd_isPC unfolding vl1 by(cases v1) auto
    hence uid': "isPC s CID uid' ∧ pref s uid' PID ≠ Conflict"
    and uid'1: "¬ isRev s1 CID uid' PID"
    using fst_isPC fst_isRev unfolding vl1 by auto
    have uid1: "isChair s1 CID uid ∧ pref s1 uid PID ≠ Conflict"
    using ss1 uid unfolding eqExcPID2_def using eqExcRLR_imp2 by metis
    define a1 where "a1 ≡ Cact (cReview CID uid (pass s uid) PID uid')"
    obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')" by (metis prod.exhaust)
    let ?trn1 = "Trans s1 a1 ou1 s1'"
    have s1s1': "eqExcPID2 s1 s1'" using a1_def step1 cReview_step_eqExcPID2 by blast
    have ss1': "eqExcPID2 s s1'" using eqExcPID2_trans[OF ss1 s1s1'] .
    hence many_s1': "PID ∈∈ paperIDs s1' CID" "isChair s1' CID uid ∧ pref s1' uid PID ≠ Conflict"
    "phase s1' CID = revPH" "pass s1' uid = pass s uid"
    "isPC s1' CID uid' ∧ pref s1' uid' PID ≠ Conflict"
    using uid' uid PID ph unfolding eqExcPID2_def using eqExcRLR_imp2 apply auto by metis+
    hence more_s1': "uid ∈∈ userIDs s1'" "CID ∈∈ confIDs s1'"
    by (metis paperIDs_confIDs reach_PairI roles_userIDs rs1 step1 many_s1'(1))+
    have ou1: "ou1 = outOK" using step1 unfolding a1_def apply ( simp add: c_defs)
    using more_s1' many_s1' uid'1 by (metis roles_userIDs rs1)
    have f: "f ?trn1 = v1" unfolding a1_def v1 apply simp
    using ss1 unfolding eqExcPID2_def using eqExcRLR_imp2
    by (metis eqExcRLR_set isRevRoleFor.simps(3))
    have rs1': "reach s1'" using rs1 step1 by (auto intro: reach_PairI)
    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 "{uid'. isRev s1' CID uid' PID} ⊆ insert uid' {uid'. isRev s1 CID uid' PID}"
      using step1 unfolding a1_def ou1 by (auto simp add: c_defs isRev_def2 )
      hence "fst ` set vl1' ∩ {uid'. isRev s1' CID uid' PID} = {}"
      using fst_isRev dis unfolding vl1 v1 by auto
      hence "Δ2 s vl s1' vl1'" unfolding Δ2_def
      using PID ph ss1' uid using vl1_all unfolding vl1 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 isChair_persistent revPH_pref_persists[OF rs PID ] by auto
      have all_vl1':
      "fst ` (set vl1) ⊆ {uid'. isPC s' CID uid' ∧ pref s' uid' PID ≠ Conflict}"
      and "snd ` (set vl1) ⊆ {{uid'. isPC s' CID uid' ∧ pref s' uid' PID ≠ Conflict}}"
      using vl1_all
      apply (metis (full_types) empty_subsetI image_empty set_empty vl1)
      by (metis (lifting, no_types) empty_set image_is_empty subset_insertI vl1)
      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': "eqExcPID2 s' s1'" using eqExcPID2_step[OF rs ss1 step step1 PID] ph φ by auto
        show ?thesis
        proof(cases "ou = outErr ∧ ¬ γ ?trn")
          case True note ou = True[THEN conjunct1] and γ = True[THEN conjunct2]
          have s': "s' = s" using step ou by (metis step_outErr_eq)
          have ?ignore proof
            show "¬ γ ?trn" by fact
          next
            show "?Δ s' vl' s1 vl1"
            proof(cases "?ph' = revPH")
              case True
              hence "Δ2 s' vl' s1 vl1" using ss1 PID' uid' vl1_all unfolding Δ2_def vl1 s' by auto
              thus ?thesis by auto
            next
              case False hence ph': "?ph' > revPH" using ph rs step s' by blast
              show ?thesis
              proof(cases vl')
                case Nil
                hence "Δ3 s' vl' s1 vl1" using ss1 PID' ph' unfolding Δ3_def vl1 s' by auto
                thus ?thesis by auto
              next
                case Cons
                hence "Δe s' vl' s1 vl1" using PID' ph' unfolding Δe_def by auto
                thus ?thesis by auto
              qed
            qed
          qed
          thus ?thesis by auto
        next
          case False note ou_γ = False
          have φ1: "¬ φ ?trn1"
          using non_eqExcPID2_step_φ_imp[OF rs ss1 PID _ step step1 φ]
                T_φ_γ_1[OF rsT rs1 PID ss1 step1 _ φ] ou_γ by auto
          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 eqExcPID2_step_out[OF ss1 step step1 rsT rs1 PID _ φ φ1] ph by simp
          next
            show "?Δ s' vl' s1' vl1"
            proof(cases "?ph' = revPH")
              case True note ph' = True
              hence "Δ2 s' vl' s1' vl1" using PID' s's1' uid' ph' vl1_all unfolding Δ2_def vl1 by auto
              thus ?thesis by auto
            next
              case False hence ph': "?ph' > revPH" using ph rs step by (metis antisym_conv2 phase_increases)
              show ?thesis
              proof(cases vl')
                case Nil
                hence "Δ3 s' vl' s1' vl1" using s's1' PID' ph' unfolding Δ3_def vl1 by auto
                thus ?thesis by auto
              next
                case Cons
                hence "Δe s' vl' s1' vl1" using PID' ph' unfolding Δe_def by auto
                thus ?thesis by auto
              qed
            qed
          qed
          thus ?thesis by simp
        qed
      next
        case True note φ = True
        have s's: "eqExcPID2 s' s" using eqExcPID2_sym using φ_step_eqExcPID2[OF φ step]  .
        have s's1: "eqExcPID2 s' s1" using eqExcPID2_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' = revPH")
            case True
            hence "Δ2 s' vl' s1 vl1" using s's1 PID' uid' vl1_all unfolding Δ2_def vl1 by auto
            thus ?thesis by auto
          next
            case False hence ph': "?ph' > revPH" using ph rs step by (metis antisym_conv2 phase_increases)
            show ?thesis
            proof(cases vl')
                case Nil
                hence "Δ3 s' vl' s1 vl1" using s's1 PID' ph' unfolding Δ3_def vl1 by auto
                thus ?thesis by auto
              next
                case Cons
                hence "Δe s' vl' s1 vl1" using PID' ph' unfolding Δe_def by auto
                thus ?thesis by auto
              qed
            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 > revPH" (is "?ph > _")
  and PID: "PID ∈∈ paperIDs s CID" and ss1: "eqExcPID2 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 > revPH" 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(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': "eqExcPID2 s' s1'" using eqExcPID2_step[OF rs ss1 step step1 PID] ph φ by auto
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID2_step_φ[OF rs rs1 ss1 PID ph 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 eqExcPID2_step_out[OF ss1 step step1 rsT rs1 PID _ φ φ1] 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
      next
        case True note φ = True
        have s's: "eqExcPID2 s' s" using eqExcPID2_sym[OF φ_step_eqExcPID2[OF φ step]] .
        have s's1: "eqExcPID2 s' s1" using eqExcPID2_trans[OF s's ss1] .
        have ?ignore proof
          show "¬ γ ?trn" using T_φ_γ φ rsT step by auto
        next
          have "Δ3 s' vl' s1 vl1" using s's1 PID' ph' vl1 unfolding Δ3_def by auto
          thus "?Δ s' vl' s1 vl1" by auto
        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 ≥ revPH ∧
                ¬ (∃ 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 (auto simp add: u_defs K1exit_def paperIDs_equals)
      apply (metis less_eq_Suc_le less_not_refl paperIDs_equals) .
    subgoal for x3 apply(cases x3) apply (auto 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)
    subgoal for x1 apply(cases x1)
      apply (auto simp add: c_defs K1exit_def)
      by (metis paperIDs_equals reachNT_reach)
    by auto
  done

definition K2exit where
"K2exit cid s v ≡
 PID ∈∈ paperIDs s cid ∧ phase s cid ≥ revPH ∧
 snd v ≠ {uid'. isPC s cid uid' ∧ pref s uid' PID ≠ Conflict}"

lemma revPH_isPC_constant:
assumes s: "reach s"
and "step s a = (ou,s')"
and "pid ∈∈ paperIDs s cid" and "phase s cid ≥ revPH"
shows "isPC s' cid uid' = isPC s cid uid'"
  using assms
  apply(cases a)
  subgoal for x1 apply(cases x1)
           apply (auto simp add: c_defs)
    by (metis paperIDs_confIDs)
  subgoal for x2 apply(cases x2) apply (auto simp add: u_defs) .
  subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs) .
  by auto

lemma revPH_pref_constant:
assumes s: "reach s"
and "step s a = (ou,s')"
and "pid ∈∈ paperIDs s cid" and "phase s cid ≥ revPH"
shows "pref s' uid pid = pref s uid pid"
  using assms
  apply(cases a)
  subgoal for x1 apply(cases x1)
           apply (auto simp add: c_defs)
      apply (metis paperIDs_getAllPaperIDs)
     apply (metis Suc_n_not_le_n le_SucI paperIDs_equals)
    apply (metis Suc_n_not_le_n le_SucI paperIDs_equals) .
  subgoal for x2 apply(cases x2)
          apply (auto simp add: u_defs)
    apply (metis Suc_n_not_le_n paperIDs_equals) .
  subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs) .
  by auto

lemma invarNT_K2exit: "invarNT (λ s. K2exit cid s v)"
unfolding invarNT_def apply (safe dest!: reachNT_reach)
unfolding K2exit_def
by (smt (verit) Collect_cong le_trans paperIDs_mono phase_increases revPH_isPC_constant revPH_pref_constant)

(* An even more interesting invariant than the one in Review_Confidentiality/RAut:
it requires the binary version noVal2  *)
lemma noVal_K2exit: "noVal2 (K2exit cid) v"
  unfolding noVal2_def
  apply safe
  subgoal for _ a apply(cases a)
    subgoal for x1 apply(cases x1)
             apply (auto simp add: c_defs K2exit_def)
      by (metis paperIDs_equals reachNT_reach)+
    by auto
  done

definition K3exit where
"K3exit cid s ≡ PID ∈∈ paperIDs s cid ∧ phase s cid > revPH"

lemma invarNT_K3exit: "invarNT (K3exit cid)"
  unfolding invarNT_def
  apply (safe dest!: reachNT_reach)
  subgoal for _ a apply(cases a)
    subgoal for x1 apply(cases x1) apply (auto simp add: c_defs K3exit_def) .
    subgoal for x2 apply(cases x2) apply (auto simp add: u_defs K3exit_def) .
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K3exit_def) .
    by auto
  done

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