Theory Review_RAut_NCPC

theory Review_RAut_NCPC
imports "../Observation_Setup" Review_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsection ‹Confidentiality protection from users who are not the review's author or a PC member›

text ‹We verify the following property:

\ \\
A group of users UIDs learn nothing
about the various updates of the N'th review of a paper PID
except for the last edited version before notification
unless/until one of the following holds:
\begin{itemize}
\item a user in UIDs is the review's author, or
\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.
\end{itemize}
›

type_synonym "value" = rcontent

fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans _ (Uact (uReview cid uid p pid n rc)) _ _) = rc"
|
"f (Trans _ (UUact (uuReview cid uid p pid n rc)) _ _) = rc"

fun T :: "(state,act,out) trans ⇒ bool" where
"T (Trans _ _ ou s') =
 (∃ uid ∈ UIDs.
    isREVNth s' uid PID N
    ∨
    (∃ 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 ≠ [] ∧ vl1 ≠ [] ∧ last vl = last vl1"

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_isRevNth_isPC_isChair:
assumes "reachNT s" and "uid ∈ UIDs"
shows
"¬ isRevNth s cid uid PID N ∧
 (PID ∈∈ paperIDs s cid ∧ isPC s cid uid ⟶ pref s uid PID = Conflict ∨ phase s cid < disPH) ∧
 (PID ∈∈ paperIDs s cid ∧ isChair s cid uid ⟶ pref s uid PID = Conflict ∨ phase s cid < disPH)"
  using assms
  apply induct
   apply (auto simp: istate_def)[]
  apply(intro conjI)
  subgoal for trn apply(cases trn, auto simp: T.simps reachNT_reach isREVNth_def)[] .
  subgoal by (metis T.elims(3) not_le_imp_less tgtOf_simps)
  by (metis T.elims(3) isChair_isPC not_le_imp_less reach.Step reachNT_reach tgtOf_simps)

(* important: *) 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_isRevNth_isPC_isChair[OF 1] 2 unfolding T.simps φ_def2
apply (auto simp add: u_defs uu_defs) by (metis isRev_imp_isRevNth_getReviewIndex)+

(* major *) lemma eqExcPID_N_step_out:
assumes s's1': "eqExcPID_N s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and sP: "reachNT s" and s1: "reach s1"
and PID: "PID ∈∈ paperIDs s cid"
and ph: "phase s cid = revPH ∨ phase s cid = disPH"
and UIDs: "userOfA a ∈ UIDs"
shows "ou = ou1"
proof-
  note Inv = reachNT_non_isRevNth_isPC_isChair[OF sP UIDs]
  note eqs = eqExcPID_N_imp[OF s's1']
  note eqs' = eqExcPID_N_imp1[OF s's1']
  note eqss = eqExcPID_N_imp2[OF s's1']
  note s = reachNT_reach[OF sP]

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

  show ?thesis
  proof (cases a)
    case (Cact x1)
    with * show ?thesis by (cases x1; auto)
  next
    case (Uact x2)
    with * show ?thesis by (cases x2; auto)
  next
    case (UUact x3)
    with * show ?thesis by (cases x3; auto)
  next
    case (Ract x4)
    with * show ?thesis
    proof (cases x4)
      case (rMyReview x81 x82 x83 x84)
      with Ract * show ?thesis
        by clarsimp (metis eqExcPID_N_imp3' getRevRole_Some_Rev_isRevNth s's1')
    next
      case (rReviews x91 x92 x93 x94)
      with Ract * show ?thesis
        by clarsimp (metis eqss not_less)
    next
      case (rFinalReviews x121 x122 x123 x124)
      with Ract * show ?thesis
        by clarsimp (metis Suc_leD Suc_n_not_le_n)
    qed auto
  next
    case (Lact x5)
    with * show ?thesis by (cases x5; auto; presburger)
  qed
qed

(* major *) lemma eqExcPID_N2_step_out:
assumes ss1: "eqExcPID_N2 s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and sP: "reachNT s" and s1: "reach s1"
and r: "isRevNth s cid uid PID N"
and ph: "phase s cid ≥ revPH"
and UIDs: "userOfA a ∈ UIDs"
and decs_exit: "(reviewsPaper (paper s PID))!N ≠ [] ∧ (reviewsPaper (paper s1 PID))!N ≠ []"
shows "ou = ou1"
proof-
  note s = reachNT_reach[OF sP]
  note Inv = reachNT_non_isRevNth_isPC_isChair[OF sP UIDs]
  note eqs = eqExcPID_N2_imp[OF ss1]
  note eqs' = eqExcPID_N2_imp1[OF ss1]
  note eqss = eqExcPID_N2_imp2[OF ss1] eqExcPID_N2_imp3'[OF s ss1] eqExcPID_N2_imp33[OF ss1]

  have PID: "PID ∈∈ paperIDs s cid" using r by (metis isRevNth_paperIDs s)
  have PID1: "PID ∈∈ paperIDs s1 cid" using PID ss1 unfolding eqExcPID_N2_def by auto
  have r1: "isRevNth s1 cid uid PID N" by (metis eqs r)
  hence decs_exit': "(reviewsPaper (paper s' PID))!N ≠ [] ∧
                     (reviewsPaper (paper s1' PID))!N ≠ []"
  using nonempty_reviews_persist s s1 PID PID1 r r1 decs_exit step step1 by metis+

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_N2_def eeqExcPID_N2_def eqExcD2

  have "eqExcD2 (paper s PID) (paper s1 PID)"
  using eqExcPID_N2_imp[OF ss1] eeqExcPID_N2_imp by blast
  hence 1: "hd (reviewsPaper (paper s PID) ! N) =
            hd (reviewsPaper (paper s1 PID) ! N)"
  unfolding eqExcD2 eqExcNth2_def by auto

  { fix cid uid p pid assume a: "a = Ract (rFinalReviews cid uid p pid)"
    have ?thesis using step step1 eqExcPID_N2_imp[OF ss1]
      unfolding a
      apply clarsimp
      apply(intro nth_equalityI)
      subgoal by simp
      subgoal for i apply (cases "i ≠ N")
        subgoal by simp (smt (verit) eqExcPID_N2_imp3 getNthReview_def ss1)
        by (auto split: list.splits)
      subgoal for i ia
        apply (cases "pid = PID")
        subgoal
          apply(cases "reviewsPaper (paper s' PID) ! i")
          subgoal apply simp
            by (smt (verit) decs_exit eqExcPID_N2_imp3 getNthReview_def list.simps(4) nth_Cons_0 ss1)
          subgoal apply(cases "reviewsPaper (paper s1' PID) ! i ")
            subgoal apply simp
              by (metis (no_types, lifting) decs_exit eqExcD2 eqExcNth2_def neq_Nil_conv)
            subgoal apply simp
              by (metis (no_types, lifting) eqExcD2 eqExcNth2_def list.sel(1)) . .
        subgoal by simp . .
  } note this[simp]

  note * = step step1 eqs eqs' s s1 PID PID1 r r1 UIDs ph paperIDs_equals[OF s] Inv

  show ?thesis
  proof (cases a)
    case (Cact x1)
    with * show ?thesis by (cases x1; auto)
  next
    case (Uact x2)
    with * show ?thesis by (cases x2; auto)
  next
    case (UUact x3)
    with * show ?thesis by (cases x3; auto)
  next
    case (Ract x4)
    with * show ?thesis
    proof (cases x4)
      case (rMyReview x81 x82 x83 x84)
      with Ract * show ?thesis
        by clarsimp (metis eqss(2) getRevRole_Some_Rev_isRevNth)
    next
      case (rReviews x91 x92 x93 x94)
      with Ract * show ?thesis
        by clarsimp (metis eqss(1) not_less)
    qed auto
  next
    case (Lact x5)
    with * show ?thesis by (cases x5; auto; presburger)
  qed
qed

lemma eqExcPID_N_step_eqExcPID_N2:
assumes rs: "reach s"
and a: "a = Uact (uReview cid uid p PID N rc) ∨
        a = UUact (uuReview cid uid p PID N rc)" (is "?L ∨ ?R")
and ss1: "eqExcPID_N s s1"
and step: "step s a = (outOK,s')" and step1: "step s1 a = (outOK,s1')"
shows "eqExcPID_N2 s' s1'"
using a proof
  assume a: ?L
  have "isRevNth s cid uid PID N" using step unfolding a apply(simp add: u_defs uu_defs)
  by (metis isRev_imp_isRevNth_getReviewIndex)
  hence N: "N < length (reviewsPaper (paper s PID))"
  using rs by (metis isRevNth_less_length)
  hence N1: "N < length (reviewsPaper (paper s1 PID))"
  using ss1 unfolding eqExcPID_N_def eeqExcPID_N_def eqExcD eqExcNth_def by auto
  have "eqExcPID_N s' s1'" using assms by (metis eqExcPID_N_step)
  moreover have "hd (reviewsPaper (paper s' PID) ! N) = hd (reviewsPaper (paper s1' PID) ! N)"
  using step step1 N N1 unfolding a by(auto simp add: u_defs uu_defs)
  ultimately show ?thesis
  unfolding eqExcPID_N_def eqExcPID_N2_def eeqExcPID_N_def eeqExcPID_N2_def eqExcD2 eqExcD
  eqExcNth_def eqExcNth2_def by auto
next
  assume a: ?R
  have "isRevNth s cid uid PID N" using step unfolding a apply(simp add: u_defs uu_defs)
  by (metis isRev_imp_isRevNth_getReviewIndex)
  hence N: "N < length (reviewsPaper (paper s PID))"
  using rs by (metis isRevNth_less_length)
  hence N1: "N < length (reviewsPaper (paper s1 PID))"
  using ss1 unfolding eqExcPID_N_def eeqExcPID_N_def eqExcD eqExcNth_def by auto
  have "eqExcPID_N s' s1'" using assms by (metis eqExcPID_N_step)
  moreover have "hd (reviewsPaper (paper s' PID) ! N) = hd (reviewsPaper (paper s1' PID) ! N)"
  using step step1 N N1 unfolding a by(auto simp add: u_defs uu_defs)
  ultimately show ?thesis
  unfolding eqExcPID_N_def eqExcPID_N2_def eeqExcPID_N_def eeqExcPID_N2_def eqExcD2 eqExcD
  eqExcNth_def eqExcNth2_def by auto
qed

(* major *) lemma eqExcPID_N_step_φ_eqExcPID_N2:
assumes rs: "reach s"
and ss1: "eqExcPID_N s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and φ: "φ (Trans s a ou s')"
shows "eqExcPID_N2 s' s1'"
proof-
  obtain cid uid p rc where
  a: "a = Uact (uReview cid uid p PID N rc) ∨
      a = UUact (uuReview cid uid p PID N rc)" (is "?L ∨ ?R")
  and ou: "ou = outOK"
  using φ unfolding φ_def2 by blast
  have φ1: "φ (Trans s1 a ou1 s1')" using φ ss1 by (metis eqExcPID_N_step_φ_imp step step1)
  hence ou1: "ou1 = outOK" using φ unfolding φ_def2 by auto
  show ?thesis using eqExcPID_N_step_eqExcPID_N2[OF rs a ss1 step[unfolded ou] step1[unfolded ou1]] .
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.
    PID ∈∈ paperIDs s cid ∧ phase s cid = revPH ∧ ¬ (∃ uid. isREVNth s uid PID N) ∧
    s = s1 ∧ B vl vl1"

definition Δ3 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ3 s vl s1 vl1 ≡
 ∃ cid uid.
    PID ∈∈ paperIDs s cid ∧ phase s cid ∈ {revPH, disPH} ∧ isREVNth s uid PID N ∧
    eqExcPID_N s s1 ∧ B vl vl1"

definition Δ4 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ4 s vl s1 vl1 ≡
 ∃ cid uid.
    PID ∈∈ paperIDs s cid ∧ phase s cid ≥ revPH ∧ isREVNth s uid PID N ∧
    (reviewsPaper (paper s PID))!N ≠ [] ∧ (reviewsPaper (paper s1 PID))!N ≠ [] ∧
    eqExcPID_N2 s s1 ∧ vl = [] ∧ 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. isREVNth s uid PID N))
  ∨
  (∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid > disPH)
 )"

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 rsP: "reachNT s" and rs1: "reach s1" and "Δ1 s vl s1 vl1"
  hence rs: "reach s" and ss1: "s1 = s"
  and vl: "vl ≠ []" and vl1: "vl1 ≠ []" and vl_vl1: "last vl1 = last vl"
  and PID_ph: "⋀ cid. PID ∈∈ paperIDs s cid ⟹ phase s cid < revPH"
  using reachNT_reach unfolding Δ1_def B_def by auto
  note vlvl1 = vl vl1 vl_vl1
  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' and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and P: "¬ 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_ph by (fastforce simp: u_defs)+
        subgoal for x3 apply(cases x3) using step PID_ph by (fastforce simp: uu_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
            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 B_def vl' using PID_ph' vlvl1 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 B_def vl' using vlvl1 ph' PID' apply auto
              by (metis reach_PairI paperIDs_equals rs step)
              thus ?thesis by auto
            next
              case False note ph' = False
              have "¬ (∃ uid. isRevNth s CID uid PID N)" using rs ph isRevNth_geq_revPH by fastforce
              hence ph_isRev': "phase s' CID = revPH ∧ ¬ (∃ uid. isRevNth s' CID uid PID N)"
              using ph' ph 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 "¬ (∃ uid. isREVNth s' uid PID N)"
              by (metis PID' isREVNth_imp_isRevNth reach_PairI rs step)
              hence "Δ2 s' vl' s' vl1" unfolding Δ2_def B_def vl' using vlvl1 ph' PID' ph_isRev' by auto
              thus ?thesis by auto
            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 rsP: "reachNT s" and rs1: "reach s1" and "Δ2 s vl s1 vl1"
  then obtain CID where rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _") and ss1: "s1 = s"
  and uuid: "¬ (∃ uid. isREVNth s uid PID N)"
  and vl: "vl ≠ []" and vl1: "vl1 ≠ []" and vl_vl1: "last vl1 = last vl"
  and PID: "PID ∈∈ paperIDs s CID" using reachNT_reach unfolding Δ2_def B_def by auto
  hence uid: "¬ (∃ uid. isRevNth s CID uid PID N)" by (metis isREVNth_def)
  note vlvl1 = vl vl1 vl_vl1
  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'"
      let ?ph' = "phase s' CID"
      assume step: "step s a = (ou, s')" and P: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have φ: "¬ φ ?trn"
        apply(cases a)
        subgoal by simp
        subgoal for x2 apply(cases x2)
          using step ph apply (auto simp: u_defs)
          by (metis PID isRev_imp_isRevNth_getReviewIndex paperIDs_equals rs uid)
        subgoal for x3 apply(cases x3)
          using step ph apply (auto simp: uu_defs)
          using PID paperIDs_equals rs by force
        by simp_all
      hence vl': "vl' = vl" using c unfolding consume_def by auto
      have PID': "PID ∈∈ paperIDs s' CID" by (metis paperIDs_mono step PID)
      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 "?ph' = revPH")
            case False
            hence 1: "?ph' > revPH ∧ ¬ (∃ uid. isRevNth s' CID uid PID N)"
            using uid 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
            hence "¬ (∃ uid. isREVNth s' uid PID N)"
            by (metis PID' isREVNth_imp_isRevNth reach_PairI rs step)
            hence "Δe s' vl' s' vl1" unfolding Δe_def vl' using PID' vl 1 by auto
            thus ?thesis by simp
          next
            case True note ph' = True
            show ?thesis proof(cases "∃ uid. isREVNth s' uid PID N")
              case False
              hence "Δ2 s' vl' s' vl1" using PID' vlvl1 ph' unfolding Δ2_def B_def vl' by auto
              thus ?thesis by simp
            next
              case True
              hence "Δ3 s' vl' s' vl1" using PID' vlvl1 ph' unfolding Δ3_def B_def vl' by auto
              thus ?thesis by simp
            qed
          qed
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl by auto
  qed
qed

lemma unwind_cont_Δ3: "unwind_cont Δ3 {Δ3,Δ4,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ3 s vl s1 vl1 ∨ Δ4 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 uid where uuid: "isREVNth s uid PID N"
  and PID: "PID ∈∈ paperIDs s CID"
  and rs: "reach s" and ph: "phase s CID = revPH ∨ phase s CID = disPH" (is "?ph = _ ∨ _")
  and ss1: "eqExcPID_N s s1" and vl: "vl ≠ []" and vl1: "vl1 ≠ []" and vl_vl1: "last vl = last vl1"
  using reachNT_reach unfolding Δ3_def B_def by auto
  hence uid: "isRevNth s CID uid PID N" by (metis isREVNth_imp_isRevNth)
  note vlvl1 = vl vl1 vl_vl1
  from vl vl1 obtain v vl' v1 vl1' where vl: "vl = v # vl'" and vl1: "vl1 = v1 # vl1'" by (metis list.exhaust)
  have uid_notin: "uid ∉ UIDs" using uid by (metis reachNT_non_isRevNth_isPC_isChair rsT)
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases "vl1' = []")
    case False note vl1' = False
    hence vl_vl1': "last vl = last vl1'" using vl_vl1 unfolding vl1 by simp
    have uid1: "isRevNth s CID uid PID N" using ss1 uid unfolding eqExcPID_N_def by auto
    define a1 where "a1 ≡
     if ?ph = revPH
      then Uact (uReview CID uid (pass s uid) PID N v1)
      else UUact (uuReview CID uid (pass s uid) PID N v1)"
    (is "_ ≡ if ?ph = revPH then ?A else ?B")
    hence a1: "a1 ∈ {?A,?B}" by auto
    obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')" by (metis prod.exhaust)
    let ?trn1 = "Trans s1 a1 ou1 s1'"
    have s1s1': "eqExcPID_N s1 s1'" using step1 by (metis a1_def uReview_uuReview_step_eqExcPID_N)
    have ss1': "eqExcPID_N s s1'" using eqExcPID_N_trans[OF ss1 s1s1'] .
    hence many_s1': "PID ∈∈ paperIDs s1' CID" "isRevNth s1' CID uid PID N"
    "pass s1' uid = pass s uid" "phase s1' CID = phase s CID"
    using uid PID ph unfolding eqExcPID_N_def by simp_all
    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 apply (simp_all add: u_defs uu_defs many_s1' more_s1')
    by (metis isRevNth_getReviewIndex isRev_def3 many_s1' rs1')+
    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 "Δ3 s vl s1' vl1'" unfolding Δ3_def B_def using ph PID ss1' uuid vl_vl1' vl1' vl by auto
      thus "?Δ s vl s1' vl1'" by simp
    qed
    thus ?thesis by auto
  next
    case True hence vl1: "vl1 = [v1]" unfolding vl1 by simp
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vll'
      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 vll'"
      have PID': "PID ∈∈ paperIDs s' CID" using PID rs by (metis paperIDs_mono step)
      have uid': "isRevNth s' CID uid PID N" using uid step rs ph PID isRevNth_persistent by auto
      hence uuid': "isREVNth s' uid PID N" by (metis isREVNth_def)
      show "match ?Δ s s1 vl1 a ou s' vll' ∨ ignore ?Δ s s1 vl1 a ou s' vll'" (is "?match ∨ ?ignore")
      proof(cases "φ ?trn")
        case False note φ = False
        have vll': "vll' = 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_N s' s1'" using eqExcPID_N_step[OF ss1 step step1] .
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID_N_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_N_step_out[OF ss1 step step1 rsT rs1 PID ph] by simp
        next
          show "?Δ s' vll' s1' vl1"
          proof(cases "?ph' = revPH ∨ ?ph' = disPH")
            case True
            hence "Δ3 s' vll' s1' vl1" using PID' s's1' uuid' vlvl1 unfolding Δ3_def B_def vll' by auto
            thus ?thesis by auto
          next
            case False hence ph': "?ph' > disPH" using ph rs step
            by (metis le_less less_antisym not_less phase_increases2 prod.sel(2))
            hence "Δe s' vll' s1' vl1" unfolding Δe_def vll' using PID' vlvl1 by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by simp
      next
        case True note φ = True
        hence vll': "vll' = vl'" using c unfolding vl consume_def by simp
        obtain cid uid p rc where a:
        "a = Uact (uReview cid uid p PID N rc) ∨
         a = UUact (uuReview cid uid p PID N rc)" (is "a = ?A ∨ a = ?B")
        and ou: "ou = outOK" and v: "v = rc"
        using φ c unfolding vl consume_def φ_def2 vll' by fastforce
        hence cid: "cid = CID" using step apply(auto simp: u_defs uu_defs)
        (* crucial use of safety: *) by (metis PID paperIDs_equals rs)+
        have a: "(?ph = revPH ⟶ a = ?A) ∧ (?ph = disPH ⟶ a = ?B)"
        using step ou a by (cases "a = ?A", auto simp: u_defs uu_defs cid)
        have γ: "¬ γ ?trn" using step T rsT by (metis T_φ_γ True)
        hence f: "f ?trn = v" using c φ unfolding consume_def vl by auto
        have s's: "eqExcPID_N s' s" using eqExcPID_N_sym[OF φ_step_eqExcPID_N[OF φ step]] .
        have s's1: "eqExcPID_N s' s1" using eqExcPID_N_trans[OF s's ss1] .
        have ph': "phase s' CID = ?ph" using s's ph unfolding eqExcPID_N_def by auto
        show ?thesis
        proof(cases "vl' = []")
          case False note vl' = False
          hence vl'_vl1: "last vl' = last vl1" using vl_vl1 unfolding vl by auto
          have ?ignore proof
            show "¬ γ ?trn" by fact
          next
            show "?Δ s' vll' s1 vl1"
            proof(cases "?ph' = revPH ∨ ?ph' = disPH")
              case True
              hence "Δ3 s' vll' s1 vl1" using s's1 PID' uuid' vl' vl1 vl_vl1 unfolding Δ3_def B_def vl vll' by auto
              thus ?thesis by auto
            next
              case False hence "?ph' > disPH" using ph rs step by (simp add: ph')
              hence "Δe s' vll' s1 vl1" unfolding Δe_def vll' using PID' vlvl1 vl' by auto
              thus ?thesis by auto
            qed
          qed
          thus ?thesis by auto
        next
          case True note vl' = True hence vl: "vl = [v]" unfolding vl by simp
(* the transition to Δ4: φ holds and both vl and vl1 are singletons: *)
          hence v1v: "v1 = v" using vl_vl1 unfolding vl1 by simp
          obtain s1' ou1 where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
          let ?trn1 = "Trans s1 a ou1 s1'"
          have φ1: "φ ?trn1" using eqExcPID_N_step_φ_imp[OF ss1 step step1 φ] .
          hence ou1: "ou1 = outOK" unfolding φ_def2 by auto
          have uid'_uid1': "isRevNth s' CID uid PID N ∧ isRevNth s1' CID uid PID N"
          using step step1 ou ou1 ph a apply(auto simp: u_defs uu_defs)
          by (metis cid isRev_imp_isRevNth_getReviewIndex)+
          hence N: "N < length (reviewsPaper (paper s' PID)) ∧ N < length (reviewsPaper (paper s1' PID))"
          by (metis isRevNth_less_length reach_PairI rs rs1 step step1)
          hence l: "reviewsPaper (paper s' PID) ! N ≠ [] ∧ reviewsPaper (paper s1' PID) ! N ≠ []"
          using step step1 ph a ou ou1 by (auto simp add: u_defs uu_defs)
          have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 []" unfolding consume_def using φ1 a ph
          by (auto simp add: a v vl1 v1v)
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqExcPID_N_step_out[OF ss1 step step1 rsT rs1 PID ph] by simp
        next
          have "Δ4 s' vll' s1' []" unfolding vll' vl' Δ4_def
          using ph' ph uuid' l eqExcPID_N_step_φ_eqExcPID_N2[OF rs ss1 step step1 φ] PID' by auto
          thus "?Δ s' vll' s1' []" by simp
        qed
        thus ?thesis by simp
        qed
      qed
    qed
    thus ?thesis using vl by auto
  qed
qed

lemma unwind_cont_Δ4: "unwind_cont Δ4 {Δ4,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ4 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 "Δ4 s vl s1 vl1"
  then obtain CID uid where uuid: "isREVNth s uid PID N"
  and rs: "reach s" and ph: "phase s CID ≥ revPH" (is "?ph ≥ _")
  and PID: "PID ∈∈ paperIDs s CID"
  and decs: "(reviewsPaper (paper s PID))!N ≠ [] ∧ (reviewsPaper (paper s1 PID))!N ≠ []"
  and ss1: "eqExcPID_N2 s s1" and vl: "vl = []" and vl1: "vl1 = []"
  using reachNT_reach unfolding Δ4_def by auto
  hence uid: "isRevNth s CID uid PID N" by (metis isREVNth_imp_isRevNth)
  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': "phase s' CID ≥ revPH" using ph rs isRevNth_geq_revPH isRevNth_persistent local.step reach_PairI uid by blast
      have PID': "PID ∈∈ paperIDs s' CID" by (metis PID paperIDs_mono step)
      have uid': "isRevNth s' CID uid PID N" using isRevNth_persistent by (metis isRevNth_persistent rs step uid)
      hence uuid': "isREVNth s' uid PID N" by (metis isREVNth_def)
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have φ: "¬ φ ?trn" and vl': "vl' = []" using c unfolding consume_def vl by 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_N2 s' s1'" using eqExcPID_N2_step[OF ss1 step step1 rs uid] .
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID_N2_step_φ[OF rs rs1 ss1 step step1] .
        have uid1: "isRevNth s1 CID uid PID N" using uid eqExcPID_N2_imp[OF ss1] by auto
        have decs': "(reviewsPaper (paper s' PID))!N ≠ []" "(reviewsPaper (paper s1' PID))!N ≠ []"
        using nonempty_reviews_persist rs rs1 step step1 uid uid1 decs by blast+
        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_N2_step_out[OF ss1 step step1 rsT rs1 uid ph _ decs] by simp
        next
          have "Δ4 s' vl' s1' vl1" using ph' uuid' s's1' PID' unfolding Δ4_def vl1 vl' by (auto simp: decs')
          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 > revPH ∧ ¬ (∃ uid. isRevNth s cid uid PID N)"

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)+ .
    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)
    subgoal by (fastforce simp add: c_defs K1exit_def)
    subgoal for x2 apply(cases x2) apply (auto simp add: u_defs K1exit_def)
     apply (metis less_not_refl paperIDs_equals reachNT_reach) .
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K1exit_def)
      apply (metis isRev_def3 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)
    subgoal by (fastforce simp add: c_defs K2exit_def)
    subgoal for x2 apply(cases x2) apply (auto simp add: u_defs K2exit_def)
      using paperIDs_equals reachNT_reach apply fastforce .
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K2exit_def)
      using paperIDs_equals reachNT_reach apply 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" using Δe
  unfolding K1exit_def K2exit_def Δe_def isREVNth_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_decomp4_secure[of Δ1 Δ2 Δe Δ3 Δ4])
using
istate_Δ1
unwind_cont_Δ1 unwind_cont_Δ2 unwind_cont_Δ2 unwind_cont_Δ3 unwind_cont_Δ4
unwind_exit_Δe
by auto


end