Theory Review_RAut_NCPC_PAut

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

subsection ‹Confidentiality from users who are not the review's author, a PC member, or an author of the paper›

text ‹We verify the following property:

\ \\
A group of users UIDs learn nothing
about the various updates to the N'th review of a paper PID
(save for the inexistence of any updates) unless/until
\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, or
\item a user in UIDs become a PC member in the paper's conference
or an author of the paper and the conference moves to the notification 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)
    
    ( cid. PID ∈∈ paperIDs s' cid  isPC s' cid uid  phase s' cid  notifPH)
    
    isAUT s' uid PID  ( cid. PID ∈∈ paperIDs s' cid  phase s' cid  notifPH)
 )"

declare T.simps [simp del]

definition B :: "value list  value list  bool" where
"B vl vl1  vl  []"

interpretation BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done

lemma reachNT_non_isPC_isChair:
assumes "reachNT s" and "uid  UIDs"
shows
"¬ isRevNth s cid uid PID N 
 (PID ∈∈ paperIDs s cid  isPC s cid uid 
    (pref s uid PID = Conflict  phase s cid < disPH)  phase s cid < notifPH) 
 (PID ∈∈ paperIDs s cid  isChair s cid uid 
    (pref s uid PID = Conflict  phase s cid < disPH)  phase s cid < notifPH) 
 (isAut s cid uid PID  phase s cid < notifPH)"
using assms apply induct
apply (auto simp: istate_def)[]
apply(intro conjI)
  subgoal for trn apply(cases trn, simp add: T.simps reachNT_reach isAUT_def isREVNth_def)[] .
  subgoal for trn apply(cases trn, simp add: T.simps reachNT_reach isAUT_def isREVNth_def)[]
    apply (metis not_less) .
  subgoal for trn apply(cases trn, simp add: T.simps reachNT_reach isAUT_def isREVNth_def)[]
    apply (metis isChair_isPC not_less reachNT_reach reach_PairI) .
  subgoal for trn apply(cases trn, simp add: T.simps reachNT_reach isAUT_def isREVNth_def)[]
    apply (metis isAut_paperIDs not_less reachNT_reach reach_PairI) .
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
apply (auto simp: u_defs uu_defs isRev_imp_isRevNth_getReviewIndex)
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 UIDs: "userOfA a  UIDs"
shows "ou = ou1"
proof-
  note s = reachNT_reach[OF sT]
  note Inv = reachNT_non_isPC_isChair[OF sT 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'] eqExcPID_N_imp3'[OF s s's1']

  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' eqss s s1 UIDs PID 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 getRevRole_Some_Rev_isRevNth)
    next
      case (rReviews x91 x92 x93 x94)
      with Ract * show ?thesis
        by clarsimp (metis not_less)
    next
      case (rFinalReviews x121 x122 x123 x124)
      with Ract * show ?thesis
        by clarsimp (metis not_less)
    qed auto
  next
    case (Lact x5)
    with * show ?thesis by (cases x5; auto; presburger)
  qed
qed

definition Δ1 :: "state  value list  state  value list  bool" where
"Δ1 s vl s1 vl1 
 ( cid. PID ∈∈ paperIDs s cid  phase s cid < 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"

(* Note: In the similar property from discussion confidentiality we have only 3 non-exit phases
instead of 4, not having a phase like Δ2: this is because there the agent affecting the documents (chairs),
must have been assigned in a previous phase; here reviewers are assigned in the same phase
in which they can edit.   *)

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"

definition Δ4 :: "state  value list  state  value list  bool" where
"Δ4 s vl s1 vl1 
  cid. PID ∈∈ paperIDs s cid  phase s cid > revPH  eqExcPID_N 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. isREVNth s uid PID N))"

lemma istate_Δ1:
assumes B: "B vl vl1"
shows "Δ1 istate vl istate vl1"
using B unfolding Δ1_def B_def istate_def by auto

lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1,Δ2,Δe}"
proof(rule, simp)
  let  = "λs vl s1 vl1. Δ1 s vl s1 vl1  Δ2 s vl s1 vl1  Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ1 s vl s1 vl1"
  hence rs: "reach s" and ss1: "s1 = s" and vl: "vl  []"
  and PID_ph: " cid. PID ∈∈ paperIDs s cid  phase s cid < 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 B_def vl' using PID_ph' vl by auto
            thus ?thesis by auto
          next
            case True
            then obtain CID where PID: "PID ∈∈ paperIDs s CID" by auto
            hence ph: "phase s CID < 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 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 rs1 ss1 step)
              hence "Δ2 s' vl' s' vl1"
              unfolding Δ2_def B_def isREVNth_def vl' using 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 rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _")
  and PID: "PID ∈∈ paperIDs s CID" and ss1: "s1 = s"
  and vl: "vl  []" and uid: "¬ ( uid. isREVNth s uid PID N)"
  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 uid apply (auto simp: u_defs isRev_def3)
          by (metis PID paperIDs_equals rs)
        subgoal for x3 apply(cases x3)
          using step ph apply (auto simp: uu_defs)
          by (metis PID n_not_Suc_n paperIDs_equals rs)
        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 reach_PairI PID' isREVNth_imp_isRevNth rs1 ss1 step)
              hence "Δ2 s' vl' s' vl1" unfolding Δ2_def B_def vl' using vl ph' PID' 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 vl ph' PID' by auto
              thus ?thesis by auto
            qed
          next
            case False hence 1: "?ph' > revPH  ¬ ( uid. isRevNth s' CID uid PID N)"
              using PID ph uid 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 reach_PairI PID' isREVNth_imp_isRevNth rs1 ss1 step)
            hence "Δe s' vl' s' vl1" unfolding Δe_def vl' using vl PID' 1 by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl by simp
  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 rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _") and ss1: "eqExcPID_N s s1"
  and PID: "PID ∈∈ paperIDs s CID" using reachNT_reach unfolding Δ3_def by blast
  hence uid: "isRevNth s CID uid PID N" by (metis isREVNth_imp_isRevNth)
  hence uid_notin: "uid  UIDs" using reachNT_non_isPC_isChair[OF rsT] by auto
  show "iaction  s vl s1 vl1 
        ((vl = []  vl1 = [])  reaction  s vl s1 vl1)" (is "?iact  (_  ?react)")
  proof(cases vl1)
    case (Cons v1 vl1') note vl1 = Cons
    have uid1: "isRevNth s 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 v1)"
    obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')" by (metis prod.exhaust)
    let ?trn1 = "Trans s1 a1 ou1 s1'"
    have s1s1': "eqExcPID_N s1 s1'" using a1_def step1 uReview_uuReview_step_eqExcPID_N by blast
    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 = 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 add: u_defs uu_defs many_s1' more_s1' isRev_def2)
    by (metis isRevNth_getReviewIndex 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 using ph PID ss1' uuid 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': "isRevNth s' CID uid PID N"
      using uid step rs ph PID isRevNth_persistent by auto
      have uuid': "isREVNth s' uid PID N" by (metis isREVNth_def uid')
      show "match  s s1 vl1 a ou s' vl'  ignore  s s1 vl1 a ou s' vl'" (is "?match  ?ignore")
      proof(cases "φ ?trn")
        case False note φ = False
        have vl: "vl' = vl" using c φ unfolding consume_def by (cases vl) auto
        obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
        let ?trn1 = "Trans s1 a ou1 s1'"
        have s's1': "eqExcPID_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] by simp
        next
          show " s' vl' s1' vl1"
          proof(cases "?ph' = revPH")
            case True
            hence "Δ3 s' vl' s1' vl1" using PID' s's1' uuid' unfolding Δ3_def by auto
            thus ?thesis by auto
          next
            case False hence "?ph' > revPH"
            using ph rs step by (metis le_less phase_increases2 prod.sel(2))
            hence "Δ4 s' vl' s1' vl1" using s's1' PID' unfolding Δ4_def vl1 by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by simp
      next
        case True note φ = True
        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 ?ignore proof
          show "¬ γ ?trn" using T_φ_γ φ rsT step by auto
        next
          show " s' vl' s1 vl1"
          proof(cases "?ph' = revPH")
            case True
            hence "Δ3 s' vl' s1 vl1" using s's1 PID' uuid' unfolding Δ3_def by auto
            thus ?thesis by auto
          next
            case False hence "?ph' > revPH"
            using ph rs step using eqExcPID_N_def s's by auto
            hence "Δ4 s' vl' s1 vl1" using s's1 PID' unfolding Δ4_def vl1 by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by auto
      qed
    qed
    thus ?thesis using vl1 by auto
  qed
qed

lemma unwind_cont_Δ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 where rs: "reach s" and ph: "phase s CID > revPH" (is "?ph > _")
  and PID: "PID ∈∈ paperIDs s CID" and ss1: "eqExcPID_N s s1" and vl1: "vl1 = []"
  using reachNT_reach unfolding Δ4_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': "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] by simp
        next
          have "Δ4 s' vl' s1' vl1" using ph' PID' s's1' unfolding Δ4_def vl1 by auto
          thus " s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      next
        case True note φ = True
        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 ?ignore proof
          show "¬ γ ?trn" using T_φ_γ φ rsT step by auto
        next
          have "Δ4 s' vl' s1 vl1" using s's1 PID' ph' vl1 unfolding Δ4_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. 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

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" using Δe unfolding K1exit_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)
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_Δ3 unwind_cont_Δ4
unwind_exit_Δe
by auto

end