diff --git a/thys/CoCon/Paper_Confidentiality/Paper_Aut.thy b/thys/CoCon/Paper_Confidentiality/Paper_Aut.thy --- a/thys/CoCon/Paper_Confidentiality/Paper_Aut.thy +++ b/thys/CoCon/Paper_Confidentiality/Paper_Aut.thy @@ -1,440 +1,440 @@ theory Paper_Aut imports "../Observation_Setup" Paper_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning" begin subsection \Confidentiality protection from non-authors\ text \We verify the following property: \ \\ A group of users UIDs learns nothing about the various uploads of a paper PID except for the last (most recent) upload unless/until a user in UIDs becomes an author of the paper. \ \\ \ fun T :: "(state,act,out) trans \ bool" where "T (Trans _ _ ou s') = (\ uid \ UIDs. isAUT s' uid PID)" 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_isAut: assumes "reachNT s" and "uid \ UIDs" shows "\ isAut s cid uid PID" using assms apply induct apply (auto simp: istate_def)[] subgoal for trn apply(cases trn, auto simp: T.simps reachNT_reach isChair_isPC isAUT_def) . 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_isAut[OF 1] 2 unfolding T.simps \_def2 by (auto simp add: u_defs) (* major *) lemma eqButPID_step_out: assumes ss1: "eqButPID 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 = subPH" and UIDs: "userOfA a \ UIDs" shows "ou = ou1" proof- note Inv = reachNT_non_isAut[OF sT UIDs] note eqs = eqButPID_imp[OF ss1] note eqs' = eqButPID_imp1[OF ss1] note s = reachNT_reach[OF sT] have PID': "PID \\ paperIDs s1 cid" and ph': "phase s cid = subPH" using PID ph ss1 unfolding eqButPID_def by auto note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqButPID_def eeqButPID_def eqButC note * = step step1 eqs eqs' s s1 PID ph PID' ph' UIDs paperIDs_equals[OF s] Inv show ?thesis proof (cases a) case (Cact x1) then show ?thesis using * by (cases x1; auto) next case (Uact x2) then show ?thesis using * by (cases x2; auto) next case (UUact x3) then show ?thesis using * by (cases x3; auto) next case (Ract x4) with * show ?thesis proof (cases x4) case (rPaperC x61 x62 x63 x64) then show ?thesis using * Ract by (clarsimp; metis Suc_n_not_le_n) next case (rMyReview x81 x82 x83 x84) then show ?thesis using * Ract by (auto simp: getNthReview_def) next case (rReviews x91 x92 x93 x94) then show ?thesis using * Ract by (clarsimp; metis Suc_leD eqButPID_imp2 not_less_eq_eq ss1) qed auto next case (Lact x5) then show ?thesis using * by (cases x5; auto) qed qed text \major\ lemma eqButPID_step_eq: assumes ss1: "eqButPID s s1" and [simp]: "a=Uact (uPaperC cid uid p PID ct)" "ou=outOK" and step: "step s a = (ou, s')" and step1: "step s1 a = (ou', s1')" shows "s' = s1'" using ss1 step step1 apply (simp add: u_defs eqButPID_paper ) subgoal by (cases s; cases s1; auto simp add: eqButPID_def eeqButPID_def) subgoal by (use ss1 step step1 in \auto simp add: eqButPID_def eeqButPID_def\) done definition \1 :: "state \ value list \ state \ value list \ bool" where "\1 s vl s1 vl1 \ \ (\ cid. PID \\ paperIDs s cid) \ 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 = subPH) \ eqButPID s s1 \ B vl vl1" definition \3 :: "state \ value list \ state \ value list \ bool" where "\3 s vl s1 vl1 \ (\ cid. PID \\ paperIDs s cid) \ s = s1 \ vl = [] \ vl1 = []" definition \e :: "state \ value list \ state \ value list \ bool" where "\e s vl s1 vl1 \ (\ cid. PID \\ paperIDs s cid \ phase s cid > subPH) \ vl \ []" lemma istate_\1: assumes B: "B vl vl1" shows "\1 istate vl istate vl1" using assms unfolding \1_def B_def istate_def by auto lemma unwind_cont_\1: "unwind_cont \1 {\1,\2,\e}" proof(rule) let ?\ = "disjAll {\1, \2, \e}" 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 cid: "\cid. \ PID \\ paperIDs s cid" and ss1: "s1 = s" and vl: "vl \ []" and vl1: "vl1 \ []" and vlvl1: "last vl = last vl1" 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 (rule, goal_cases) case (1 a ou s' vl') assume STET: "step s a = (ou, s')" and "\ T (Trans s a ou s')" and CONSUME: "consume (Trans s a ou s') vl vl'" have not_phi: "\\ (Trans s a ou s')" using STET cid by (auto simp: \_def2 u_defs) with CONSUME have vlvl': "vl'=vl" by (simp add: consume_def) have "match (disjAll {\1, \2, \e}) s s1 vl1 a ou s' vl'" proof show "validTrans (Trans s1 a ou s')" using STET by (simp add: ss1) show "consume (Trans s1 a ou s') vl1 vl1" by (simp add: consume_def ss1 not_phi) show "\ (Trans s a ou s') = \ (Trans s1 a ou s')" by simp show "g (Trans s a ou s') = g (Trans s1 a ou s')" by simp show "disjAll {\1, \2, \e} s' vl' s' vl1" proof (cases "\cid. PID \\ paperIDs s' cid") case False hence "\1 s' vl' s' vl1" by (simp add: \1_def B_def vlvl' vl vl1 vlvl1) thus ?thesis by simp next case True hence "\2 s' vl' s' vl1" apply (simp add: \2_def B_def vlvl' vl vl1 vlvl1) apply (erule exE) subgoal for cid apply(rule exI[of _ cid]) apply simp apply (use STET cid in \cases a\) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . subgoal by simp subgoal by simp done done thus ?thesis by simp qed qed thus ?case by simp qed thus ?thesis using vl vl1 by auto qed qed lemma unwind_cont_\2: "unwind_cont \2 {\2,\3,\e}" proof (rule, goal_cases) case (1 s vl s1 vl1) assume rsT: "reachNT s" and rs1: "reach s1" and "\2 s vl s1 vl1" then obtain cid where rs: "reach s" and pid: "PID \\ paperIDs s cid" and ph: "phase s cid = subPH" and ss1: "eqButPID s s1" and vl: "vl \ []" and vl1: "vl1 \ []" and vlvl1: "last vl = last vl1" using reachNT_reach unfolding \2_def B_def by auto have cid: "cid \\ confIDs s" by (metis paperIDs_confIDs pid rs) from pid ph cid have pid1: "PID \\ paperIDs s1 cid" and ph1: "phase s1 cid = subPH" and cid1: "cid \\ confIDs s1" by (auto simp add: eqButPID_imp[OF ss1]) show ?case (is "?iact \ (_ \ ?react)") proof (cases "length vl1>1") case True then obtain v vl1' where [simp]: "vl1 = v#vl1'" "vl1'\[]" by (cases vl1) auto obtain uid1 where aut1: "isAut s1 cid uid1 PID" thm paperID_ex_userID using paperID_ex_userID[OF rs1 pid1] by auto have uid1: "uid1 \\ userIDs s1" by (metis roles_userIDs rs1 aut1) from aut1 have "isAut s cid uid1 PID" using ss1 aut1 by (simp add: eqButPID_imp[OF ss1]) with reachNT_non_isAut[OF rsT] uid1 have uid1_ne: "uid1\UIDs" by auto let ?a1 = "(Uact (uPaperC cid uid1 (pass s1 uid1) PID v))" obtain s1' where step: "step s1 ?a1 = (outOK,s1')" and s1's1: "eqButPID s1' s1" apply (simp add: u_defs cid1 uid1 pid1 ph1 aut1) apply (cases "paper s1 PID") apply (auto simp: eqButPID_def eeqButPID_def) done have "?iact" proof show "step s1 ?a1 = (outOK,s1')" using step . show "\ (Trans s1 ?a1 outOK s1')" by simp show "consume (Trans s1 ?a1 outOK s1') vl1 vl1'" by (simp add: consume_def) show "\\ (Trans s1 ?a1 outOK s1')" by (simp add: uid1_ne) have "\2 s vl s1' vl1'" unfolding \2_def B_def using vl vlvl1 ph pid apply simp_all by (metis s1's1 eqButPID_sym eqButPID_trans ss1) thus "disjAll {\2, \3, \e} s vl s1' vl1'" by simp qed thus ?thesis by simp next case False then obtain v1 where [simp]: "vl1=[v1]" using vl1 by (cases vl1) auto have "?react" proof (rule, goal_cases) case (1 a ou s' vl') assume STET: "step s a = (ou, s')" and "\ T (Trans s a ou s')" and CONSUME: "consume (Trans s a ou s') vl vl'" have ph': "phase s' cid \ subPH" - by (smt STET ph phase_increases) + by (smt (verit) STET ph phase_increases) have pid': "PID \\ paperIDs s' cid" using pid STET by (metis paperIDs_mono) { fix s1 vl1 assume "phase s' cid \ subPH" hence "\e s' vl' s1 vl1" unfolding \e_def using STET CONSUME vl ph apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs consume_def pid) apply metis . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by simp_all } note \e=this obtain s1' ou' where STET': "step s1 a = (ou',s1')" and s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 STET] by fastforce from eqButPID_step_\[OF ss1 STET STET'] have \_eq: "\ (Trans s1 a ou' s1') = \ (Trans s a ou s')" by simp show ?case (is "?match \ ?ignore") proof (cases "\ (Trans s a ou s')") case True note \=this then obtain cid' uid p where a[simp]: "a=Uact (uPaperC cid' uid p PID (hd vl))" "ou=outOK" using CONSUME by (cases "(Trans s a ou s')" rule: f.cases) (auto simp add: consume_def vl) from STET pid have [simp]: "cid'=cid" by (simp add: u_defs paperIDs_equals[OF rs]) from \_step_eqButPID[OF \ STET] have ss': "eqButPID s s'" . have n\: "\\ (Trans s a ou s')" using T_\_\[OF rsT STET] by simp have ph': "phase s' cid = subPH" using STET by (auto simp add: u_defs) show ?thesis proof (cases "length vl = 1") case True hence [simp]: "vl=[v1]" using vlvl1 by (cases vl) simp_all from CONSUME have [simp]: "vl'=[]" by (simp add: consume_def \) from STET STET' have [simp]: "s1'=s'" using eqButPID_step_eq ss1 a by blast have ?match proof show "validTrans (Trans s1 a ou' s1')" using STET' by simp show "consume (Trans s1 a ou' s1') vl1 []" using \ \_eq CONSUME by (simp add: consume_def) show "\ (Trans s a ou s') = \ (Trans s1 a ou' s1')" by simp show "\ (Trans s a ou s') \ g (Trans s a ou s') = g (Trans s1 a ou' s1')" using n\ by simp have "\3 s' vl' s1' []" unfolding \3_def using ph' pid' by force thus "disjAll {\2, \3, \e} s' vl' s1' []" by simp qed thus ?thesis by simp next case False then obtain v where [simp]: "vl=v#vl'" "vl'\[]" using CONSUME vl by (cases vl) (simp_all add: consume_def) have ?ignore proof show "\ \ (Trans s a ou s')" by (rule n\) have "\2 s' vl' s1 vl1" unfolding \2_def B_def using vlvl1 ph' pid' eqButPID_trans[OF eqButPID_sym[OF ss'] ss1] by auto thus "disjAll {\2, \3, \e} s' vl' s1 vl1" by simp qed thus ?thesis by simp qed next case False note \=this with CONSUME have [simp]: "vl'=vl" by (simp add: consume_def) have ?match proof show "validTrans (Trans s1 a ou' s1')" using STET' by simp show "consume (Trans s1 a ou' s1') vl1 vl1" using \ by (simp add: consume_def \_eq) show "\ (Trans s a ou s') = \ (Trans s1 a ou' s1')" by simp show "\ (Trans s a ou s') \ g (Trans s a ou s') = g (Trans s1 a ou' s1')" using eqButPID_step_out[OF ss1 STET STET' rsT rs1 pid ph] by simp show "disjAll {\2, \3, \e} s' vl' s1' vl1" proof (cases "phase s' cid = subPH") case True hence "\2 s' vl' s1' vl1" unfolding \2_def B_def using eqButPID_step[OF ss1 STET STET'] using ph' pid' vl vl1 vlvl1 by auto thus ?thesis by simp next case False hence "\e s' vl' s1' vl1" using \e by simp thus ?thesis by simp qed qed thus ?thesis by simp qed qed thus ?thesis using vl vl1 by simp qed qed lemma unwind_cont_\3: "unwind_cont \3 {\3,\e}" proof (rule, goal_cases) case (1 s vl s1 vl1) assume rsT: "reachNT s" and rs1: "reach s1" and \: "\3 s vl s1 vl1" thm \3_def then obtain cid where [simp]: "s1=s" "vl=[]" "vl1=[]" and pid: "PID \\ paperIDs s cid" unfolding \3_def by auto thus ?case (is "_ \ (_ \ ?react)") proof - have "?react" proof (rule, goal_cases) case (1 a ou s' vl') assume STET: "step s a = (ou, s')" and NT: "\ T (Trans s a ou s')" and CONSUME: "consume (Trans s a ou s') vl vl'" have \3: "\3 s' vl' s' vl'" and [simp]: "vl'=[]" using CONSUME paperIDs_mono[OF STET pid] unfolding \3_def by (auto simp add: consume_def) thus ?case (is "?match \ ?ignore") proof - have ?match apply (rule matchI[of s1 a ou s' vl1 vl1]) using STET CONSUME \3 by simp_all thus ?thesis by simp qed qed thus ?thesis by simp qed qed definition K1exit where "K1exit s \ \cid. phase s cid > subPH \ PID \\ paperIDs s cid" lemma invarNT_K1exit: "invarNT K1exit" unfolding invarNT_def apply (safe dest!: reachNT_reach) subgoal for _ a apply(cases a) subgoal for x1 apply(cases x1) apply (auto simp: c_defs K1exit_def) . subgoal for x2 apply(cases x2) apply (auto simp: u_defs K1exit_def paperIDs_equals,force+) . subgoal for x3 apply(cases x3) apply (auto simp: uu_defs K1exit_def) . by simp_all done lemma noVal_K1exit: "noVal K1exit v" apply(rule no\_noVal) unfolding no\_def apply safe subgoal for _ a apply(cases a) subgoal by simp subgoal for x2 apply(cases x2, auto simp add: u_defs K1exit_def) [] apply (metis reachNT_reach less_not_refl paperIDs_equals) . by simp_all 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 hence "K1exit s" using \e unfolding K1exit_def \e_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_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 diff --git a/thys/CoCon/Paper_Confidentiality/Paper_Aut_PC.thy b/thys/CoCon/Paper_Confidentiality/Paper_Aut_PC.thy --- a/thys/CoCon/Paper_Confidentiality/Paper_Aut_PC.thy +++ b/thys/CoCon/Paper_Confidentiality/Paper_Aut_PC.thy @@ -1,468 +1,468 @@ theory Paper_Aut_PC imports "../Observation_Setup" Paper_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning" begin subsection \Confidentiality protection from users who are not the paper's authors or PC members\ text \We verify the following property: \ \\ A group of users UIDs learns nothing about the various uploads of a paper PID (save for the non-existence of any upload) unless/until one of the following occurs: \begin{itemize} \item a user in UIDs becomes the paper's author or \item a user in UIDs becomes a PC member in the paper's conference and the conference moves to the bidding phase. \end{itemize} \ fun T :: "(state,act,out) trans \ bool" where "T (Trans _ _ ou s') = (\ uid \ UIDs. isAUT s' uid PID \ (\ cid. PID \\ paperIDs s' cid \ isPC s' cid uid \ phase s' cid \ bidPH) )" 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_isAut_isPC_isChair: assumes "reachNT s" and "uid \ UIDs" shows "\ isAut s cid uid PID \ (isPC s cid uid \ \ PID \\ paperIDs s cid \ phase s cid \ subPH) \ (isChair s cid uid \ \ PID \\ paperIDs s cid \ phase s cid \ subPH)" using assms apply (cases rule: reachNT_state_cases) apply (auto simp: istate_def)[] apply clarsimp (* safety property used: isChair_isPC *) by (simp add: T.simps assms(1) isAUT_def isChair_isPC not_less_eq_eq reachNT_reach) 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_isAut_isPC_isChair[OF 1] 2 unfolding T.simps \_def2 by (auto simp add: u_defs) (* Note: the following alternative formulation is not always guaranteed to hold, due to the trigger T speaking about s', not s: lemma P_\_\: assumes 1: "\ T (Trans s a ou s')" and 2: "step s a = (ou,s')" "\ (Trans s a ou s')" shows "\ \ (Trans s a ou s')" using 1 2 unfolding T.simps \_def2 by (auto simp add: u_defs) *) text \major\ lemma eqButPID_step_out: assumes s's1': "eqButPID s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and sT: "reachNT s" and s1: "reach s1" and PID: "PID \\ paperIDs s cid" and UIDs: "userOfA a \ UIDs" shows "ou = ou1" proof- note Inv = reachNT_non_isAut_isPC_isChair[OF sT UIDs] note eqs = eqButPID_imp[OF s's1'] note eqs' = eqButPID_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 eqButPID_def eeqButPID_def eqButC note * = step step1 eqs eqs' s s1 PID UIDs paperIDs_equals[OF s] Inv show ?thesis proof (cases a) case (Cact x1) then show ?thesis using * by (cases x1; auto) next case (Uact x2) then show ?thesis using * by (cases x2; auto) next case (UUact x3) then show ?thesis using * by (cases x3; auto) next case (Ract x4) with * show ?thesis proof (cases x4) case (rPaperC x61 x62 x63 x64) then show ?thesis using * Ract by (clarsimp; metis not_less_eq_eq) next case (rMyReview x81 x82 x83 x84) then show ?thesis using * Ract by (auto simp: getNthReview_def) next case (rReviews x91 x92 x93 x94) then show ?thesis using * Ract by (clarsimp; metis Suc_leD eqButPID_imp2 not_less_eq_eq s's1') qed auto next case (Lact x5) then show ?thesis using * by (cases x5; auto) qed qed definition \1 :: "state \ value list \ state \ value list \ bool" where "\1 s vl s1 vl1 \ \ (\cid. PID \\ paperIDs s cid) \ 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 = subPH \ eqButPID s s1" definition \3 :: "state \ value list \ state \ value list \ bool" where "\3 s vl s1 vl1 \ \cid. PID \\ paperIDs s cid \ eqButPID s s1 \ phase s cid > subPH \ vl=[] \ vl1=[]" definition \e :: "state \ value list \ state \ value list \ bool" where "\e s vl s1 vl1 \ \cid. PID \\ paperIDs s cid \ phase s cid > subPH \ vl \ []" 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, goal_cases) case (1 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: "\cid. PID \ set (paperIDs s cid)" using reachNT_reach unfolding \1_def B_def by auto show ?case (is "?iact \ (_ \ ?react)") proof- have ?react proof (rule, goal_cases) case (1 a ou s' 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 by(auto simp: u_defs) by simp_all hence vl': "vl' = vl" using c unfolding consume_def by auto show ?case (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 "disjAll {\1, \2, \e} s' vl' s' vl1" proof (cases "\cid. PID \\ paperIDs s' cid") case False hence "\1 s' vl' s' vl1" by (simp add: \1_def B_def vl vl') thus ?thesis by simp next case True hence "\2 s' vl' s' vl1" using step pid apply (simp add: \2_def vl' vl) apply (erule exE) subgoal for cid apply (rule exI[of _ cid]) apply (cases a) subgoal for x1 apply (cases x1, auto simp: c_defs) [] . subgoal for x2 apply (cases x2, auto simp: u_defs) [] . subgoal for x3 apply (cases x3, auto simp: uu_defs) [] . by simp_all done thus ?thesis by simp qed qed thus ?thesis by simp qed qed thus ?thesis using vl by simp qed qed lemma unwind_cont_\2: "unwind_cont \2 {\2,\3,\e}" proof(rule,goal_cases) case (1 s vl s1 vl1) assume rsT: "reachNT s" and rs1: "reach s1" and "\2 s vl s1 vl1" then obtain cid where rs: "reach s" and pid: "PID \\ paperIDs s cid" and ss1: "eqButPID s s1" and ph: "phase s cid = subPH" using reachNT_reach unfolding \2_def by auto have cid: "cid \\ confIDs s" by (metis paperIDs_confIDs pid rs) from pid ph cid have pid1: "PID \\ paperIDs s1 cid" and ph1: "phase s1 cid = subPH" and cid1: "cid \\ confIDs s1" by (auto simp add: eqButPID_imp[OF ss1]) show ?case (is "?iact \ (_ \ ?react)") proof (cases vl1) case (Cons v vl1') note this[simp] obtain uid1 where aut1: "isAut s1 cid uid1 PID" thm paperID_ex_userID using paperID_ex_userID[OF rs1 pid1] by auto have uid1: "uid1 \\ userIDs s1" by (metis roles_userIDs rs1 aut1) from aut1 have "isAut s cid uid1 PID" using ss1 aut1 by (simp add: eqButPID_imp[OF ss1]) with reachNT_non_isAut_isPC_isChair[OF rsT] uid1 have uid1_ne: "uid1\UIDs" by auto let ?a1 = "(Uact (uPaperC cid uid1 (pass s1 uid1) PID v))" obtain s1' where step: "step s1 ?a1 = (outOK,s1')" and s1's1: "eqButPID s1' s1" by (cases "paper s1 PID") (auto simp add: u_defs cid1 uid1 pid1 ph1 aut1 eqButPID_def eeqButPID_def) have "?iact" proof show "step s1 ?a1 = (outOK,s1')" using step . show "\ (Trans s1 ?a1 outOK s1')" by simp show "consume (Trans s1 ?a1 outOK s1') vl1 vl1'" by (simp add: consume_def) show "\\ (Trans s1 ?a1 outOK s1')" by (simp add: uid1_ne) have "\2 s vl s1' vl1'" unfolding \2_def apply (rule exI[where x=cid]) using ph pid apply clarsimp by (metis s1's1 eqButPID_sym eqButPID_trans ss1) thus "disjAll {\2, \3, \e} s vl s1' vl1'" by simp qed thus ?thesis by simp next case Nil note this[simp] have "?react" proof (rule, goal_cases) case (1 a ou s' vl') assume STEP: "step s a = (ou, s')" and "\ T (Trans s a ou s')" and CONSUME: "consume (Trans s a ou s') vl vl'" have ph': "phase s' cid \ subPH" - by (smt STEP ph phase_increases) + by (smt (verit) STEP ph phase_increases) have pid': "PID \\ paperIDs s' cid" using pid STEP by (metis paperIDs_mono) { fix s1 vl1 assume "phase s' cid \ subPH" "vl'\[]" hence "\e s' vl' s1 vl1" unfolding \e_def apply - apply(rule exI[of _ cid]) using STEP CONSUME ph apply (cases a) subgoal for x1 apply (cases x1) apply(auto simp: c_defs) . subgoal for x2 apply (cases x2) apply(auto simp: u_defs consume_def pid) . subgoal for x3 apply (cases x3) apply(auto simp: uu_defs) . by simp_all } note \e=this obtain s1' ou' where STEP': "step s1 a = (ou',s1')" and s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 STEP] by fastforce from eqButPID_step_\[OF ss1 STEP STEP'] have \_eq: "\ (Trans s1 a ou' s1') = \ (Trans s a ou s')" by simp show ?case (is "?match \ ?ignore") proof (cases "\ (Trans s a ou s')") case True note \=this then obtain cid' uid p where a[simp]: "a=Uact (uPaperC cid' uid p PID (hd vl))" "ou=outOK" using CONSUME by (cases "(Trans s a ou s')" rule: f.cases) (auto simp add: consume_def) from STEP pid have [simp]: "cid'=cid" by (simp add: u_defs paperIDs_equals[OF rs]) from \_step_eqButPID[OF \ STEP] have ss': "eqButPID s s'" . have n\: "\\ (Trans s a ou s')" using P_\_\[OF rsT STEP] by simp have ph': "phase s' cid = subPH" using STEP by (auto simp add: u_defs) have ?ignore proof show "\ \ (Trans s a ou s')" by (rule n\) have "\2 s' vl' s1 vl1" unfolding \2_def using ph' pid' eqButPID_trans[OF eqButPID_sym[OF ss'] ss1] by auto thus "disjAll {\2, \3, \e} s' vl' s1 vl1" by simp qed thus ?thesis by simp next case False note \=this with CONSUME have [simp]: "vl'=vl" by (simp add: consume_def) have ?match proof show "validTrans (Trans s1 a ou' s1')" using STEP' by simp show "consume (Trans s1 a ou' s1') vl1 vl1" using \ by (simp add: consume_def \_eq) show "\ (Trans s a ou s') = \ (Trans s1 a ou' s1')" by simp show "\ (Trans s a ou s') \ g (Trans s a ou s') = g (Trans s1 a ou' s1')" using eqButPID_step_out[OF ss1 STEP STEP' rsT rs1 pid] by simp show "disjAll {\2, \3, \e} s' vl' s1' vl1" proof (cases "phase s' cid = subPH") case True hence "\2 s' vl' s1' vl1" unfolding \2_def using eqButPID_step[OF ss1 STEP STEP'] using ph' pid' by auto thus ?thesis by simp next case False with ph' have ph': "subPH < phase s' cid" by simp show ?thesis proof (cases "vl'=[]") case False hence "\e s' vl' s1' vl1" using \e ph' by simp thus ?thesis by simp next case True hence "\3 s' vl' s1' vl1" unfolding \3_def apply(intro exI[of _ cid]) using ph' pid' eqButPID_step[OF ss1 STEP STEP'] by simp thus ?thesis by simp qed qed qed thus ?thesis by simp qed qed thus ?thesis by simp qed qed lemma unwind_cont_\3: "unwind_cont \3 {\3,\e}" proof (rule, goal_cases) case (1 s vl s1 vl1) assume rsT: "reachNT s" and rs1: "reach s1" and \: "\3 s vl s1 vl1" thm \3_def then obtain cid where ss1: "eqButPID s s1" and [simp]: "vl=[]" "vl1=[]" and pid: "PID \\ paperIDs s cid" and ph: "subPH < phase s cid" unfolding \3_def by auto from rsT have rs: "reach s" by (metis reachNT_reach) from pid ph have pid1: "PID \\ paperIDs s1 cid" and ph1: "subPH < phase s1 cid" using ss1 by (auto simp add: eqButPID_imp) thus ?case (is "_ \ (_ \ ?react)") proof - have "?react" proof (rule, goal_cases) case (1 a ou s' vl') assume STEP: "step s a = (ou, s')" and NT: "\ T (Trans s a ou s')" (is "\T ?trn") and CONSUME: "consume (Trans s a ou s') vl vl'" show ?case (is "?match \ _") proof - have ph': "subPH < phase s' cid" using STEP ph phase_increases by (meson le_trans not_less) have [simp]: "vl'=[]" using CONSUME by (auto simp add: consume_def) 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': "eqButPID s' s1'" using eqButPID_step[OF ss1 STEP STEP1] . from s's1' ph' have ph1': "subPH < phase s1' cid" by (simp add: eqButPID_imp) have \: "\ \ ?trn1" using STEP1 ph1' unfolding \_def2 by (auto simp: u_defs paperIDs_equals[OF rs1 pid1]) have ?match proof show "validTrans ?trn1" using STEP1 by simp next show "consume ?trn1 vl1 vl1" unfolding consume_def using \ by auto next show "\ ?trn = \ ?trn1" unfolding ss1 by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" using eqButPID_step_out[OF ss1 STEP STEP1 rsT rs1 pid] by simp next have "\3 s' vl' s1' vl1" using ph' s's1' paperIDs_mono[OF STEP pid] unfolding \3_def by auto thus "disjAll {\3, \e} s' vl' s1' vl1" by simp qed thus ?thesis by simp qed qed thus ?case by simp qed qed definition K1exit where "K1exit s \ \cid. phase s cid > subPH \ PID \\ paperIDs s cid" lemma invarNT_K1exit: "invarNT K1exit" unfolding invarNT_def apply (safe dest!: reachNT_reach) subgoal for _ a apply(cases a) subgoal for x1 apply (cases x1, auto simp: c_defs K1exit_def) . subgoal for x2 apply (cases x2) apply(auto simp: u_defs K1exit_def paperIDs_equals) apply (metis less_nat_zero_code) apply (metis Suc_lessD) . subgoal for x3 apply (cases x3, auto simp: uu_defs K1exit_def) . by simp_all done lemma noVal_K1exit: "noVal K1exit v" apply(rule no\_noVal) unfolding no\_def apply safe subgoal for _ a apply(cases a) subgoal by simp subgoal for x2 apply(cases x2, auto simp add: u_defs K1exit_def) [] apply (metis reachNT_reach less_not_refl paperIDs_equals) . by simp_all 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 hence "K1exit s" using \e unfolding K1exit_def \e_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_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 diff --git a/thys/CoCon/Review_Confidentiality/Review_RAut_NCPC.thy b/thys/CoCon/Review_Confidentiality/Review_RAut_NCPC.thy --- a/thys/CoCon/Review_Confidentiality/Review_RAut_NCPC.thy +++ b/thys/CoCon/Review_Confidentiality/Review_RAut_NCPC.thy @@ -1,744 +1,744 @@ 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 eqExcPID_N2_imp3 getNthReview_def ss1) + 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 decs_exit eqExcPID_N2_imp3 getNthReview_def list.simps(4) nth_Cons_0 ss1) + 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 diff --git a/thys/CoCon/Review_Confidentiality/Review_Value_Setup.thy b/thys/CoCon/Review_Confidentiality/Review_Value_Setup.thy --- a/thys/CoCon/Review_Confidentiality/Review_Value_Setup.thy +++ b/thys/CoCon/Review_Confidentiality/Review_Value_Setup.thy @@ -1,610 +1,610 @@ (* The value setup for reviewer confidentiality *) theory Review_Value_Setup imports Review_Intro begin consts PID :: paperID consts N :: nat text \\<^term>\(PID,N)\ identifies uniquely the review under scrutiny\ subsection \Preliminaries\ declare updates_commute_paper[simp] text \Auxiliary definitions:\ definition eqExcNth where "eqExcNth xs ys n \ length xs = length ys \ (\ i < length xs. i \ n \ xs!i = ys!i)" lemma eqExcNth_eq[simp,intro!]: "eqExcNth xs xs n" unfolding eqExcNth_def by auto lemma eqExcNth_sym: assumes "eqExcNth xs xs1 n" shows "eqExcNth xs1 xs n" using assms unfolding eqExcNth_def by auto lemma eqExcNth_trans: assumes "eqExcNth xs xs1 n" and "eqExcNth xs1 xs2 n" shows "eqExcNth xs xs2 n" using assms unfolding eqExcNth_def by auto fun eqExcD :: "paper \ paper \ bool" where "eqExcD (Paper name info ct reviews dis decs) (Paper name1 info1 ct1 reviews1 dis1 decs1) = (name = name1 \ info = info1 \ ct = ct1 \ dis = dis1 \ decs = decs1 \ eqExcNth reviews reviews1 N)" lemma eqExcD: "eqExcD pap pap1 = (titlePaper pap = titlePaper pap1 \ abstractPaper pap = abstractPaper pap1 \ contentPaper pap = contentPaper pap1 \ disPaper pap = disPaper pap1 \ decsPaper pap = decsPaper pap1 \ eqExcNth (reviewsPaper pap) (reviewsPaper pap1) N)" by(cases pap, cases pap1, auto) lemma eqExcD_eq[simp,intro!]: "eqExcD pap pap" unfolding eqExcD using eqExcNth_eq by auto lemma eqExcD_sym: assumes "eqExcD pap pap1" shows "eqExcD pap1 pap" using assms unfolding eqExcD using eqExcNth_sym by auto lemma eqExcD_trans: assumes "eqExcD pap pap1" and "eqExcD pap1 pap2" shows "eqExcD pap pap2" using assms unfolding eqExcD using eqExcNth_trans by auto definition eeqExcPID_N where "eeqExcPID_N paps paps1 \ \ pid. if pid = PID then eqExcD (paps pid) (paps1 pid) else paps pid = paps1 pid" lemma eeqExcPID_N_eeq[simp,intro!]: "eeqExcPID_N s s" unfolding eeqExcPID_N_def by auto lemma eeqExcPID_N_sym: assumes "eeqExcPID_N s s1" shows "eeqExcPID_N s1 s" using assms eqExcD_sym unfolding eeqExcPID_N_def by auto lemma eeqExcPID_N_trans: assumes "eeqExcPID_N s s1" and "eeqExcPID_N s1 s2" shows "eeqExcPID_N s s2" using assms eqExcD_trans unfolding eeqExcPID_N_def by simp blast lemma eeqExcPID_N_imp: "eeqExcPID_N paps paps1 \ eqExcD (paps PID) (paps1 PID)" "\eeqExcPID_N paps paps1; pid \ PID\ \ paps pid = paps1 pid" unfolding eeqExcPID_N_def by auto lemma eeqExcPID_N_cong: assumes "eeqExcPID_N paps paps1" and "pid = PID \ eqExcD uu uu1" and "pid \ PID \ uu = uu1" shows "eeqExcPID_N (paps (pid := uu)) (paps1(pid := uu1))" using assms unfolding eeqExcPID_N_def by auto lemma eeqExcPID_N_RDD: "eeqExcPID_N paps paps1 \ titlePaper (paps PID) = titlePaper (paps1 PID) \ abstractPaper (paps PID) = abstractPaper (paps1 PID) \ contentPaper (paps PID) = contentPaper (paps1 PID) \ disPaper (paps PID) = disPaper (paps1 PID) \ decsPaper (paps PID) = decsPaper (paps1 PID)" using eeqExcPID_N_def unfolding eqExcD by auto text \The notion of two states being equal everywhere except on the the review \<^term>\(N,PID)\:\ definition eqExcPID_N :: "state \ state \ bool" where "eqExcPID_N s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ roles s = roles s1 \ paperIDs s = paperIDs s1 \ eeqExcPID_N (paper s) (paper s1) \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1" lemma eqExcPID_N_eq[simp,intro!]: "eqExcPID_N s s" unfolding eqExcPID_N_def by auto lemma eqExcPID_N_sym: assumes "eqExcPID_N s s1" shows "eqExcPID_N s1 s" using assms eeqExcPID_N_sym unfolding eqExcPID_N_def by auto lemma eqExcPID_N_trans: assumes "eqExcPID_N s s1" and "eqExcPID_N s1 s2" shows "eqExcPID_N s s2" using assms eeqExcPID_N_trans unfolding eqExcPID_N_def by auto text \Implications from \<^term>\eqExcPID_N\, including w.r.t. auxiliary operations:\ lemma eqExcPID_N_imp: "eqExcPID_N s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ roles s = roles s1 \ paperIDs s = paperIDs s1 \ eeqExcPID_N (paper s) (paper s1) \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1 \ getAllPaperIDs s = getAllPaperIDs s1 \ isRev s cid uid pid = isRev s1 cid uid pid \ getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid \ getRevRole s cid uid pid = getRevRole s1 cid uid pid \ length (reviewsPaper (paper s pid)) = length (reviewsPaper (paper s1 pid))" unfolding eqExcPID_N_def getAllPaperIDs_def unfolding isRev_def getReviewIndex_def getRevRole_def apply auto unfolding eeqExcPID_N_def eqExcD eqExcNth_def by (cases "pid = PID") auto lemma eqExcPID_N_imp1: "eqExcPID_N s s1 \ eqExcD (paper s pid) (paper s1 pid)" "eqExcPID_N s s1 \ pid \ PID \ PID \ pid \ paper s pid = paper s1 pid \ getNthReview s pid n = getNthReview s1 pid n" unfolding eqExcPID_N_def eeqExcPID_N_def getNthReview_def apply auto by (metis eqExcD_eq) lemma eqExcPID_N_imp2: assumes "eqExcPID_N s s1" and "pid \ PID \ PID \ pid" shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid" proof- have "(\uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])" apply(rule ext) using assms by (auto simp: eqExcPID_N_imp eqExcPID_N_imp1) thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID_N_imp) qed lemma eqExcPID_N_imp3: "eqExcPID_N s s1 \ pid \ PID \ PID \ pid \ (n < length (reviewsPaper (paper s PID)) \ n \ N) \ getNthReview s pid n = getNthReview s1 pid n" unfolding eqExcPID_N_def apply auto apply (metis eeqExcPID_N_imp(2) getNthReview_def) unfolding eeqExcPID_N_def apply simp unfolding eqExcD eqExcNth_def by (metis getNthReview_def) lemma eqExcPID_N_imp3': assumes s: "reach s" and "eqExcPID_N s s1" and "pid \ PID \ (isRevNth s cid uid pid n \ n \ N)" shows "getNthReview s pid n = getNthReview s1 pid n" proof- have "isRevNth s cid uid pid n \ pid \ PID \ n < length (reviewsPaper (paper s PID))" using s by (metis isRevNth_less_length) thus ?thesis using eqExcPID_N_imp3 assms by auto qed lemma eqExcPID_N_RDD: "eqExcPID_N s s1 \ titlePaper (paper s PID) = titlePaper (paper s1 PID) \ abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \ contentPaper (paper s PID) = contentPaper (paper s1 PID) \ disPaper (paper s PID) = disPaper (paper s1 PID) \ decsPaper (paper s PID) = decsPaper (paper s1 PID)" using eqExcPID_N_imp eeqExcPID_N_RDD by auto lemma eqExcPID_N_cong[simp, intro]: "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \confIDs := uu1\) (s1 \confIDs := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \conf := uu1\) (s1 \conf := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \userIDs := uu1\) (s1 \userIDs := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \pass := uu1\) (s1 \pass := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \user := uu1\) (s1 \user := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \roles := uu1\) (s1 \roles := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \paperIDs := uu1\) (s1 \paperIDs := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ eeqExcPID_N uu1 uu2 \ eqExcPID_N (s \paper := uu1\) (s1 \paper := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \pref := uu1\) (s1 \pref := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \voronkov := uu1\) (s1 \voronkov := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \news := uu1\) (s1 \news := uu2\)" "\ uu1 uu2. eqExcPID_N s s1 \ uu1 = uu2 \ eqExcPID_N (s \phase := uu1\) (s1 \phase := uu2\)" unfolding eqExcPID_N_def by auto lemma eqExcPID_N_Paper: assumes s's1': "eqExcPID_N s s1" and "paper s pid = Paper title abstract content reviews dis decs" and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1" shows "title = title1 \ abstract = abstract1 \ content = content1 \ dis = dis1 \ decs = decs1" using assms unfolding eqExcPID_N_def apply (auto simp: eqExcD eeqExcPID_N_def) by (metis titlePaper.simps abstractPaper.simps contentPaper.simps disPaper.simps decsPaper.simps)+ text \Auxiliary definitions for a slightly weaker equivalence relation defined below:\ definition eqExcNth2 where "eqExcNth2 rl rl1 n \ length rl = length rl1 \ (\ i < length rl. i \ n \ rl!i = rl1!i) \ hd (rl!n) = hd (rl1!n)" lemma eqExcNth2_eq[simp,intro!]: "eqExcNth2 rl rl n" unfolding eqExcNth2_def by auto lemma eqExcNth2_sym: assumes "eqExcNth2 rl rl1 n" shows "eqExcNth2 rl1 rl n" using assms unfolding eqExcNth2_def by auto lemma eqExcNth2_trans: assumes "eqExcNth2 rl rl1 n" and "eqExcNth2 rl1 rl2 n" shows "eqExcNth2 rl rl2 n" using assms unfolding eqExcNth2_def by auto fun eqExcD2 :: "paper \ paper \ bool" where "eqExcD2 (Paper title abstract ct reviews dis decs) (Paper title1 abstract1 ct1 reviews1 dis1 decs1) = (title = title1 \ abstract = abstract1 \ ct = ct1 \ dis = dis1 \ decs = decs1 \ eqExcNth2 reviews reviews1 N)" lemma eqExcD2: "eqExcD2 pap pap1 = (titlePaper pap = titlePaper pap1 \ abstractPaper pap = abstractPaper pap1 \ contentPaper pap = contentPaper pap1 \ disPaper pap = disPaper pap1 \ decsPaper pap = decsPaper pap1 \ eqExcNth2 (reviewsPaper pap) (reviewsPaper pap1) N)" by(cases pap, cases pap1, auto) lemma eqExcD2_eq[simp,intro!]: "eqExcD2 pap pap" unfolding eqExcD2 using eqExcNth2_eq by auto lemma eqExcD2_sym: assumes "eqExcD2 pap pap1" shows "eqExcD2 pap1 pap" using assms unfolding eqExcD2 using eqExcNth2_sym by auto lemma eqExcD2_trans: assumes "eqExcD2 pap pap1" and "eqExcD2 pap1 pap2" shows "eqExcD2 pap pap2" using assms unfolding eqExcD2 using eqExcNth2_trans by auto definition eeqExcPID_N2 where "eeqExcPID_N2 paps paps1 \ \ pid. if pid = PID then eqExcD2 (paps pid) (paps1 pid) else paps pid = paps1 pid" lemma eeqExcPID_N2_eeq[simp,intro!]: "eeqExcPID_N2 s s" unfolding eeqExcPID_N2_def by auto lemma eeqExcPID_N2_sym: assumes "eeqExcPID_N2 s s1" shows "eeqExcPID_N2 s1 s" using assms eqExcD2_sym unfolding eeqExcPID_N2_def by auto lemma eeqExcPID_N2_trans: assumes "eeqExcPID_N2 s s1" and "eeqExcPID_N2 s1 s2" shows "eeqExcPID_N2 s s2" using assms eqExcD2_trans unfolding eeqExcPID_N2_def by simp blast lemma eeqExcPID_N2_imp: "eeqExcPID_N2 paps paps1 \ eqExcD2 (paps PID) (paps1 PID)" "\eeqExcPID_N2 paps paps1; pid \ PID\ \ paps pid = paps1 pid" unfolding eeqExcPID_N2_def by auto lemma eeqExcPID_N2_cong: assumes "eeqExcPID_N2 paps paps1" and "pid = PID \ eqExcD2 uu uu1" and "pid \ PID \ uu = uu1" shows "eeqExcPID_N2 (paps (pid := uu)) (paps1(pid := uu1))" using assms unfolding eeqExcPID_N2_def by auto lemma eeqExcPID_N2_RDD: "eeqExcPID_N2 paps paps1 \ titlePaper (paps PID) = titlePaper (paps1 PID) \ abstractPaper (paps PID) = abstractPaper (paps1 PID) \ contentPaper (paps PID) = contentPaper (paps1 PID) \ disPaper (paps PID) = disPaper (paps1 PID) \ decsPaper (paps PID) = decsPaper (paps1 PID)" using eeqExcPID_N2_def unfolding eqExcD2 by auto text \A weaker state equivalence that allows differences in old versions of the score and comments of the review \<^term>\(N, PID)\. It is used for the confidentiality property that does not cover PC members in the discussion phase, when they will learn about scores and comments.\ definition eqExcPID_N2 :: "state \ state \ bool" where "eqExcPID_N2 s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ roles s = roles s1 \ paperIDs s = paperIDs s1 \ eeqExcPID_N2 (paper s) (paper s1) \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1" lemma eqExcPID_N2_eq[simp,intro!]: "eqExcPID_N2 s s" unfolding eqExcPID_N2_def by auto lemma eqExcPID_N2_sym: assumes "eqExcPID_N2 s s1" shows "eqExcPID_N2 s1 s" using assms eeqExcPID_N2_sym unfolding eqExcPID_N2_def by auto lemma eqExcPID_N2_trans: assumes "eqExcPID_N2 s s1" and "eqExcPID_N2 s1 s2" shows "eqExcPID_N2 s s2" using assms eeqExcPID_N2_trans unfolding eqExcPID_N2_def by auto text \Implications from \<^term>\eqExcPID_N2\, including w.r.t. auxiliary operations:\ lemma eqExcPID_N2_imp: "eqExcPID_N2 s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ roles s = roles s1 \ paperIDs s = paperIDs s1 \ eeqExcPID_N2 (paper s) (paper s1) \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1 \ getAllPaperIDs s = getAllPaperIDs s1 \ isRev s cid uid pid = isRev s1 cid uid pid \ getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid \ getRevRole s cid uid pid = getRevRole s1 cid uid pid \ length (reviewsPaper (paper s pid)) = length (reviewsPaper (paper s1 pid))" unfolding eqExcPID_N2_def getAllPaperIDs_def unfolding isRev_def getReviewIndex_def getRevRole_def apply auto unfolding eeqExcPID_N2_def eqExcD2 eqExcNth2_def by simp metis lemma eqExcPID_N2_imp1: "eqExcPID_N2 s s1 \ eqExcD2 (paper s pid) (paper s1 pid)" "eqExcPID_N2 s s1 \ pid \ PID \ PID \ pid \ paper s pid = paper s1 pid \ getNthReview s pid n = getNthReview s1 pid n" unfolding eqExcPID_N2_def getNthReview_def eeqExcPID_N2_def apply auto by (metis eqExcD2_eq) lemma eqExcPID_N2_imp2: assumes "eqExcPID_N2 s s1" and "pid \ PID \ PID \ pid" shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid" proof- have "(\uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])" apply(rule ext) using assms by (auto simp: eqExcPID_N2_imp eqExcPID_N2_imp1) thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID_N2_imp) qed lemma eqExcPID_N2_eqExcPID_N: "eqExcPID_N2 s s1 \ eqExcPID_N s s1" unfolding eqExcPID_N_def eqExcPID_N2_def eeqExcPID_N_def eeqExcPID_N2_def eqExcD2 eqExcD by (auto simp: eqExcNth_def eqExcNth2_def) lemma eqExcPID_N2_imp3: "eqExcPID_N2 s s1 \ pid \ PID \ PID \ pid \ (n < length (reviewsPaper (paper s PID)) \ n \ N) \ getNthReview s pid n = getNthReview s1 pid n" by (metis eqExcPID_N2_eqExcPID_N eqExcPID_N_imp3) lemma eqExcPID_N2_imp3': assumes s: "reach s" and "eqExcPID_N2 s s1" and "pid \ PID \ (isRevNth s cid uid pid n \ n \ N)" shows "getNthReview s pid n = getNthReview s1 pid n" by (metis assms eqExcPID_N2_eqExcPID_N eqExcPID_N_imp3') lemma eqExcPID_N2_imp33: assumes "eqExcPID_N2 s s1" shows "hd (getNthReview s pid N) = hd (getNthReview s1 pid N)" proof(cases "pid = PID") case False thus ?thesis using eqExcPID_N2_imp3[OF assms] by auto next case True thus ?thesis apply simp using assms unfolding eqExcPID_N2_def eeqExcPID_N2_def eqExcD2 eqExcNth2_def getNthReview_def by auto qed lemma eqExcPID_N2_RDD: "eqExcPID_N2 s s1 \ titlePaper (paper s PID) = titlePaper (paper s1 PID) \ abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \ contentPaper (paper s PID) = contentPaper (paper s1 PID) \ disPaper (paper s PID) = disPaper (paper s1 PID) \ decsPaper (paper s PID) = decsPaper (paper s1 PID)" using eqExcPID_N2_imp eeqExcPID_N2_RDD by auto lemma eqExcPID_N2_cong[simp, intro]: "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \confIDs := uu1\) (s1 \confIDs := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \conf := uu1\) (s1 \conf := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \userIDs := uu1\) (s1 \userIDs := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \pass := uu1\) (s1 \pass := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \user := uu1\) (s1 \user := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \roles := uu1\) (s1 \roles := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \paperIDs := uu1\) (s1 \paperIDs := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ eeqExcPID_N2 uu1 uu2 \ eqExcPID_N2 (s \paper := uu1\) (s1 \paper := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \pref := uu1\) (s1 \pref := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \voronkov := uu1\) (s1 \voronkov := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \news := uu1\) (s1 \news := uu2\)" "\ uu1 uu2. eqExcPID_N2 s s1 \ uu1 = uu2 \ eqExcPID_N2 (s \phase := uu1\) (s1 \phase := uu2\)" unfolding eqExcPID_N2_def by auto lemma eqExcPID_N2_Paper: assumes s's1': "eqExcPID_N2 s s1" and "paper s pid = Paper title abstract content reviews dis decs" and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1" shows "title = title1 \ abstract = abstract1 \ content = content1 \ dis = dis1 \ decs = decs1" using assms unfolding eqExcPID_N2_def apply (auto simp: eqExcD2 eeqExcPID_N2_def) by (metis titlePaper.simps abstractPaper.simps contentPaper.simps disPaper.simps decsPaper.simps)+ (* major *) lemma eqExcPID_N2_step: assumes ss1: "eqExcPID_N2 s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and s: "reach s" and r: "isRevNth s cid uid PID N" (* new *) shows "eqExcPID_N2 s' s1'" proof - note eqs = eqExcPID_N2_imp[OF ss1] note eqs' = eqExcPID_N2_imp1[OF ss1] have r: "N < length (reviewsPaper (paper s PID))" using s r by (metis isRevNth_less_length) have r1: "N < length (reviewsPaper (paper s1 PID))" using r eqs unfolding eeqExcPID_N2_def eqExcD2 eqExcNth2_def by simp note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_N2_def eeqExcPID_N2_def eqExcD2 eqExcNth2_def note * = step step1 eqs eqs' r r1 then show ?thesis proof (cases a) case (Cact x1) with * show ?thesis proof (cases x1) case (cReview x81 x82 x83 x84 x85) with Cact * show ?thesis by (clarsimp; metis (no_types, lifting) less_SucE nth_append_length right_cons_left) qed auto next case (Uact x2) with * show ?thesis proof (cases x2) case (uReview x71 x72 x73 x74 x75 x76) with Uact * show ?thesis by (clarsimp; metis (no_types, lifting) nth_list_update nth_list_update_neq) qed auto next case (UUact x3) with * show ?thesis proof (cases x3) case (uuReview x31 x32 x33 x34 x35 x36) with UUact * show ?thesis - by (clarsimp; smt list.sel(1) nth_list_update nth_list_update_neq) + by (clarsimp; smt (verit) list.sel(1) nth_list_update nth_list_update_neq) qed auto qed auto qed subsection \Value Setup\ fun \ :: "(state,act,out) trans \ bool" where "\ (Trans _ (Uact (uReview cid uid p pid n rc)) ou _) = (pid = PID \ n = N \ ou = outOK)" | "\ (Trans _ (UUact (uuReview cid uid p pid n rc)) ou _) = (pid = PID \ n = N \ ou = outOK)" | "\ _ = False" lemma \_def2: "\ (Trans s a ou s') = (ou = outOK \ (\ cid uid p rc. a = Uact (uReview cid uid p PID N rc) \ a = UUact (uuReview cid uid p PID N rc) ))" apply(cases a) subgoal by simp subgoal for x2 apply (cases x2, auto) . subgoal for x3 apply(cases x3, auto) . by simp_all lemma uReview_uuReview_step_eqExcPID_N: assumes a: "a = Uact (uReview cid uid p PID N rc) \ a = UUact (uuReview cid uid p PID N rc)" and "step s a = (ou,s')" shows "eqExcPID_N s s'" using assms unfolding eqExcPID_N_def eeqExcPID_N_def by (auto simp: u_defs uu_defs eqExcNth_def) lemma \_step_eqExcPID_N: assumes \: "\ (Trans s a ou s')" and s: "step s a = (ou,s')" shows "eqExcPID_N s s'" using \ uReview_uuReview_step_eqExcPID_N[OF _ s] unfolding \_def2 by blast (* major *) lemma eqExcPID_N_step: assumes s's1': "eqExcPID_N s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" shows "eqExcPID_N s' s1'" proof - note eqs = eqExcPID_N_imp[OF s's1'] note eqs' = eqExcPID_N_imp1[OF 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 eqExcNth_def note * = step step1 eqs eqs' then show ?thesis proof (cases a) case (Cact x1) with * show ?thesis proof (cases x1) case (cReview x81 x82 x83 x84 x85) with Cact * show ?thesis by (clarsimp; metis (no_types, lifting) less_SucE nth_append_length right_cons_left) qed auto next case (Uact x2) with * show ?thesis proof (cases x2) case (uReview x71 x72 x73 x74 x75 x76) with Uact * show ?thesis by (clarsimp; metis (no_types, lifting) nth_list_update nth_list_update_neq) qed auto next case (UUact x3) with * show ?thesis proof (cases x3) case (uuReview x31 x32 x33 x34 x35 x36) with UUact * show ?thesis by (clarsimp; metis (no_types, lifting) nth_list_update nth_list_update_neq) qed auto qed auto qed lemma eqExcPID_N_step_\_imp: assumes 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 "\ (Trans s1 a ou1 s1')" using assms unfolding \_def2 by (auto simp add: u_defs uu_defs eqExcPID_N_imp) lemma eqExcPID_N_step_\: assumes s's1': "eqExcPID_N s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" shows "\ (Trans s a ou s') = \ (Trans s1 a ou1 s1')" by (metis eqExcPID_N_step_\_imp eqExcPID_N_sym assms) lemma eqExcPID_N2_step_\_imp: assumes ss1: "eqExcPID_N2 s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and r: "N < length (reviewsPaper (paper s PID))" (* new *) and \: "\ (Trans s a ou s')" shows "\ (Trans s1 a ou1 s1')" using assms unfolding \_def2 by (auto simp add: u_defs uu_defs eqExcPID_N2_imp) (* More complex, roundabout proof than for other types of documents: *) lemma eqExcPID_N2_step_\: assumes s: "reach s" and s1: "reach s1" and ss1: "eqExcPID_N2 s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" shows "\ (Trans s a ou s') = \ (Trans s1 a ou1 s1')" proof(cases "\ cid uid. isRevNth s cid uid PID N") case False hence "\ \ (Trans s a ou s')" unfolding \_def2 using step by (auto simp add: u_defs uu_defs) (metis isRev_imp_isRevNth_getReviewIndex)+ moreover have "\ \ (Trans s1 a ou1 s1')" using step1 False unfolding \_def2 by (auto simp add: u_defs uu_defs) (metis eqExcPID_N2_def isRev_imp_isRevNth_getReviewIndex ss1)+ ultimately show ?thesis by auto next case True note r = True note eqs = eqExcPID_N2_imp[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_N2_def eqExcD2 eqExcNth2_def by simp thus ?thesis by (metis eqExcPID_N2_step_\_imp eqExcPID_N2_sym assms r) qed end diff --git a/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC.thy b/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC.thy --- a/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC.thy +++ b/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC.thy @@ -1,1142 +1,1142 @@ theory Reviewer_Assignment_NCPC imports "../Observation_Setup" Reviewer_Assignment_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning" begin subsection \Confidentiality protection from non-PC-members\ text \We verify the following property: \ \\ A group of users UIDs learn nothing about the reviewers assigned to a paper PID except for their number and the fact that they are PC members having no conflict with that paper unless/until 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. \ \\ \ 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)" term isAUT declare T.simps [simp del] (* The explanation of what this bound says is similar to that of the bound in Reviewer_Assignment_NCPC_Aut, just that the value vl' is additionally assumed to have the same length as vl (i.e., using the notations from that explanation, m = n). *) definition B :: "value list \ value list \ bool" where "B vl vl1 \ vl \ [] \ length vl = length vl1 \ 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)" using assms apply induct subgoal by (auto simp: istate_def) subgoal apply(intro conjI) apply (metis T.simps not_le_imp_less trans.collapse) by (metis T.simps isChair_isPC not_le_imp_less reachNT.Step reachNT_reach 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: "eqExcPID 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 eqExcPID_def using eqExcRLR_imp2 by fastforce have PID1: "PID \\ paperIDs s1 cid" using PID ss1 eqExcPID_imp by auto show ?thesis apply(rule T_\_\_stronger[OF s1 PID1 step1 \1]) using 1 by auto qed lemma notIsPCorConflict_eqExcPID_roles_eq: assumes s: "reach s" and s1: "reach s1" and PID: "PID \\ paperIDs s cid" and pc: "\ isPC s cid uid \ pref s uid PID = Conflict" and eeq: "eqExcPID s s1" shows "roles s cid uid = roles s1 cid uid" proof- have eq: "eqExcRLR (roles s cid uid) (roles s1 cid uid)" using eeq unfolding eqExcPID_def by auto have "\ isPC s1 cid uid \ pref s1 uid PID = Conflict" using pc eqExcPID_imp[OF eeq] eqExcRLR_imp2[OF eq] by auto hence "\ isRev s cid uid PID \ \ isRev s1 cid uid PID" using pc s s1 PID by (metis isRev_pref_notConflict_isPC) thus ?thesis using eq unfolding eqExcRLR_def by (metis Bex_set_list_ex filter_id_conv isRev_def) qed lemma notInPaperIDs_eqExcPID_roles_eq: assumes s: "reach s" and s1: "reach s1" and PID: "\ PID \\ paperIDs s cid" and eq: "eqExcPID s s1" shows "roles s cid uid = roles s1 cid uid" proof- have "\ PID \\ paperIDs s1 cid" using PID eq unfolding eqExcPID_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 eqExcPID_def eqExcRLR_def by (metis Bex_set_list_ex filter_True isRev_def) qed (* major *) lemma eqExcPID_step_out: assumes ss1: "eqExcPID s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and sT: "reachNT s" and s1: "reach s1" and PID: "PID \\ paperIDs s cid" and ph: "phase s cid \ revPH" and \: "\ \ (Trans s a ou s')" and \1: "\ \ (Trans s1 a ou1 s1')" and \: "\ \ a" 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': "eqExcPID s' s1'" using \ \ \1 eqExcPID_step eqExcPID_sym s s1 ss1 step step1 step_outErr_eq by (metis PID isAut_paperIDs notInPaperIDs_eqExcPID_roles_eq paperID_ex_userID1 paperID_ex_userID_def) have s1's': "eqExcPID s1' s'" by (metis eqExcPID_sym s's1') have s': "reach s'" by (metis reach_PairI s step) have ph1: "phase s1 cid \ revPH" using ph ss1 unfolding eqExcPID_def by auto have ph': "phase s' cid \ revPH" and ph1': "phase s1' cid \ revPH" using ph ph1 by (metis dual_order.trans phase_increases step step1)+ note Inv = reachNT_non_isPC_isChair[OF sT UIDs] note eqs = eqExcPID_imp[OF ss1] note eqs' = eqExcPID_imp1[OF ss1] note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_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 \ paperIDs_equals[OF s] Inv apply (auto simp add: isRev_getRevRole getRevRole_Some)[] apply (metis eqExcPID_imp' isRev_isPC not_less option.inject pref_Conflict_isRev role.distinct role.inject s1's' isRev_isPC not_less pref_Conflict_isRev simps2(1) simps2(8) isRev_getRevRole getRevRole_Some)+ done } note this[simp] have ?thesis using step step1 eqs eqs' s s1 UIDs PID \ \1 \ paperIDs_equals[OF s] Inv apply(cases a, simp_all only:) subgoal for x1 apply(cases x1) apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] . subgoal for x2 apply(cases x2) apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] . subgoal for x3 apply(cases x3) apply auto[] apply auto[] apply auto[] apply auto[] . subgoal for x4 apply(cases x4) apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply clarsimp apply (metis eqExcPID_imp2 not_less ph' s's1') apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] . subgoal for x5 apply(cases x5) apply auto[] apply auto[] apply auto[] apply clarsimp apply (metis (opaque_lifting) empty_iff list.set(1) notInPaperIDs_eqExcPID_roles_eq notIsPCorConflict_eqExcPID_roles_eq s's1' s1's') apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply auto[] apply clarsimp apply (metis Suc_leI filter_cong isRev_pref_notConflict_isPC not_less_eq_eq simps2(2)) apply clarsimp apply (metis not_less simps2(1)) . done note * = step step1 eqs eqs' s s1 UIDs PID \ \1 \ 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 (rReviews x91 x92 x93 x94) with Ract * show ?thesis by clarsimp (metis eqExcPID_imp2 not_less ph' s's1') qed auto next case (Lact x5) with * show ?thesis proof (cases x5) case (lMyConfs x41 x42) with Lact * show ?thesis by clarsimp (metis (opaque_lifting) empty_iff list.set(1) notInPaperIDs_eqExcPID_roles_eq notIsPCorConflict_eqExcPID_roles_eq s's1' s1's') next case (lMyAssignedPapers x111 x112 x113) with Lact * show ?thesis by clarsimp (metis Suc_leI filter_cong isRev_pref_notConflict_isPC not_less_eq_eq simps2(2)) next case (lAssignedReviewers x121 x122 x123 x124) with Lact * show ?thesis by clarsimp (metis not_less simps2(1)) qed auto qed qed lemma eqExcPID_step_\_eqExcPID_out: assumes s: "reach s" and s1: "reach s1" and a: "a = Cact (cReview cid uid p PID uid')" and a1: "a1 = Cact (cReview cid uid p PID uid1')" and ss1: "eqExcPID s s1" and step: "step s a = (outOK,s')" and pc: "isPC s cid uid1' \ pref s uid1' PID \ Conflict" and rv1: "\ isRev s1 cid uid1' PID" and step1: "step s1 a1 = (ou1,s1')" shows "eqExcPID s' s1' \ ou1 = outOK" proof- have s': "reach s'" and s1': "reach s1'" by (metis reach_PairI s s1 step step1)+ have c: "isChair s cid uid \ pref s uid PID \ Conflict \ phase s cid = revPH \ pass s uid = p \ PID \\ paperIDs s cid \ cid \\ confIDs s" using step unfolding a by (auto simp: c_defs) hence c1: "isChair s1 cid uid \ pref s1 uid PID \ Conflict \ phase s1 cid = revPH \ pass s1 uid = p \ PID \\ paperIDs s1 cid \ cid \\ confIDs s1" and pc1: "isPC s1 cid uid1' \ pref s1 uid1' PID \ Conflict" using pc ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by metis+ note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_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 show ?thesis using pc1 c1 ss1 step step1 c c1 pc rv1 unfolding eqExcPID_def a a1 using roles_userIDs s1' by force qed lemma eqExcPID_ex_isNthReview: assumes s: "reach s" and s1: "reach s1" and e: "eqExcPID s s1" and i: "isRevNth s cid uid PID n" shows "\ uid1. isRevNth s1 cid uid1 PID n" proof- have PID: "PID \\ paperIDs s cid" by (metis i isRevNth_paperIDs s) have "n < length (reviewsPaper (paper s PID))" using s i by (metis isRevNth_less_length) hence "PID \\ paperIDs s1 cid \ n < length (reviewsPaper (paper s1 PID))" using e PID unfolding eqExcPID_def by auto thus ?thesis using s1 by (metis reviews_compact) qed lemma eqExcPID_step_\1: assumes s: "reach s" and s1: "reach s1" and a: "a = Uact (uReview cid uid p PID n rc)" and ss1: "eqExcPID s s1" and step: "step s a = (outOK,s')" shows "\ s1' uid1 p. isRevNth s1 cid uid1 PID n \ step s1 (Uact (uReview cid uid1 p PID n rc)) = (outOK,s1') \ eqExcPID s' s1'" proof- have s': "reach s'" by (metis reach_PairI s step) have c: "isRevNth s cid uid PID n \ phase s cid = revPH \ PID \\ paperIDs s cid \ cid \\ confIDs s" using step unfolding a apply (auto simp: u_defs) by (metis isRev_imp_isRevNth_getReviewIndex) obtain uid1 where rv1: "isRevNth s1 cid uid1 PID n" using s s1 ss1 by (metis c eqExcPID_ex_isNthReview) let ?p = "pass s1 uid1" define a1 where a1: "a1 \ Uact (uReview cid uid1 (pass s1 uid1) PID n rc)" obtain ou1 s1' where step1: "step s1 a1 = (ou1,s1')" by (metis surj_pair) have s1': "reach s1'" by (metis reach_PairI s1 step1) have c1: "phase s1 cid = revPH \ PID \\ paperIDs s1 cid \ cid \\ confIDs s1" using ss1 c unfolding eqExcPID_def using eqExcRLR_imp2 by auto show ?thesis apply(intro exI[of _ s1'] exI[of _ uid1] exI[of _ ?p]) using rv1 c1 ss1 step step1 c c1 rv1 unfolding eqExcPID_def a a1 using isRevNth_getReviewIndex isRev_def2 roles_userIDs s1' by ((auto simp: u_defs simp: Paper_dest_conv simp: eqExcPID_def )) qed lemma eqExcPID_step_\2: assumes s: "reach s" and s1: "reach s1" and a: "a = UUact (uuReview cid uid p PID n rc)" and ss1: "eqExcPID s s1" and step: "step s a = (outOK,s')" shows "\ s1' uid1 p. isRevNth s1 cid uid1 PID n \ step s1 (UUact (uuReview cid uid1 p PID n rc)) = (outOK,s1') \ eqExcPID s' s1'" proof- have s': "reach s'" by (metis reach_PairI s step) have c: "isRevNth s cid uid PID n \ phase s cid = disPH \ PID \\ paperIDs s cid \ cid \\ confIDs s" using step unfolding a apply (auto simp: uu_defs) by (metis isRev_imp_isRevNth_getReviewIndex) obtain uid1 where rv1: "isRevNth s1 cid uid1 PID n" using s s1 ss1 by (metis c eqExcPID_ex_isNthReview) let ?p = "pass s1 uid1" define a1 where a1: "a1 \ UUact (uuReview cid uid1 (pass s1 uid1) PID n rc)" obtain ou1 s1' where step1: "step s1 a1 = (ou1,s1')" by (metis surj_pair) have s1': "reach s1'" by (metis reach_PairI s1 step1) have c1: "phase s1 cid = disPH \ PID \\ paperIDs s1 cid \ cid \\ confIDs s1" using ss1 c unfolding eqExcPID_def using eqExcRLR_imp2 by auto show ?thesis apply(intro exI[of _ s1'] exI[of _ uid1] exI[of _ ?p]) using rv1 c1 ss1 step step1 c c1 rv1 unfolding eqExcPID_def a a1 using isRevNth_getReviewIndex isRev_def2 roles_userIDs s1' by ((force simp: uu_defs simp: Paper_dest_conv simp: eqExcPID_def )) 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 \ eqExcPID s s1 \ length vl = length vl1 \ 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 \ eqExcPID s s1 \ vl1 = []" definition \e :: "state \ value list \ state \ value list \ bool" where "\e s vl s1 vl1 \ vl \ [] \ ( (\ cid. PID \\ paperIDs s cid \ phase s cid \ 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 l: "length vl = length 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 l 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' l 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' l 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' l 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 not_\_isRev_isPC_persists: assumes "reach s" "PID \\ paperIDs s cid" and "\ \ (Trans s a ou s')" and "step s a = (ou,s')" shows "isRev s' cid uid PID = isRev s cid uid PID \ isPC s' cid uid = isPC s cid uid" using assms apply(cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs isRev_def2 roles_confIDs paperIDs_confIDs) apply (metis Suc_n_not_le_n paperIDs_geq_subPH)+ . subgoal for x2 apply(cases x2,auto simp: u_defs isRev_def2) . subgoal for x3 apply(cases x3,auto simp: uu_defs isRev_def2) . by auto lemma \_not\_eqButPID_outErr: assumes sT: "reachNT s" and s1: "reach s1" and UIDs: "userOfA a \ UIDs" and step: "step s a = (outErr,s')" (* and \: "\ \ a" *) and ss1: "eqExcPID s s1" and PID: "PID \\ paperIDs s CID" shows "step s1 a = (outErr,s1)" proof- have s: "reach s" by (metis reachNT_reach sT) have step: "step s a = (outErr,s)" using step by (metis step_outErr_eq) note Inv = reachNT_non_isPC_isChair[OF sT UIDs] note eqs = eqExcPID_imp[OF ss1] note eqs' = eqExcPID_imp1[OF ss1] have PID1: "PID \\ paperIDs s1 CID" using ss1 PID unfolding eqExcPID_def by auto note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def note simps2[simp] = eqExcRLR_imp[of s _ _ _ s1, OF s] eqExcRLR_imp2[of s _ _ s1] eqExcRLR_set[of "(roles s cid uid)" "(roles s1 cid uid)" for cid uid] foo2 foo3 eqExcRLR_imp_isRevRole_imp note * = step eqs eqs' s s1 UIDs (* \ *) PID PID1 paperIDs_equals[OF s] Inv show ?thesis proof (cases a) case (Cact x1) with * show ?thesis by (cases x1; auto; metis less_irrefl_nat simps2(1)) next case (Uact x2) with * show ?thesis by (cases x2; auto; metis isRev_pref_notConflict_isPC less_irrefl_nat simps2(1)) next case (UUact x3) with * show ?thesis by (cases x3; auto; metis eqs isRev_isPC less_Suc_eq less_irrefl_nat pref_Conflict_isRev simps2(1)) next case (Ract x4) with * show ?thesis by (cases x4; auto; metis isRev_isPC not_less pref_Conflict_isRev s1 simps2(1)) next case (Lact x5) with * show ?thesis by (cases x5; auto) qed qed lemma exists_failedAct: "\ a. step s a = (outErr,s) \ userOfA a = uid" proof- obtain p where p: "pass s uid = Password p" by (cases "pass s uid") let ?a = "Cact (cConf undefined uid (Password (fresh {p} p)) undefined undefined)" show ?thesis apply(rule exI[of _ ?a]) using p fresh_notIn[of "{p}" p] by(auto simp: c_defs) 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 uidc where uidc: "isChair s CID uidc \ pref s uidc PID \ Conflict" and rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _") and ss1: "eqExcPID s s1" and PID: "PID \\ paperIDs s CID" and dis: "distinct (map fst vl1)" and l: "length vl = length 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 uidc_notin: "uidc \ UIDs" using less_not_refl3 reachNT_non_isPC_isChair rsT by fastforce note vl1_all = dis fst_isPC fst_isRev snd_isPC have PID1: "PID \\ paperIDs s1 CID" using PID ss1 unfolding eqExcPID_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 uidc': "isChair s' CID uidc \ pref s' uidc PID \ Conflict" using uidc step rs ph PID isChair_persistent revPH_pref_persists[OF rs PID ] by auto show "match ?\ s s1 vl1 a ou s' vl' \ ignore ?\ s s1 vl1 a ou s' vl'" (is "?match \ ?ignore") proof(cases "\ ?trn") case False note \ = False have vl': "vl' = vl" using c \ unfolding consume_def by (cases vl) auto obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust) let ?trn1 = "Trans s1 a ou1 s1'" show ?thesis proof(cases "ou = outErr") case True note ou = True have s': "s' = s" by (metis ou step step_outErr_eq) show ?thesis proof (cases "userOfA a \ UIDs") case True note uidUIDs = True hence ou1: "ou1 = outErr" using \_not\_eqButPID_outErr by (metis PID Pair_inject ou rs1 rsT ss1 step step1) hence s1': "s1' = s1" by (metis step1 step_outErr_eq) have \1: "\ \ ?trn1" unfolding \_def2 ou1 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" by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" unfolding ou ou1 by simp next show "?\ s' vl' s1' vl1" unfolding s' s1' vl' by (metis \\2 s vl s1 vl1\) qed thus ?thesis by simp next case False note uidUIDs = False obtain a1 where ua1: "userOfA a1 = userOfA a" and step1: "step s1 a1 = (outErr,s1)" by (metis exists_failedAct ou) let ?trn1 = "Trans s1 a1 outErr s1" have ?match proof show "validTrans ?trn1" using step1 by simp next show "consume ?trn1 vl1 vl1" unfolding consume_def \_def2 ou by auto next show "\ ?trn = \ ?trn1" by (simp add: ua1) next assume "\ ?trn" thus "g ?trn = g ?trn1" using uidUIDs unfolding ou by simp next show "?\ s' vl' s1 vl1" unfolding s' vl' by (metis \\2 s vl s1 vl1\) qed thus ?thesis by simp qed next case False note ou = False show ?thesis proof(cases "\ a") case False note \ = False have s's1': "eqExcPID s' s1'" using eqExcPID_step rs rs1 ss1 step step1 PID \ \ ou by blast have \1: "\ \ ?trn1" using \ using non_eqExcPID_step_\_imp rs rs1 ss1 PID step step1 ou by auto have out: "userOfA a \ UIDs \ ou1 = ou" using eqExcPID_step_out[OF ss1 step step1 rsT rs1 PID _ \ \1 \] ph 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 out by simp next show "?\ s' vl' s1' vl1" proof(cases "phase s' CID = revPH") case True hence "\2 s' vl' s1' vl1" using uidc' PID' s's1' vl1_all l unfolding \2_def vl' apply(intro exI[of _ CID] exI[of _ uidc]) apply simp apply(intro conjI) using isPC_persistent[OF _ step] revPH_pref_persists[OF rs PID _ step] ph not_\_isRev_isPC_persists[OF rs1 PID1 \1 step1] revPH_pref_persists[OF rs PID _ step] not_\_isRev_isPC_persists[OF rs PID \ step] ph by auto thus "?\ s' vl' s1' vl1" by simp next case False hence ph': "phase s' CID > revPH" using rs step ph by (metis antisym_conv2 phase_increases) show ?thesis proof(cases "vl = []") case True hence "vl1 = []" using l by simp hence "\3 s' vl' s1' vl1" using uidc' PID' s's1' ph' unfolding \3_def vl' by auto thus ?thesis by simp next case False hence "\e s' vl' s1' vl1" using PID' ph' unfolding \e_def vl' by auto thus ?thesis by simp qed qed qed thus ?thesis by simp next case True thus ?thesis unfolding \_def2 proof(elim exE disjE) fix cid uid p n rc assume a: "a = Uact (uReview cid uid p PID n rc)" hence ou: "ou = outOK" using step ou unfolding a by (auto simp: u_defs) obtain s1' uid1 p where uid1: "isRevNth s1 cid uid1 PID n" and step1: "step s1 (Uact (uReview cid uid1 p PID n rc)) = (outOK,s1')" (is "step _ ?a1 = _") and s's1': "eqExcPID s' s1'" using eqExcPID_step_\1 rs rs1 a ss1 step ou by metis let ?trn1 = "Trans s1 ?a1 outOK s1'" have \1: "\ \ ?trn1" by simp have "isPC s cid uid \ pref s uid PID \ Conflict" using step unfolding a ou apply(auto simp: u_defs) by (metis isRev_pref_notConflict_isPC rs)+ hence uidUIDs: "\ uid \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis PID PID1 isRevNth_paperIDs less_irrefl_nat paperIDs_equals rs1 uid1) have "isPC s1 cid uid1 \ pref s1 uid1 PID \ Conflict" using step1 apply(auto simp: u_defs) by (metis isRev_pref_notConflict_isPC rs1)+ hence "isPC s cid uid1 \ pref s uid1 PID \ Conflict" using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by fastforce hence uid1UIDs: "\ uid1 \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) have ph': "phase s' CID = revPH" using ph step unfolding a by (auto simp: u_defs) 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" using uidUIDs uid1UIDs unfolding a by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" using uidUIDs unfolding a by simp next have "\2 s' vl' s1' vl1" using ph' PID' s's1' unfolding \2_def vl' apply(intro exI[of _ CID] exI[of _ uidc]) using l vl1_all using isPC_persistent[OF _ step] revPH_pref_persists[OF rs PID _ step] ph not_\_isRev_isPC_persists[OF rs1 PID1 \1 step1] revPH_pref_persists[OF rs PID _ step] not_\_isRev_isPC_persists[OF rs PID \ step] ph uidc' by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp next fix cid uid p n rc assume a: "a = UUact (uuReview cid uid p PID n rc)" hence ou: "ou = outOK" using step ou unfolding a by (auto simp: uu_defs) obtain s1' uid1 p where uid1: "isRevNth s1 cid uid1 PID n" and step1: "step s1 (UUact (uuReview cid uid1 p PID n rc)) = (outOK,s1')" (is "step _ ?a1 = _") and s's1': "eqExcPID s' s1'" using eqExcPID_step_\2 rs rs1 a ss1 step ou by metis let ?trn1 = "Trans s1 ?a1 outOK s1'" have \1: "\ \ ?trn1" by simp have "isPC s cid uid \ pref s uid PID \ Conflict" using step unfolding a ou apply(auto simp: uu_defs) by (metis isRev_pref_notConflict_isPC rs)+ hence uidUIDs: "\ uid \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) have "isPC s1 cid uid1 \ pref s1 uid1 PID \ Conflict" using step1 apply(auto simp: uu_defs) by (metis isRev_pref_notConflict_isPC rs1)+ hence "isPC s cid uid1 \ pref s uid1 PID \ Conflict" using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by fastforce hence uid1UIDs: "\ uid1 \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) have ph': "phase s' CID = revPH" using ph step unfolding a by (auto simp: uu_defs) 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" using uidUIDs uid1UIDs unfolding a by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" using uidUIDs unfolding a by simp next have "\2 s' vl' s1' vl1" using ph' PID' s's1' unfolding \2_def vl' apply(intro exI[of _ CID] exI[of _ uidc]) using l vl1_all using isPC_persistent[OF _ step] revPH_pref_persists[OF rs PID _ step] ph not_\_isRev_isPC_persists[OF rs1 PID1 \1 step1] revPH_pref_persists[OF rs PID _ step] not_\_isRev_isPC_persists[OF rs PID \ step] ph uidc' by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp qed qed qed next case True note \ = True then obtain cid uid p uid' where a: "a = Cact (cReview cid uid p PID uid')" (* have ua: "userOfA a \ UIDs" by (metis \ T_\_\ \.simps rsT step) *) and ou: "ou = outOK" unfolding \_def2 by auto have cid: "cid = CID" using step unfolding a ou apply(auto simp: c_defs) by (metis PID paperIDs_equals rs) obtain v vll' where "vl = v # vll'" using \ c unfolding consume_def by (cases vl) auto hence vl: "vl = v # vl'" by (metis \ c consume_def list.sel(2-3)) obtain v1 vl1' where vl1: "vl1 = v1 # vl1'" using l vl by (cases vl1) auto obtain uid1' where v1: "v1 = (uid1', {uid1'. isPC s CID uid1' \ pref s uid1' PID \ Conflict})" using snd_isPC unfolding vl1 by(cases v1) auto hence uid1': "isPC s CID uid1' \ pref s uid1' PID \ Conflict" and uid1'1: "\ isRev s1 CID uid1' PID" using fst_isPC fst_isRev unfolding vl1 by auto have uid: "isChair s CID uid \ pref s uid PID \ Conflict" using step unfolding a ou cid by (auto simp: c_defs) have uid1: "isChair s1 CID uid \ pref s1 uid PID \ Conflict" using ss1 uid unfolding eqExcPID_def using eqExcRLR_imp2 by metis have uuid1': "isPC s1 CID uid1' \ pref s1 uid1' PID \ Conflict" using uid1' ss1 unfolding eqExcPID_def apply auto by (metis eqExcRLR_imp2) obtain a1 where a1: "a1 = Cact (cReview CID uid p PID uid1')" by blast obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')" by (metis prod.exhaust) have ph1: "phase s1 CID = revPH" using ss1 ph unfolding eqExcPID_def by auto let ?trn1 = "Trans s1 a1 ou1 s1'" have s's1': "eqExcPID s' s1'" and ou1: "ou1 = outOK" using eqExcPID_step_\_eqExcPID_out[OF rs rs1 a[unfolded cid] a1 ss1 step[unfolded ou] uid1' uid1'1 step1] by auto hence many_s1': "PID \\ paperIDs s1' CID" "isChair s1' CID uid \ pref s1' uid PID \ Conflict" "phase s1' CID = revPH" "pass s1' uid = pass s1 uid" "isPC s1' CID uid1' \ pref s1' uid1' PID \ Conflict" subgoal by (metis PID1 paperIDs_mono step1) subgoal by (metis (no_types, lifting) PID1 Suc_leI eqExcPID_def isChair_persistent lessI ph revPH_pref_persists rs1 ss1 step1 uid1) subgoal using step1 ph1 unfolding a1 by (fastforce simp: c_defs) subgoal using step1 ph1 unfolding a1 by (fastforce simp: c_defs) subgoal by (metis (no_types, lifting) PID1 Suc_leI eqExcPID_def isPC_persistent lessI ph revPH_pref_persists rs1 ss1 step1 uuid1') done hence more_s1': "uid \\ userIDs s1'" "CID \\ confIDs s1'" by (metis paperIDs_confIDs reach_PairI roles_userIDs rs1 step1 many_s1'(1))+ have \1: "\ ?trn1" unfolding a1 ou1 \_def2 by auto have f1: "f ?trn1 = v1" unfolding a1 v1 apply simp using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by (metis eqExcRLR_set isRevRoleFor.simps(3)) have rs1': "reach s1'" using rs1 step1 by (auto intro: reach_PairI) have ph': "phase s' CID = revPH" using step ph unfolding a by(auto simp: c_defs) have ?match proof show "validTrans ?trn1" using step1 by simp next show "consume ?trn1 vl1 vl1'" unfolding consume_def vl1 using \1 f1 by auto next show "\ ?trn = \ ?trn1" unfolding a a1 by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" by (metis \ T_\_\ \.simps rsT step) next have 0: "{uid'. isPC s' CID uid' \ pref s' uid' PID \ Conflict} = {uid'. isPC s CID uid' \ pref s uid' PID \ Conflict}" using step rs ph unfolding a ou by (auto simp: c_defs) have 1: "{uid'. isRev s1' CID uid' PID} \ {uid'. isRev s1 CID uid' PID} \ {uid1'}" using step1 unfolding a1 ou1 by (auto simp: c_defs isRev_def2) have 2: "fst ` set vl1' \ fst ` set vl1 - {uid1'}" using dis unfolding vl1 apply simp unfolding image_set unfolding v1 by simp have 3: "fst ` set vl1' \ {uid'. isRev s1' CID uid' PID} = {}" using 1 2 vl1_all(3) by blast have "\2 s' vl' s1' vl1'" unfolding \2_def apply(intro exI[of _ CID] exI[of _ uidc]) using l vl1_all unfolding vl1 vl apply simp using PID' ph' uidc' s's1' apply simp unfolding 0 using 3 by simp thus "?\ s' vl' s1' vl1'" by simp qed thus ?thesis by simp qed qed thus ?thesis using l by (metis length_0_conv) 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: "eqExcPID s s1" and vl1: "vl1 = []" using reachNT_reach unfolding \3_def by auto have PID1: "PID \\ paperIDs s1 CID" by (metis PID eqExcPID_sym isAut_paperIDs notInPaperIDs_eqExcPID_roles_eq paperID_ex_userID rs rs1 ss1) 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) have \: "\ \ ?trn" using step ph unfolding \_def2 apply(auto simp: c_defs) using PID paperIDs_equals rs by force have vl': "vl' = vl" using c \ unfolding consume_def by (cases vl) auto show "match ?\ s s1 vl1 a ou s' vl' \ ignore ?\ s s1 vl1 a ou s' vl'" (is "?match \ ?ignore") proof(cases "\ a") case True thus ?thesis unfolding \_def2 proof(elim exE disjE) fix cid uid p n rc assume a: "a = Uact (uReview cid uid p PID n rc)" show ?thesis proof(cases "ou = outErr") case True note ou = True hence s's: "s' = s" by (metis step step_outErr_eq) show ?thesis proof(cases "uid \ UIDs") case True note uidUIDs = True obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust) let ?trn1 = "Trans s1 a ou1 s1'" have "isPC s CID uid \ pref s uid PID = Conflict" using reachNT_non_isPC_isChair[OF rsT uidUIDs] ph PID by force hence 1: "isPC s1 CID uid \ pref s1 uid PID = Conflict" using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by fastforce have ou1: "ou1 = outErr" using step1 uidUIDs unfolding a apply(auto simp: u_defs) apply(cases "cid = CID", auto) apply (metis 1 isRev_isPC isRev_pref_notConflict rs1) by (metis rs1 PID1 paperIDs_equals) have s1's1: "s1' = s1" by (metis ou ou1 step step1 step_outErr_eq) have \1: "\ \ ?trn1" using \ unfolding eqExcPID_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" unfolding ou ou1 by simp next have "\3 s' vl' s1' vl1" using ph' PID' ss1 unfolding \3_def s's s1's1 vl1 by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp next case False note uidUIDs = False have ?ignore proof show "\ \ ?trn" using uidUIDs unfolding a by auto next have "\3 s' vl' s1 vl1" using ph' PID' ss1 unfolding \3_def s's vl1 by auto thus "?\ s' vl' s1 vl1" by simp qed thus ?thesis by simp qed next case False hence ou: "ou = outOK" using step unfolding a by (auto simp: u_defs) obtain s1' uid1 p where uid1: "isRevNth s1 cid uid1 PID n" and step1: "step s1 (Uact (uReview cid uid1 p PID n rc)) = (outOK,s1')" (is "step _ ?a1 = _") and s's1': "eqExcPID s' s1'" using eqExcPID_step_\1 rs rs1 a ss1 step ou by metis let ?trn1 = "Trans s1 ?a1 outOK s1'" have \1: "\ \ ?trn1" by simp have "isPC s cid uid \ pref s uid PID \ Conflict" using step unfolding a ou apply(auto simp: u_defs) by (metis isRev_pref_notConflict_isPC rs)+ hence uidUIDs: "\ uid \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) have "isPC s1 cid uid1 \ pref s1 uid1 PID \ Conflict" using step1 apply(auto simp: u_defs) by (metis isRev_pref_notConflict_isPC rs1)+ hence "isPC s cid uid1 \ pref s uid1 PID \ Conflict" using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by fastforce hence uid1UIDs: "\ uid1 \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) 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" using uidUIDs uid1UIDs unfolding a by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" using uidUIDs unfolding a by simp next have "\3 s' vl' s1' vl1" using ph' PID' s's1' unfolding \3_def vl1 by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp qed next fix cid uid p n rc assume a: "a = UUact (uuReview cid uid p PID n rc)" show ?thesis proof(cases "ou = outErr") case True note ou = True hence s's: "s' = s" by (metis step step_outErr_eq) show ?thesis proof(cases "uid \ UIDs") case True note uidUIDs = True obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust) let ?trn1 = "Trans s1 a ou1 s1'" have "isPC s CID uid \ pref s uid PID = Conflict" using reachNT_non_isPC_isChair[OF rsT uidUIDs] ph PID by force hence 1: "isPC s1 CID uid \ pref s1 uid PID = Conflict" using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by fastforce have ou1: "ou1 = outErr" using step1 uidUIDs unfolding a apply(auto simp: uu_defs) apply(cases "cid = CID", auto) apply (metis 1 isRev_isPC isRev_pref_notConflict rs1) by (metis rs1 PID1 paperIDs_equals) have s1's1: "s1' = s1" by (metis ou ou1 step step1 step_outErr_eq) have \1: "\ \ ?trn1" using \ unfolding eqExcPID_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" unfolding ou ou1 by simp next have "\3 s' vl' s1' vl1" using ph' PID' ss1 unfolding \3_def s's s1's1 vl1 by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp next case False note uidUIDs = False have ?ignore proof show "\ \ ?trn" using uidUIDs unfolding a by auto next have "\3 s' vl' s1 vl1" using ph' PID' ss1 unfolding \3_def s's vl1 by auto thus "?\ s' vl' s1 vl1" by simp qed thus ?thesis by simp qed next case False hence ou: "ou = outOK" using step unfolding a by (auto simp: u_defs) obtain s1' uid1 p where uid1: "isRevNth s1 cid uid1 PID n" and step1: "step s1 (UUact (uuReview cid uid1 p PID n rc)) = (outOK,s1')" (is "step _ ?a1 = _") and s's1': "eqExcPID s' s1'" using eqExcPID_step_\2 rs rs1 a ss1 step ou by metis let ?trn1 = "Trans s1 ?a1 outOK s1'" have \1: "\ \ ?trn1" by simp have "isPC s cid uid \ pref s uid PID \ Conflict" using step unfolding a ou apply(auto simp: uu_defs) by (metis isRev_pref_notConflict_isPC rs)+ hence uidUIDs: "\ uid \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) have "isPC s1 cid uid1 \ pref s1 uid1 PID \ Conflict" using step1 apply(auto simp: uu_defs) by (metis isRev_pref_notConflict_isPC rs1)+ hence "isPC s cid uid1 \ pref s uid1 PID \ Conflict" using ss1 unfolding eqExcPID_def using eqExcRLR_imp2 by fastforce hence uid1UIDs: "\ uid1 \ UIDs" using ph reachNT_non_isPC_isChair[OF rsT] apply auto by (metis (no_types, opaque_lifting) eqExcPID_def isRevNth_geq_revPH isRevNth_paperIDs not_le rs1 ss1 uid1) 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" using uidUIDs uid1UIDs unfolding a by simp next assume "\ ?trn" thus "g ?trn = g ?trn1" using uidUIDs unfolding a by simp next have "\3 s' vl' s1' vl1" using ph' PID' s's1' unfolding \3_def vl1 by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp qed qed next case False note \ = False obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust) let ?trn1 = "Trans s1 a ou1 s1'" have \1: "\ \ ?trn1" using \ unfolding eqExcPID_step_\[OF rs rs1 ss1 PID ph step step1] . have out: "userOfA a \ UIDs \ ou1 = ou" using eqExcPID_step_out[OF ss1 step step1 rsT rs1 PID _ \ \1 \] ph by auto have s's1': "eqExcPID s' s1'" using eqExcPID_step rs rs1 ss1 step step1 PID ph \ \ 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 out by simp next have "\3 s' vl' s1' vl1" using ph' PID' s's1' unfolding \3_def vl1 by auto thus "?\ s' vl' s1' vl1" by simp qed thus ?thesis by simp qed qed thus ?thesis using vl1 by simp qed qed (* Exit arguments: *) definition K1exit where "K1exit cid s \ PID \\ paperIDs s cid \ phase s cid \ 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) apply (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 Collect_cong le_trans paperIDs_mono phase_increases revPH_isPC_constant revPH_pref_constant) +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) apply (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 reachNT_reach paperIDs_equals 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 diff --git a/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC_Aut.thy b/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC_Aut.thy --- a/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC_Aut.thy +++ b/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_NCPC_Aut.thy @@ -1,724 +1,724 @@ 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 Suc_le_lessD eqExcRLR_imp filter_cong isRev_pref_notConflict_isPC not_less_eq) + 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 Collect_cong le_trans paperIDs_mono phase_increases revPH_isPC_constant revPH_pref_constant) +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 diff --git a/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_Value_Setup.thy b/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_Value_Setup.thy --- a/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_Value_Setup.thy +++ b/thys/CoCon/Reviewer_Assignment_Confidentiality/Reviewer_Assignment_Value_Setup.thy @@ -1,695 +1,695 @@ (* The value setup for reviewer confidentiality *) theory Reviewer_Assignment_Value_Setup imports Reviewer_Assignment_Intro begin subsection \Preliminaries\ declare updates_commute_paper[simp] consts PID :: paperID (* Equality of two role lists everywhere except on their PID reviewer roles *) definition eqExcRLR :: "role list \ role list \ bool" where "eqExcRLR rl rl1 \ [r \ rl . \ isRevRoleFor PID r] = [r \ rl1 . \ isRevRoleFor PID r]" lemma eqExcRLR_set: assumes 1: "eqExcRLR rl rl1" and 2: "\ isRevRoleFor PID r" shows "r \\ rl \ r \\ rl1" proof- have "set ([r\rl . \ isRevRoleFor PID r]) = set ([r\rl1 . \ isRevRoleFor PID r])" using 1 unfolding eqExcRLR_def by auto thus ?thesis using 2 unfolding set_filter by auto qed lemmas eqExcRLR = eqExcRLR_def lemma eqExcRLR_eq[simp,intro!]: "eqExcRLR rl rl" unfolding eqExcRLR by auto lemma eqExcRLR_sym: assumes "eqExcRLR rl rl1" shows "eqExcRLR rl1 rl" using assms unfolding eqExcRLR by auto lemma eqExcRLR_trans: assumes "eqExcRLR rl rl1" and "eqExcRLR rl1 rl2" shows "eqExcRLR rl rl2" using assms unfolding eqExcRLR by auto lemma eqExcRLR_imp: assumes s: "reach s" and pid: "pid \ PID" and 1: "eqExcRLR (roles s cid uid) (roles s1 cid uid)" shows "isRevNth s cid uid pid = isRevNth s1 cid uid pid \ isRev s cid uid pid = isRev s1 cid uid pid \ getRevRole s cid uid pid = getRevRole s1 cid uid pid \ getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid" (is "?A \ ?B \ ?C \ ?D") proof(intro conjI) show A: ?A apply(rule ext) using 1 by (metis eqExcRLR_set isRevRoleFor.simps(1) pid) show B: ?B using A unfolding isRev_def2 by auto show C: ?C apply(cases "isRev s cid uid pid") subgoal by (metis A B getRevRole_Some_Rev_isRevNth isRevNth_equals isRev_getRevRole2 s) by (metis B Bex_set_list_ex find_None_iff getRevRole_def isRev_def) show D: ?D unfolding getReviewIndex_def using C by auto qed lemma eqExcRLR_imp2: assumes "eqExcRLR (roles s cid uid) (roles s1 cid uid)" shows "isPC s cid uid = isPC s1 cid uid \ isChair s cid uid = isChair s1 cid uid \ isAut s cid uid = isAut s1 cid uid" by (metis (opaque_lifting, no_types) assms eqExcRLR_set isRevRoleFor.simps) (* fixme: move where belong *) lemma filter_eq_imp: assumes "\ x. P x \ Q x" and "filter Q xs = filter Q ys" shows "filter P xs = filter P ys" using assms filter_filter proof- have "filter P xs = filter P (filter Q xs)" unfolding filter_filter using assms by metis also have "... = filter P (filter Q ys)" using assms by simp also have "... = filter P ys" unfolding filter_filter using assms by metis finally show ?thesis . qed lemma arg_cong3: "a = a1 \ b = b1 \ c = c1 \ h a b c = h a1 b1 c1" by auto lemmas map_concat_cong1 = arg_cong[where f = concat, OF arg_cong2[where f = map, OF _ refl]] lemmas If_cong1 = arg_cong3[where h = If, OF _ refl refl] lemma diff_cong1: "a = a1 \ (a \ b) = (a1 \ b)" by auto lemma isRev_pref_notConflict: assumes "reach s" and "isRev s cid uid pid" shows "pref s uid pid \ Conflict" by (metis assms pref_Conflict_isRev) lemma isRev_pref_notConflict_isPC: assumes "reach s" and "isRev s cid uid pid" shows "pref s uid pid \ Conflict \ isPC s cid uid" by (metis assms(1) assms(2) isRev_isPC isRev_pref_notConflict) lemma eqExcRLR_imp_isRevRole_imp: assumes "eqExcRLR rl rl1" shows "[r\ rl. \ isRevRole r] = [r\ rl1 . \ isRevRole r]" using assms filter_eq_imp unfolding eqExcRLR_def by (metis isRevRole.simps(1) isRevRoleFor.elims(2)) lemma notIsPC_eqExLRL_roles_eq: assumes s: "reach s" and s1: "reach s1" and PID: "PID \\ paperIDs s cid" and pc: "\ isPC s cid uid" and eq: "eqExcRLR (roles s cid uid) (roles (s1::state) cid uid)" shows "roles s cid uid = roles s1 cid uid" proof- have "\ isPC s1 cid uid" using pc eqExcRLR_imp2[OF eq] by auto hence "\ isRev s cid uid PID \ \ isRev s1 cid uid PID" using pc s s1 PID by (metis isRev_pref_notConflict_isPC) thus ?thesis using eq unfolding eqExcRLR_def by (metis Bex_set_list_ex filter_id_conv isRev_def) qed lemma foo1: "P a \ [r\List.insert a l . P r] = (if a\set l then filter P l else a#filter P l)" by (metis filter.simps(2) in_set_insert not_in_set_insert) lemma foo2: "\eqExcRLR rl rl'; \ isRevRoleFor PID x\ \ eqExcRLR (List.insert x rl) (List.insert x rl')" unfolding eqExcRLR_def apply (auto simp: foo1) [] apply (metis eqExcRLR_def eqExcRLR_set isRevRoleFor.simps)+ done lemma foo3: assumes "eqExcRLR rl rl'" "isRevRoleFor PID x" shows "eqExcRLR (List.insert x rl) (rl')" and "eqExcRLR (rl) (List.insert x rl')" using assms unfolding eqExcRLR_def by (auto simp: List.insert_def) text \The notion of two states being equal everywhere except on the reviewer roles for PID:\ definition eqExcPID :: "state \ state \ bool" where "eqExcPID s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ (\ cid uid. eqExcRLR (roles s cid uid) (roles s1 cid uid)) \ paperIDs s = paperIDs s1 \ paper s = paper s1 \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1" lemma eqExcPID_eq[simp,intro!]: "eqExcPID s s" unfolding eqExcPID_def by auto lemma eqExcPID_sym: assumes "eqExcPID s s1" shows "eqExcPID s1 s" using assms eqExcRLR_sym unfolding eqExcPID_def by auto lemma eqExcPID_trans: assumes "eqExcPID s s1" and "eqExcPID s1 s2" shows "eqExcPID s s2" using assms eqExcRLR_trans unfolding eqExcPID_def by metis (* Implications from eqExcPID, including w.r.t. auxiliary operations: *) lemma eqExcPID_imp: "eqExcPID s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ eqExcRLR (roles s cid uid) (roles s1 cid uid) \ paperIDs s = paperIDs s1 \ paper s = paper s1 \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1 \ getAllPaperIDs s = getAllPaperIDs s1" unfolding eqExcPID_def eqExcRLR_def getAllPaperIDs_def by auto (* does not work well with simp: *) lemma eqExcPID_imp': assumes s: "reach s" and ss1: "eqExcPID s s1" and pid: "pid \ PID \ PID \ pid" shows "isRev s cid uid pid = isRev s1 cid uid pid \ getRevRole s cid uid pid = getRevRole s1 cid uid pid \ getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid" proof- have 1: "eqExcRLR (roles s cid uid) (roles s1 cid uid)" using eqExcPID_imp[OF ss1] by auto show ?thesis proof (intro conjI) show 3: "isRev s cid uid pid = isRev s1 cid uid pid" by (metis "1" eqExcRLR_imp pid s) show 4: "getRevRole s cid uid pid = getRevRole s1 cid uid pid" by (metis "1" eqExcRLR_imp pid s) show "getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid" unfolding getReviewIndex_def using 4 by auto qed qed lemma eqExcPID_imp1: "eqExcPID s s1 \ pid \ PID \ PID \ pid \ getNthReview s pid n = getNthReview s1 pid n" unfolding eqExcPID_def getNthReview_def by auto lemma eqExcPID_imp2: assumes "reach s" and "eqExcPID s s1" and "pid \ PID \ PID \ pid" shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid" proof- have "(\uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])" apply(rule ext) using assms using assms by (auto simp add: eqExcPID_imp' eqExcPID_imp1) thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID_imp) qed lemma eqExcPID_imp3: "reach s \ eqExcPID s s1 \ pid \ PID \ PID \ pid \ getNthReview s pid = getNthReview s1 pid" unfolding eqExcPID_def apply auto apply (rule ext) by (metis getNthReview_def) lemma eqExcPID_cong[simp, intro]: "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \confIDs := uu1\) (s1 \confIDs := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \conf := uu1\) (s1 \conf := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \userIDs := uu1\) (s1 \userIDs := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \pass := uu1\) (s1 \pass := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \user := uu1\) (s1 \user := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \roles := uu1\) (s1 \roles := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \paperIDs := uu1\) (s1 \paperIDs := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \paper := uu1\) (s1 \paper := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \pref := uu1\) (s1 \pref := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \voronkov := uu1\) (s1 \voronkov := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \news := uu1\) (s1 \news := uu2\)" "\ uu1 uu2. eqExcPID s s1 \ uu1 = uu2 \ eqExcPID (s \phase := uu1\) (s1 \phase := uu2\)" unfolding eqExcPID_def by auto text \A slightly weaker state equivalence that allows differences in the reviews of paper \<^term>\PID\. It is used for the confidentiality property that doesn't cover the authors of that paper in the notification phase (when the authors will learn the contents of the reviews).\ (* Equality of two papers everywhere except on their reviews *) fun eqExcR :: "paper \ paper \ bool" where "eqExcR (Paper name info ct reviews dis decs) (Paper name1 info1 ct1 reviews1 dis1 decs1) = (name = name1 \ info = info1 \ ct = ct1 \ dis = dis1 \ decs = decs1)" lemma eqExcR: "eqExcR pap pap1 = (titlePaper pap = titlePaper pap1 \ abstractPaper pap = abstractPaper pap1 \ contentPaper pap = contentPaper pap1 \ disPaper pap = disPaper pap1 \ decsPaper pap = decsPaper pap1)" by(cases pap, cases pap1, auto) lemma eqExcR_eq[simp,intro!]: "eqExcR pap pap" unfolding eqExcR by auto lemma eqExcR_sym: assumes "eqExcR pap pap1" shows "eqExcR pap1 pap" using assms unfolding eqExcR by auto lemma eqExcR_trans: assumes "eqExcR pap pap1" and "eqExcR pap1 pap2" shows "eqExcR pap pap2" using assms unfolding eqExcR by auto (* Auxiliary notion: *) definition eeqExcPID where "eeqExcPID paps paps1 \ \ pid. if pid = PID then eqExcR (paps pid) (paps1 pid) else paps pid = paps1 pid" lemma eeqExcPID_eeq[simp,intro!]: "eeqExcPID s s" unfolding eeqExcPID_def by auto lemma eeqExcPID_sym: assumes "eeqExcPID s s1" shows "eeqExcPID s1 s" using assms eqExcR_sym unfolding eeqExcPID_def by auto lemma eeqExcPID_trans: assumes "eeqExcPID s s1" and "eeqExcPID s1 s2" shows "eeqExcPID s s2" using assms eqExcR_trans unfolding eeqExcPID_def by simp blast lemma eeqExcPID_imp: "eeqExcPID paps paps1 \ eqExcR (paps PID) (paps1 PID)" "\eeqExcPID paps paps1; pid \ PID\ \ paps pid = paps1 pid" unfolding eeqExcPID_def by auto lemma eeqExcPID_cong: assumes "eeqExcPID paps paps1" and "pid = PID \ eqExcR uu uu1" and "pid \ PID \ uu = uu1" shows "eeqExcPID (paps (pid := uu)) (paps1(pid := uu1))" using assms unfolding eeqExcPID_def by auto lemma eeqExcPID_RDD: "eeqExcPID paps paps1 \ titlePaper (paps PID) = titlePaper (paps1 PID) \ abstractPaper (paps PID) = abstractPaper (paps1 PID) \ contentPaper (paps PID) = contentPaper (paps1 PID) \ disPaper (paps PID) = disPaper (paps1 PID) \ decsPaper (paps PID) = decsPaper (paps1 PID)" using eeqExcPID_def unfolding eqExcR by auto (* The notion of two states being equal everywhere except on the the reviews of PID and on the reviewer roles for PID *) definition eqExcPID2 :: "state \ state \ bool" where "eqExcPID2 s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ (\ cid uid. eqExcRLR (roles s cid uid) (roles s1 cid uid)) \ paperIDs s = paperIDs s1 \ eeqExcPID (paper s) (paper s1) \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1" lemma eqExcPID2_eq[simp,intro!]: "eqExcPID2 s s" unfolding eqExcPID2_def by auto lemma eqExcPID2_sym: assumes "eqExcPID2 s s1" shows "eqExcPID2 s1 s" using assms eeqExcPID_sym eqExcRLR_sym unfolding eqExcPID2_def by auto lemma eqExcPID2_trans: assumes "eqExcPID2 s s1" and "eqExcPID2 s1 s2" shows "eqExcPID2 s s2" using assms eeqExcPID_trans eqExcRLR_trans unfolding eqExcPID2_def by metis (* Implications from eqExcPID2, including w.r.t. auxiliary operations: *) lemma eqExcPID2_imp: "eqExcPID2 s s1 \ confIDs s = confIDs s1 \ conf s = conf s1 \ userIDs s = userIDs s1 \ pass s = pass s1 \ user s = user s1 \ eqExcRLR (roles s cid uid) (roles s1 cid uid) \ paperIDs s = paperIDs s1 \ eeqExcPID (paper s) (paper s1) \ pref s = pref s1 \ voronkov s = voronkov s1 \ news s = news s1 \ phase s = phase s1 \ getAllPaperIDs s = getAllPaperIDs s1" unfolding eqExcPID2_def eqExcRLR_def getAllPaperIDs_def by auto lemma eeqExcPID_imp2: assumes pid: "pid \ PID" and 1: "eeqExcPID (paper s) (paper s1)" shows "reviewsPaper (paper s pid) = reviewsPaper (paper s1 pid)" by (metis "1" eeqExcPID_imp(2) pid) (* does not work well with simp: *) lemma eqExcPID2_imp': assumes s: "reach s" and ss1: "eqExcPID2 s s1" and pid: "pid \ PID \ PID \ pid" shows "isRev s cid uid pid = isRev s1 cid uid pid \ getRevRole s cid uid pid = getRevRole s1 cid uid pid \ getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid \ reviewsPaper (paper s pid) = reviewsPaper (paper s1 pid)" proof- have 1: "eqExcRLR (roles s cid uid) (roles s1 cid uid)" and 2: "eeqExcPID (paper s) (paper s1)" using eqExcPID2_imp[OF ss1] by auto show ?thesis proof (intro conjI) show 3: "isRev s cid uid pid = isRev s1 cid uid pid" by (metis "1" eqExcRLR_imp pid s) show 4: "getRevRole s cid uid pid = getRevRole s1 cid uid pid" by (metis "1" eqExcRLR_imp pid s) show "getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid" unfolding getReviewIndex_def using 4 by auto show "reviewsPaper (paper s pid) = reviewsPaper (paper s1 pid)" using pid 2 unfolding eeqExcPID_def by auto qed qed lemma eqExcPID2_imp1: "eqExcPID2 s s1 \ eqExcR (paper s pid) (paper s1 pid)" "eqExcPID2 s s1 \ pid \ PID \ PID \ pid \ paper s pid = paper s1 pid \ getNthReview s pid n = getNthReview s1 pid n" unfolding eqExcPID2_def eeqExcPID_def getNthReview_def apply auto by (metis eqExcR_eq) lemma eqExcPID2_imp2: assumes "reach s" and "eqExcPID2 s s1" and "pid \ PID \ PID \ pid" shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid" proof- have "(\uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])" apply(rule ext) using assms using assms by (auto simp add: eqExcPID2_imp' eqExcPID2_imp1) thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID2_imp) qed lemma eqExcPID2_imp3: "reach s \ eqExcPID2 s s1 \ pid \ PID \ PID \ pid \ getNthReview s pid = getNthReview s1 pid" unfolding eqExcPID2_def apply auto apply (rule ext) by (metis eeqExcPID_imp getNthReview_def) lemma eqExcPID2_RDD: "eqExcPID2 s s1 \ titlePaper (paper s PID) = titlePaper (paper s1 PID) \ abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \ contentPaper (paper s PID) = contentPaper (paper s1 PID) \ disPaper (paper s PID) = disPaper (paper s1 PID) \ decsPaper (paper s PID) = decsPaper (paper s1 PID)" using eqExcPID2_imp eeqExcPID_RDD by auto lemma eqExcPID2_cong[simp, intro]: "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \confIDs := uu1\) (s1 \confIDs := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \conf := uu1\) (s1 \conf := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \userIDs := uu1\) (s1 \userIDs := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \pass := uu1\) (s1 \pass := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \user := uu1\) (s1 \user := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \roles := uu1\) (s1 \roles := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \paperIDs := uu1\) (s1 \paperIDs := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ eeqExcPID uu1 uu2 \ eqExcPID2 (s \paper := uu1\) (s1 \paper := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \pref := uu1\) (s1 \pref := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \voronkov := uu1\) (s1 \voronkov := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \news := uu1\) (s1 \news := uu2\)" "\ uu1 uu2. eqExcPID2 s s1 \ uu1 = uu2 \ eqExcPID2 (s \phase := uu1\) (s1 \phase := uu2\)" unfolding eqExcPID2_def by auto lemma eqExcPID2_Paper: assumes s's1': "eqExcPID2 s s1" and "paper s pid = Paper title abstract content reviews dis decs" and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1" shows "title = title1 \ abstract = abstract1 \ content = content1 \ dis = dis1 \ decs = decs1" using assms unfolding eqExcPID2_def apply (auto simp: eqExcR eeqExcPID_def) by (metis titlePaper.simps abstractPaper.simps contentPaper.simps disPaper.simps decsPaper.simps)+ lemma cReview_step_eqExcPID2: assumes a: "a = Cact (cReview cid uid p PID uid')" and "step s a = (ou,s')" shows "eqExcPID2 s s'" using assms unfolding eqExcPID2_def eeqExcPID_def eqExcRLR_def apply (auto simp: c_defs) -unfolding List.insert_def by (smt filter.simps(2) isRevRoleFor.simps(1)) +unfolding List.insert_def by (smt (verit) filter.simps(2) isRevRoleFor.simps(1)) subsection \Value Setup\ type_synonym "value" = "userID \ userID set" fun \ :: "(state,act,out) trans \ bool" where "\ (Trans _ (Cact (cReview cid uid p pid uid')) ou _) = (pid = PID \ ou = outOK)" | "\ _ = False" fun f :: "(state,act,out) trans \ value" where "f (Trans s (Cact (cReview cid uid p pid uid')) _ s') = (uid', {uid'. isPC s cid uid' \ pref s uid' PID \ Conflict})" lemma \_def2: "\ (Trans s a ou s') = (ou = outOK \ (\ cid uid p uid'. a = Cact (cReview cid uid p PID uid')))" apply(cases a, simp_all) subgoal for x1 by (cases x1, auto) . fun \ :: "act \ bool" where "\ (Uact (uReview cid uid p pid n rc)) = (pid = PID)" | "\ (UUact (uuReview cid uid p pid n rc)) = (pid = PID)" | "\ _ = False" lemma \_def2: "\ a = (\ cid uid p n rc. a = Uact (uReview cid uid p PID n rc) \ a = UUact (uuReview cid uid p PID n rc))" apply(cases a, simp_all) subgoal for x2 apply (cases x2, auto) . subgoal for x3 by (cases x3, auto) . lemma eqExcPID_step_\_imp: assumes s: "reach s" and ss1: "eqExcPID s s1" (* new compared to the other properties: *) and PID: "PID \\ paperIDs s cid" and ph: "phase s cid > revPH" (* end new *) and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and \: "\ \ (Trans s a ou s')" shows "\ \ (Trans s1 a ou1 s1')" using assms unfolding \_def2 apply (auto simp add: c_defs eqExcPID_imp) unfolding eqExcPID_def apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2) apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2) using eqExcRLR_imp[OF s] PID by (metis less_not_refl paperIDs_equals) lemma eqExcPID_step_\: assumes "reach s" and "reach s1" and ss1: "eqExcPID s s1" (* new compared to the other properties: *) and PID: "PID \\ paperIDs s cid" and ph: "phase s cid > revPH" (* end new *) and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" shows "\ (Trans s a ou s') = \ (Trans s1 a ou1 s1')" proof- have "PID \\ paperIDs s1 cid \ phase s1 cid > revPH" using eqExcPID_imp[OF ss1] PID ph by auto thus ?thesis by (metis eqExcPID_step_\_imp eqExcPID_sym assms) qed (* new lemma compared to the other properties: *) lemma non_eqExcPID_step_\_imp: assumes s: "reach s" and ss1: "eqExcPID s s1" and PID: "PID \\ paperIDs s cid" and ou: "ou \ outErr" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and \: "\ \ (Trans s a ou s')" shows "\ \ (Trans s1 a ou1 s1')" using assms unfolding \_def2 by (auto simp add: c_defs eqExcPID_imp) (* major *) lemma eqExcPID_step: assumes s: "reach s" and s1: "reach s1" and ss1: "eqExcPID s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and PID: "PID \\ paperIDs s cid" and ou_ph: "ou \ outErr \ phase s cid > revPH" and \: "\ \ (Trans s a ou s')" and \: "\ \ a" shows "eqExcPID s' s1'" proof - have s': "reach s'" by (metis reach_PairI s step) note eqs = eqExcPID_imp[OF ss1] note eqs' = eqExcPID_imp1[OF ss1] note eqss = eqExcPID_imp'[OF s ss1] note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def note simps2[simp] = eqExcRLR_imp2[where s=s and ?s1.0 = s1'] eqExcRLR_imp2[where s=s' and ?s1.0 = s1] eqExcRLR_set[of "(roles s cid uid)" "(roles s1' cid uid)" for uid cid] eqExcRLR_set[of "(roles s' cid uid)" "(roles s1 cid uid)" for uid cid] foo2 foo3 eqExcRLR_imp[OF s, where ?s1.0=s1'] eqExcRLR_imp[OF s', where ?s1.0=s1] note * = step step1 eqs eqs' \ \ PID ou_ph then show ?thesis proof (cases a) case (Cact x1) with * show ?thesis proof (cases x1) case (cReview x81 x82 x83 x84 x85) with Cact * show ?thesis by clarsimp (metis less_irrefl_nat paperIDs_equals s1 simps2(9)) qed auto next case (Uact x2) with * show ?thesis proof (cases x2) case (uReview x71 x72 x73 x74 x75 x76) with Uact * show ?thesis by (clarsimp simp del: simps2) auto qed auto next case (UUact x3) with * show ?thesis proof (cases x3) case (uuReview x31 x32 x33 x34 x35 x36) with UUact * show ?thesis by (clarsimp simp del: simps2) auto qed auto qed auto qed lemma \_step_eqExcPID2: assumes \: "\ (Trans s a ou s')" and s: "step s a = (ou,s')" shows "eqExcPID2 s s'" using \ cReview_step_eqExcPID2[OF _ s] unfolding \_def2 by blast (* major *) lemma eqExcPID2_step: assumes s: "reach s" and ss1: "eqExcPID2 s s1" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and PID: "PID \\ paperIDs s cid" and ph: "phase s cid \ revPH" and \: "\ \ (Trans s a ou s')" shows "eqExcPID2 s' s1'" proof - have s': "reach s'" by (metis reach_PairI s step) note eqs = eqExcPID2_imp[OF ss1] (* note eqss = eqExcPID2_imp'[OF s ss1] *) note eqs' = eqExcPID2_imp1[OF ss1] note eqss = eqExcPID2_imp'[OF s ss1] note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID2_def eeqExcPID_def eqExcR note simps2[simp] = eqExcRLR_imp2[where s=s and ?s1.0 = s1'] eqExcRLR_imp2[where s=s' and ?s1.0 = 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] foo2 foo3 eqExcRLR_imp[OF s, where ?s1.0=s1'] eqExcRLR_imp[OF s', where ?s1.0=s1] note * = step step1 eqs eqs' ph PID \ then show ?thesis proof (cases a) case (Cact x1) with * show ?thesis proof (cases x1) case (cReview x81 x82 x83 x84 x85) with Cact * show ?thesis by clarsimp (metis simps2(9)) qed auto next case (Uact x2) with * show ?thesis proof (cases x2) case (uReview x71 x72 x73 x74 x75 x76) with Uact * show ?thesis by (clarsimp simp del: simps2) auto qed auto next case (UUact x3) with * show ?thesis proof (cases x3) case (uuReview x31 x32 x33 x34 x35 x36) with UUact * show ?thesis by (clarsimp simp del: simps2) auto qed auto next case (Lact x5) with * show ?thesis by (cases x5; auto) qed auto qed lemma eqExcPID2_step_\_imp: assumes s: "reach s" and ss1: "eqExcPID2 s s1" (* new compared to the other properties: *) and PID: "PID \\ paperIDs s cid" and ph: "phase s cid > revPH" (* end new *) and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and \: "\ \ (Trans s a ou s')" shows "\ \ (Trans s1 a ou1 s1')" using assms unfolding \_def2 apply (auto simp add: c_defs eqExcPID2_imp) unfolding eqExcPID2_def apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2) apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2) using eqExcRLR_imp[OF s] PID by (metis less_not_refl paperIDs_equals) lemma eqExcPID2_step_\: assumes "reach s" and "reach s1" and ss1: "eqExcPID2 s s1" (* new compared to the other properties: *) and PID: "PID \\ paperIDs s cid" and ph: "phase s cid > revPH" (* end new *) and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" shows "\ (Trans s a ou s') = \ (Trans s1 a ou1 s1')" proof- have "PID \\ paperIDs s1 cid \ phase s1 cid > revPH" using eqExcPID2_imp[OF ss1] PID ph by auto thus ?thesis by (metis eqExcPID2_step_\_imp eqExcPID2_sym assms) qed (* new lemma compared to the other properties: *) lemma non_eqExcPID2_step_\_imp: assumes s: "reach s" and ss1: "eqExcPID2 s s1" and PID: "PID \\ paperIDs s cid" and ou: "ou \ outErr" and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')" and \: "\ \ (Trans s a ou s')" shows "\ \ (Trans s1 a ou1 s1')" using assms unfolding \_def2 by (auto simp add: c_defs eqExcPID2_imp) end diff --git a/thys/CoCon/Safety_Properties.thy b/thys/CoCon/Safety_Properties.thy --- a/thys/CoCon/Safety_Properties.thy +++ b/thys/CoCon/Safety_Properties.thy @@ -1,1339 +1,1339 @@ section \Safety properties\ (* Verification of safety properties *) theory Safety_Properties imports Automation_Setup "Bounded_Deducibility_Security.IO_Automaton" begin (* Note that the safety properties are only concerned with the step actions (creation, update and u-update) and their action on the state; they have nothing to do with the observation actions. *) interpretation IO_Automaton where istate = istate and step = step done subsection \Infrastructure for invariance reasoning\ definition cIsInvar :: "(state \ bool) \ bool" where "cIsInvar \ \ \ s ca. reach s \ \ s \ \ (snd (cStep s ca))" definition uIsInvar :: "(state \ bool) \ bool" where "uIsInvar \ \ \ s ua. reach s \ \ s \ \ (snd (uStep s ua))" definition uuIsInvar :: "(state \ bool) \ bool" where "uuIsInvar \ \ \ s uua. reach s \ \ s \ \ (snd (uuStep s uua))" (* for properties on states, of course the observations do not count: *) lemma invar_cIsInvar_uIsInvar_uuIsInvar: "invar \ \ cIsInvar \ \ uIsInvar \ \ uuIsInvar \" (is "?L \ ?R") unfolding invar_def cIsInvar_def uIsInvar_def uuIsInvar_def fun_eq_iff apply standard apply (metis snd_eqD step.simps) apply safe subgoal for _ a apply(cases a, auto) . done lemma cIsInvar[case_names cUser cConf cPC cChair cPaper cAuthor cConflict cReview]: assumes "\s uID p name info email. \reach s; \ s; e_createUser s uID p name info email\ \ \ (createUser s uID p name info email)" and "\s confID uID p name info. \reach s; \ s; e_createConf s confID uID p name info\ \ \ (createConf s confID uID p name info)" and "\s confID uID p uID'. \reach s; \ s; e_createPC s confID uID p uID'\ \ \ (createPC s confID uID p uID')" and "\s confID uID p uID'. \reach s; \ s; e_createChair s confID uID p uID'\ \ \ (createChair s confID uID p uID')" and "\s confID uID p papID name info. \reach s; \ s; e_createPaper s confID uID p papID name info\ \ \ (createPaper s confID uID p papID name info)" and "\s confID uID p papID uID'. \reach s; \ s; e_createAuthor s confID uID p papID uID'\ \ \ (createAuthor s confID uID p papID uID')" and "\s confID uID p papID uID'. \reach s; \ s; e_createConflict s confID uID p papID uID'\ \ \ (createConflict s confID uID p papID uID')" and "\s confID uID p papID uID'. \reach s; \ s; e_createReview s confID uID p papID uID'\ \ \ (createReview s confID uID p papID uID')" shows "cIsInvar \" unfolding cIsInvar_def apply safe subgoal for _ ca using assms by (cases ca, auto) . lemma uIsInvar[case_names uUser uConfA uNextPhase uPaperTA uPaperC uPref uReview]: assumes "\s uID p p' name info email. \reach s; \ s; e_updateUser s uID p p' name info email\ \ \ (updateUser s uID p p' name info email)" and "\s confID uID p. \reach s; \ s; e_updateConfA s confID uID p\ \ \ (updateConfA s confID uID p)" and "\s confID uID p ph. \reach s; \ s; e_updatePhase s confID uID p ph\ \ \ (updatePhase s confID uID p ph)" and "\s confID uID p paperID name info. \reach s; \ s; e_updatePaperTA s confID uID p paperID name info\ \ \ (updatePaperTA s confID uID p paperID name info)" and "\s confID uID p paperID pc. \reach s; \ s; e_updatePaperC s confID uID p paperID pc\ \ \ (updatePaperC s confID uID p paperID pc)" and "\s confID uID p paperID preference. \reach s; \ s; e_updatePref s confID uID p paperID preference\ \ \ (updatePref s confID uID p paperID preference)" and "\s confID uID p paperID n rc. \reach s; \ s; e_updateReview s confID uID p paperID n rc\ \ \ (updateReview s confID uID p paperID n rc)" and "\s confID uID p paperID fpc. \reach s; \ s; e_updateFPaperC s confID uID p paperID fpc\ \ \ (updateFPaperC s confID uID p paperID fpc)" shows "uIsInvar \" unfolding uIsInvar_def apply safe using assms subgoal for _ ua by (cases ua, auto) . lemma uuIsInvar[case_names uuNews uuDis uuReview uuDec]: assumes "\s confID uID p comm. \reach s; \ s; e_uupdateNews s confID uID p comm\ \ \ (uupdateNews s confID uID p comm)" and "\s confID uID p paperID comm. \reach s; \ s; e_uupdateDis s confID uID p paperID comm\ \ \ (uupdateDis s confID uID p paperID comm)" and "\s confID uID p paperID n rc. \reach s; \ s; e_uupdateReview s confID uID p paperID n rc\ \ \ (uupdateReview s confID uID p paperID n rc)" and "\s confID uID p paperID decision. \reach s; \ s; e_uupdateDec s confID uID p paperID decision\ \ \ (uupdateDec s confID uID p paperID decision)" shows "uuIsInvar \" unfolding uuIsInvar_def apply safe subgoal for _ uua using assms by (cases uua, auto) . subsection \Safety proofs\ (* Simplification and splitting setup: *) declare option.splits[split] paper.splits[split] discussion.splits[split] role.splits[split] Let_def[simp] list_all_iff[simp] list_ex_iff[simp] fun_upd2_def[simp] IDsOK_def[simp] if_splits[split] fun papIDsOfRole where "papIDsOfRole (Aut papID) = [papID]" | "papIDsOfRole (Rev papID n) = [papID]" | "papIDsOfRole _ = []" (* The phase is always \ closedPH: *) definition phase_leq_closedPH :: "state \ bool" where "phase_leq_closedPH s \ \ confID. phase s confID \ closedPH" lemma holdsIstate_phase_leq_closedPH: "holdsIstate phase_leq_closedPH" unfolding IO_Automaton.holdsIstate_def istate_def phase_leq_closedPH_def by auto lemma cIsInvar_phase_leq_closedPH: "cIsInvar phase_leq_closedPH" apply (cases phase_leq_closedPH rule: cIsInvar) by (auto simp: c_defs phase_leq_closedPH_def) lemma uIsInvar_phase_leq_closedPH: "uIsInvar phase_leq_closedPH" apply (cases phase_leq_closedPH rule: uIsInvar) by (auto simp: u_defs phase_leq_closedPH_def) lemma uuIsInvar_phase_leq_closedPH: "uuIsInvar phase_leq_closedPH" apply (cases phase_leq_closedPH rule: uuIsInvar) by (auto simp: uu_defs phase_leq_closedPH_def) lemma invar_phase_leq_closedPH: "invar phase_leq_closedPH" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_phase_leq_closedPH uIsInvar_phase_leq_closedPH uuIsInvar_phase_leq_closedPH by auto lemmas phase_leq_closedPH1 = holdsIstate_invar[OF holdsIstate_phase_leq_closedPH invar_phase_leq_closedPH] theorem phase_leq_closedPH: assumes a: "reach s" shows "phase s confID \ closedPH" using phase_leq_closedPH1[OF a] unfolding phase_leq_closedPH_def by auto (* A conference ID exsists if its phase is > noPH: *) definition geq_noPH_confIDs :: "state \ bool" where "geq_noPH_confIDs s \ \ confID. phase s confID > noPH \ confID \\ confIDs s" lemma holdsIstate_geq_noPH_confIDs: "holdsIstate geq_noPH_confIDs" unfolding IO_Automaton.holdsIstate_def istate_def istate_def geq_noPH_confIDs_def by auto lemma cIsInvar_geq_noPH_confIDs: "cIsInvar geq_noPH_confIDs" apply (cases geq_noPH_confIDs rule: cIsInvar) by (auto simp: c_defs geq_noPH_confIDs_def) lemma uIsInvar_geq_noPH_confIDs: "uIsInvar geq_noPH_confIDs" apply (cases geq_noPH_confIDs rule: uIsInvar) by (auto simp: u_defs geq_noPH_confIDs_def) lemma uuIsInvar_geq_noPH_confIDs: "uuIsInvar geq_noPH_confIDs" apply (cases geq_noPH_confIDs rule: uuIsInvar) by (auto simp: uu_defs geq_noPH_confIDs_def) lemma invar_geq_noPH_confIDs: "invar geq_noPH_confIDs" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_geq_noPH_confIDs uIsInvar_geq_noPH_confIDs uuIsInvar_geq_noPH_confIDs by auto lemmas geq_noPH_confIDs1 = holdsIstate_invar[OF holdsIstate_geq_noPH_confIDs invar_geq_noPH_confIDs] theorem geq_noPH_confIDs: assumes a: "reach s" shows "phase s confID > noPH \ confID \\ confIDs s" using geq_noPH_confIDs1[OF a] unfolding geq_noPH_confIDs_def by auto (* All the IDs involved in the "roles" relation are valid IDs of the system: *) definition roles_IDsOK :: "state \ bool" where "roles_IDsOK s \ \ confID uID rl. rl \\ roles s confID uID \ IDsOK s [confID] [uID] (papIDsOfRole rl)" lemma holdsIstate_roles_IDsOK: "holdsIstate roles_IDsOK" unfolding IO_Automaton.holdsIstate_def istate_def istate_def roles_IDsOK_def by auto lemma cIsInvar_roles_IDsOK: "cIsInvar roles_IDsOK" apply (cases roles_IDsOK rule: cIsInvar) by (auto simp: c_defs roles_IDsOK_def) lemma uIsInvar_roles_IDsOK: "uIsInvar roles_IDsOK" apply (cases roles_IDsOK rule: uIsInvar) by (auto simp: u_defs roles_IDsOK_def) lemma uuIsInvar_roles_IDsOK: "uuIsInvar roles_IDsOK" apply (cases roles_IDsOK rule: uuIsInvar) by (auto simp: uu_defs roles_IDsOK_def) lemma invar_roles_IDsOK: "invar roles_IDsOK" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_roles_IDsOK uIsInvar_roles_IDsOK uuIsInvar_roles_IDsOK by auto lemmas roles_IDsOK1 = holdsIstate_invar[OF holdsIstate_roles_IDsOK invar_roles_IDsOK] theorem roles_IDsOK: assumes a: "reach s" and rl: "rl \\ roles s confID uID" shows "IDsOK s [confID] [uID] (papIDsOfRole rl)" using roles_IDsOK1[OF a] rl unfolding roles_IDsOK_def by auto corollary roles_confIDs: assumes a: "reach s" and A: "rl \\ roles s confID uID" shows "confID \\ confIDs s" using roles_IDsOK[OF a] A unfolding IDsOK_def by auto corollary roles_userIDs: assumes a: "reach s" and A: "rl \\ roles s confID uID" shows "uID \\ userIDs s" using roles_IDsOK[OF a] A unfolding IDsOK_def by auto corollary isAut_paperIDs: assumes a: "reach s" and A: "isAut s confID uID papID" shows "papID \\ paperIDs s confID" using roles_IDsOK[OF a] A unfolding IDsOK_def by auto corollary isRevNth_paperIDs: assumes a: "reach s" and A: "isRevNth s confID uID papID n" shows "papID \\ paperIDs s confID" using roles_IDsOK[OF a] A unfolding IDsOK_def by auto corollary isRev_paperIDs: assumes a: "reach s" and A: "isRev s confID uID papID" shows "papID \\ paperIDs s confID" using isRevNth_paperIDs[OF a] A unfolding isRev_def2 by auto corollary isRev_userIDs: assumes a: "reach s" and A: "isRev s confID uID papID" shows "uID \\ userIDs s" using roles_userIDs[OF a] A unfolding isRev_def2 by auto corollary isRev_confIDs: assumes a: "reach s" and A: "isRev s confID uID papID" shows "confID \\ confIDs s" using roles_confIDs[OF a] A unfolding isRev_def2 by auto (* The lists of (conference, user and paper) IDs are non-repetitive *) definition distinct_IDs :: "state \ bool" where "distinct_IDs s \ distinct (confIDs s) \ distinct (userIDs s) \ (\ confID. distinct (paperIDs s confID))" lemma holdsIstate_distinct_IDs: "holdsIstate distinct_IDs" unfolding IO_Automaton.holdsIstate_def istate_def istate_def distinct_IDs_def by auto lemma cIsInvar_distinct_IDs: "cIsInvar distinct_IDs" apply (cases distinct_IDs rule: cIsInvar) by (auto simp: c_defs distinct_IDs_def getAllPaperIDs_def) lemma uIsInvar_distinct_IDs: "uIsInvar distinct_IDs" apply (cases distinct_IDs rule: uIsInvar) by (auto simp: u_defs distinct_IDs_def) lemma uuIsInvar_distinct_IDs: "uuIsInvar distinct_IDs" apply (cases distinct_IDs rule: uuIsInvar) by (auto simp: uu_defs distinct_IDs_def) lemma invar_distinct_IDs: "invar distinct_IDs" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_distinct_IDs uIsInvar_distinct_IDs uuIsInvar_distinct_IDs by auto lemmas distinct_IDs1 = holdsIstate_invar[OF holdsIstate_distinct_IDs invar_distinct_IDs] theorem distinct_IDs: assumes a: "reach s" shows "distinct (confIDs s) \ distinct (userIDs s) \ (\ confID. distinct (paperIDs s confID))" using distinct_IDs1[OF a] unfolding distinct_IDs_def by auto lemmas distinct_confIDs = distinct_IDs[THEN conjunct1] lemmas distinct_userIDs = distinct_IDs[THEN conjunct2, THEN conjunct1] lemmas distinct_paperIDs = distinct_IDs[THEN conjunct2, THEN conjunct2, rule_format] (* The list of roles of a user at a conference is non-repetitive *) definition distinct_roles :: "state \ bool" where "distinct_roles s \ \ confID uID. distinct (roles s confID uID)" lemma holdsIstate_distinct_roles: "holdsIstate distinct_roles" unfolding IO_Automaton.holdsIstate_def istate_def istate_def distinct_roles_def by auto lemma cIsInvar_distinct_roles: "cIsInvar distinct_roles" apply (cases distinct_roles rule: cIsInvar) by (auto simp: c_defs distinct_roles_def) lemma uIsInvar_distinct_roles: "uIsInvar distinct_roles" apply (cases distinct_roles rule: uIsInvar) by (auto simp: u_defs distinct_roles_def) lemma uuIsInvar_distinct_roles: "uuIsInvar distinct_roles" apply (cases distinct_roles rule: uuIsInvar) by (auto simp: uu_defs distinct_roles_def) lemma invar_distinct_roles: "invar distinct_roles" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_distinct_roles uIsInvar_distinct_roles uuIsInvar_distinct_roles by auto lemmas distinct_roles1 = holdsIstate_invar[OF holdsIstate_distinct_roles invar_distinct_roles] theorem distinct_roles: assumes a: "reach s" shows "distinct (roles s confID uID)" using distinct_roles1[OF a] unfolding distinct_roles_def by auto (* Only committee members become reviewers: *) definition isRevNth_isPC :: "state \ bool" where "isRevNth_isPC s \ \ confID uID papID n. isRevNth s confID uID papID n \ isPC s confID uID" lemma holdsIstate_isRevNth_isPC: "holdsIstate isRevNth_isPC" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isRevNth_isPC_def by auto lemma cIsInvar_isRevNth_isPC: "cIsInvar isRevNth_isPC" apply (cases isRevNth_isPC rule: cIsInvar) by (auto simp: c_defs isRevNth_isPC_def) lemma uIsInvar_isRevNth_isPC: "uIsInvar isRevNth_isPC" apply (cases isRevNth_isPC rule: uIsInvar) by (auto simp: u_defs isRevNth_isPC_def) lemma uuIsInvar_isRevNth_isPC: "uuIsInvar isRevNth_isPC" apply (cases isRevNth_isPC rule: uuIsInvar) by (auto simp: uu_defs isRevNth_isPC_def) lemma invar_isRevNth_isPC: "invar isRevNth_isPC" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isRevNth_isPC uIsInvar_isRevNth_isPC uuIsInvar_isRevNth_isPC by auto lemmas isRevNth_isPC1 = holdsIstate_invar[OF holdsIstate_isRevNth_isPC invar_isRevNth_isPC] theorem isRevNth_isPC: assumes a: "reach s" and R: "isRevNth s confID uID papID n" shows "isPC s confID uID" using isRevNth_isPC1[OF a] R unfolding isRevNth_isPC_def by auto corollary isRev_isPC: assumes a: "reach s" and R: "isRev s confID uID papID" shows "isPC s confID uID" using isRevNth_isPC[OF a] R unfolding isRev_def2 by auto (* Every conference that has papers is registered: *) definition paperIDs_confIDs :: "state \ bool" where "paperIDs_confIDs s \ \ confID papID. papID \\ paperIDs s confID \ confID \\ confIDs s" lemma holdsIstate_paperIDs_confIDs: "holdsIstate paperIDs_confIDs" unfolding IO_Automaton.holdsIstate_def istate_def istate_def paperIDs_confIDs_def by auto lemma cIsInvar_paperIDs_confIDs: "cIsInvar paperIDs_confIDs" apply (cases paperIDs_confIDs rule: cIsInvar) by (auto simp: c_defs paperIDs_confIDs_def ) lemma uIsInvar_paperIDs_confIDs: "uIsInvar paperIDs_confIDs" apply (cases paperIDs_confIDs rule: uIsInvar) by (auto simp: u_defs paperIDs_confIDs_def) lemma uuIsInvar_paperIDs_confIDs: "uuIsInvar paperIDs_confIDs" apply (cases paperIDs_confIDs rule: uuIsInvar) by (auto simp: uu_defs paperIDs_confIDs_def) lemma invar_paperIDs_confIDs: "invar paperIDs_confIDs" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_paperIDs_confIDs uIsInvar_paperIDs_confIDs uuIsInvar_paperIDs_confIDs by auto lemmas paperIDs_confIDs1 = holdsIstate_invar[OF holdsIstate_paperIDs_confIDs invar_paperIDs_confIDs] theorem paperIDs_confIDs: assumes a: "reach s" and p: "papID \\ paperIDs s confID" shows "confID \\ confIDs s" using paperIDs_confIDs1[OF a] p unfolding paperIDs_confIDs_def by auto corollary paperIDs_getAllPaperIDs: assumes a: "reach s" and p: "papID \\ paperIDs s confID" shows "papID \\ getAllPaperIDs s" using paperIDs_confIDs[OF assms] p unfolding getAllPaperIDs_def by auto corollary isRevNth_getAllPaperIDs: assumes a: "reach s" and "isRevNth s confID uID papID n" shows "papID \\ getAllPaperIDs s" using paperIDs_getAllPaperIDs[OF a isRevNth_paperIDs[OF assms]] . (* No paper is registered at two conferences: *) definition paperIDs_equals :: "state \ bool" where "paperIDs_equals s \ \ confID1 confID2 papID. papID \\ paperIDs s confID1 \ papID \\ paperIDs s confID2 \ confID1 = confID2" lemma holdsIstate_paperIDs_equals: "holdsIstate paperIDs_equals" unfolding IO_Automaton.holdsIstate_def istate_def istate_def paperIDs_equals_def by auto lemma cIsInvar_paperIDs_equals: "cIsInvar paperIDs_equals" apply (cases paperIDs_equals rule: cIsInvar) by (auto simp: c_defs paperIDs_equals_def paperIDs_getAllPaperIDs) lemma uIsInvar_paperIDs_equals: "uIsInvar paperIDs_equals" apply (cases paperIDs_equals rule: uIsInvar) by (auto simp: u_defs paperIDs_equals_def) lemma uuIsInvar_paperIDs_equals: "uuIsInvar paperIDs_equals" apply (cases paperIDs_equals rule: uuIsInvar) by (auto simp: uu_defs paperIDs_equals_def) lemma invar_paperIDs_equals: "invar paperIDs_equals" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_paperIDs_equals uIsInvar_paperIDs_equals uuIsInvar_paperIDs_equals by auto lemmas paperIDs_equals1 = holdsIstate_invar[OF holdsIstate_paperIDs_equals invar_paperIDs_equals] theorem paperIDs_equals: assumes a: "reach s" and p: "papID \\ paperIDs s confID1" "papID \\ paperIDs s confID2" shows "confID1 = confID2" using paperIDs_equals1[OF a] p unfolding paperIDs_equals_def by auto (* Everybody has conflict with their own papers *) definition isAut_pref_Conflict :: "state \ bool" where "isAut_pref_Conflict s \ \ confID uID papID. isAut s confID uID papID \ pref s uID papID = Conflict" lemma holdsIstate_isAut_pref_Conflict: "holdsIstate isAut_pref_Conflict" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isAut_pref_Conflict_def by auto lemma cIsInvar_isAut_pref_Conflict: "cIsInvar isAut_pref_Conflict" apply (cases isAut_pref_Conflict rule: cIsInvar) by (auto simp: c_defs isAut_pref_Conflict_def) lemma uIsInvar_isAut_pref_Conflict: "uIsInvar isAut_pref_Conflict" proof(cases isAut_pref_Conflict rule: uIsInvar) case (uPref s confID uID p paperID preference) thus ?case apply (auto simp: u_defs isAut_pref_Conflict_def) apply(frule isAut_paperIDs, simp) apply(frule paperIDs_equals, simp, simp, fastforce) done qed (auto simp: u_defs isAut_pref_Conflict_def) lemma uuIsInvar_isAut_pref_Conflict: "uuIsInvar isAut_pref_Conflict" apply (cases isAut_pref_Conflict rule: uuIsInvar) by (auto simp: uu_defs isAut_pref_Conflict_def) lemma invar_isAut_pref_Conflict: "invar isAut_pref_Conflict" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isAut_pref_Conflict uIsInvar_isAut_pref_Conflict uuIsInvar_isAut_pref_Conflict by auto lemmas isAut_pref_Conflict1 = holdsIstate_invar[OF holdsIstate_isAut_pref_Conflict invar_isAut_pref_Conflict] theorem isAut_pref_Conflict: assumes a: "reach s" and i: "isAut s confID uID papID" shows "pref s uID papID = Conflict" using isAut_pref_Conflict1[OF a] i unfolding isAut_pref_Conflict_def by auto (* A conference in phase noPH has no assigned papers *) definition phase_noPH_paperIDs :: "state \ bool" where "phase_noPH_paperIDs s \ \ confID. phase s confID = noPH \ paperIDs s confID = []" lemma holdsIstate_phase_noPH_paperIDs: "holdsIstate phase_noPH_paperIDs" unfolding IO_Automaton.holdsIstate_def istate_def istate_def phase_noPH_paperIDs_def by auto lemma cIsInvar_phase_noPH_paperIDs: "cIsInvar phase_noPH_paperIDs" apply (cases phase_noPH_paperIDs rule: cIsInvar) by (auto simp: c_defs phase_noPH_paperIDs_def) lemma uIsInvar_phase_noPH_paperIDs: "uIsInvar phase_noPH_paperIDs" apply(cases phase_noPH_paperIDs rule: uIsInvar) by (auto simp: u_defs phase_noPH_paperIDs_def) lemma uuIsInvar_phase_noPH_paperIDs: "uuIsInvar phase_noPH_paperIDs" apply (cases phase_noPH_paperIDs rule: uuIsInvar) by (auto simp: uu_defs phase_noPH_paperIDs_def) lemma invar_phase_noPH_paperIDs: "invar phase_noPH_paperIDs" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_phase_noPH_paperIDs uIsInvar_phase_noPH_paperIDs uuIsInvar_phase_noPH_paperIDs by auto lemmas phase_noPH_paperIDs1 = holdsIstate_invar[OF holdsIstate_phase_noPH_paperIDs invar_phase_noPH_paperIDs] theorem phase_noPH_paperIDs: assumes a: "reach s" and p: "phase s confID = noPH" shows "paperIDs s confID = []" using phase_noPH_paperIDs1[OF a] p unfolding phase_noPH_paperIDs_def by auto (* Papers only exist starting from the submission phase: *) definition paperIDs_geq_subPH :: "state \ bool" where "paperIDs_geq_subPH s \ \ confID papID. papID \\ paperIDs s confID \ phase s confID \ subPH" lemma holdsIstate_paperIDs_geq_subPH: "holdsIstate paperIDs_geq_subPH" unfolding IO_Automaton.holdsIstate_def istate_def istate_def paperIDs_geq_subPH_def by auto lemma cIsInvar_paperIDs_geq_subPH: "cIsInvar paperIDs_geq_subPH" apply (cases paperIDs_geq_subPH rule: cIsInvar) by (auto simp: c_defs paperIDs_geq_subPH_def) lemma uIsInvar_paperIDs_geq_subPH: "uIsInvar paperIDs_geq_subPH" apply (cases paperIDs_geq_subPH rule: uIsInvar) by (fastforce simp: u_defs paperIDs_geq_subPH_def)+ lemma uuIsInvar_paperIDs_geq_subPH: "uuIsInvar paperIDs_geq_subPH" apply (cases paperIDs_geq_subPH rule: uuIsInvar) by (auto simp: uu_defs paperIDs_geq_subPH_def) lemma invar_paperIDs_geq_subPH: "invar paperIDs_geq_subPH" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_paperIDs_geq_subPH uIsInvar_paperIDs_geq_subPH uuIsInvar_paperIDs_geq_subPH by auto lemmas paperIDs_geq_subPH1 = holdsIstate_invar[OF holdsIstate_paperIDs_geq_subPH invar_paperIDs_geq_subPH] theorem paperIDs_geq_subPH: assumes a: "reach s" and i: "papID \\ paperIDs s confID" shows "phase s confID \ subPH" using paperIDs_geq_subPH1[OF a] i unfolding paperIDs_geq_subPH_def by auto (* Reviewers only exist starting from the reviewing phase: *) definition isRevNth_geq_revPH :: "state \ bool" where "isRevNth_geq_revPH s \ \ confID uID papID n. isRevNth s confID uID papID n \ phase s confID \ revPH" lemma holdsIstate_isRevNth_geq_revPH: "holdsIstate isRevNth_geq_revPH" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isRevNth_geq_revPH_def by auto lemma cIsInvar_isRevNth_geq_revPH: "cIsInvar isRevNth_geq_revPH" apply (cases isRevNth_geq_revPH rule: cIsInvar) by (auto simp: c_defs isRevNth_geq_revPH_def) lemma uIsInvar_isRevNth_geq_revPH: "uIsInvar isRevNth_geq_revPH" proof (cases isRevNth_geq_revPH rule: uIsInvar) case (uConfA s confID uID p) thus ?case by (fastforce simp: u_defs isRevNth_geq_revPH_def) qed(fastforce simp: u_defs isRevNth_geq_revPH_def)+ lemma uuIsInvar_isRevNth_geq_revPH: "uuIsInvar isRevNth_geq_revPH" apply (cases isRevNth_geq_revPH rule: uuIsInvar) by (auto simp: uu_defs isRevNth_geq_revPH_def) lemma invar_isRevNth_geq_revPH: "invar isRevNth_geq_revPH" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isRevNth_geq_revPH uIsInvar_isRevNth_geq_revPH uuIsInvar_isRevNth_geq_revPH by auto lemmas isRevNth_geq_revPH1 = holdsIstate_invar[OF holdsIstate_isRevNth_geq_revPH invar_isRevNth_geq_revPH] theorem isRevNth_geq_revPH: assumes a: "reach s" and i: "isRevNth s confID uID papID n" shows "phase s confID \ revPH" using isRevNth_geq_revPH1[OF a] i unfolding isRevNth_geq_revPH_def by auto corollary isRev_geq_revPH: assumes a: "reach s" and i: "isRev s confID uID papID" shows "phase s confID \ revPH" using isRevNth_geq_revPH[OF a] i unfolding isRev_def2 by auto (* Every paper has at least one author: *) definition paperID_ex_userID :: "state \ bool" where "paperID_ex_userID s \ \ confID papID. papID \\ paperIDs s confID \ (\ uID. isAut s confID uID papID)" lemma holdsIstate_paperID_ex_userID: "holdsIstate paperID_ex_userID" unfolding IO_Automaton.holdsIstate_def istate_def istate_def paperID_ex_userID_def by auto lemma cIsInvar_paperID_ex_userID: "cIsInvar paperID_ex_userID" apply (cases paperID_ex_userID rule: cIsInvar) by (fastforce simp: c_defs paperID_ex_userID_def paperIDs_confIDs)+ lemma uIsInvar_paperID_ex_userID: "uIsInvar paperID_ex_userID" apply (cases paperID_ex_userID rule: uIsInvar) by (fastforce simp: u_defs paperID_ex_userID_def)+ lemma uuIsInvar_paperID_ex_userID: "uuIsInvar paperID_ex_userID" apply (cases paperID_ex_userID rule: uuIsInvar) by (auto simp: uu_defs paperID_ex_userID_def) lemma invar_paperID_ex_userID: "invar paperID_ex_userID" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_paperID_ex_userID uIsInvar_paperID_ex_userID uuIsInvar_paperID_ex_userID by auto lemmas paperID_ex_userID1 = holdsIstate_invar[OF holdsIstate_paperID_ex_userID invar_paperID_ex_userID] theorem paperID_ex_userID: assumes a: "reach s" and i: "papID \\ paperIDs s confID" shows "\ uID. isAut s confID uID papID" using paperID_ex_userID1[OF a] i unfolding paperID_ex_userID_def by auto (* Nobody reviews a paper with which one has conflict: *) definition pref_Conflict_isRevNth :: "state \ bool" where "pref_Conflict_isRevNth s \ \ confID uID papID n. pref s uID papID = Conflict \ \ isRevNth s confID uID papID n" lemma holdsIstate_pref_Conflict_isRevNth: "holdsIstate pref_Conflict_isRevNth" unfolding IO_Automaton.holdsIstate_def istate_def istate_def pref_Conflict_isRevNth_def by auto lemma cIsInvar_pref_Conflict_isRevNth: "cIsInvar pref_Conflict_isRevNth" proof (cases pref_Conflict_isRevNth rule: cIsInvar) case (cAuthor s confID uID p papID uID') thus ?case apply (auto simp: c_defs pref_Conflict_isRevNth_def) apply(frule isRevNth_geq_revPH, simp, simp) apply(frule isRevNth_paperIDs, simp) apply(frule paperIDs_equals, simp, simp, force) done next case (cConflict s confID uID p papID uID') thus ?case apply (auto simp: c_defs pref_Conflict_isRevNth_def) apply(frule isRevNth_geq_revPH, simp) apply(frule isRevNth_paperIDs, simp) apply(frule paperIDs_equals, simp, simp, force) done qed (auto simp: c_defs pref_Conflict_isRevNth_def isRevNth_getAllPaperIDs) lemma uIsInvar_pref_Conflict_isRevNth: "uIsInvar pref_Conflict_isRevNth" proof(cases pref_Conflict_isRevNth rule: uIsInvar) case (uPref s confID uID p paperID pref) thus ?case apply (auto simp: u_defs pref_Conflict_isRevNth_def) apply(frule isRevNth_geq_revPH, simp) apply(frule isRevNth_paperIDs, simp) apply(frule paperIDs_equals, simp, simp, force) done qed (auto simp: u_defs pref_Conflict_isRevNth_def) lemma uuIsInvar_pref_Conflict_isRevNth: "uuIsInvar pref_Conflict_isRevNth" apply (cases pref_Conflict_isRevNth rule: uuIsInvar) by (auto simp: uu_defs pref_Conflict_isRevNth_def) lemma invar_pref_Conflict_isRevNth: "invar pref_Conflict_isRevNth" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_pref_Conflict_isRevNth uIsInvar_pref_Conflict_isRevNth uuIsInvar_pref_Conflict_isRevNth by auto lemmas pref_Conflict_isRevNth1 = holdsIstate_invar[OF holdsIstate_pref_Conflict_isRevNth invar_pref_Conflict_isRevNth] theorem pref_Conflict_isRevNth: assumes a: "reach s" and i: "pref s uID papID = Conflict" shows "\ isRevNth s confID uID papID n" using pref_Conflict_isRevNth1[OF a] i unfolding pref_Conflict_isRevNth_def by auto corollary pref_Conflict_isRev: assumes a: "reach s" and i: "pref s uID papID = Conflict" shows "\ isRev s confID uID papID" using pref_Conflict_isRevNth[OF a] i unfolding isRev_def2 by auto (* Nobody reviews her own paper: *) corollary pref_isAut_isRevNth: assumes a: "reach s" and i: "isAut s confID uID papID" shows "\ isRevNth s confID uID papID n" using pref_Conflict_isRevNth[OF a] isAut_pref_Conflict[OF a i] by auto corollary pref_isAut_isRev: assumes a: "reach s" and i: "isAut s confID uID papID" shows "\ isRev s confID uID papID" using pref_isAut_isRevNth[OF a] i unfolding isRev_def2 by auto (* Every chair is also a committee member *) definition isChair_isPC :: "state \ bool" where "isChair_isPC s \ \ confID uID. isChair s confID uID \ isPC s confID uID" lemma holdsIstate_isChair_isPC: "holdsIstate isChair_isPC" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isChair_isPC_def by auto lemma cIsInvar_isChair_isPC: "cIsInvar isChair_isPC" apply (cases isChair_isPC rule: cIsInvar) by (auto simp: c_defs isChair_isPC_def) lemma uIsInvar_isChair_isPC: "uIsInvar isChair_isPC" apply(cases isChair_isPC rule: uIsInvar) by (auto simp: u_defs isChair_isPC_def) lemma uuIsInvar_isChair_isPC: "uuIsInvar isChair_isPC" apply (cases isChair_isPC rule: uuIsInvar) by (auto simp: uu_defs isChair_isPC_def) lemma invar_isChair_isPC: "invar isChair_isPC" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isChair_isPC uIsInvar_isChair_isPC uuIsInvar_isChair_isPC by auto lemmas isChair_isPC1 = holdsIstate_invar[OF holdsIstate_isChair_isPC invar_isChair_isPC] theorem isChair_isPC: assumes a: "reach s" and p: "isChair s confID uID" shows "isPC s confID uID" using isChair_isPC1[OF a] p unfolding isChair_isPC_def by auto (* A user does not get to write more than one review of any given paper: *) definition isRevNth_equals :: "state \ bool" where "isRevNth_equals s \ \ confID uID papID m n. isRevNth s confID uID papID m \ isRevNth s confID uID papID n \ m = n" lemma holdsIstate_isRevNth_equals: "holdsIstate isRevNth_equals" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isRevNth_equals_def by auto lemma cIsInvar_isRevNth_equals: "cIsInvar isRevNth_equals" proof (cases isRevNth_equals rule: cIsInvar) (* this case is merely singled out for documentation: *) case (cReview s confID uID p papID uID') thus ?case by(fastforce simp add: c_defs isRevNth_equals_def isRev_def2) qed (auto simp: c_defs isRevNth_equals_def) lemma uIsInvar_isRevNth_equals: "uIsInvar isRevNth_equals" apply(cases isRevNth_equals rule: uIsInvar) by (auto simp: u_defs isRevNth_equals_def) lemma uuIsInvar_isRevNth_equals: "uuIsInvar isRevNth_equals" apply (cases isRevNth_equals rule: uuIsInvar) by (auto simp: uu_defs isRevNth_equals_def) lemma invar_isRevNth_equals: "invar isRevNth_equals" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isRevNth_equals uIsInvar_isRevNth_equals uuIsInvar_isRevNth_equals by auto lemmas isRevNth_equals1 = holdsIstate_invar[OF holdsIstate_isRevNth_equals invar_isRevNth_equals] theorem isRevNth_equals: assumes a: "reach s" and r: "isRevNth s confID uID papID m" "isRevNth s confID uID papID n" shows "m = n" using isRevNth_equals1[OF a] r unfolding isRevNth_equals_def by blast corollary isRevNth_getReviewIndex: assumes a: "reach s" and r: "isRevNth s confID uID papID n" shows "n = getReviewIndex s confID uID papID" using isRevNth_equals[OF a r] r by (metis isRev_def2 isRev_def3) (* A reviewer is always assigned a valid review number: *) definition isRevNth_less_length :: "state \ bool" where "isRevNth_less_length s \ \ confID uID papID n. isRevNth s confID uID papID n \ n < length (reviewsPaper (paper s papID))" lemma holdsIstate_isRevNth_less_length: "holdsIstate isRevNth_less_length" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isRevNth_less_length_def by auto lemma cIsInvar_isRevNth_less_length: "cIsInvar isRevNth_less_length" apply(cases isRevNth_less_length rule: cIsInvar) by(fastforce simp: c_defs isRevNth_less_length_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma uIsInvar_isRevNth_less_length: "uIsInvar isRevNth_less_length" apply(cases isRevNth_less_length rule: uIsInvar) by(fastforce simp: u_defs isRevNth_less_length_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma uuIsInvar_isRevNth_less_length: "uuIsInvar isRevNth_less_length" apply (cases isRevNth_less_length rule: uuIsInvar) by(fastforce simp: uu_defs isRevNth_less_length_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma invar_isRevNth_less_length: "invar isRevNth_less_length" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isRevNth_less_length uIsInvar_isRevNth_less_length uuIsInvar_isRevNth_less_length by auto lemmas isRevNth_less_length1 = holdsIstate_invar[OF holdsIstate_isRevNth_less_length invar_isRevNth_less_length] theorem isRevNth_less_length: assumes "reach s" and "isRevNth s cid uid pid n" shows "n < length (reviewsPaper (paper s pid))" using isRevNth_less_length1 assms unfolding isRevNth_less_length_def by blast (* No two reviewers get assigned the same review: *) definition isRevNth_equalsU :: "state \ bool" where "isRevNth_equalsU s \ \ confID uID uID1 papID n. isRevNth s confID uID papID n \ isRevNth s confID uID1 papID n \ uID = uID1" lemma holdsIstate_isRevNth_equalsU: "holdsIstate isRevNth_equalsU" unfolding IO_Automaton.holdsIstate_def istate_def istate_def isRevNth_equalsU_def by auto lemma cIsInvar_isRevNth_equalsU: "cIsInvar isRevNth_equalsU" apply (cases isRevNth_equalsU rule: cIsInvar) apply(fastforce simp: c_defs isRevNth_equalsU_def)+ proof- fix s confID uID p papID uID' assume s: "reach s" and 0: "isRevNth_equalsU s" "e_createReview s confID uID p papID uID'" let ?s' = "createReview s confID uID p papID uID'" show "isRevNth_equalsU ?s'" unfolding isRevNth_equalsU_def proof clarify fix confIDa uIDa uID1 papIDa n assume "isRevNth ?s' confIDa uIDa papIDa n" "isRevNth ?s' confIDa uID1 papIDa n" thus "uIDa = uID1" apply(cases "confIDa = confID \ papIDa = papID") apply(cases "uIDa = uID", cases "uID1 = uID") using s 0 isRevNth_less_length[OF s, of papID n] unfolding isRevNth_less_length_def by (fastforce simp: c_defs isRevNth_equalsU_def)+ qed qed lemma uIsInvar_isRevNth_equalsU: "uIsInvar isRevNth_equalsU" apply(cases isRevNth_equalsU rule: uIsInvar) by (auto simp: u_defs isRevNth_equalsU_def) lemma uuIsInvar_isRevNth_equalsU: "uuIsInvar isRevNth_equalsU" apply (cases isRevNth_equalsU rule: uuIsInvar) by (auto simp: uu_defs isRevNth_equalsU_def) lemma invar_isRevNth_equalsU: "invar isRevNth_equalsU" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_isRevNth_equalsU uIsInvar_isRevNth_equalsU uuIsInvar_isRevNth_equalsU by auto lemmas isRevNth_equalsU1 = holdsIstate_invar[OF holdsIstate_isRevNth_equalsU invar_isRevNth_equalsU] theorem isRevNth_equalsU: assumes a: "reach s" and r: "isRevNth s confID uID papID n" "isRevNth s confID uID1 papID n" shows "uID = uID1" using isRevNth_equalsU1[OF a] r unfolding isRevNth_equalsU_def by blast (* The reviews form a compact interval (with no gaps): *) definition reviews_compact :: "state \ bool" where "reviews_compact s \ \ confID papID n. papID \\ paperIDs s confID \ n < length (reviewsPaper (paper s papID)) \ (\ uID. isRevNth s confID uID papID n)" lemma holdsIstate_reviews_compact: "holdsIstate reviews_compact" unfolding IO_Automaton.holdsIstate_def istate_def istate_def reviews_compact_def by auto lemma cIsInvar_reviews_compact: "cIsInvar reviews_compact" apply(cases reviews_compact rule: cIsInvar) apply(auto simp: c_defs reviews_compact_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI) using paperIDs_confIDs apply fastforce apply metis apply metis apply metis using less_Suc_eq apply auto[1] apply metis done lemma uIsInvar_reviews_compact: "uIsInvar reviews_compact" apply(cases reviews_compact rule: uIsInvar) by(fastforce simp: u_defs reviews_compact_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma uuIsInvar_reviews_compact: "uuIsInvar reviews_compact" apply (cases reviews_compact rule: uuIsInvar) by(fastforce simp: uu_defs reviews_compact_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma invar_reviews_compact: "invar reviews_compact" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_reviews_compact uIsInvar_reviews_compact uuIsInvar_reviews_compact by auto lemmas reviews_compact1 = holdsIstate_invar[OF holdsIstate_reviews_compact invar_reviews_compact] theorem reviews_compact: assumes "reach s" and "n < length (reviewsPaper (paper s pid))" and "pid \\ paperIDs s cid" shows "\ uid. isRevNth s cid uid pid n" using reviews_compact1 assms unfolding reviews_compact_def by blast (* The list of roles for each conference-user is nonrepetitive: *) definition roles_nonrep :: "state \ bool" where "roles_nonrep s \ \ confID uID. distinct (roles s confID uID)" lemma holdsIstate_roles_nonrep: "holdsIstate roles_nonrep" unfolding IO_Automaton.holdsIstate_def istate_def istate_def roles_nonrep_def by auto lemma cIsInvar_roles_nonrep: "cIsInvar roles_nonrep" apply(cases roles_nonrep rule: cIsInvar) by (auto simp: c_defs roles_nonrep_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI) lemma uIsInvar_roles_nonrep: "uIsInvar roles_nonrep" apply(cases roles_nonrep rule: uIsInvar) by(fastforce simp: u_defs roles_nonrep_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma uuIsInvar_roles_nonrep: "uuIsInvar roles_nonrep" apply (cases roles_nonrep rule: uuIsInvar) by(fastforce simp: uu_defs roles_nonrep_def isRevNth_getAllPaperIDs isRev_def2 isRevNth_paperIDs paperIDs_equals less_SucI)+ lemma invar_roles_nonrep: "invar roles_nonrep" unfolding invar_cIsInvar_uIsInvar_uuIsInvar using cIsInvar_roles_nonrep uIsInvar_roles_nonrep uuIsInvar_roles_nonrep by auto lemmas roles_nonrep1 = holdsIstate_invar[OF holdsIstate_roles_nonrep invar_roles_nonrep] theorem roles_nonrep: assumes "reach s" shows "distinct (roles s confID uID)" using roles_nonrep1 assms unfolding roles_nonrep_def by blast subsection\Properties of the step function\ lemma step_outErr_eq: "step s a = (outErr, s') \ s'= s" apply (cases a) subgoal for x1 apply (cases x1, simp_all add: c_defs) . subgoal for x2 apply (cases x2, simp_all add: u_defs) . subgoal for x3 apply (cases x3, simp_all add: uu_defs) . by auto lemma phase_increases: assumes "step s a = (ou,s')" shows "phase s cid \ phase s' cid" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto lemma phase_increases2: "phase s CID \ phase (snd (step s a)) CID" by (metis phase_increases snd_conv surj_pair) lemma confIDs_mono: assumes "step s a = (ou,s')" and "cid \\ confIDs s" shows "cid \\ confIDs s'" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto lemma userIDs_mono: assumes "step s a = (ou,s')" and "uid \\ userIDs s" shows "uid \\ userIDs s'" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto lemma paperIDs_mono: assumes "step s a = (ou,s')" and "pid \\ paperIDs s cid" shows "pid \\ paperIDs s' cid" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto lemma isPC_persistent: assumes "isPC s cid uid" and "step s a = (ou, s')" shows "isPC s' cid uid" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto lemma isChair_persistent: assumes "isChair s cid uid" and "step s a = (ou, s')" shows "isChair s' cid uid" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto subsection \Action-safety properties\ lemma pref_Conflict_disPH: assumes "reach s" and "pid \\ paperIDs s cid" and "pref s uid pid \ Conflict" and "phase s cid = disPH" and "step s a = (ou, s')" shows "pref s' uid pid \ Conflict" proof- have 1: "cid \\ confIDs s" using assms by (metis geq_noPH_confIDs zero_less_Suc) thus ?thesis using assms apply(cases a) subgoal for x1 apply(cases x1, auto simp: c_defs getAllPaperIDs_def) apply (metis Suc_inject Zero_not_Suc paperIDs_equals) apply (metis Suc_inject Zero_not_Suc paperIDs_equals) . subgoal for x2 apply(cases x2, auto simp: u_defs) apply (metis Suc_inject Zero_not_Suc paperIDs_equals) . subgoal for x3 apply(cases x3, auto simp: uu_defs) . by auto qed lemma isRevNth_persistent: assumes "reach s" and "isRevNth s cid uid pid n" and "step s a = (ou, s')" shows "isRevNth s' cid uid pid n" using assms apply (cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs roles_confIDs) . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) . subgoal for x3 apply(cases x3) apply(auto simp: uu_defs) . by auto lemma nonempty_decsPaper_persist: assumes s: "reach s" and pid: "pid \\ paperIDs s cid" and "decsPaper (paper s pid) \ []" and "step s a = (ou,s')" shows "decsPaper (paper s' pid) \ []" proof- have "cid \\ confIDs s" using s pid by (metis paperIDs_confIDs) thus ?thesis using assms apply(cases a) subgoal for x1 apply(cases x1, auto simp: c_defs getAllPaperIDs_def) . subgoal for x2 apply(cases x2, auto simp: u_defs) . subgoal for x3 apply(cases x3, auto simp: uu_defs) . by auto qed lemma nonempty_reviews_persist: assumes s: "reach s" and r: "isRevNth s cid uid pid n" and "(reviewsPaper (paper s pid))!n \ []" and "step s a = (ou,s')" shows "(reviewsPaper (paper s' pid))!n \ []" proof- have pid: "pid \\ paperIDs s cid" using s r by (metis isRevNth_paperIDs) have cid: "cid \\ confIDs s" using s pid by (metis paperIDs_confIDs) have n: "n < length (reviewsPaper (paper s pid))" using s r by (metis isRevNth_less_length) show ?thesis using assms pid cid n apply(cases a) subgoal for x1 apply(cases x1, auto simp: c_defs getAllPaperIDs_def) . subgoal for x2 apply(cases x2, auto simp: u_defs) apply (metis not_Cons_self2 nth_list_update_eq nth_list_update_neq) . subgoal for x3 apply(cases x3, auto simp: uu_defs) apply (metis list.distinct(1) nth_list_update_eq nth_list_update_neq) . by auto qed lemma revPH_pref_persists: assumes "reach s" "pid \\ paperIDs s cid" and "phase s cid \ revPH" and "step s a = (ou,s')" shows "pref s' uid pid = pref s uid pid" using assms apply(cases a) subgoal for x1 apply(cases x1) apply(auto simp: c_defs paperIDs_getAllPaperIDs) using paperIDs_equals apply fastforce using paperIDs_equals apply fastforce . subgoal for x2 apply(cases x2) apply(auto simp: u_defs) using paperIDs_equals apply fastforce . subgoal for x3 apply(cases x3) apply(fastforce simp: uu_defs)+ . by auto subsection \Miscellaneous\ (* Simps bringing the "paper" field all the way to the left---useful for situations where the states are equal everywhere but on the paper field. *) lemma updates_commute_paper: "\ uu. s \confIDs := uu, paper := pp\ = s \paper := pp, confIDs := uu\" "\ uu. s \conf := uu, paper := pp\ = s \paper := pp, conf := uu\" "\ uu. s \userIDs := uu, paper := pp\ = s \paper := pp, userIDs := uu\" "\ uu. s \pass := uu, paper := pp\ = s \paper := pp, pass := uu\" "\ uu. s \user := uu, paper := pp\ = s \paper := pp, user := uu\" "\ uu. s \roles := uu, paper := pp\ = s \paper := pp, roles := uu\" "\ uu. s \paperIDs := uu, paper := pp\ = s \paper := pp, paperIDs := uu\" "\ uu. s \pref := uu, paper := pp\ = s \paper := pp, pref := uu\" "\ uu. s \voronkov := uu, paper := pp\ = s \paper := pp, voronkov := uu\" "\ uu. s \news := uu, paper := pp\ = s \paper := pp, news := uu\" "\ uu. s \phase := uu, paper := pp\ = s \paper := pp, phase := uu\" by (auto intro: state.equality) (* The implication between the implicit- and explicit conference ID selectors *) lemma isAUT_imp_isAut: assumes "reach s" and "pid \\ paperIDs s cid" and "isAUT s uid pid" shows "isAut s cid uid pid" by (metis assms isAUT_def isAut_paperIDs paperIDs_equals) lemma isREVNth_imp_isRevNth: assumes "reach s" and "pid \\ paperIDs s cid" and "isREVNth s uid pid n" shows "isRevNth s cid uid pid n" by (metis assms isREVNth_def isRevNth_paperIDs paperIDs_equals) (* BEGIN phase properties *) lemma phase_increases_validTrans: assumes "validTrans (Trans s a ou s')" shows "phase s cid \ phase s' cid" using assms apply(cases a) subgoal for x1 apply(cases x1, auto simp: c_defs split: if_splits) . subgoal for x2 apply(cases x2, auto simp: u_defs split: if_splits paper.splits) . subgoal for x3 apply(cases x3, auto simp: uu_defs split: if_splits paper.splits) . by auto lemma phase_increases_validTrans2: assumes "validTrans tr" shows "phase (srcOf tr) cid \ phase (tgtOf tr) cid" using assms phase_increases_validTrans by (cases tr) auto lemma phase_increases_trace: assumes vtr: "valid tr" and ij: "i \ j" and j: "j < length tr" shows "phase (srcOf (tr!i)) cid \ phase (srcOf (tr!j)) cid" proof(cases "i < j") case False thus ?thesis using ij by auto next case True thus ?thesis using j proof(induction j) case (Suc jj) show ?case proof(cases "jj = i") case True obtain tr1 tr2 where tr: "tr = tr1 @ (tr!i) # (tr!(Suc jj)) # tr2" unfolding True by (metis Cons_nth_drop_Suc Suc.prems(2) Suc_lessD True id_take_nth_drop) hence "validTrans (tr!i) \ tgtOf (tr!i) = srcOf (tr!(Suc jj))" unfolding True by (metis Suc Suc_lessD True valid_validTrans_nth valid_validTrans_nth_srcOf_tgtOf vtr) thus ?thesis using phase_increases_validTrans Suc by (cases "tr!i") auto next case False hence 1: "i < jj \ jj < length tr" using Suc by auto hence "phase (srcOf (tr!i)) cid \ phase (srcOf (tr!jj)) cid" using Suc by auto also have "phase (srcOf (tr!jj)) cid \ phase (tgtOf (tr!jj)) cid" using phase_increases_validTrans2 by (metis 1 valid_validTrans_nth vtr) also have "... = phase (srcOf (tr!(Suc jj))) cid" by (metis Suc valid_validTrans_nth_srcOf_tgtOf vtr) finally show ?thesis . qed qed auto qed lemma phase_increases_trace_srcOf_tgtOf: assumes vtr: "valid tr" and ij: "i \ j" and j: "j < length tr" shows "phase (srcOf (tr!i)) cid \ phase (tgtOf (tr!j)) cid" using phase_increases_trace[OF assms] using j le_trans phase_increases_validTrans2 valid_validTrans_nth vtr by blast lemma phase_increases_trace_srcOf_hd: assumes v: "valid tr" and l: "length tr > 1" and "i < length tr" shows "phase (srcOf (hd tr)) cid \ phase (srcOf (tr!i)) cid" using phase_increases_trace assms by (metis gr_implies_not0 hd_Cons_tl leI length_0_conv nth_Cons_0) lemma phase_increases_trace_srcOf_last: assumes v: "valid tr" and l: "length tr > 1" and i: "i < length tr" shows "phase (srcOf (tr!i)) cid \ phase (srcOf (last tr)) cid" proof- have 1: "last tr = tr!(length tr - 1)" by (metis i last_conv_nth list.size(3) not_less0) show ?thesis unfolding 1 using assms by (metis Suc_diff_1 Suc_leI Suc_le_mono gr_implies_not0 length_0_conv length_greater_0_conv lessI phase_increases_trace) qed lemma phase_increases_trace_srcOf_tgtOf_last: assumes v: "valid tr" and l: "length tr > 1" and i: "i < length tr" shows "phase (srcOf (tr!i)) cid \ phase (tgtOf (last tr)) cid" proof- have 1: "last tr = tr!(length tr - 1)" by (metis i last_conv_nth list.size(3) not_less0) have "phase (srcOf (tr!i)) cid \ phase (srcOf (last tr)) cid" using phase_increases_trace_srcOf_last[OF assms] . also have "... \ phase (tgtOf (last tr)) cid" unfolding 1 by (metis Suc_le_D diff_Suc_1 l lessI less_eq_Suc_le phase_increases_validTrans2 v valid_validTrans_nth) finally show ?thesis by (simp add: le_funD) qed lemma valid_tgtPf_last_srcOf: assumes "valid tr" and "s \\ map tgtOf tr" shows "s = tgtOf (last tr) \ s \\ map srcOf tr" using assms by induction auto lemma phase_constant: assumes v: "valid tr" and l: "length tr > 0" and ph: "phase (srcOf (hd tr)) cid = phase (tgtOf (last tr)) cid" shows "set (map (\ trn. phase (srcOf trn) cid) tr) \ {phase (srcOf (hd tr)) cid} \ set (map (\ trn. phase (tgtOf trn) cid) tr) \ {phase (srcOf (hd tr)) cid}" proof(cases "length tr > 1") case False then obtain trn where tr: "tr = [trn]" using l by (cases tr) auto show ?thesis using assms unfolding tr by auto next case True note l = True show ?thesis proof safe {fix ph assume "ph \\ map (\ trn. phase (srcOf trn) cid) tr" then obtain i where i: "i < length tr" and phe: "ph = phase (srcOf(tr!i)) cid" - by (smt comp_apply in_set_conv_nth length_map nth_map) + by (smt (verit) comp_apply in_set_conv_nth length_map nth_map) have "phase (srcOf (hd tr)) cid \ ph" unfolding phe using v l i phase_increases_trace_srcOf_hd by blast moreover have "ph \ phase (tgtOf (last tr)) cid" unfolding phe using v l i phase_increases_trace_srcOf_tgtOf_last by auto ultimately show "ph = phase (srcOf (hd tr)) cid" using ph by simp } note 0 = this fix ph assume "ph \\ map (\ trn. phase (tgtOf trn) cid) tr" then obtain s where "s \\ map tgtOf tr" and phs: "ph = phase s cid" by auto hence "s = tgtOf (last tr) \ s \\ map srcOf tr" using valid_tgtPf_last_srcOf[OF v] by auto thus "ph = phase (srcOf (hd tr)) cid" using 0[of ph] ph unfolding phs by auto qed qed lemma phase_cases: assumes "step s a = (ou, s')" obtains (noPH) "\ cid \\ confIDs s \ phase s cid = noPH" (* the conf. does not exist yet or the voronkov has not yet approved it *) | (Id) "phase s' cid = phase s cid" | (Upd) uid p ph where "phase s' cid = ph" "a = Uact (uPhase cid uid p ph)" "e_updatePhase s cid uid p ph" using assms proof (cases a) case (Cact ca) then show thesis using assms by (cases ca) (auto simp: c_defs split: if_splits intro: that) next case (Uact ua) then show thesis using assms apply (cases ua) subgoal by (auto simp: u_defs split: if_splits paper.splits intro: that) subgoal for x21 apply(cases "x21 = cid") by (auto simp: u_defs split: if_splits paper.splits intro: that) subgoal for x31 apply(cases "cid = x31") by (auto simp: u_defs split: if_splits paper.splits intro: that) by (auto simp: u_defs split: if_splits paper.splits intro: that) next case (UUact uua) then show thesis using assms by (cases uua) (auto simp: uu_defs split: if_splits paper.splits intro: that) qed auto lemma phase_mono: "reachFrom s s' \ phase s cid \ phase s' cid" proof (induction rule: reachFrom_step_induct) case (Step s' a ou s'') then show ?case proof (cases a) case (Cact cAct) with Step show ?thesis by (cases cAct) (auto simp add: c_defs split: if_splits) next case (Uact uAct) with Step show ?thesis by (cases uAct) (auto simp add: u_defs split: if_splits paper.split) next case (UUact uAct) with Step show ?thesis by (cases uAct) (auto simp add: uu_defs split: if_splits paper.split) qed (auto) qed (auto) lemma validTrans_rAct_lAct_srcOf_tgtOf: assumes "validTrans trn" and "actOf trn = Ract rAct \ actOf trn = Lact lAct" shows "tgtOf trn = srcOf trn" using assms by (cases trn) auto lemma valid_rAct_lAct_srcOf_tgtOf: assumes "valid tr" and "\ a. a \\ map actOf tr \ (\ rAct. a = Ract rAct) \ (\ lAct. a = Lact lAct)" shows "srcOf ` (set tr) \ {srcOf (hd tr)}" using assms by (induction) (simp_all, metis validTrans_rAct_lAct_srcOf_tgtOf) lemma validFrom_rAct_lAct_srcOf_tgtOf: assumes "validFrom s tr" and "\ a. a \\ map actOf tr \ (\ rAct. a = Ract rAct) \ (\ lAct. a = Lact lAct)" shows "srcOf ` (set tr) \ {s}" using assms valid_rAct_lAct_srcOf_tgtOf unfolding validFrom_def by auto lemma tgtOf_last_traceOf_Ract_Lact[simp]: assumes "al \ []" "set al \ range Ract \ range Lact" shows "tgtOf (last (traceOf s al)) = s" using assms by (induction al arbitrary: s) auto (* END phase properties *) lemma paperIDs_cases: assumes "step s a = (ou, s')" obtains (Id) "paperIDs s' cid = paperIDs s cid" | (Create) cid uid p pid tit ab where "paperIDs s' cid = pid # paperIDs s cid" "a = Cact (cPaper cid uid p pid tit ab)" "e_createPaper s cid uid p pid tit ab" using assms proof (cases a) case (Cact ca) then show thesis using assms by (cases ca) (auto simp: c_defs split: if_splits intro: that) next case (Uact ua) then show thesis using assms by (cases ua) (auto simp: u_defs split: if_splits paper.splits intro: that) next case (UUact ua) then show thesis using assms by (cases ua) (auto simp: uu_defs split: if_splits paper.splits intro: that) qed auto lemma paperIDs_decPH_const: assumes s: "step s a = (ou, s')" and "phase s cid > subPH" shows "paperIDs s' cid = paperIDs s cid" using assms apply (elim paperIDs_cases[where cid = cid]) subgoal . subgoal for cida apply(cases "cida = cid", auto) using s by (auto simp: c_defs) . end