(* Title: Conservation of CSP Noninterference Security under Sequential Composition Author: Pasquale Noce Security Certification Specialist at Arjo Systems, Italy pasquale dot noce dot lavoro at gmail dot com pasquale dot noce at arjosystems dot com *) section "Propaedeutic definitions and lemmas" theory Propaedeutics imports Noninterference_Ipurge_Unwinding.DeterministicProcesses begin text ‹ \null \emph{To our Lord Jesus Christ, my dear parents, and my "little" sister,} \emph{for the immense love with which they surround me.} \null In his outstanding work on Communicating Sequential Processes \<^cite>‹"R4"›, Hoare has defined two fundamental binary operations allowing to compose the input processes into another, typically more complex, process: sequential composition and concurrent composition. Particularly, the output of the former operation is a process that initially behaves like the first operand, and then like the second operand once the execution of the first one has terminated successfully, as long as it does. In order to distinguish it from deadlock, successful termination is regarded as a special event in the process alphabet (required to be the same for both the input processes and the output one). This paper formalizes Hoare's definition of sequential composition and proves, in the general case of a possibly intransitive policy, that CSP noninterference security \<^cite>‹"R2"› is conserved under this operation, viz. the security of both of the input processes implies that of the output process. This property is conditional on two nontrivial assumptions. The first assumption is that the policy do not allow successful termination to be affected by confidential events, viz. by other events not allowed to affect some event in the process alphabet. The second assumption is that successful termination do not occur as an alternative to other events in the traces of the first operand, viz. that whenever the process can terminate successfully, it cannot engage in any other event. Both of these assumptions are shown, by means of counterexamples, to be necessary for the theorem to hold. From the above sketch of the sequential composition of two processes @{term P} and @{term Q}, notwithstanding its informal character, it clearly follows that any failure of the output process is either a failure of @{term P} (case A), or a pair @{term "(xs @ ys, Y)"}, where @{term xs} is a trace of @{term P} and @{term "(ys, Y)"} is a failure of @{term Q} (case B). On the other hand, according to the definition of security given in \<^cite>‹"R2"›, the output process is secure just in case, for each of its failures, any event @{term x} contained in the failure trace can be removed from the trace, or inserted into the trace of another failure after the same previous events as in the original trace, and the resulting pair is still a failure of the process, provided that the future of @{term x} is deprived of the events that may be affected by @{term x}. In case A, this transformation is performed on a failure of process @{term P}; being it secure, the result is still a failure of @{term P}, and then of the output process. In case B, the transformation may involve either @{term ys} alone, or both @{term xs} and @{term ys}, depending on the position at which @{term x} is removed or inserted. In the former subcase, being @{term Q} secure, the result has the form @{term "(xs @ ys', Y')"} where @{term "(ys', Y')"} is a failure of @{term Q}, thus it is still a failure of the output process. In the latter subcase, @{term ys} has to be deprived of the events that may be affected by @{term x}, as well as by any event affected by @{term x} in the involved portion of @{term xs}, and a similar transformation applies to @{term Y}. In order that the output process be secure, the resulting pair @{term "(ys'', Y'')"} must still be a failure of @{term Q}, so that the pair @{term "(xs' @ ys'', Y'')"}, where @{term xs'} results from the transformation of @{term xs}, be a failure of the output process. The transformations bringing from @{term ys} and @{term Y} to @{term ys''} and @{term Y''} are implemented by the functions @{term ipurge_tr_aux} and @{term ipurge_ref_aux} defined in \<^cite>‹"R3"›. Therefore, the proof of the target security conservation theorem requires that of the following lemma: given a process @{term P}, a noninterference policy @{term I}, and an event-domain map @{term D}, if @{term P} is secure with respect to @{term I} and @{term D} and @{term "(xs, X)"} is a failure of @{term P}, then @{term "(ipurge_tr_aux I D U xs, ipurge_ref_aux I D U xs X)"} is still a failure of @{term P}. In other words, the lemma states that the failures of a secure process are closed under intransitive purge. This section contains a proof of such closure lemma, as well as further definitions and lemmas required for the proof of the target theorem. Throughout this paper, the salient points of definitions and proofs are commented; for additional information, cf. Isabelle documentation, particularly \<^cite>‹"R6"›, \<^cite>‹"R7"›, \<^cite>‹"R8"›, and \<^cite>‹"R9"›. › subsection "Preliminary propaedeutic lemmas" text ‹ In what follows, some lemmas required for the demonstration of the target closure lemma are proven. Here below is the proof of some properties of functions @{term ipurge_tr} and @{term ipurge_ref}. \null › lemma ipurge_tr_length: "length (ipurge_tr I D u xs) ≤ length xs" by (induction xs rule: rev_induct, simp_all) lemma ipurge_ref_swap: "ipurge_ref I D u xs {x ∈ X. P x} = {x ∈ ipurge_ref I D u xs X. P x}" proof (simp add: ipurge_ref_def) qed blast lemma ipurge_ref_last: "ipurge_ref I D u (xs @ [x]) X = (if (u, D x) ∈ I ∨ (∃v ∈ sinks I D u xs. (v, D x) ∈ I) then ipurge_ref I D u xs {x' ∈ X. (D x, D x') ∉ I} else ipurge_ref I D u xs X)" proof (cases "(u, D x) ∈ I ∨ (∃v ∈ sinks I D u xs. (v, D x) ∈ I)", simp_all add: ipurge_ref_def) qed blast text ‹ \null Here below is the proof of some properties of function @{term sinks_aux}. \null › lemma sinks_aux_append: "sinks_aux I D U (xs @ ys) = sinks_aux I D (sinks_aux I D U xs) ys" proof (induction ys rule: rev_induct, simp, subst append_assoc [symmetric]) qed (simp del: append_assoc) lemma sinks_aux_union: "sinks_aux I D (U ∪ V) xs = sinks_aux I D U xs ∪ sinks_aux I D V (ipurge_tr_aux I D U xs)" proof (induction xs rule: rev_induct, simp) fix x xs assume A: "sinks_aux I D (U ∪ V) xs = sinks_aux I D U xs ∪ sinks_aux I D V (ipurge_tr_aux I D U xs)" show "sinks_aux I D (U ∪ V) (xs @ [x]) = sinks_aux I D U (xs @ [x]) ∪ sinks_aux I D V (ipurge_tr_aux I D U (xs @ [x]))" proof (cases "∃w ∈ sinks_aux I D (U ∪ V) xs. (w, D x) ∈ I") case True hence "∃w ∈ sinks_aux I D U xs ∪ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I" using A by simp hence "(∃w ∈ sinks_aux I D U xs. (w, D x) ∈ I) ∨ (∃w ∈ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I)" by blast thus ?thesis using A and True by (cases "∃w ∈ sinks_aux I D U xs. (w, D x) ∈ I", simp_all) next case False hence "¬ (∃w ∈ sinks_aux I D U xs ∪ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I)" using A by simp hence "¬ (∃w ∈ sinks_aux I D U xs. (w, D x) ∈ I) ∧ ¬ (∃w ∈ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I)" by blast thus ?thesis using A and False by simp qed qed lemma sinks_aux_subset_dom: assumes A: "U ⊆ V" shows "sinks_aux I D U xs ⊆ sinks_aux I D V xs" proof (induction xs rule: rev_induct, simp add: A, rule subsetI) fix x xs w assume B: "sinks_aux I D U xs ⊆ sinks_aux I D V xs" and C: "w ∈ sinks_aux I D U (xs @ [x])" show "w ∈ sinks_aux I D V (xs @ [x])" proof (cases "∃u ∈ sinks_aux I D U xs. (u, D x) ∈ I") case True hence "w = D x ∨ w ∈ sinks_aux I D U xs" using C by simp moreover { assume D: "w = D x" obtain u where E: "u ∈ sinks_aux I D U xs" and F: "(u, D x) ∈ I" using True .. have "u ∈ sinks_aux I D V xs" using B and E .. with F have "∃u ∈ sinks_aux I D V xs. (u, D x) ∈ I" .. hence ?thesis using D by simp } moreover { assume "w ∈ sinks_aux I D U xs" with B have "w ∈ sinks_aux I D V xs" .. hence ?thesis by simp } ultimately show ?thesis .. next case False hence "w ∈ sinks_aux I D U xs" using C by simp with B have "w ∈ sinks_aux I D V xs" .. thus ?thesis by simp qed qed lemma sinks_aux_subset_ipurge_tr_aux: "sinks_aux I D U (ipurge_tr_aux I' D' U' xs) ⊆ sinks_aux I D U xs" proof (induction xs rule: rev_induct, simp, rule subsetI) fix x xs w assume A: "sinks_aux I D U (ipurge_tr_aux I' D' U' xs) ⊆ sinks_aux I D U xs" and B: "w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' (xs @ [x]))" show "w ∈ sinks_aux I D U (xs @ [x])" proof (cases "∃u ∈ sinks_aux I D U xs. (u, D x) ∈ I", simp_all (no_asm_simp)) from B have "w = D x ∨ w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs)" proof (cases "∃u' ∈ sinks_aux I' D' U' xs. (u', D' x) ∈ I'", simp_all) qed (cases "∃u ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs). (u, D x) ∈ I", simp_all) moreover { assume "w = D x" hence "w = D x ∨ w ∈ sinks_aux I D U xs" .. } moreover { assume "w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs)" with A have "w ∈ sinks_aux I D U xs" .. hence "w = D x ∨ w ∈ sinks_aux I D U xs" .. } ultimately show "w = D x ∨ w ∈ sinks_aux I D U xs" .. next assume C: "¬ (∃u ∈ sinks_aux I D U xs. (u, D x) ∈ I)" have "w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs)" proof (cases "∃u' ∈ sinks_aux I' D' U' xs. (u', D' x) ∈ I'") case True thus "w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs)" using B by simp next case False hence "w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs @ [x])" using B by simp moreover have "¬ (∃u ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs). (u, D x) ∈ I)" (is "¬ ?P") proof assume ?P then obtain u where D: "u ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs)" and E: "(u, D x) ∈ I" .. have "u ∈ sinks_aux I D U xs" using A and D .. with E have "∃u ∈ sinks_aux I D U xs. (u, D x) ∈ I" .. thus False using C by contradiction qed ultimately show "w ∈ sinks_aux I D U (ipurge_tr_aux I' D' U' xs)" by simp qed with A show "w ∈ sinks_aux I D U xs" .. qed qed lemma sinks_aux_subset_ipurge_tr: "sinks_aux I D U (ipurge_tr I' D' u' xs) ⊆ sinks_aux I D U xs" by (simp add: ipurge_tr_aux_single_dom [symmetric] sinks_aux_subset_ipurge_tr_aux) lemma sinks_aux_member_ipurge_tr_aux [rule_format]: "u ∈ sinks_aux I D (U ∪ V) xs ⟶ (u, w) ∈ I ⟶ ¬ (∃v ∈ sinks_aux I D V xs. (v, w) ∈ I) ⟶ u ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" proof (induction xs arbitrary: u w rule: rev_induct, (rule_tac [!] impI)+, simp) fix u w assume A: "(u, w) ∈ I" and B: "∀v ∈ V. (v, w) ∉ I" assume "u ∈ U ∨ u ∈ V" moreover { assume "u ∈ U" } moreover { assume "u ∈ V" with B have "(u, w) ∉ I" .. hence "u ∈ U" using A by contradiction } ultimately show "u ∈ U" .. next fix x xs u w assume A: "⋀u w. u ∈ sinks_aux I D (U ∪ V) xs ⟶ (u, w) ∈ I ⟶ ¬ (∃v ∈ sinks_aux I D V xs. (v, w) ∈ I) ⟶ u ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" and B: "u ∈ sinks_aux I D (U ∪ V) (xs @ [x])" and C: "(u, w) ∈ I" and D: "¬ (∃v ∈ sinks_aux I D V (xs @ [x]). (v, w) ∈ I)" show "u ∈ sinks_aux I D U (ipurge_tr_aux I D V (xs @ [x]))" proof (cases "∃u' ∈ sinks_aux I D (U ∪ V) xs. (u', D x) ∈ I") case True hence "u = D x ∨ u ∈ sinks_aux I D (U ∪ V) xs" using B by simp moreover { assume E: "u = D x" obtain u' where "u' ∈ sinks_aux I D (U ∪ V) xs" and F: "(u', D x) ∈ I" using True .. moreover have "u' ∈ sinks_aux I D (U ∪ V) xs ⟶ (u', D x) ∈ I ⟶ ¬ (∃v ∈ sinks_aux I D V xs. (v, D x) ∈ I) ⟶ u' ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" (is "_ ⟶ _ ⟶ ¬ ?P ⟶ ?Q") using A . ultimately have "¬ ?P ⟶ ?Q" by simp moreover have "¬ ?P" proof have "(D x, w) ∈ I" using C and E by simp moreover assume ?P hence "D x ∈ sinks_aux I D V (xs @ [x])" by simp ultimately have "∃v ∈ sinks_aux I D V (xs @ [x]). (v, w) ∈ I" .. moreover have "¬ (∃v ∈ sinks_aux I D V (xs @ [x]). (v, w) ∈ I)" using D by simp ultimately show False by contradiction qed ultimately have ?Q .. with F have "∃u' ∈ sinks_aux I D U (ipurge_tr_aux I D V xs). (u', D x) ∈ I" .. hence "D x ∈ sinks_aux I D U (ipurge_tr_aux I D V xs @ [x])" by simp moreover have "ipurge_tr_aux I D V xs @ [x] = ipurge_tr_aux I D V (xs @ [x])" using ‹¬ ?P› by simp ultimately have ?thesis using E by simp } moreover { assume "u ∈ sinks_aux I D (U ∪ V) xs" moreover have "u ∈ sinks_aux I D (U ∪ V) xs ⟶ (u, w) ∈ I ⟶ ¬ (∃v ∈ sinks_aux I D V xs. (v, w) ∈ I) ⟶ u ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" (is "_ ⟶ _ ⟶ ¬ ?P ⟶ ?Q") using A . ultimately have "¬ ?P ⟶ ?Q" using C by simp moreover have "¬ ?P" proof assume ?P hence "∃v ∈ sinks_aux I D V (xs @ [x]). (v, w) ∈ I" by simp thus False using D by contradiction qed ultimately have "u ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" .. hence ?thesis by simp } ultimately show ?thesis .. next case False hence "u ∈ sinks_aux I D (U ∪ V) xs" using B by simp moreover have "u ∈ sinks_aux I D (U ∪ V) xs ⟶ (u, w) ∈ I ⟶ ¬ (∃v ∈ sinks_aux I D V xs. (v, w) ∈ I) ⟶ u ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" (is "_ ⟶ _ ⟶ ¬ ?P ⟶ ?Q") using A . ultimately have "¬ ?P ⟶ ?Q" using C by simp moreover have "¬ ?P" proof assume ?P hence "∃v ∈ sinks_aux I D V (xs @ [x]). (v, w) ∈ I" by simp thus False using D by contradiction qed ultimately have "u ∈ sinks_aux I D U (ipurge_tr_aux I D V xs)" .. thus ?thesis by simp qed qed lemma sinks_aux_member_ipurge_tr: assumes A: "u ∈ sinks_aux I D (insert v U) xs" and B: "(u, w) ∈ I" and C: "¬ ((v, w) ∈ I ∨ (∃v' ∈ sinks I D v xs. (v', w) ∈ I))" shows "u ∈ sinks_aux I D U (ipurge_tr I D v xs)" proof (subst ipurge_tr_aux_single_dom [symmetric], rule_tac w = w in sinks_aux_member_ipurge_tr_aux) show "u ∈ sinks_aux I D (U ∪ {v}) xs" using A by simp next show "(u, w) ∈ I" using B . next show "¬ (∃v' ∈ sinks_aux I D {v} xs. (v', w) ∈ I)" using C by (simp add: sinks_aux_single_dom) qed text ‹ \null Here below is the proof of some properties of functions @{term ipurge_tr_aux} and @{term ipurge_ref_aux}. \null › lemma ipurge_tr_aux_append: "ipurge_tr_aux I D U (xs @ ys) = ipurge_tr_aux I D U xs @ ipurge_tr_aux I D (sinks_aux I D U xs) ys" proof (induction ys rule: rev_induct, simp, subst append_assoc [symmetric]) qed (simp add: sinks_aux_append del: append_assoc) lemma ipurge_tr_aux_single_event: "ipurge_tr_aux I D U [x] = (if ∃v ∈ U. (v, D x) ∈ I then [] else [x])" by (subst (2) append_Nil [symmetric], simp del: append_Nil) lemma ipurge_tr_aux_cons: "ipurge_tr_aux I D U (x # xs) = (if ∃u ∈ U. (u, D x) ∈ I then ipurge_tr_aux I D (insert (D x) U) xs else x # ipurge_tr_aux I D U xs)" proof - have "ipurge_tr_aux I D U (x # xs) = ipurge_tr_aux I D U ([x] @ xs)" by simp also have "… = ipurge_tr_aux I D U [x] @ ipurge_tr_aux I D (sinks_aux I D U [x]) xs" by (simp only: ipurge_tr_aux_append) finally show ?thesis by (simp add: sinks_aux_single_event ipurge_tr_aux_single_event) qed lemma ipurge_tr_aux_union: "ipurge_tr_aux I D (U ∪ V) xs = ipurge_tr_aux I D V (ipurge_tr_aux I D U xs)" proof (induction xs rule: rev_induct, simp) fix x xs assume A: "ipurge_tr_aux I D (U ∪ V) xs = ipurge_tr_aux I D V (ipurge_tr_aux I D U xs)" show "ipurge_tr_aux I D (U ∪ V) (xs @ [x]) = ipurge_tr_aux I D V (ipurge_tr_aux I D U (xs @ [x]))" proof (cases "∃v ∈ sinks_aux I D (U ∪ V) xs. (v, D x) ∈ I") case True hence "∃w ∈ sinks_aux I D U xs ∪ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I" by (simp add: sinks_aux_union) hence "(∃w ∈ sinks_aux I D U xs. (w, D x) ∈ I) ∨ (∃w ∈ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I)" by blast thus ?thesis using A and True by (cases "∃w ∈ sinks_aux I D U xs. (w, D x) ∈ I", simp_all) next case False hence "¬ (∃w ∈ sinks_aux I D U xs ∪ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I)" by (simp add: sinks_aux_union) hence "¬ (∃w ∈ sinks_aux I D U xs. (w, D x) ∈ I) ∧ ¬ (∃w ∈ sinks_aux I D V (ipurge_tr_aux I D U xs). (w, D x) ∈ I)" by blast thus ?thesis using A and False by simp qed qed lemma ipurge_tr_aux_insert: "ipurge_tr_aux I D (insert v U) xs = ipurge_tr_aux I D U (ipurge_tr I D v xs)" by (subst insert_is_Un, simp only: ipurge_tr_aux_union ipurge_tr_aux_single_dom) lemma ipurge_ref_aux_subset: "ipurge_ref_aux I D U xs X ⊆ X" by (subst ipurge_ref_aux_def, rule subsetI, simp) subsection "Intransitive purge of event sets with trivial base case" text ‹ Here below are the definitions of variants of functions @{term sinks_aux} and @{term ipurge_ref_aux}, respectively named ‹sinks_aux_less› and ‹ipurge_ref_aux_less›, such that their base cases in correspondence with an empty input list are trivial, viz. such that @{term "sinks_aux_less I D U [] = {}"} and @{term "ipurge_ref_aux_less I D U [] X = X"}. These functions will prove to be useful in what follows. \null › function sinks_aux_less :: "('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ 'd set ⇒ 'a list ⇒ 'd set" where "sinks_aux_less _ _ _ [] = {}" | "sinks_aux_less I D U (xs @ [x]) = (if ∃v ∈ U ∪ sinks_aux_less I D U xs. (v, D x) ∈ I then insert (D x) (sinks_aux_less I D U xs) else sinks_aux_less I D U xs)" proof (atomize_elim, simp_all add: split_paired_all) qed (rule rev_cases, rule disjI1, assumption, simp) termination by lexicographic_order definition ipurge_ref_aux_less :: "('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ 'd set ⇒ 'a list ⇒ 'a set ⇒ 'a set" where "ipurge_ref_aux_less I D U xs X ≡ {x ∈ X. ∀v ∈ sinks_aux_less I D U xs. (v, D x) ∉ I}" text ‹ \null Here below is the proof of some properties of function @{term sinks_aux_less} used in what follows. \null › lemma sinks_aux_sinks_aux_less: "sinks_aux I D U xs = U ∪ sinks_aux_less I D U xs" by (induction xs rule: rev_induct, simp_all) lemma sinks_aux_less_single_dom: "sinks_aux_less I D {u} xs = sinks I D u xs" by (induction xs rule: rev_induct, simp_all) lemma sinks_aux_less_single_event: "sinks_aux_less I D U [x] = (if ∃u ∈ U. (u, D x) ∈ I then {D x} else {})" by (subst append_Nil [symmetric], simp del: append_Nil) lemma sinks_aux_less_append: "sinks_aux_less I D U (xs @ ys) = sinks_aux_less I D U xs ∪ sinks_aux_less I D (U ∪ sinks_aux_less I D U xs) ys" proof (induction ys rule: rev_induct, simp, subst append_assoc [symmetric]) qed (simp del: append_assoc) lemma sinks_aux_less_cons: "sinks_aux_less I D U (x # xs) = (if ∃u ∈ U. (u, D x) ∈ I then insert (D x) (sinks_aux_less I D (insert (D x) U) xs) else sinks_aux_less I D U xs)" proof - have "sinks_aux_less I D U (x # xs) = sinks_aux_less I D U ([x] @ xs)" by simp also have "… = sinks_aux_less I D U [x] ∪ sinks_aux_less I D (U ∪ sinks_aux_less I D U [x]) xs" by (simp only: sinks_aux_less_append) finally show ?thesis by (cases "∃u ∈ U. (u, D x) ∈ I", simp_all add: sinks_aux_less_single_event) qed text ‹ \null Here below is the proof of some properties of function @{term ipurge_ref_aux_less} used in what follows. \null › lemma ipurge_ref_aux_less_last: "ipurge_ref_aux_less I D U (xs @ [x]) X = (if ∃v ∈ U ∪ sinks_aux_less I D U xs. (v, D x) ∈ I then ipurge_ref_aux_less I D U xs {x' ∈ X. (D x, D x') ∉ I} else ipurge_ref_aux_less I D U xs X)" by (cases "∃v ∈ U ∪ sinks_aux_less I D U xs. (v, D x) ∈ I", simp_all add: ipurge_ref_aux_less_def) lemma ipurge_ref_aux_less_nil: "ipurge_ref_aux_less I D U xs (ipurge_ref_aux I D U [] X) = ipurge_ref_aux I D U xs X" proof (simp add: ipurge_ref_aux_def ipurge_ref_aux_less_def sinks_aux_sinks_aux_less) qed blast lemma ipurge_ref_aux_less_cons_1: assumes A: "∃u ∈ U. (u, D x) ∈ I" shows "ipurge_ref_aux_less I D U (x # xs) X = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs) (ipurge_ref I D (D x) xs X)" proof (induction xs arbitrary: X rule: rev_induct, simp add: ipurge_ref_def ipurge_ref_aux_less_def sinks_aux_less_single_event A) fix x' xs X assume B: "⋀X. ipurge_ref_aux_less I D U (x # xs) X = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs) (ipurge_ref I D (D x) xs X)" show "ipurge_ref_aux_less I D U (x # xs @ [x']) X = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) (xs @ [x'])) (ipurge_ref I D (D x) (xs @ [x']) X)" proof (cases "∃v ∈ U ∪ sinks_aux_less I D U (x # xs). (v, D x') ∈ I") assume C: "∃v ∈ U ∪ sinks_aux_less I D U (x # xs). (v, D x') ∈ I" hence "ipurge_ref_aux_less I D U (x # xs @ [x']) X = ipurge_ref_aux_less I D U (x # xs) {y ∈ X. (D x', D y) ∉ I}" by (subst append_Cons [symmetric], simp add: ipurge_ref_aux_less_last del: append_Cons) also have "… = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs) (ipurge_ref I D (D x) xs {y ∈ X. (D x', D y) ∉ I})" using B . finally have D: "ipurge_ref_aux_less I D U (x # xs @ [x']) X = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs) (ipurge_ref I D (D x) xs {y ∈ X. (D x', D y) ∉ I})" . show ?thesis proof (cases "(D x, D x') ∈ I ∨ (∃v ∈ sinks I D (D x) xs. (v, D x') ∈ I)") case True hence "ipurge_ref I D (D x) xs {y ∈ X. (D x', D y) ∉ I} = ipurge_ref I D (D x) (xs @ [x']) X" by (simp add: ipurge_ref_last) moreover have "D x' ∈ sinks I D (D x) (xs @ [x'])" using True by (simp only: sinks_interference_eq) hence "ipurge_tr I D (D x) xs = ipurge_tr I D (D x) (xs @ [x'])" by simp ultimately show ?thesis using D by simp next case False hence "ipurge_ref I D (D x) xs {y ∈ X. (D x', D y) ∉ I} = ipurge_ref I D (D x) (xs @ [x']) {y ∈ X. (D x', D y) ∉ I}" by (simp add: ipurge_ref_last) also have "… = {y ∈ ipurge_ref I D (D x) (xs @ [x']) X. (D x', D y) ∉ I}" by (simp add: ipurge_ref_swap) finally have "ipurge_ref_aux_less I D U (x # xs @ [x']) X = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs) {y ∈ ipurge_ref I D (D x) (xs @ [x']) X. (D x', D y) ∉ I}" using D by simp also have "… = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs @ [x']) (ipurge_ref I D (D x) (xs @ [x']) X)" proof - have "∃v ∈ U ∪ sinks_aux_less I D U (ipurge_tr I D (D x) xs). (v, D x') ∈ I" proof - obtain v where E: "v ∈ U ∪ sinks_aux_less I D U (x # xs)" and F: "(v, D x') ∈ I" using C .. have "v ∈ sinks_aux I D U (x # xs)" using E by (simp add: sinks_aux_sinks_aux_less) hence "v ∈ sinks_aux I D (insert (D x) U) xs" using A by (simp add: sinks_aux_cons) hence "v ∈ sinks_aux I D U (ipurge_tr I D (D x) xs)" using F and False by (rule sinks_aux_member_ipurge_tr) hence "v ∈ U ∪ sinks_aux_less I D U (ipurge_tr I D (D x) xs)" by (simp add: sinks_aux_sinks_aux_less) with F show ?thesis .. qed thus ?thesis by (simp add: ipurge_ref_aux_less_last) qed finally have "ipurge_ref_aux_less I D U (x # xs @ [x']) X = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs @ [x']) (ipurge_ref I D (D x) (xs @ [x']) X)" . moreover have "D x' ∉ sinks I D (D x) (xs @ [x'])" using False by (simp only: sinks_interference_eq, simp) hence "ipurge_tr I D (D x) xs @ [x'] = ipurge_tr I D (D x) (xs @ [x'])" by simp ultimately show ?thesis by simp qed next assume C: "¬ (∃v ∈ U ∪ sinks_aux_less I D U (x # xs). (v, D x') ∈ I)" hence "ipurge_ref_aux_less I D U (x # xs @ [x']) X = ipurge_ref_aux_less I D U (x # xs) X" by (subst append_Cons [symmetric], simp add: ipurge_ref_aux_less_last del: append_Cons) also have "… = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs) (ipurge_ref I D (D x) xs X)" using B . also have "… = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) xs @ [x']) (ipurge_ref I D (D x) xs X)" proof - have "¬ (∃v ∈ U ∪ sinks_aux_less I D U (ipurge_tr I D (D x) xs). (v, D x') ∈ I)" (is "¬ ?P") proof assume ?P then obtain v where D: "v ∈ U ∪ sinks_aux_less I D U (ipurge_tr I D (D x) xs)" and E: "(v, D x') ∈ I" .. have "sinks_aux I D U (ipurge_tr I D (D x) xs) ⊆ sinks_aux I D U xs" by (rule sinks_aux_subset_ipurge_tr) moreover have "v ∈ sinks_aux I D U (ipurge_tr I D (D x) xs)" using D by (simp add: sinks_aux_sinks_aux_less) ultimately have "v ∈ sinks_aux I D U xs" .. moreover have "U ⊆ insert (D x) U" by (rule subset_insertI) hence "sinks_aux I D U xs ⊆ sinks_aux I D (insert (D x) U) xs" by (rule sinks_aux_subset_dom) ultimately have "v ∈ sinks_aux I D (insert (D x) U) xs" .. hence "v ∈ sinks_aux I D U (x # xs)" using A by (simp add: sinks_aux_cons) hence "v ∈ U ∪ sinks_aux_less I D U (x # xs)" by (simp add: sinks_aux_sinks_aux_less) with E have "∃v ∈ U ∪ sinks_aux_less I D U (x # xs). (v, D x') ∈ I" .. thus False using C by contradiction qed thus ?thesis by (simp add: ipurge_ref_aux_less_last) qed also have "… = ipurge_ref_aux_less I D U (ipurge_tr I D (D x) (xs @ [x'])) (ipurge_ref I D (D x) (xs @ [x']) X)" proof - have "¬ ((D x, D x') ∈ I ∨ (∃v ∈ sinks I D (D x) xs. (v, D x') ∈ I))" (is "¬ ?P") proof (rule notI, erule disjE) assume D: "(D x, D x') ∈ I" have "insert (D x) U ⊆ sinks_aux I D (insert (D x) U) xs" by (rule sinks_aux_subset) moreover have "D x ∈ insert (D x) U" by simp ultimately have "D x ∈ sinks_aux I D (insert (D x) U) xs" .. hence "D x ∈ sinks_aux I D U (x # xs)" using A by (simp add: sinks_aux_cons) hence "D x ∈ U ∪ sinks_aux_less I D U (x # xs)" by (simp add: sinks_aux_sinks_aux_less) with D have "∃v ∈ U ∪ sinks_aux_less I D U (x # xs). (v, D x') ∈ I" .. thus False using C by contradiction next assume "∃v ∈ sinks I D (D x) xs. (v, D x') ∈ I" then obtain v where D: "v ∈ sinks I D (D x) xs" and E: "(v, D x') ∈ I" .. have "{D x} ⊆ insert (D x) U" by simp hence "sinks_aux I D {D x} xs ⊆ sinks_aux I D (insert (D x) U) xs" by (rule sinks_aux_subset_dom) moreover have "v ∈ sinks_aux I D {D x} xs" using D by (simp add: sinks_aux_single_dom) ultimately have "v ∈ sinks_aux I D (insert (D x) U) xs" .. hence "v ∈ sinks_aux I D U (x # xs)" using A by (simp add: sinks_aux_cons) hence "v ∈ U ∪ sinks_aux_less I D U (x # xs)" by (simp add: sinks_aux_sinks_aux_less) with E have "∃v ∈ U ∪ sinks_aux_less I D U (x # xs). (v, D x') ∈ I" .. thus False using C by contradiction qed hence "ipurge_tr I D (D x) xs @ [x'] = ipurge_tr I D (D x) (xs @ [x'])" by (simp only: sinks_interference_eq, simp) moreover have "ipurge_ref I D (D x) xs X = ipurge_ref I D (D x) (xs @ [x']) X" using ‹¬ ?P› by (simp add: ipurge_ref_last) ultimately show ?thesis by simp qed finally show ?thesis . qed qed lemma ipurge_ref_aux_less_cons_2: "¬ (∃u ∈ U. (u, D x) ∈ I) ⟹ ipurge_ref_aux_less I D U (x # xs) X = ipurge_ref_aux_less I D U xs X" by (simp add: ipurge_ref_aux_less_def sinks_aux_less_cons) subsection "Closure of the failures of a secure process under intransitive purge" text ‹ The intransitive purge of an event list @{term xs} with regard to a policy @{term I}, an event-domain map @{term D}, and a set of domains @{term U} can equivalently be computed as follows: for each item @{term x} of @{term xs}, if @{term x} may be affected by some domain in @{term U}, discard @{term x} and go on recursively using @{term "ipurge_tr I D (D x) xs'"} as input, where @{term xs'} is the sublist of @{term xs} following @{term x}; otherwise, retain @{term x} and go on recursively using @{term xs'} as input. In fact, in each recursive step, any item allowed to be indirectly affected by @{term U} through the effect of some item preceding @{term x} within @{term xs} has already been removed from the list. Hence, it is sufficient to check whether @{term x} may be directly affected by @{term U}, and remove @{term x}, as well as any residual item allowed to be affected by @{term x}, if this is the case. Similarly, the intransitive purge of an event set @{term X} with regard to a policy @{term I}, an event-domain map @{term D}, a set of domains @{term U}, and an event list @{term xs} can be computed as follows. First of all, compute @{term "ipurge_ref_aux I D U [] X"} and use this set, along with @{term xs}, as the input for the subsequent step. Then, for each item @{term x} of @{term xs}, if @{term x} may be affected by some domain in @{term U}, go on recursively using @{term "ipurge_tr I D (D x) xs'"} and @{term "ipurge_ref I D (D x) xs' X'"} as input, where @{term X'} is the set input to the current recursive step; otherwise, go on recursively using @{term xs'} and @{term X'} as input. In fact, in each recursive step, any item allowed to be affected by @{term U} either directly, or through the effect of some item preceding @{term x} within @{term xs}, has already been removed from the set (in the initial step and in subsequent steps, respectively). Thus, it is sufficient to check whether @{term x} may be directly affected by @{term U}, and remove any residual item allowed to be affected by @{term x} if this is the case. Assume that the two computations be performed simultaneously by a single function, which will then take as input an event list-event set pair and return as output another such pair. Then, if the input pair is a failure of a secure process, the output pair is still a failure. In fact, for each item @{term x} of @{term xs} allowed to be affected by @{term U}, if @{term ys} is the partial output list for the sublist of @{term xs} preceding @{term x}, then @{term "(ys @ ipurge_tr I D (D x) xs', ipurge_ref I D (D x) xs' X')"} is a failure provided that such is @{term "(ys @ x # xs', X')"}, by virtue of the definition of CSP noninterference security \<^cite>‹"R2"›. Hence, the property of being a failure is conserved upon each recursive call by the event list-event set pair such that the list matches the concatenation of the partial output list with the residual input list, and the set matches the residual input set. This holds until the residual input list is nil, which is the base case determining the end of the computation. As shown by this argument, a proof by induction that the output event list-event set pair, under the aforesaid assumptions, is still a failure, requires that the partial output list be passed to the function as a further argument, in addition to the residual input list, in the recursive calls contained within the definition of the function. Therefore, the output list has to be accumulated into a parameter of the function, viz. the function needs to be tail-recursive. This suggests to prove the properties of interest of the function by applying the ten-step proof method for theorems on tail-recursive functions described in \<^cite>‹"R1"›. The starting point is to formulate a naive definition of the function, which will then be refined as specified by the proof method. A slight complication is due to the preliminary replacement of the input event set @{term X} with @{term "ipurge_ref_aux I D U [] X"}, to be performed before the items of the input event list start to be consumed recursively. A simple solution to this problem is to nest the accumulator of the output list within data type ‹option›. In this way, the initial state can be distinguished from the subsequent one, in which the input event list starts to be consumed, by assigning the distinct values @{term None} and @{term "Some []"}, respectively, to the accumulator. Everything is now ready for giving a naive definition of the function under consideration: \null › function (sequential) ipurge_fail_aux_t_naive :: "('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ 'd set ⇒ 'a list ⇒ 'a list option ⇒ 'a set ⇒ 'a failure" where "ipurge_fail_aux_t_naive I D U xs None X = ipurge_fail_aux_t_naive I D U xs (Some []) (ipurge_ref_aux I D U [] X)" | "ipurge_fail_aux_t_naive I D U (x # xs) (Some ys) X = (if ∃u ∈ U. (u, D x) ∈ I then ipurge_fail_aux_t_naive I D U (ipurge_tr I D (D x) xs) (Some ys) (ipurge_ref I D (D x) xs X) else ipurge_fail_aux_t_naive I D U xs (Some (ys @ [x])) X)" | "ipurge_fail_aux_t_naive _ _ _ _ (Some ys) X = (ys, X)" oops text ‹ \null The parameter into which the output list is accumulated is the last but one. As shown by the above informal argument, function ‹ipurge_fail_aux_t_naive› enjoys the following properties: \null @{term "fst (ipurge_fail_aux_t_naive I D U xs None X) = ipurge_tr_aux I D U xs"} \null @{term "snd (ipurge_fail_aux_t_naive I D U xs None X) = ipurge_ref_aux I D U xs X"} \null @{term "⟦secure P I D; (xs, X) ∈ failures P⟧ ⟹ ipurge_fail_aux_t_naive I D U xs None X ∈ failures P"} \null which altogether imply the target lemma, viz. the closure of the failures of a secure process under intransitive purge. In what follows, the steps provided for by the aforesaid proof method will be dealt with one after the other, with the purpose of proving the target closure lemma in the final step. For more information on this proof method, cf. \<^cite>‹"R1"›. › subsubsection "Step 1" text ‹ In the definition of the auxiliary tail-recursive function ‹ipurge_fail_aux_t_aux›, the Cartesian product of the input parameter types of function ‹ipurge_fail_aux_t_naive› will be implemented as the following record type: \null ›