Theory Review_RAut

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

subsection ‹Confidentiality protection from users who are not the review's author›


text ‹We verify the following property:

\ \\
A group UIDs of users learn nothing
about the various updates of the N'th review of a paper PID
except for the last edited version before discussion and all the later versions
unless a user in UIDs is that review's author.

\ \\
›

type_synonym "value" = "phase * rcontent"

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

fun T :: "(state,act,out) trans ⇒ bool" where
"T (Trans _ _ ou s') =
 (∃ uid ∈ UIDs. isREVNth s' uid PID N)"

declare T.simps [simp del]

definition B :: "value list ⇒ value list ⇒ bool" where
"B vl vl1 ≡
 ∃ ul ul1 wl.
   vl = (map (Pair revPH) ul) @ (map (Pair disPH) wl) ∧
   vl1 = (map (Pair revPH) ul1) @ (map (Pair disPH) wl) ∧
   ul ≠ [] ∧ ul1 ≠ [] ∧ last ul = last ul1"

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:
assumes "reachNT s" and "uid ∈ UIDs"
shows "¬ isRevNth s cid uid PID N"
  using assms
  apply induct
   apply (auto simp: istate_def)[]
  subgoal for trn apply(cases trn, auto simp: T.simps reachNT_reach isREVNth_def) .
  done


(* important: *) 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_isRevNth[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 sT: "reachNT s" and s1: "reach s1"
and PID: "PID ∈∈ paperIDs s cid"
and ph: "phase s cid = revPH"
and UIDs: "userOfA a ∈ UIDs"
shows "ou = ou1"
proof-
  note Inv = reachNT_non_isRevNth[OF sT UIDs]
  note eqs = eqExcPID_N_imp[OF s's1']
  note eqs' = eqExcPID_N_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_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 Suc_n_not_le_n eqExcPID_N_imp2 s's1')
    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

lemma eeqExcPID_N_imp_eq:
assumes "eeqExcPID_N paps paps1"
and "reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N"
shows "paps = paps1"
proof(rule ext)
  fix pid
  show "paps pid = paps1 pid"
  using assms unfolding eeqExcPID_N_def eqExcD eqExcNth_def
  apply(cases "paps PID", cases "paps1 PID", cases "pid = PID")
  by simp_all (metis nth_equalityI)
qed

lemma eqExcPID_N_imp_eq:
assumes e: "eqExcPID_N s s1"
and "reviewsPaper (paper s PID) ! N = reviewsPaper (paper s1 PID) ! N"
shows "s = s1"
proof-
  have "paper s = paper s1" using assms eeqExcPID_N_imp_eq
  unfolding eqExcPID_N_def by metis
  thus ?thesis
  using e unfolding eqExcPID_N_def by (intro state.equality) auto
qed


(* major *) lemma eqExcPID_N_step_eq:
assumes s: "reach s" and ss1: "eqExcPID_N s s1"
and a: "a = Uact (uReview cid uid p PID N rc)"
and step: "step s a = (outOK, s')" and step1: "step s1 a = (ou', s1')"
shows "s' = s1'"
proof(cases "∃ cid uid. isRevNth s cid uid PID N")
  case False
  hence False
  using step unfolding a
  by (auto simp add: u_defs uu_defs) (metis isRev_imp_isRevNth_getReviewIndex)+
  thus ?thesis by auto
next
  case True note r = True
  note eqs = eqExcPID_N_imp[OF ss1]
  note eqsT = eqExcPID_N_Paper[OF ss1]
  have r: "N < length (reviewsPaper (paper s PID))"
  using isRevNth_less_length[OF s] r by auto
  have r1: "N < length (reviewsPaper (paper s1 PID))"
  using eqs r unfolding eeqExcPID_N_def eqExcD eqExcNth_def by simp
  have s's1': "eqExcPID_N s' s1'" using assms by (metis eqExcPID_N_step)

  have "e_updateReview s cid uid p PID N rc"
  using step a by auto
  hence "e_updateReview s1 cid uid p PID N rc"
  using eqExcPID_N_imp[OF ss1] u_defs by auto
  hence ou': "ou' = outOK" using step1 a by auto

  let ?p = "paper s PID" let ?p1 = "paper s1 PID"

  have 1: "eqExcD ?p ?p1"
  using ss1 eqExcPID_N_imp unfolding eeqExcPID_N_def by auto

  have 2: "reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N"
  using step step1[unfolded ou'] r r1 unfolding a
  by (cases ?p, cases ?p1) (auto simp : u_defs)

  from 1 2 show ?thesis using eqExcPID_N_imp_eq s's1' by blast
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 ∧ 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 ∧
    s = s1 ∧ (∃ wl. vl = map (Pair disPH) wl ∧ vl1 = map (Pair disPH) wl)"

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 > revPH ∧ fst (hd vl) = 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 vl: "vl ≠ []" and vl1: "vl1 ≠ []" and PID_ph: "⋀ cid. PID ∈∈ paperIDs s cid ⟶ phase s cid < revPH"
  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"
        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
            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 vl' using B 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 < 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 vl' using B vl 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
              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 "¬ (∃ 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 vl' using B vl 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 rsT: "reachNT s" and rs1: "reach s1" and "Δ2 s vl s1 vl1"
  then obtain CID where uuid: "¬ (∃ uid. isREVNth s uid PID N)" and PID: "PID ∈∈ paperIDs s CID"
  and rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _") and ss1: "s1 = s"
  and B: "B vl vl1"
  and vl: "vl ≠ []" and vl1: "vl1 ≠ []"
  using reachNT_reach unfolding Δ2_def B_def by auto
  hence uid: "¬ (∃ uid. isRevNth s CID uid PID N)" by (metis isREVNth_def)
  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 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 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 True note ph' = True
            show ?thesis proof(cases "∃ uid. isRevNth s' CID uid PID N")
              case False
              hence "¬ (∃ uid. isREVNth s' uid PID N)"
              by (metis PID' isREVNth_def isRevNth_paperIDs paperIDs_equals reach_PairI rs1 ss1 step)
              hence "Δ2 s' vl' s' vl1" unfolding Δ2_def vl' using B ph' PID' unfolding B_def by auto
              thus ?thesis by auto
            next
              case True hence "∃ uid. isREVNth s' uid PID N" by (metis isREVNth_def)
              hence "Δ3 s' vl' s' vl1" unfolding Δ3_def vl' using B ph' PID' unfolding B_def by auto
              thus ?thesis by auto
            qed
          next
            case False
            hence ph': "?ph' > revPH" by (metis le_less step ph phase_increases)
            hence "¬ (∃ uid. isRevNth s' CID uid PID N)" using PID uid ph 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 "¬ (∃ uid. isREVNth s' uid PID N)"
            by (metis IO_Automaton.reach_PairI PID' isREVNth_imp_isRevNth rs1 ss1 step)
            hence "Δe s' vl' s' vl1" using ph' vl PID' unfolding Δe_def vl' by auto
            thus ?thesis by auto
          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 ul ul1 wl where uuid: "isREVNth s uid PID N"
  and rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _")  and ss1: "eqExcPID_N s s1"
  and PID: "PID ∈∈ paperIDs s CID" and B: "B vl vl1"
  and vlvl1: "vl ≠ []" "vl1 ≠ []"
  and vl_wl: "vl = (map (Pair revPH) ul) @ (map (Pair disPH) wl)"
  and vl1_wl: "vl1 = (map (Pair revPH) ul1) @ (map (Pair disPH) wl)"
  and ulul1: "ul ≠ [] ∧ ul1 ≠ [] ∧ last ul = last ul1"
  using reachNT_reach unfolding Δ3_def B_def by blast
  hence uid: "isRevNth s CID uid PID N" by (metis isREVNth_imp_isRevNth)
  have ph1: "phase s1 CID = revPH" using ss1 ph eqExcPID_N_imp by auto
  from ulul1 obtain u ul' u1 ul1' where ul: "ul = u # ul'" and ul1: "ul1 = u1 # ul1'" by (metis list.exhaust)
  obtain vl' vl1' where
  vl:  "vl = (revPH, u) # vl'"    and vl'_wl: "vl' = (map (Pair revPH) ul') @ (map (Pair disPH) wl)" and
  vl1: "vl1 = (revPH, u1) # vl1'" and vl1'_wl: "vl1' = (map (Pair revPH) ul1') @ (map (Pair disPH) wl)"
  unfolding vl_wl ul vl1_wl ul1 by auto
  have uid_notin: "uid ∉ UIDs" using uid by (metis reachNT_non_isRevNth rsT)
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases "ul1' = []")
    case False note ul1' = False
    hence ul_ul1': "last ul = last ul1'" using ulul1 unfolding ul1 by simp
    have uid1: "isRevNth s1 CID uid PID N" using ss1 uid unfolding eqExcPID_N_def by auto
    define a1 where "a1 ≡ Uact (uReview CID uid (pass s uid) PID N u1)"
    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 a1_def step1 by (metis 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"
    "phase s1' CID = revPH" "pass s1' uid = pass s uid"
    using uid PID ph unfolding eqExcPID_N_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 = (revPH,u1)" unfolding a1_def using ph1 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 (auto simp add: u_defs many_s1' more_s1')
    by (metis isRevNth_getReviewIndex isRev_def3 many_s1'(2) 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 ul1 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 ul1' vl_wl vl1'_wl ulul1 ul_ul1' by fastforce
      thus "?Δ s vl s1' vl1'" by simp
    qed
    thus ?thesis by auto
  next
    case True hence ul1: "ul1 = [u1]" unfolding ul1 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" 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' 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 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")
            case True
            hence "Δ3 s' vll' s1' vl1"
            unfolding Δ3_def B_def vll' using ph PID s's1' PID' uuid' vl_wl vl1_wl ulul1 by fastforce
            thus ?thesis by auto
          next
            case False hence "?ph' > revPH" using ph rs step by (metis le_less phase_increases2 snd_conv)
            hence "Δe s' vll' s1' vl1" using vlvl1 PID' unfolding Δe_def vll' vl_wl ul 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 = Uact (uReview cid uid' p PID N rc) ∨
               a = UUact (uuReview cid uid' p PID N rc)" and ou: "ou = outOK"
        using φ c ph step ph unfolding vl consume_def φ_def2 vll' by force
        hence a: "a = Uact (uReview cid uid' p PID N rc)"
        using step ph unfolding ou apply (auto simp: uu_defs) using PID paperIDs_equals rs by force
        have cid: "cid = CID"
          using step unfolding a
          apply(simp add: u_defs uu_defs)
           apply (metis PID e_updateReview_def isRev_paperIDs paperIDs_equals rs)
          by (metis ou out.distinct(1))
        hence γ: "¬ γ ?trn" using step T rsT by (metis P_φ_γ True)
        hence f: "f ?trn = (revPH,u)" using c φ ph unfolding consume_def vl by simp
        have u: "u = rc" using f unfolding a by (auto simp: u_defs)
        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 = revPH" using s's ph unfolding eqExcPID_N_def by auto
        show ?thesis
        proof(cases "ul' = []")
          case False note ul' = False
          hence ul'ul1: "last ul' = last ul1" using ulul1 unfolding ul by auto
          have ?ignore proof
            show "¬ γ ?trn" by fact
          next
            show "?Δ s' vll' s1 vl1"
            proof(cases "?ph' = revPH")
              case True
              hence "Δ3 s' vll' s1 vl1"
                unfolding Δ3_def B_def using ph PID s's1 PID'
                apply - apply(rule exI[of _ CID]) apply(rule exI[of _ uid])
                apply safe
                subgoal using uuid' by simp
                subgoal
                  apply(rule exI[of _ ul']) apply(rule exI[of _ ul1]) apply(rule exI[of _ wl])
                  unfolding vll' using vl'_wl vl1_wl ul'ul1 ul' ulul1 by auto
                done
              thus ?thesis by auto
            next
              case False hence "?ph' > revPH" using rs step ph' by blast
              hence "Δe s' vll' s1 vl1" unfolding Δe_def vll' vl'_wl using ul' PID' by (cases ul') auto
              thus ?thesis by auto
            qed
          qed
          thus ?thesis by auto
        next
          case True note ul' = True hence ul: "ul = [u]" unfolding ul by simp
(* the transition to Δ4: φ holds and both ul and ul1 (the parts of vl and vl1 that
cover the reviewing phase) are singletons: *)
          hence u1u: "u1 = u" using ulul1 unfolding ul1 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 "PID ∈∈ paperIDs s1 CID" "∃ uid. isRevNth s1 CID uid PID N"
          using eqExcPID_N_imp[OF ss1] PID uid by auto
          hence many_s1': "revPH ≤ phase s1' CID" "PID ∈∈ paperIDs s1' CID"
          "∃uid. isRevNth s1' CID uid PID N"
          by (metis ph1 phase_increases step1 paperIDs_mono a
                    eqExcPID_N_step_eq ou rs ss1 step step1 uid')+
          hence uuid1': "∃uid. isREVNth s1' uid PID N" by (metis isREVNth_def)
          have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 (map (Pair disPH) wl)"
          using φ1 ph1 unfolding consume_def by (simp add: a ul1 vl1_wl ul1 u1u u ph1 cid)
        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
          note s's1' = eqExcPID_N_step_eq[OF rs ss1 a step[unfolded ou] step1]
          have "Δ4 s' vll' s1' (map (Pair disPH) wl)"
          unfolding Δ4_def B_def using ph PID s's1' many_s1' uuid1'
          unfolding vll' vl'_wl ul' by auto
          thus "?Δ s' vll' s1' (map (Pair disPH) wl)" 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 uid CID  wl where uuid: "isREVNth s uid PID N"
  and rs: "reach s" and ph: "phase s CID ≥ revPH" (is "?ph ≥ revPH") and ss1: "s1 = s"
  and PID: "PID ∈∈ paperIDs s CID" and vl: "vl = map (Pair disPH) wl"
  and vl1: "vl1 = map (Pair disPH) wl"
  using reachNT_reach unfolding Δ4_def by blast
  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 uid': "isRevNth s' CID uid PID N" by (metis isRevNth_persistent rs step uid)
      hence uuid': "isREVNth s' uid PID N" by (metis isREVNth_def)
      have PID': "PID ∈∈ paperIDs s' CID" using PID rs by (metis paperIDs_mono step)
      have ph': "phase s' CID ≥ revPH" using rs isRevNth_geq_revPH local.step reach_PairI uid' by blast
      let ?trn1 = "Trans s1 a ou s'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof(cases "φ ?trn")
        case True note φ = True
        hence φ1: "φ ?trn1" unfolding ss1 by simp
        obtain w wl' where wl: "wl = w # wl'" and vl: "vl = (disPH,w) # map (Pair disPH) wl'"
        and vl1: "vl1 = (disPH,w) # map (Pair disPH) wl'" and vl': "vl' = map (Pair disPH) wl'"
        using φ φ1 c unfolding vl vl1 consume_def by (cases wl) auto
        have f: "f ?trn = (disPH, w)" "f ?trn1 = (disPH, w)"
        using φ φ1 c unfolding consume_def vl vl1 ss1 by auto
        have ?match proof
          show "validTrans ?trn1" using step unfolding ss1 by simp
        next
          show "consume ?trn1 vl1 vl'" unfolding consume_def vl1 vl' using φ1 f by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1" by simp
        next
          have "Δ4 s' vl' s' vl'"
          using ph' PID' uuid' unfolding Δ4_def vl' by auto
          thus "?Δ s' vl' s' vl'" by simp
        qed
        thus ?thesis by simp
      next
        case False note φ = False
        hence φ1: "¬ φ ?trn1" unfolding ss1 by simp
        hence vl': "vl' = vl" using φ c unfolding vl consume_def by auto
        have ?match proof
          show "validTrans ?trn1" using step unfolding ss1 by simp
        next
          show "consume ?trn1 vl1 vl" unfolding consume_def vl1 vl using φ1 by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1" by simp
        next
          have "Δ4 s' vl' s' vl"
          using ph' PID' uuid' unfolding Δ4_def vl' vl by auto
          thus "?Δ s' vl' s' vl" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl vl1 by simp
  qed
qed

(* Exit arguments: *)
definition K2exit where
"K2exit cid s ≡
 PID ∈∈ paperIDs s cid ∧ phase s cid > revPH ∧ ¬ (∃ uid. isRevNth s cid uid PID N)"

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)
     apply (metis less_not_refl paperIDs_equals reachNT_reach) .
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K2exit_def)
      apply (metis isRev_def3 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 (fastforce simp add: c_defs K3exit_def geq_noPH_confIDs)+ .
    subgoal for x2 apply(cases x2) apply (fastforce simp add: u_defs K3exit_def paperIDs_equals)+ .
    subgoal for x3 apply(cases x3) apply (fastforce simp add: uu_defs K3exit_def)+ .
    by auto
  done

(* The most interesting exit condition so far, not reducible to the "noφ" condition *)
lemma noVal_K3exit: "noVal (K3exit cid) (revPH,u)"
unfolding noVal_def apply safe
  subgoal for _ a apply(cases a)
    subgoal by (fastforce simp add: c_defs K3exit_def)
    subgoal for x2 apply(cases x2) apply (auto simp add: u_defs K3exit_def)
     apply (metis less_not_refl paperIDs_equals reachNT_reach) .
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K3exit_def) .
    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 rs:  "reach s" and vl: "vl ≠ []" using reachNT_reach unfolding Δe_def by auto
  then obtain CID where K: "K2exit CID s ∨ K3exit CID s" and PID: "PID ∈∈ paperIDs s CID"
  using Δe unfolding K2exit_def K3exit_def Δe_def by auto
  show "vl ≠ [] ∧ exit s (hd vl)" proof(simp add: vl, cases "K2exit CID s")
    case True
    thus "exit s (hd vl)"
    by (metis rsT exitI2 invarNT_K2exit noVal_K2exit)
  next
    case False
    then obtain u where h: "hd vl = (revPH,u)" and K3: "K3exit CID s"
    using Δe K PID rs unfolding Δe_def K2exit_def K3exit_def
    by (cases vl) (auto simp: isREVNth_def)
    show "exit s (hd vl)" unfolding h using K3
    by (metis rsT exitI2 invarNT_K3exit noVal_K3exit)
  qed
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