Theory SequentialComposition
section "Sequential composition and noninterference security"
theory SequentialComposition
imports Propaedeutics
begin
text ‹
\null
This section formalizes the definitions of sequential processes and sequential composition given in
\<^cite>‹"R4"›, and then proves that under the assumptions discussed above, noninterference security is
conserved under sequential composition for any pair of processes sharing an alphabet that contains
successful termination. Finally, this result is generalized to an arbitrary list of processes.
›
subsection "Sequential processes"
text ‹
In \<^cite>‹"R4"›, a \emph{sequential process} is defined as a process whose alphabet contains successful
termination. Since sequential composition applies to sequential processes, the first problem put by
the formalization of this operation is that of finding a suitable way to represent such a process.
A simple but effective strategy is to identify it with a process having alphabet @{typ "'a option"},
where @{typ 'a} is the native type of its ordinary (i.e. distinct from termination) events. Then,
ordinary events will be those matching pattern ‹Some _›, whereas successful termination will
be denoted by the special event @{term None}. This means that the \emph{sentences} of a sequential
process, defined in \<^cite>‹"R4"› as the traces after which the process can terminate successfully, will
be nothing but the event lists @{term xs} such that @{term "xs @ [None]"} is a trace (which implies
that @{term xs} is a trace as well).
Once a suitable representation of successful termination has been found, the next step is to
formalize the properties of sequential processes related to this event, expressing them in terms of
the selected representation. The first of the resulting predicates, ‹weakly_sequential›, is
the minimum required for allowing the identification of event @{term None} with successful
termination, namely that @{term None} may occur in a trace as its last event only. The second
predicate, ‹sequential›, following what Hoare does in \<^cite>‹"R4"›, extends the first predicate
with an additional requirement, namely that whenever the process can engage in event @{term None},
it cannot engage in any other event. A simple counterexample shows that this requirement does not
imply the first one: a process whose traces are @{term "{[], [None], [None, None]}"} satisfies the
second requirement, but not the first one.
Moreover, here below is the definition of a further predicate, ‹secure_termination›, which
applies to a security policy rather than to a process, and is satisfied just in case the policy does
not allow event @{term None} to be affected by confidential events, viz. by ordinary events not
allowed to affect some event in the alphabet. Interestingly, this property, which will prove to be
necessary for the target theorem to hold, is nothing but the CSP counterpart of a condition required
for a security type system to enforce termination-sensitive noninterference security of programs,
namely that program termination must not depend on confidential data (cf. \<^cite>‹"R5"›, section 9.2.6).
\null
›
definition sentences :: "'a option process ⇒ 'a option list set" where
"sentences P ≡ {xs. xs @ [None] ∈ traces P}"
definition weakly_sequential :: "'a option process ⇒ bool" where
"weakly_sequential P ≡
∀xs ∈ traces P. None ∉ set (butlast xs)"
definition sequential :: "'a option process ⇒ bool" where
"sequential P ≡
(∀xs ∈ traces P. None ∉ set (butlast xs)) ∧
(∀xs ∈ sentences P. next_events P xs = {None})"
definition secure_termination :: "('d × 'd) set ⇒ ('a option ⇒ 'd) ⇒ bool" where
"secure_termination I D ≡
∀x. (D x, D None) ∈ I ∧ x ≠ None ⟶ (∀u ∈ range D. (D x, u) ∈ I)"
text ‹
\null
Here below is the proof of some useful lemmas involving the constants just defined. Particularly, it
is proven that process sequentiality is indeed stronger than weak sequentiality, and a sentence of a
refusals union closed (cf. \<^cite>‹"R3"›), sequential process admits the set of all the ordinary events
of the process as a refusal. The use of the latter lemma in the proof of the target security
conservation theorem is the reason why the theorem requires to assume that the first of the
processes to be composed be refusals union closed (cf. below).
\null
›
lemma seq_implies_weakly_seq:
"sequential P ⟹ weakly_sequential P"
by (simp add: weakly_sequential_def sequential_def)
lemma weakly_seq_sentences_none:
assumes
WS: "weakly_sequential P" and
A: "xs ∈ sentences P"
shows "None ∉ set xs"
proof -
have "∀xs ∈ traces P. None ∉ set (butlast xs)"
using WS by (simp add: weakly_sequential_def)
moreover have "xs @ [None] ∈ traces P"
using A by (simp add: sentences_def)
ultimately have "None ∉ set (butlast (xs @ [None]))" ..
thus ?thesis
by simp
qed
lemma seq_sentences_none:
assumes
S: "sequential P" and
A: "xs ∈ sentences P" and
B: "xs @ y # ys ∈ traces P"
shows "y = None"
proof -
have "∀xs ∈ sentences P. next_events P xs = {None}"
using S by (simp add: sequential_def)
hence "next_events P xs = {None}"
using A ..
moreover have "(xs @ [y]) @ ys ∈ traces P"
using B by simp
hence "xs @ [y] ∈ traces P"
by (rule process_rule_2_traces)
hence "y ∈ next_events P xs"
by (simp add: next_events_def)
ultimately show ?thesis
by simp
qed
lemma seq_sentences_ref:
assumes
A: "ref_union_closed P" and
B: "sequential P" and
C: "xs ∈ sentences P"
shows "(xs, {x. x ≠ None}) ∈ failures P"
(is "(_, ?X) ∈ _")
proof -
have "(∃X. X ∈ singleton_set ?X) ⟶
(∀X ∈ singleton_set ?X. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ singleton_set ?X. X) ∈ failures P"
using A by (simp add: ref_union_closed_def)
moreover have "∃x. x ∈ ?X"
by blast
hence "∃X. X ∈ singleton_set ?X"
by (simp add: singleton_set_some)
ultimately have "(∀X ∈ singleton_set ?X. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ singleton_set ?X. X) ∈ failures P" ..
moreover have "∀X ∈ singleton_set ?X. (xs, X) ∈ failures P"
proof (rule ballI, simp add: singleton_set_def del: not_None_eq,
erule exE, erule conjE, simp (no_asm_simp))
fix x :: "'a option"
assume D: "x ≠ None"
have "xs @ [None] ∈ traces P"
using C by (simp add: sentences_def)
hence "xs ∈ traces P"
by (rule process_rule_2_traces)
hence "(xs, {}) ∈ failures P"
by (rule traces_failures)
hence "(xs @ [x], {}) ∈ failures P ∨ (xs, {x}) ∈ failures P"
by (rule process_rule_4)
thus "(xs, {x}) ∈ failures P"
proof (rule disjE, rule_tac ccontr, simp_all)
assume "(xs @ [x], {}) ∈ failures P"
hence "xs @ [x] ∈ traces P"
by (rule failures_traces)
with B and C have "x = None"
by (rule seq_sentences_none)
thus False
using D by contradiction
qed
qed
ultimately have "(xs, ⋃X ∈ singleton_set ?X. X) ∈ failures P" ..
thus ?thesis
by (simp only: singleton_set_union)
qed
subsection "Sequential composition"
text ‹
In what follows, the definition of the failures resulting from the sequential composition of two
processes @{term P}, @{term Q} given in \<^cite>‹"R4"› is formalized as the inductive definition of set
‹seq_comp_failures P Q›. Then, the sequential composition of @{term P} and @{term Q},
denoted by means of notation ‹P ; Q› following \<^cite>‹"R4"›, is defined as the process having
‹seq_comp_failures P Q› as failures set and the empty set as divergences set.
For the sake of generality, this definition is based on the mere implicit assumption that the input
processes be weakly sequential, rather than sequential. This slightly complicates things, since the
sentences of process @{term P} may number further events in addition to @{term None} in their
future.
Therefore, the resulting refusals of a sentence @{term xs} of @{term P} will have the form
@{term "insert None X ∩ Y"}, where @{term X} is a refusal of @{term xs} in @{term P} and @{term Y}
is an initial refusal of @{term Q} (cf. rule ‹SCF_R2›). In fact, after @{term xs}, process
‹P ; Q› must be able to refuse @{term None} if @{term Q} is, whereas it cannot refuse an
ordinary event unless both @{term P} and @{term Q}, in their respective states, can.
Moreover, a trace @{term xs} of ‹P ; Q› may result from different combinations of a sentence
of @{term P} with a trace of @{term Q}. Thus, in order that the refusals of ‹P ; Q› be
closed under set union, the union of any two refusals of @{term xs} must still be a refusal (cf.
rule ‹SCF_R4›). Indeed, this property will prove to be sufficient to ensure that for any two
processes whose refusals are closed under set union, their sequential composition still be such,
which is what is expected for any process of practical significance (cf. \<^cite>‹"R3"›).
According to the definition given in \<^cite>‹"R4"›, a divergence of ‹P ; Q› is either a
divergence of @{term P}, or the concatenation of a sentence of @{term P} with a divergence of
@{term Q}. Apparently, this definition does not match the formal one stated here below, which
identifies the divergences set of ‹P ; Q› with the empty set. Nonetheless, as remarked
above, sequential composition does not make sense unless the input processes are weakly sequential,
since this is the minimum required to confer the meaning of successful termination on the
corresponding alphabet symbol. But a weakly sequential process cannot have any divergence, so that
the two definitions are actually equivalent. In fact, a divergence is a trace such that, however it
is extended with arbitrary additional events, the resulting event list is still a trace (cf. process
properties @{term process_prop_5} and @{term process_prop_6} in \<^cite>‹"R2"›). Therefore, if @{term xs}
were a divergence, then @{term "xs @ [None, None]"} would be a trace, which is impossible in case
the process satisfies predicate @{term weakly_sequential}.
\null
›
inductive_set seq_comp_failures ::
"'a option process ⇒ 'a option process ⇒ 'a option failure set"
for P :: "'a option process" and Q :: "'a option process" where
SCF_R1: "⟦xs ∉ sentences P; (xs, X) ∈ failures P; None ∉ set xs⟧ ⟹
(xs, X) ∈ seq_comp_failures P Q" |
SCF_R2: "⟦xs ∈ sentences P; (xs, X) ∈ failures P; ([], Y) ∈ failures Q⟧ ⟹
(xs, insert None X ∩ Y) ∈ seq_comp_failures P Q" |
SCF_R3: "⟦xs ∈ sentences P; (ys, Y) ∈ failures Q; ys ≠ []⟧ ⟹
(xs @ ys, Y) ∈ seq_comp_failures P Q" |
SCF_R4: "⟦(xs, X) ∈ seq_comp_failures P Q; (xs, Y) ∈ seq_comp_failures P Q⟧ ⟹
(xs, X ∪ Y) ∈ seq_comp_failures P Q"
definition seq_comp ::
"'a option process ⇒ 'a option process ⇒ 'a option process" (infixl ";" 60)
where
"P ; Q ≡ Abs_process (seq_comp_failures P Q, {})"
text ‹
\null
Here below is the proof that, for any two processes @{term P}, @{term Q} defined over the same
alphabet containing successful termination, set @{term "seq_comp_failures P Q"} indeed enjoys the
characteristic properties of the failures set of a process as defined in \<^cite>‹"R2"› provided that
@{term P} is weakly sequential, which is what happens in any meaningful case.
\null
›
lemma seq_comp_prop_1:
"([], {}) ∈ seq_comp_failures P Q"
proof (cases "[] ∈ sentences P")
case False
moreover have "([], {}) ∈ failures P"
by (rule process_rule_1)
moreover have "None ∉ set []"
by simp
ultimately show ?thesis
by (rule SCF_R1)
next
case True
moreover have "([], {}) ∈ failures P"
by (rule process_rule_1)
moreover have "([], {}) ∈ failures Q"
by (rule process_rule_1)
ultimately have "([], {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
lemma seq_comp_prop_2_aux [rule_format]:
assumes WS: "weakly_sequential P"
shows "(ws, X) ∈ seq_comp_failures P Q ⟹
ws = xs @ [x] ⟶ (xs, {}) ∈ seq_comp_failures P Q"
proof (erule seq_comp_failures.induct, rule_tac [!] impI, simp_all, erule conjE)
fix X'
assume
A: "(xs @ [x], X') ∈ failures P" and
B: "None ∉ set xs"
have A': "(xs, {}) ∈ failures P"
using A by (rule process_rule_2)
show "(xs, {}) ∈ seq_comp_failures P Q"
proof (cases "xs ∈ sentences P")
case False
thus ?thesis
using A' and B by (rule SCF_R1)
next
case True
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with True and A' have "(xs, {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
next
fix X'
assume A: "(xs @ [x], X') ∈ failures P"
hence A': "(xs, {}) ∈ failures P"
by (rule process_rule_2)
show "(xs, {}) ∈ seq_comp_failures P Q"
proof (cases "xs ∈ sentences P")
case False
have "∀xs ∈ traces P. None ∉ set (butlast xs)"
using WS by (simp add: weakly_sequential_def)
moreover have "xs @ [x] ∈ traces P"
using A by (rule failures_traces)
ultimately have "None ∉ set (butlast (xs @ [x]))" ..
hence "None ∉ set xs" by simp
with False and A' show ?thesis
by (rule SCF_R1)
next
case True
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with True and A' have "(xs, {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
next
fix xs' ys Y
assume
A: "xs' @ ys = xs @ [x]" and
B: "xs' ∈ sentences P" and
C: "(ys, Y) ∈ failures Q" and
D: "ys ≠ []"
have "∃y ys'. ys = ys' @ [y]"
using D by (rule_tac xs = ys in rev_cases, simp_all)
then obtain y and ys' where D': "ys = ys' @ [y]"
by blast
hence "xs = xs' @ ys'"
using A by simp
thus "(xs, {}) ∈ seq_comp_failures P Q"
proof (cases "ys' = []", simp_all)
case True
have "xs' @ [None] ∈ traces P"
using B by (simp add: sentences_def)
hence "xs' ∈ traces P"
by (rule process_rule_2_traces)
hence "(xs', {}) ∈ failures P"
by (rule traces_failures)
moreover have "([], {}) ∈ failures Q"
by (rule process_rule_1)
ultimately have "(xs', {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2 [OF B])
thus "(xs', {}) ∈ seq_comp_failures P Q"
by simp
next
case False
have "(ys' @ [y], Y) ∈ failures Q"
using C and D' by simp
hence C': "(ys', {}) ∈ failures Q"
by (rule process_rule_2)
with B show "(xs' @ ys', {}) ∈ seq_comp_failures P Q"
using False by (rule SCF_R3)
qed
qed
lemma seq_comp_prop_2:
assumes WS: "weakly_sequential P"
shows "(xs @ [x], X) ∈ seq_comp_failures P Q ⟹
(xs, {}) ∈ seq_comp_failures P Q"
by (erule seq_comp_prop_2_aux [OF WS], simp)
lemma seq_comp_prop_3 [rule_format]:
"(xs, Y) ∈ seq_comp_failures P Q ⟹ X ⊆ Y ⟶
(xs, X) ∈ seq_comp_failures P Q"
proof (induction arbitrary: X rule: seq_comp_failures.induct, rule_tac [!] impI)
fix xs X Y
assume
A: "xs ∉ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "None ∉ set xs" and
D: "Y ⊆ X"
have "(xs, Y) ∈ failures P"
using B and D by (rule process_rule_3)
with A show "(xs, Y) ∈ seq_comp_failures P Q"
using C by (rule SCF_R1)
next
fix xs X Y Z
assume
A: "xs ∈ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "([], Y) ∈ failures Q" and
D: "Z ⊆ insert None X ∩ Y"
have "Z - {None} ⊆ X"
using D by blast
with B have "(xs, Z - {None}) ∈ failures P"
by (rule process_rule_3)
moreover have "Z ⊆ Y"
using D by simp
with C have "([], Z) ∈ failures Q"
by (rule process_rule_3)
ultimately have "(xs, insert None (Z - {None}) ∩ Z) ∈ seq_comp_failures P Q"
by (rule SCF_R2 [OF A])
moreover have "insert None (Z - {None}) ∩ Z = Z"
by blast
ultimately show "(xs, Z) ∈ seq_comp_failures P Q"
by simp
next
fix xs ys X Y
assume
A: "xs ∈ sentences P" and
B: "(ys, Y) ∈ failures Q" and
C: "ys ≠ []" and
D: "X ⊆ Y"
have "(ys, X) ∈ failures Q"
using B and D by (rule process_rule_3)
with A show "(xs @ ys, X) ∈ seq_comp_failures P Q"
using C by (rule SCF_R3)
next
fix xs X Y Z
assume
A: "⋀W. W ⊆ X ⟶ (xs, W) ∈ seq_comp_failures P Q" and
B: "⋀W. W ⊆ Y ⟶ (xs, W) ∈ seq_comp_failures P Q" and
C: "Z ⊆ X ∪ Y"
have "Z ∩ X ⊆ X ⟶ (xs, Z ∩ X) ∈ seq_comp_failures P Q"
using A .
hence "(xs, Z ∩ X) ∈ seq_comp_failures P Q"
by simp
moreover have "Z ∩ Y ⊆ Y ⟶ (xs, Z ∩ Y) ∈ seq_comp_failures P Q"
using B .
hence "(xs, Z ∩ Y) ∈ seq_comp_failures P Q"
by simp
ultimately have "(xs, Z ∩ X ∪ Z ∩ Y) ∈ seq_comp_failures P Q"
by (rule SCF_R4)
hence "(xs, Z ∩ (X ∪ Y)) ∈ seq_comp_failures P Q"
by (simp add: Int_Un_distrib)
moreover have "Z ∩ (X ∪ Y) = Z"
using C by (rule Int_absorb2)
ultimately show "(xs, Z) ∈ seq_comp_failures P Q"
by simp
qed
lemma seq_comp_prop_4:
assumes WS: "weakly_sequential P"
shows "(xs, X) ∈ seq_comp_failures P Q ⟹
(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x X) ∈ seq_comp_failures P Q"
proof (erule seq_comp_failures.induct, simp_all)
fix xs X
assume
A: "xs ∉ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "None ∉ set xs"
have "(xs @ [x], {}) ∈ failures P ∨
(xs, insert x X) ∈ failures P"
using B by (rule process_rule_4)
thus "(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x X) ∈ seq_comp_failures P Q"
proof
assume D: "(xs @ [x], {}) ∈ failures P"
show ?thesis
proof (cases "xs @ [x] ∈ sentences P")
case False
have "None ∉ set (xs @ [x])"
proof (simp add: C, rule notI)
assume "None = x"
hence "(xs @ [None], {}) ∈ failures P"
using D by simp
hence "xs @ [None] ∈ traces P"
by (rule failures_traces)
hence "xs ∈ sentences P"
by (simp add: sentences_def)
thus False
using A by contradiction
qed
with False and D have "(xs @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R1)
thus ?thesis ..
next
case True
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with True and D have "(xs @ [x], {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
qed
next
assume "(xs, insert x X) ∈ failures P"
with A have "(xs, insert x X) ∈ seq_comp_failures P Q"
using C by (rule SCF_R1)
thus ?thesis ..
qed
next
fix xs X Y
assume
A: "xs ∈ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "([], Y) ∈ failures Q"
show "(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
proof (cases "x = None", simp)
case True
have "([] @ [None], {}) ∈ failures Q ∨ ([], insert None Y) ∈ failures Q"
using C by (rule process_rule_4)
thus "(xs @ [None], {}) ∈ seq_comp_failures P Q ∨
(xs, insert None (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
proof (rule disjE, simp)
assume "([None], {}) ∈ failures Q"
moreover have "[None] ≠ []"
by simp
ultimately have "(xs @ [None], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF A])
thus ?thesis ..
next
assume "([], insert None Y) ∈ failures Q"
with A and B have "(xs, insert None X ∩ insert None Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2)
moreover have "insert None X ∩ insert None Y =
insert None (insert None X ∩ Y)"
by blast
ultimately have "(xs, insert None (insert None X ∩ Y))
∈ seq_comp_failures P Q"
by simp
thus ?thesis ..
qed
next
case False
have "(xs @ [x], {}) ∈ failures P ∨ (xs, insert x X) ∈ failures P"
using B by (rule process_rule_4)
thus ?thesis
proof (rule disjE, cases "xs @ [x] ∈ sentences P")
assume
D: "xs @ [x] ∉ sentences P" and
E: "(xs @ [x], {}) ∈ failures P"
have "None ∉ set xs"
using WS and A by (rule weakly_seq_sentences_none)
hence "None ∉ set (xs @ [x])"
using False by (simp del: not_None_eq)
with D and E have "(xs @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R1)
thus ?thesis ..
next
assume
"xs @ [x] ∈ sentences P" and
"(xs @ [x], {}) ∈ failures P"
moreover have "([], {}) ∈ failures Q"
by (rule process_rule_1)
ultimately have "(xs @ [x], {None} ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus ?thesis by simp
next
assume D: "(xs, insert x X) ∈ failures P"
have "([] @ [x], {}) ∈ failures Q ∨ ([], insert x Y) ∈ failures Q"
using C by (rule process_rule_4)
thus ?thesis
proof (rule disjE, simp)
assume "([x], {}) ∈ failures Q"
moreover have "[x] ≠ []"
by simp
ultimately have "(xs @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF A])
thus ?thesis ..
next
assume "([], insert x Y) ∈ failures Q"
with A and D have "(xs, insert None (insert x X) ∩ insert x Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2)
moreover have "insert None (insert x X) ∩ insert x Y =
insert x (insert None X ∩ Y)"
by blast
ultimately have "(xs, insert x (insert None X ∩ Y))
∈ seq_comp_failures P Q"
by simp
thus ?thesis ..
qed
qed
qed
next
fix xs ys Y
assume
A: "xs ∈ sentences P" and
B: "(ys, Y) ∈ failures Q" and
C: "ys ≠ []"
have "(ys @ [x], {}) ∈ failures Q ∨ (ys, insert x Y) ∈ failures Q"
using B by (rule process_rule_4)
thus "(xs @ ys @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs @ ys, insert x Y) ∈ seq_comp_failures P Q"
proof
assume "(ys @ [x], {}) ∈ failures Q"
moreover have "ys @ [x] ≠ []"
by simp
ultimately have "(xs @ ys @ [x], {}) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF A])
thus ?thesis ..
next
assume "(ys, insert x Y) ∈ failures Q"
with A have "(xs @ ys, insert x Y) ∈ seq_comp_failures P Q"
using C by (rule SCF_R3)
thus ?thesis ..
qed
next
fix xs X Y
assume
"(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x X) ∈ seq_comp_failures P Q" and
"(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x Y) ∈ seq_comp_failures P Q"
thus "(xs @ [x], {}) ∈ seq_comp_failures P Q ∨
(xs, insert x (X ∪ Y)) ∈ seq_comp_failures P Q"
proof (cases "(xs @ [x], {}) ∈ seq_comp_failures P Q", simp_all)
assume
"(xs, insert x X) ∈ seq_comp_failures P Q" and
"(xs, insert x Y) ∈ seq_comp_failures P Q"
hence "(xs, insert x X ∪ insert x Y) ∈ seq_comp_failures P Q"
by (rule SCF_R4)
thus "(xs, insert x (X ∪ Y)) ∈ seq_comp_failures P Q"
by simp
qed
qed
lemma seq_comp_rep:
assumes WS: "weakly_sequential P"
shows "Rep_process (P ; Q) = (seq_comp_failures P Q, {})"
proof (subst seq_comp_def, rule Abs_process_inverse, simp add: process_set_def,
(subst conj_assoc [symmetric])+, (rule conjI)+)
show "process_prop_1 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_1_def)
qed (rule seq_comp_prop_1)
next
show "process_prop_2 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_2_def del: all_simps, (rule allI)+, rule impI)
qed (rule seq_comp_prop_2 [OF WS])
next
show "process_prop_3 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_3_def del: all_simps, (rule allI)+, rule impI,
erule conjE)
qed (rule seq_comp_prop_3)
next
show "process_prop_4 (seq_comp_failures P Q, {})"
proof (simp add: process_prop_4_def, (rule allI)+, rule impI)
qed (rule seq_comp_prop_4 [OF WS])
next
show "process_prop_5 (seq_comp_failures P Q, {})"
by (simp add: process_prop_5_def)
next
show "process_prop_6 (seq_comp_failures P Q, {})"
by (simp add: process_prop_6_def)
qed
text ‹
\null
Here below, the previous result is applied to derive useful expressions for the outputs of the
functions returning the elements of a process, as defined in \<^cite>‹"R2"› and \<^cite>‹"R3"›, when acting on
the sequential composition of a pair of processes.
\null
›
lemma seq_comp_failures:
"weakly_sequential P ⟹
failures (P ; Q) = seq_comp_failures P Q"
by (drule seq_comp_rep [where Q = Q], simp add: failures_def)
lemma seq_comp_divergences:
"weakly_sequential P ⟹
divergences (P ; Q) = {}"
by (drule seq_comp_rep [where Q = Q], simp add: divergences_def)
lemma seq_comp_futures:
"weakly_sequential P ⟹
futures (P ; Q) xs = {(ys, Y). (xs @ ys, Y) ∈ seq_comp_failures P Q}"
by (simp add: futures_def seq_comp_failures)
lemma seq_comp_traces:
"weakly_sequential P ⟹
traces (P ; Q) = Domain (seq_comp_failures P Q)"
by (simp add: traces_def seq_comp_failures)
lemma seq_comp_refusals:
"weakly_sequential P ⟹
refusals (P ; Q) xs ≡ seq_comp_failures P Q `` {xs}"
by (simp add: refusals_def seq_comp_failures)
lemma seq_comp_next_events:
"weakly_sequential P ⟹
next_events (P ; Q) xs = {x. xs @ [x] ∈ Domain (seq_comp_failures P Q)}"
by (simp add: next_events_def seq_comp_traces)
subsection "Conservation of refusals union closure and sequentiality under sequential composition"
text ‹
Here below is the proof that, for any two processes @{term P}, @{term Q} and any failure
@{term "(xs, X)"} of @{term "P ; Q"}, the refusal @{term X} is the union of a set of refusals where,
for any such refusal @{term W}, @{term "(xs, W)"} is a failure of @{term "P ; Q"} by virtue of one
of rules ‹SCF_R1›, ‹SCF_R2›, or ‹SCF_R3›.
The converse is also proven, under the assumption that the refusals of both @{term P} and @{term Q}
be closed under union: namely, for any trace @{term xs} of @{term "P ; Q"} and any set of refusals
where, for any such refusal @{term W}, @{term "(xs, W)"} is a failure of the aforesaid kind, the
union of these refusals is still a refusal of @{term xs}.
The proof of the latter lemma makes use of the axiom of choice.
\null
›
lemma seq_comp_refusals_1:
"(xs, X) ∈ seq_comp_failures P Q ⟹ ∃R.
X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q) ∧
(∃n ∈ {..length xs}. ∃W. W ∈ R n)"
(is "_ ⟹ ∃R. ?T R xs X")
proof (erule seq_comp_failures.induct, (erule_tac [4] exE)+)
fix xs X
assume
A: "xs ∉ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "None ∉ set xs"
show "∃R. ?T R xs X"
proof (rule_tac x = "λn. if n = 0 then {X} else {}" in exI,
simp add: A B C, rule equalityI, rule_tac [!] subsetI, simp_all)
fix x
assume "∃n ∈ {..length xs}.
∃W ∈ if n = 0 then {X} else {}. x ∈ W"
thus "x ∈ X"
by (simp split: if_split_asm)
qed
next
fix xs X Y
assume
A: "xs ∈ sentences P" and
B: "(xs, X) ∈ failures P" and
C: "([], Y) ∈ failures Q"
show "∃R. ?T R xs (insert None X ∩ Y)"
proof (rule_tac x = "λn. if n = 0 then {insert None X ∩ Y} else {}" in exI,
simp add: A, rule conjI, rule equalityI, rule_tac [1-2] subsetI, simp_all)
fix x
assume "∃n ∈ {..length xs}.
∃W ∈ if n = 0 then {insert None X ∩ Y} else {}. x ∈ W"
thus "(x = None ∨ x ∈ X) ∧ x ∈ Y"
by (simp split: if_split_asm)
next
show "∃U. (xs, U) ∈ failures P ∧ (∃V. ([], V) ∈ failures Q ∧
insert None X ∩ Y = insert None U ∩ V)"
proof (rule_tac x = X in exI, rule conjI, simp add: B)
qed (rule_tac x = Y in exI, rule conjI, simp_all add: C)
qed
next
fix xs ys Y
assume
A: "xs ∈ sentences P" and
B: "(ys, Y) ∈ failures Q" and
C: "ys ≠ []"
show "∃R. ?T R (xs @ ys) Y"
proof (rule_tac x = "λn. if n = length ys then {Y} else {}" in exI,
simp add: A B C, rule equalityI, rule_tac [!] subsetI, simp_all)
fix x
assume "∃n ∈ {..length xs + length ys}.
∃W ∈ if n = length ys then {Y} else {}. x ∈ W"
thus "x ∈ Y"
by (simp split: if_split_asm)
qed
next
fix xs X Y Rx Ry
assume
A: "?T Rx xs X" and
B: "?T Ry xs Y"
show "∃R. ?T R xs (X ∪ Y)"
proof (rule_tac x = "λn. Rx n ∪ Ry n" in exI, rule conjI, rule_tac [2] conjI,
rule_tac [3] conjI, rule_tac [2] ballI, (rule_tac [3] ballI)+)
have "X ∪ Y = (⋃n ≤ length xs. ⋃W ∈ Rx n. W) ∪
(⋃n ≤ length xs. ⋃W ∈ Ry n. W)"
using A and B by simp
also have "… = (⋃n ≤ length xs. (⋃W ∈ Rx n. W) ∪ (⋃W ∈ Ry n. W))"
by blast
also have "… = (⋃n ≤ length xs. ⋃W ∈ Rx n ∪ Ry n. W)"
by simp
finally show "X ∪ Y = (⋃n ≤ length xs. ⋃W ∈ Rx n ∪ Ry n. W)" .
next
fix W
assume "W ∈ Rx 0 ∪ Ry 0"
thus
"xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "?T' W")
proof
have "∀W ∈ Rx 0. ?T' W"
using A by simp
moreover assume "W ∈ Rx 0"
ultimately show ?thesis ..
next
have "∀W ∈ Ry 0. ?T' W"
using B by simp
moreover assume "W ∈ Ry 0"
ultimately show ?thesis ..
qed
next
fix n W
assume C: "n ∈ {0<..length xs}"
assume "W ∈ Rx n ∪ Ry n"
thus
"take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q"
(is "?T' n W")
proof
have "∀n ∈ {0<..length xs}. ∀W ∈ Rx n. ?T' n W"
using A by simp
hence "∀W ∈ Rx n. ?T' n W"
using C ..
moreover assume "W ∈ Rx n"
ultimately show ?thesis ..
next
have "∀n ∈ {0<..length xs}. ∀W ∈ Ry n. ?T' n W"
using B by simp
hence "∀W ∈ Ry n. ?T' n W"
using C ..
moreover assume "W ∈ Ry n"
ultimately show ?thesis ..
qed
next
have "∃n ∈ {..length xs}. ∃W. W ∈ Rx n"
using A by simp
then obtain n where C: "n ∈ {..length xs}" and D: "∃W. W ∈ Rx n" ..
obtain W where "W ∈ Rx n"
using D ..
hence "W ∈ Rx n ∪ Ry n" ..
hence "∃W. W ∈ Rx n ∪ Ry n" ..
thus "∃n ∈ {..length xs}. ∃W. W ∈ Rx n ∪ Ry n"
using C ..
qed
qed
lemma seq_comp_refusals_finite [rule_format]:
assumes A: "xs ∈ Domain (seq_comp_failures P Q)"
shows "finite A ⟹ (∀x ∈ A. (xs, F x) ∈ seq_comp_failures P Q) ⟶
(xs, ⋃x ∈ A. F x) ∈ seq_comp_failures P Q"
proof (erule finite_induct, simp, rule_tac [2] impI)
have "∃X. (xs, X) ∈ seq_comp_failures P Q"
using A by (simp add: Domain_iff)
then obtain X where "(xs, X) ∈ seq_comp_failures P Q" ..
moreover have "{} ⊆ X" ..
ultimately show "(xs, {}) ∈ seq_comp_failures P Q"
by (rule seq_comp_prop_3)
next
fix x' A
assume B: "∀x ∈ insert x' A. (xs, F x) ∈ seq_comp_failures P Q"
hence "(xs, F x') ∈ seq_comp_failures P Q"
by simp
moreover assume "(∀x ∈ A. (xs, F x) ∈ seq_comp_failures P Q) ⟶
(xs, ⋃x ∈ A. F x) ∈ seq_comp_failures P Q"
hence "(xs, ⋃x ∈ A. F x) ∈ seq_comp_failures P Q"
using B by simp
ultimately have "(xs, F x' ∪ (⋃x ∈ A. F x)) ∈ seq_comp_failures P Q"
by (rule SCF_R4)
thus "(xs, ⋃x ∈ insert x' A. F x) ∈ seq_comp_failures P Q"
by simp
qed
lemma seq_comp_refusals_2:
assumes
A: "ref_union_closed P" and
B: "ref_union_closed Q" and
C: "xs ∈ Domain (seq_comp_failures P Q)" and
D: "X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q)"
shows "(xs, X) ∈ seq_comp_failures P Q"
proof -
have "∃Y. (xs, Y) ∈ seq_comp_failures P Q"
using C by (simp add: Domain_iff)
then obtain Y where "(xs, Y) ∈ seq_comp_failures P Q" ..
moreover have "{} ⊆ Y" ..
ultimately have E: "(xs, {}) ∈ seq_comp_failures P Q"
by (rule seq_comp_prop_3)
have "(xs, ⋃W ∈ R 0. W) ∈ seq_comp_failures P Q"
proof (cases "∃W. W ∈ R 0", cases "xs ∈ sentences P")
assume "¬ (∃W. W ∈ R 0)"
thus ?thesis
using E by simp
next
assume
F: "∃W. W ∈ R 0" and
G: "xs ∉ sentences P"
have H: "∀W ∈ R 0. None ∉ set xs ∧ (xs, W) ∈ failures P"
using D and G by simp
show ?thesis
proof (rule SCF_R1 [OF G])
have "∀xs A. (∃W. W ∈ A) ⟶ (∀W ∈ A. (xs, W) ∈ failures P) ⟶
(xs, ⋃W ∈ A. W) ∈ failures P"
using A by (simp add: ref_union_closed_def)
hence "(∃W. W ∈ R 0) ⟶ (∀W ∈ R 0. (xs, W) ∈ failures P) ⟶
(xs, ⋃W ∈ R 0. W) ∈ failures P"
by blast
thus "(xs, ⋃W ∈ R 0. W) ∈ failures P"
using F and H by simp
next
obtain W where "W ∈ R 0" using F ..
thus "None ∉ set xs"
using H by simp
qed
next
assume
F: "∃W. W ∈ R 0" and
G: "xs ∈ sentences P"
have "∀W ∈ R 0. ∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V"
using D and G by simp
hence "∃F. ∀W ∈ R 0. ∃V. (xs, F W) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None (F W) ∩ V"
by (rule bchoice)
then obtain F where "∀W ∈ R 0.
∃V. (xs, F W) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None (F W) ∩ V" ..
hence "∃G. ∀W ∈ R 0. (xs, F W) ∈ failures P ∧ ([], G W) ∈ failures Q ∧
W = insert None (F W) ∩ G W"
by (rule bchoice)
then obtain G where H: "∀W ∈ R 0.
(xs, F W) ∈ failures P ∧ ([], G W) ∈ failures Q ∧
W = insert None (F W) ∩ G W" ..
have "(xs, insert None (⋃W ∈ R 0. F W) ∩ (⋃W ∈ R 0. G W))
∈ seq_comp_failures P Q"
(is "(_, ?S) ∈ _")
proof (rule SCF_R2 [OF G])
have "∀xs A. (∃X. X ∈ A) ⟶ (∀X ∈ A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ A. X) ∈ failures P"
using A by (simp add: ref_union_closed_def)
hence "(∃X. X ∈ F ` R 0) ⟶ (∀X ∈ F ` R 0. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ F ` R 0. X) ∈ failures P"
(is "?A ⟶ ?B ⟶ ?C")
by (erule_tac x = xs in allE, erule_tac x = "F ` R 0" in allE)
moreover obtain W where "W ∈ R 0" using F ..
hence ?A
proof (simp add: image_def, rule_tac x = "F W" in exI)
qed (rule bexI, simp)
ultimately have "?B ⟶ ?C" ..
moreover have ?B
proof (rule ballI, simp add: image_def, erule bexE)
fix W X
assume "W ∈ R 0"
hence "(xs, F W) ∈ failures P"
using H by simp
moreover assume "X = F W"
ultimately show "(xs, X) ∈ failures P"
by simp
qed
ultimately have ?C ..
thus "(xs, ⋃W ∈ R 0. F W) ∈ failures P"
by simp
next
have "∀xs A. (∃Y. Y ∈ A) ⟶ (∀Y ∈ A. (xs, Y) ∈ failures Q) ⟶
(xs, ⋃Y ∈ A. Y) ∈ failures Q"
using B by (simp add: ref_union_closed_def)
hence "(∃Y. Y ∈ G ` R 0) ⟶ (∀Y ∈ G ` R 0. ([], Y) ∈ failures Q) ⟶
([], ⋃Y ∈ G ` R 0. Y) ∈ failures Q"
(is "?A ⟶ ?B ⟶ ?C")
by (erule_tac x = "[]" in allE, erule_tac x = "G ` R 0" in allE)
moreover obtain W where "W ∈ R 0" using F ..
hence ?A
proof (simp add: image_def, rule_tac x = "G W" in exI)
qed (rule bexI, simp)
ultimately have "?B ⟶ ?C" ..
moreover have ?B
proof (rule ballI, simp add: image_def, erule bexE)
fix W Y
assume "W ∈ R 0"
hence "([], G W) ∈ failures Q"
using H by simp
moreover assume "Y = G W"
ultimately show "([], Y) ∈ failures Q"
by simp
qed
ultimately have ?C ..
thus "([], ⋃W ∈ R 0. G W) ∈ failures Q"
by simp
qed
moreover have "(⋃W ∈ R 0. W) ⊆ ?S"
proof (rule subsetI, simp, erule bexE)
fix x W
assume I: "W ∈ R 0"
hence "W = insert None (F W) ∩ G W"
using H by simp
moreover assume "x ∈ W"
ultimately have "x ∈ insert None (F W) ∩ G W"
by simp
thus "(x = None ∨ (∃W ∈ R 0. x ∈ F W)) ∧ (∃W ∈ R 0. x ∈ G W)"
(is "?A ∧ ?B")
proof (rule IntE, simp)
assume "x = None ∨ x ∈ F W"
moreover {
assume "x = None"
hence ?A ..
}
moreover {
assume "x ∈ F W"
hence "∃W ∈ R 0. x ∈ F W" using I ..
hence ?A ..
}
ultimately have ?A ..
moreover assume "x ∈ G W"
hence ?B using I ..
ultimately show ?thesis ..
qed
qed
ultimately show ?thesis
by (rule seq_comp_prop_3)
qed
moreover have "∀n ∈ {0<..length xs}.
(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
proof
fix n
assume F: "n ∈ {0<..length xs}"
hence G: "∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q"
using D by simp
show "(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
proof (cases "∃W. W ∈ R n")
case False
thus ?thesis
using E by simp
next
case True
have "(take (length xs - n) xs @ drop (length xs - n) xs, ⋃W ∈ R n. W)
∈ seq_comp_failures P Q"
proof (rule SCF_R3)
obtain W where "W ∈ R n" using True ..
thus "take (length xs - n) xs ∈ sentences P"
using G by simp
next
have "∀xs A. (∃W. W ∈ A) ⟶ (∀W ∈ A. (xs, W) ∈ failures Q) ⟶
(xs, ⋃W ∈ A. W) ∈ failures Q"
using B by (simp add: ref_union_closed_def)
hence "(∃W. W ∈ R n) ⟶
(∀W ∈ R n. (drop (length xs - n) xs, W) ∈ failures Q) ⟶
(drop (length xs - n) xs, ⋃W ∈ R n. W) ∈ failures Q"
by blast
thus "(drop (length xs - n) xs, ⋃W ∈ R n. W) ∈ failures Q"
using G and True by simp
next
show "drop (length xs - n) xs ≠ []"
using F by (simp, arith)
qed
thus ?thesis
by simp
qed
qed
ultimately have F: "∀n ∈ {..length xs}.
(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
by auto
have "(xs, ⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∈ seq_comp_failures P Q"
proof (rule seq_comp_refusals_finite [OF C], simp)
fix n
assume "n ∈ {..length xs}"
with F show "(xs, ⋃W ∈ R n. W) ∈ seq_comp_failures P Q" ..
qed
moreover have "X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W)"
using D by simp
ultimately show ?thesis
by simp
qed
text ‹
\null
In what follows, the previous results are used to prove that refusals union closure, weak
sequentiality, and sequentiality are conserved under sequential composition. The proof of the first
of these lemmas makes use of the axiom of choice.
Since the target security conservation theorem, in addition to the security of both of the processes
to be composed, also requires to assume that the first process be refusals union closed and
sequential (cf. below), these further conservation lemmas will permit to generalize the theorem to
the sequential composition of an arbitrary list of processes.
\null
›
lemma seq_comp_ref_union_closed:
assumes
WS: "weakly_sequential P" and
A: "ref_union_closed P" and
B: "ref_union_closed Q"
shows "ref_union_closed (P ; Q)"
proof (simp only: ref_union_closed_def seq_comp_failures [OF WS],
(rule allI)+, (rule impI)+, erule exE)
fix xs A X'
assume
C: "∀X ∈ A. (xs, X) ∈ seq_comp_failures P Q" and
D: "X' ∈ A"
have "∀X ∈ A. ∃R.
X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q)"
(is "∀X ∈ A. ∃R. ?T R X")
proof
fix X
assume "X ∈ A"
with C have "(xs, X) ∈ seq_comp_failures P Q" ..
hence "∃R. X = (⋃n ∈ {..length xs}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length xs}. ∀W ∈ R n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q) ∧
(∃n ∈ {..length xs}. ∃W. W ∈ R n)"
by (rule seq_comp_refusals_1)
thus "∃R. ?T R X"
by blast
qed
hence "∃R. ∀X ∈ A. ?T (R X) X"
by (rule bchoice)
then obtain R where E: "∀X ∈ A. ?T (R X) X" ..
have "xs ∈ Domain (seq_comp_failures P Q)"
proof (simp add: Domain_iff)
have "(xs, X') ∈ seq_comp_failures P Q"
using C and D ..
thus "∃X. (xs, X) ∈ seq_comp_failures P Q" ..
qed
moreover have "?T (λn. ⋃X ∈ A. R X n) (⋃X ∈ A. X)"
proof (rule conjI, rule_tac [2] conjI)
show "(⋃X ∈ A. X) = (⋃n ∈ {..length xs}. ⋃W ∈ ⋃X ∈ A. R X n. W)"
proof (rule equalityI, rule_tac [!] subsetI, simp_all,
erule bexE, (erule_tac [2] bexE)+)
fix x X
assume F: "X ∈ A"
hence "X = (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
using E by simp
moreover assume "x ∈ X"
ultimately have "x ∈ (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
by simp
hence "∃n ∈ {..length xs}. ∃W ∈ R X n. x ∈ W"
by simp
hence "∃X ∈ A. ∃n ∈ {..length xs}. ∃W ∈ R X n. x ∈ W"
using F ..
thus "∃n ∈ {..length xs}. ∃X ∈ A. ∃W ∈ R X n. x ∈ W"
by blast
next
fix x n X W
assume F: "X ∈ A"
hence G: "X = (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
using E by simp
assume "x ∈ W" and "W ∈ R X n"
hence "∃W ∈ R X n. x ∈ W" ..
moreover assume "n ∈ {..length xs}"
ultimately have "∃n ∈ {..length xs}. ∃W ∈ R X n. x ∈ W" ..
hence "x ∈ (⋃n ∈ {..length xs}. ⋃W ∈ R X n. W)"
by simp
hence "x ∈ X"
by (subst G)
thus "∃X ∈ A. x ∈ X"
using F ..
qed
next
show "∀W ∈ ⋃X ∈ A. R X 0.
xs ∉ sentences P ∧ None ∉ set xs ∧ (xs, W) ∈ failures P ∨
xs ∈ sentences P ∧ (∃U V. (xs, U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "∀W ∈ _. ?T W")
proof (rule ballI, simp only: UN_iff, erule bexE)
fix W X
assume "X ∈ A"
hence "∀W ∈ R X 0. ?T W"
using E by simp
moreover assume "W ∈ R X 0"
ultimately show "?T W" ..
qed
next
show "∀n ∈ {0<..length xs}. ∀W ∈ ⋃X ∈ A. R X n.
take (length xs - n) xs ∈ sentences P ∧
(drop (length xs - n) xs, W) ∈ failures Q"
(is "∀n ∈ _. ∀W ∈ _. ?T n W")
proof ((rule ballI)+, simp only: UN_iff, erule bexE)
fix n W X
assume "X ∈ A"
hence "∀n ∈ {0<..length xs}. ∀W ∈ R X n. ?T n W"
using E by simp
moreover assume "n ∈ {0<..length xs}"
ultimately have "∀W ∈ R X n. ?T n W" ..
moreover assume "W ∈ R X n"
ultimately show "?T n W" ..
qed
qed
ultimately show "(xs, ⋃X ∈ A. X) ∈ seq_comp_failures P Q"
by (rule seq_comp_refusals_2 [OF A B])
qed
lemma seq_comp_weakly_sequential:
assumes
A: "weakly_sequential P" and
B: "weakly_sequential Q"
shows "weakly_sequential (P ; Q)"
proof (subst weakly_sequential_def, rule ballI, drule traces_failures,
subst (asm) seq_comp_failures [OF A], erule seq_comp_failures.induct, simp_all)
fix xs :: "'a option list"
assume C: "None ∉ set xs"
show "None ∉ set (butlast xs)"
proof
assume "None ∈ set (butlast xs)"
hence "None ∈ set xs"
by (rule in_set_butlastD)
thus False
using C by contradiction
qed
next
fix xs
assume "xs ∈ sentences P"
with A have C: "None ∉ set xs"
by (rule weakly_seq_sentences_none)
show "None ∉ set (butlast xs)"
proof
assume "None ∈ set (butlast xs)"
hence "None ∈ set xs"
by (rule in_set_butlastD)
thus False
using C by contradiction
qed
next
fix xs ys Y
assume "xs ∈ sentences P"
with A have C: "None ∉ set xs"
by (rule weakly_seq_sentences_none)
have "∀xs ∈ traces Q. None ∉ set (butlast xs)"
using B by (simp add: weakly_sequential_def)
moreover assume "(ys, Y) ∈ failures Q"
hence "ys ∈ traces Q"
by (rule failures_traces)
ultimately have "None ∉ set (butlast ys)" ..
hence "None ∉ set (xs @ butlast ys)"
using C by simp
moreover assume "ys ≠ []"
hence "butlast (xs @ ys) = xs @ butlast ys"
by (simp add: butlast_append)
ultimately show "None ∉ set (butlast (xs @ ys))"
by simp
qed
lemma seq_comp_sequential:
assumes
A: "sequential P" and
B: "sequential Q"
shows "sequential (P ; Q)"
proof (subst sequential_def, rule conjI)
have "weakly_sequential P"
using A by (rule seq_implies_weakly_seq)
moreover have "weakly_sequential Q"
using B by (rule seq_implies_weakly_seq)
ultimately have "weakly_sequential (P ; Q)"
by (rule seq_comp_weakly_sequential)
thus "∀xs ∈ traces (P ; Q). None ∉ set (butlast xs)"
by (simp add: weakly_sequential_def)
next
have C: "weakly_sequential P"
using A by (rule seq_implies_weakly_seq)
show "∀xs ∈ sentences (P ; Q). next_events (P ; Q) xs = {None}"
proof (rule ballI, simp add: sentences_def next_events_def, rule equalityI,
rule_tac [!] subsetI, simp_all, (drule traces_failures)+,
simp add: seq_comp_failures [OF C])
fix xs x
assume
D: "(xs @ [None], {}) ∈ seq_comp_failures P Q" and
E: "(xs @ [x], {}) ∈ seq_comp_failures P Q"
have "∃R. {} = (⋃n ∈ {..length (xs @ [None])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [None] ∉ sentences P ∧
None ∉ set (xs @ [None]) ∧ (xs @ [None], W) ∈ failures P ∨
xs @ [None] ∈ sentences P ∧
(∃U V. (xs @ [None], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [None])}. ∀W ∈ R n.
take (length (xs @ [None]) - n) (xs @ [None]) ∈ sentences P ∧
(drop (length (xs @ [None]) - n) (xs @ [None]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [None])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using D by (rule seq_comp_refusals_1)
then obtain R where F: "?T R" ..
hence "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R n"
by simp
moreover have "R 0 = {}"
proof (rule equals0I)
fix W
assume "W ∈ R 0"
hence "xs @ [None] ∈ sentences P"
using F by simp
with C have "None ∉ set (xs @ [None])"
by (rule weakly_seq_sentences_none)
thus False
by simp
qed
ultimately have "∃n ∈ {0<..Suc (length xs)}. ∃W. W ∈ R n"
proof -
assume "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R n"
then obtain n where G: "n ∈ {..Suc (length xs)}" and H: "∃W. W ∈ R n" ..
assume I: "R 0 = {}"
show "∃n ∈ {0<..Suc (length xs)}. ∃W. W ∈ R n"
proof (cases n)
case 0
hence "∃W. W ∈ R 0"
using H by simp
then obtain W where "W ∈ R 0" ..
moreover have "W ∉ R 0"
using I by (rule equals0D)
ultimately show ?thesis
by contradiction
next
case (Suc m)
hence "n ∈ {0<..Suc (length xs)}"
using G by simp
with H show ?thesis ..
qed
qed
then obtain n and W where G: "n ∈ {0<..Suc (length xs)}" and "W ∈ R n"
by blast
hence
"take (Suc (length xs) - n) (xs @ [None]) ∈ sentences P ∧
(drop (Suc (length xs) - n) (xs @ [None]), W) ∈ failures Q"
using F by simp
moreover have H: "Suc (length xs) - n ≤ length xs"
using G by (simp, arith)
ultimately have I:
"take (Suc (length xs) - n) xs ∈ sentences P ∧
(drop (Suc (length xs) - n) xs @ [None], W) ∈ failures Q"
by simp
have "∃R. {} = (⋃n ∈ {..length (xs @ [x])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [x] ∉ sentences P ∧
None ∉ set (xs @ [x]) ∧ (xs @ [x], W) ∈ failures P ∨
xs @ [x] ∈ sentences P ∧
(∃U V. (xs @ [x], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [x])}. ∀W ∈ R n.
take (length (xs @ [x]) - n) (xs @ [x]) ∈ sentences P ∧
(drop (length (xs @ [x]) - n) (xs @ [x]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [x])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using E by (rule seq_comp_refusals_1)
then obtain R' where J: "?T R'" ..
hence "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R' n"
by simp
then obtain n' where K: "n' ∈ {..Suc (length xs)}" and L: "∃W. W ∈ R' n'" ..
have "n' = 0 ∨ n' ∈ {0<..Suc (length xs)}"
using K by auto
thus "x = None"
proof
assume "n' = 0"
hence "∃W. W ∈ R' 0"
using L by simp
then obtain W' where "W' ∈ R' 0" ..
hence
"xs @ [x] ∉ sentences P ∧
None ∉ set (xs @ [x]) ∧ (xs @ [x], W') ∈ failures P ∨
xs @ [x] ∈ sentences P ∧
(∃U V. (xs @ [x], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W' = insert None U ∩ V)"
using J by simp
hence M: "xs @ [x] ∈ traces P ∧ None ∉ set (xs @ [x])"
proof (cases "xs @ [x] ∈ sentences P", simp_all, (erule_tac [2] conjE)+,
simp_all)
case False
assume "(xs @ [x], W') ∈ failures P"
thus "xs @ [x] ∈ traces P"
by (rule failures_traces)
next
case True
hence "(xs @ [x]) @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "xs @ [x] ∈ traces P"
by (rule process_rule_2_traces)
moreover have "None ∉ set (xs @ [x])"
using C and True by (rule weakly_seq_sentences_none)
ultimately show "xs @ [x] ∈ traces P ∧ None ≠ x ∧ None ∉ set xs"
by simp
qed
have "xs @ [x] = take (Suc (length xs) - n) (xs @ [x]) @
drop (Suc (length xs) - n) (xs @ [x])"
by (simp only: append_take_drop_id)
hence "xs @ [x] = take (Suc (length xs) - n) xs @
drop (Suc (length xs) - n) xs @ [x]"
using H by simp
moreover have "∃y ys. drop (Suc (length xs) - n) xs @ [x] = y # ys"
by (cases "drop (Suc (length xs) - n) xs @ [x]", simp_all)
then obtain y and ys where "drop (Suc (length xs) - n) xs @ [x] = y # ys"
by blast
ultimately have N: "xs @ [x] = take (Suc (length xs) - n) xs @ y # ys"
by simp
have "take (Suc (length xs) - n) xs ∈ sentences P"
using I ..
moreover have "take (Suc (length xs) - n) xs @ y # ys ∈ traces P"
using M and N by simp
ultimately have "y = None"
by (rule seq_sentences_none [OF A])
moreover have "y ≠ None"
using M and N by (rule_tac not_sym, simp)
ultimately show ?thesis
by contradiction
next
assume M: "n' ∈ {0<..Suc (length xs)}"
moreover obtain W' where "W' ∈ R' n'"
using L ..
ultimately have
"take (Suc (length xs) - n') (xs @ [x]) ∈ sentences P ∧
(drop (Suc (length xs) - n') (xs @ [x]), W') ∈ failures Q"
using J by simp
moreover have N: "Suc (length xs) - n' ≤ length xs"
using M by (simp, arith)
ultimately have O:
"take (Suc (length xs) - n') xs ∈ sentences P ∧
(drop (Suc (length xs) - n') xs @ [x], W') ∈ failures Q"
by simp
moreover have "n = n'"
proof (rule ccontr, simp add: neq_iff, erule disjE)
assume P: "n < n'"
have "take (Suc (length xs) - n) xs =
take (Suc (length xs) - n') (take (Suc (length xs) - n) xs) @
drop (Suc (length xs) - n') (take (Suc (length xs) - n) xs)"
by (simp only: append_take_drop_id)
also have "… =
take (Suc (length xs) - n') xs @
drop (Suc (length xs) - n') (take (Suc (length xs) - n) xs)"
using P by (simp add: min_def)
also have "… =
take (Suc (length xs) - n') xs @
take (n' - n) (drop (Suc (length xs) - n') xs)"
using M by (subst drop_take, simp)
finally have "take (Suc (length xs) - n) xs =
take (Suc (length xs) - n') xs @
take (n' - n) (drop (Suc (length xs) - n') xs)" .
moreover have "take (n' - n) (drop (Suc (length xs) - n') xs) ≠ []"
proof (rule_tac notI, simp, erule disjE)
assume "n' ≤ n"
thus False
using P by simp
next
assume "length xs ≤ Suc (length xs) - n'"
moreover have "Suc (length xs) - n' < Suc (length xs) - n"
using M and P by simp
hence "Suc (length xs) - n' < length xs"
using H by simp
ultimately show False
by simp
qed
hence "∃y ys. take (n' - n) (drop (Suc (length xs) - n') xs) = y # ys"
by (cases "take (n' - n) (drop (Suc (length xs) - n') xs)", simp_all)
then obtain y and ys where
"take (n' - n) (drop (Suc (length xs) - n') xs) = y # ys"
by blast
ultimately have Q: "take (Suc (length xs) - n) xs =
take (Suc (length xs) - n') xs @ y # ys"
by simp
have "take (Suc (length xs) - n') xs ∈ sentences P"
using O ..
moreover have R: "take (Suc (length xs) - n) xs ∈ sentences P"
using I ..
hence "take (Suc (length xs) - n) xs @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "take (Suc (length xs) - n) xs ∈ traces P"
by (rule process_rule_2_traces)
hence "take (Suc (length xs) - n') xs @ y # ys ∈ traces P"
using Q by simp
ultimately have "y = None"
by (rule seq_sentences_none [OF A])
moreover have "None ∉ set (take (Suc (length xs) - n) xs)"
using C and R by (rule weakly_seq_sentences_none)
hence "y ≠ None"
using Q by (rule_tac not_sym, simp)
ultimately show False
by contradiction
next
assume P: "n' < n"
have "take (Suc (length xs) - n') xs =
take (Suc (length xs) - n) (take (Suc (length xs) - n') xs) @
drop (Suc (length xs) - n) (take (Suc (length xs) - n') xs)"
by (simp only: append_take_drop_id)
also have "… =
take (Suc (length xs) - n) xs @
drop (Suc (length xs) - n) (take (Suc (length xs) - n') xs)"
using P by (simp add: min_def)
also have "… =
take (Suc (length xs) - n) xs @
take (n - n') (drop (Suc (length xs) - n) xs)"
using G by (subst drop_take, simp)
finally have "take (Suc (length xs) - n') xs =
take (Suc (length xs) - n) xs @
take (n - n') (drop (Suc (length xs) - n) xs)" .
moreover have "take (n - n') (drop (Suc (length xs) - n) xs) ≠ []"
proof (rule_tac notI, simp, erule disjE)
assume "n ≤ n'"
thus False
using P by simp
next
assume "length xs ≤ Suc (length xs) - n"
moreover have "Suc (length xs) - n < Suc (length xs) - n'"
using G and P by simp
hence "Suc (length xs) - n < length xs"
using N by simp
ultimately show False
by simp
qed
hence "∃y ys. take (n - n') (drop (Suc (length xs) - n) xs) = y # ys"
by (cases "take (n - n') (drop (Suc (length xs) - n) xs)", simp_all)
then obtain y and ys where
"take (n - n') (drop (Suc (length xs) - n) xs) = y # ys"
by blast
ultimately have Q: "take (Suc (length xs) - n') xs =
take (Suc (length xs) - n) xs @ y # ys"
by simp
have "take (Suc (length xs) - n) xs ∈ sentences P"
using I ..
moreover have R: "take (Suc (length xs) - n') xs ∈ sentences P"
using O ..
hence "take (Suc (length xs) - n') xs @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "take (Suc (length xs) - n') xs ∈ traces P"
by (rule process_rule_2_traces)
hence "take (Suc (length xs) - n) xs @ y # ys ∈ traces P"
using Q by simp
ultimately have "y = None"
by (rule seq_sentences_none [OF A])
moreover have "None ∉ set (take (Suc (length xs) - n') xs)"
using C and R by (rule weakly_seq_sentences_none)
hence "y ≠ None"
using Q by (rule_tac not_sym, simp)
ultimately show False
by contradiction
qed
ultimately have "(drop (Suc (length xs) - n) xs @ [x], W') ∈ failures Q"
by simp
hence P: "drop (Suc (length xs) - n) xs @ [x] ∈ traces Q"
by (rule failures_traces)
have "(drop (Suc (length xs) - n) xs @ [None], W) ∈ failures Q"
using I ..
hence "drop (Suc (length xs) - n) xs @ [None] ∈ traces Q"
by (rule failures_traces)
hence "drop (Suc (length xs) - n) xs ∈ sentences Q"
by (simp add: sentences_def)
with B show ?thesis
using P by (rule seq_sentences_none)
qed
qed
qed
subsection "Conservation of noninterference security under sequential composition"
text ‹
Everything is now ready for proving the target security conservation theorem. The two closure
properties that the definition of noninterference security requires process futures to satisfy, one
for the addition of events into traces and the other for the deletion of events from traces (cf.
\<^cite>‹"R2"›), will be faced separately; here below is the proof of the former property.
Unsurprisingly, rule induction on set @{term seq_comp_failures} is applied, and the closure of the
failures of a secure process under intransitive purge (proven in the previous section) is used to
meet the proof obligations arising from rule ‹SCF_R3›.
\null
›
lemma seq_comp_secure_aux_1_case_1:
assumes
A: "secure_termination I D" and
B: "sequential P" and
C: "secure P I D" and
D: "xs @ y # ys ∉ sentences P" and
E: "(xs @ y # ys, X) ∈ failures P" and
F: "None ≠ y" and
G: "None ∉ set xs" and
H: "None ∉ set ys"
shows "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X)
∈ seq_comp_failures P Q"
proof -
have "(y # ys, X) ∈ futures P xs"
using E by (simp add: futures_def)
hence "(ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X) ∈
futures P xs"
using C by (simp add: secure_def)
hence I: "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X) ∈
failures P"
by (simp add: futures_def)
show ?thesis
proof (cases "xs @ ipurge_tr I D (D y) ys ∈ sentences P",
cases "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) ys. (u, D None) ∈ I)",
simp_all)
assume "xs @ ipurge_tr I D (D y) ys ∉ sentences P"
thus ?thesis using I
proof (rule SCF_R1, simp add: F G)
have "set (ipurge_tr I D (D y) ys) ⊆ set ys"
by (rule ipurge_tr_set)
thus "None ∉ set (ipurge_tr I D (D y) ys)"
using H by (rule contra_subsetD)
qed
next
assume
J: "xs @ ipurge_tr I D (D y) ys ∈ sentences P" and
K: "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) ys. (u, D None) ∈ I)"
have "ipurge_ref I D (D y) ys X = {}"
proof (rule disjE [OF K], erule_tac [2] bexE)
assume L: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_ref_empty [of "D y"], simp)
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
hence "∀u ∈ range D. (D y, u) ∈ I"
using F and L by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
L: "u ∈ sinks I D (D y) ys" and
M: "(u, D None) ∈ I"
have "∃y' ∈ set ys. u = D y'"
using L by (rule sinks_elem)
then obtain y' where N: "y' ∈ set ys" and O: "u = D y'" ..
have P: "y' ≠ None"
proof
assume "y' = None"
hence "None ∈ set ys"
using N by simp
thus False
using H by contradiction
qed
show ?thesis
proof (rule ipurge_ref_empty [of u], simp add: L)
fix x
have "(D y', D None) ∈ I ∧ y' ≠ None ⟶ (∀v ∈ range D. (D y', v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D y', D None) ∈ I"
using M and O by simp
ultimately have "∀v ∈ range D. (D y', v) ∈ I"
using P by simp
thus "(u, D x) ∈ I"
using O by simp
qed
qed
thus ?thesis
proof simp
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with J and I have "(xs @ ipurge_tr I D (D y) ys,
insert None (ipurge_ref I D (D y) ys X) ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus "(xs @ ipurge_tr I D (D y) ys, {}) ∈ seq_comp_failures P Q"
by simp
qed
next
assume
J: "xs @ ipurge_tr I D (D y) ys ∈ sentences P" and
K: "(D y, D None) ∉ I ∧ (∀u ∈ sinks I D (D y) ys. (u, D None) ∉ I)"
have "(xs @ [y]) @ ys ∈ sentences P"
proof (simp add: sentences_def del: append_assoc, subst (2) append_assoc,
rule ipurge_tr_del_traces [OF C, where u = "D y"], simp_all add: K)
have "(y # ys, X) ∈ futures P xs"
using E by (simp add: futures_def)
moreover have "xs @ ipurge_tr I D (D y) ys @ [None] ∈ traces P"
using J by (simp add: sentences_def)
hence "(xs @ ipurge_tr I D (D y) ys @ [None], {}) ∈ failures P"
by (rule traces_failures)
hence "(ipurge_tr I D (D y) ys @ [None], {}) ∈ futures P xs"
by (simp add: futures_def)
ultimately have "(y # ipurge_tr I D (D y) (ipurge_tr I D (D y) ys @ [None]),
ipurge_ref I D (D y) (ipurge_tr I D (D y) ys @ [None]) {}) ∈ futures P xs"
using C by (simp add: secure_def del: ipurge_tr.simps)
hence "(xs @ y # ipurge_tr I D (D y) (ipurge_tr I D (D y) ys @ [None]), {})
∈ failures P"
by (simp add: futures_def ipurge_ref_def)
moreover have "sinks I D (D y) (ipurge_tr I D (D y) ys) = {}"
by (rule sinks_idem)
hence "¬ ((D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) (ipurge_tr I D (D y) ys). (u, D None) ∈ I))"
using K by simp
hence "D None ∉ sinks I D (D y) (ipurge_tr I D (D y) ys @ [None])"
by (simp only: sinks_interference_eq, simp)
ultimately have "(xs @ y # ipurge_tr I D (D y) (ipurge_tr I D (D y) ys)
@ [None], {}) ∈ failures P"
by simp
hence "(xs @ y # ipurge_tr I D (D y) ys @ [None], {}) ∈ failures P"
by (simp add: ipurge_tr_idem)
thus "xs @ y # ipurge_tr I D (D y) ys @ [None] ∈ traces P"
by (rule failures_traces)
next
show "xs @ y # ys ∈ traces P"
using E by (rule failures_traces)
qed
hence "xs @ y # ys ∈ sentences P"
by simp
thus ?thesis
using D by contradiction
qed
qed
lemma seq_comp_secure_aux_1_case_2:
assumes
A: "secure_termination I D" and
B: "sequential P" and
C: "secure P I D" and
D: "secure Q I D" and
E: "xs @ y # ys ∈ sentences P" and
F: "(xs @ y # ys, X) ∈ failures P" and
G: "([], Y) ∈ failures Q"
shows "(xs @ ipurge_tr I D (D y) ys,
ipurge_ref I D (D y) ys (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
proof -
have "(y # ys, X) ∈ futures P xs"
using F by (simp add: futures_def)
hence "(ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X)
∈ futures P xs"
using C by (simp add: secure_def)
hence H: "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X)
∈ failures P"
by (simp add: futures_def)
have "weakly_sequential P"
using B by (rule seq_implies_weakly_seq)
hence I: "None ∉ set (xs @ y # ys)"
using E by (rule weakly_seq_sentences_none)
show ?thesis
proof (cases "xs @ ipurge_tr I D (D y) ys ∈ sentences P",
case_tac [2] "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) ys. (u, D None) ∈ I)",
simp_all)
assume J: "xs @ ipurge_tr I D (D y) ys ∈ sentences P"
have "ipurge_ref I D (D y) ys Y ⊆ Y"
by (rule ipurge_ref_subset)
with G have "([], ipurge_ref I D (D y) ys Y) ∈ failures Q"
by (rule process_rule_3)
with J and H have "(xs @ ipurge_tr I D (D y) ys,
insert None (ipurge_ref I D (D y) ys X) ∩ ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2)
moreover have
"ipurge_ref I D (D y) ys (insert None X) ∩ ipurge_ref I D (D y) ys Y ⊆
insert None (ipurge_ref I D (D y) ys X) ∩ ipurge_ref I D (D y) ys Y"
proof (rule subsetI, simp del: insert_iff, erule conjE)
fix x
have "ipurge_ref I D (D y) ys (insert None X) ⊆
insert None (ipurge_ref I D (D y) ys X)"
by (rule ipurge_ref_subset_insert)
moreover assume "x ∈ ipurge_ref I D (D y) ys (insert None X)"
ultimately show "x ∈ insert None (ipurge_ref I D (D y) ys X)" ..
qed
ultimately have "(xs @ ipurge_tr I D (D y) ys,
ipurge_ref I D (D y) ys (insert None X) ∩ ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
by (rule seq_comp_prop_3)
thus ?thesis
by (simp add: ipurge_ref_distrib_inter)
next
assume
J: "xs @ ipurge_tr I D (D y) ys ∉ sentences P" and
K: "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) ys. (u, D None) ∈ I)"
have "ipurge_ref I D (D y) ys (insert None X ∩ Y) = {}"
proof (rule disjE [OF K], erule_tac [2] bexE)
assume L: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_ref_empty [of "D y"], simp)
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using I by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using L by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
L: "u ∈ sinks I D (D y) ys" and
M: "(u, D None) ∈ I"
have "∃y' ∈ set ys. u = D y'"
using L by (rule sinks_elem)
then obtain y' where N: "y' ∈ set ys" and O: "u = D y'" ..
have P: "y' ≠ None"
proof
assume "y' = None"
hence "None ∈ set ys"
using N by simp
moreover have "None ∉ set ys"
using I by simp
ultimately show False
by contradiction
qed
show ?thesis
proof (rule ipurge_ref_empty [of u], simp add: L)
fix x
have "(D y', D None) ∈ I ∧ y' ≠ None ⟶ (∀v ∈ range D. (D y', v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D y', D None) ∈ I"
using M and O by simp
ultimately have "∀v ∈ range D. (D y', v) ∈ I"
using P by simp
thus "(u, D x) ∈ I"
using O by simp
qed
qed
thus ?thesis
proof simp
have "{} ⊆ ipurge_ref I D (D y) ys X" ..
with H have "(xs @ ipurge_tr I D (D y) ys, {}) ∈ failures P"
by (rule process_rule_3)
with J show "(xs @ ipurge_tr I D (D y) ys, {}) ∈ seq_comp_failures P Q"
proof (rule SCF_R1)
show "None ∉ set (xs @ ipurge_tr I D (D y) ys)"
using I
proof (simp, (erule_tac conjE)+)
have "set (ipurge_tr I D (D y) ys) ⊆ set ys"
by (rule ipurge_tr_set)
moreover assume "None ∉ set ys"
ultimately show "None ∉ set (ipurge_tr I D (D y) ys)"
by (rule contra_subsetD)
qed
qed
qed
next
assume
J: "xs @ ipurge_tr I D (D y) ys ∉ sentences P" and
K: "(D y, D None) ∉ I ∧ (∀u ∈ sinks I D (D y) ys. (u, D None) ∉ I)"
have "xs @ y # ys @ [None] ∈ traces P"
using E by (simp add: sentences_def)
hence "(xs @ y # ys @ [None], {}) ∈ failures P"
by (rule traces_failures)
hence "(y # ys @ [None], {}) ∈ futures P xs"
by (simp add: futures_def)
hence "(ipurge_tr I D (D y) (ys @ [None]),
ipurge_ref I D (D y) (ys @ [None]) {}) ∈ futures P xs"
(is "(_, ?Y) ∈ _")
using C by (simp add: secure_def del: ipurge_tr.simps)
hence "(xs @ ipurge_tr I D (D y) (ys @ [None]), ?Y) ∈ failures P"
by (simp add: futures_def)
hence "xs @ ipurge_tr I D (D y) (ys @ [None]) ∈ traces P"
by (rule failures_traces)
moreover have "¬ ((D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ys. (u, D None) ∈ I))"
using K by simp
hence "D None ∉ sinks I D (D y) (ys @ [None])"
by (simp only: sinks_interference_eq, simp)
ultimately have "xs @ ipurge_tr I D (D y) ys @ [None] ∈ traces P"
by simp
hence "xs @ ipurge_tr I D (D y) ys ∈ sentences P"
by (simp add: sentences_def)
thus ?thesis
using J by contradiction
qed
qed
lemma seq_comp_secure_aux_1_case_3:
assumes
A: "secure_termination I D" and
B: "ref_union_closed Q" and
C: "sequential Q" and
D: "secure Q I D" and
E: "secure R I D" and
F: "ws ∈ sentences Q" and
G: "(ys', Y) ∈ failures R" and
H: "ws @ ys' = xs @ y # ys"
shows "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures Q R"
proof (cases "length xs < length ws")
case True
have "drop (Suc (length xs)) (xs @ y # ys) = drop (Suc (length xs)) (ws @ ys')"
using H by simp
hence I: "ys = drop (Suc (length xs)) ws @ ys'"
(is "_ = ?ws' @ _")
using True by simp
let ?U = "insert (D y) (sinks I D (D y) ?ws')"
have "ipurge_tr I D (D y) ys =
ipurge_tr I D (D y) ?ws' @ ipurge_tr_aux I D ?U ys'"
using I by (simp add: ipurge_tr_append)
moreover have "ipurge_ref I D (D y) ys Y = ipurge_ref_aux I D ?U ys' Y"
using I by (simp add: ipurge_ref_append)
ultimately show ?thesis
proof (cases "xs @ ipurge_tr I D (D y) ?ws' ∈ sentences Q", simp_all)
assume J: "xs @ ipurge_tr I D (D y) ?ws' ∈ sentences Q"
have K: "(ipurge_tr_aux I D ?U ys', ipurge_ref_aux I D ?U ys' Y) ∈ failures R"
using E and G by (rule ipurge_tr_ref_aux_failures)
show "(xs @ ipurge_tr I D (D y) ?ws' @ ipurge_tr_aux I D ?U ys',
ipurge_ref_aux I D ?U ys' Y) ∈ seq_comp_failures Q R"
proof (cases "ipurge_tr_aux I D ?U ys'")
case Nil
have "(xs @ ipurge_tr I D (D y) ?ws', {x. x ≠ None}) ∈ failures Q"
using B and C and J by (rule seq_sentences_ref)
moreover have "([], ipurge_ref_aux I D ?U ys' Y) ∈ failures R"
using K and Nil by simp
ultimately have "(xs @ ipurge_tr I D (D y) ?ws',
insert None {x. x ≠ None} ∩ ipurge_ref_aux I D ?U ys' Y)
∈ seq_comp_failures Q R"
by (rule SCF_R2 [OF J])
moreover have "insert None {x. x ≠ None} ∩
ipurge_ref_aux I D ?U ys' Y = ipurge_ref_aux I D ?U ys' Y"
by blast
ultimately show ?thesis
using Nil by simp
next
case Cons
hence "ipurge_tr_aux I D ?U ys' ≠ []"
by simp
with J and K have
"((xs @ ipurge_tr I D (D y) ?ws') @ ipurge_tr_aux I D ?U ys',
ipurge_ref_aux I D ?U ys' Y) ∈ seq_comp_failures Q R"
by (rule SCF_R3)
thus ?thesis
by simp
qed
next
assume J: "xs @ ipurge_tr I D (D y) ?ws' ∉ sentences Q"
have "ws = take (Suc (length xs)) ws @ ?ws'"
by simp
moreover have "take (Suc (length xs)) (ws @ ys') =
take (Suc (length xs)) (xs @ y # ys)"
using H by simp
hence "take (Suc (length xs)) ws = xs @ [y]"
using True by simp
ultimately have K: "xs @ y # ?ws' ∈ sentences Q"
using F by simp
hence "xs @ y # ?ws' @ [None] ∈ traces Q"
by (simp add: sentences_def)
hence "(xs @ y # ?ws' @ [None], {}) ∈ failures Q"
by (rule traces_failures)
hence "(y # ?ws' @ [None], {}) ∈ futures Q xs"
by (simp add: futures_def)
hence "(ipurge_tr I D (D y) (?ws' @ [None]),
ipurge_ref I D (D y) (?ws' @ [None]) {}) ∈ futures Q xs"
using D by (simp add: secure_def del: ipurge_tr.simps)
hence L: "(xs @ ipurge_tr I D (D y) (?ws' @ [None]), {}) ∈ failures Q"
by (simp add: futures_def ipurge_ref_def)
have "weakly_sequential Q"
using C by (rule seq_implies_weakly_seq)
hence N: "None ∉ set (xs @ y # ?ws')"
using K by (rule weakly_seq_sentences_none)
show "(xs @ ipurge_tr I D (D y) ?ws' @ ipurge_tr_aux I D ?U ys',
ipurge_ref_aux I D ?U ys' Y) ∈ seq_comp_failures Q R"
proof (cases "(D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ?ws'. (u, D None) ∈ I)")
assume M: "(D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ?ws'. (u, D None) ∈ I)"
have "ipurge_tr_aux I D ?U ys' = []"
proof (rule disjE [OF M], erule_tac [2] bexE)
assume O: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_tr_aux_nil [of "D y"], simp)
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using N by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using O by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
O: "u ∈ sinks I D (D y) ?ws'" and
P: "(u, D None) ∈ I"
have "∃w ∈ set ?ws'. u = D w"
using O by (rule sinks_elem)
then obtain w where Q: "w ∈ set ?ws'" and R: "u = D w" ..
have S: "w ≠ None"
proof
assume "w = None"
hence "None ∈ set ?ws'"
using Q by simp
moreover have "None ∉ set ?ws'"
using N by simp
ultimately show False
by contradiction
qed
show ?thesis
proof (rule ipurge_tr_aux_nil [of u], simp add: O)
fix x
have "(D w, D None) ∈ I ∧ w ≠ None ⟶ (∀v ∈ range D. (D w, v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D w, D None) ∈ I"
using P and R by simp
ultimately have "∀v ∈ range D. (D w, v) ∈ I"
using S by simp
thus "(u, D x) ∈ I"
using R by simp
qed
qed
moreover have "ipurge_ref_aux I D ?U ys' Y = {}"
proof (rule disjE [OF M], erule_tac [2] bexE)
assume O: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_ref_aux_empty [of "D y"])
have "?U ⊆ sinks_aux I D ?U ys'"
by (rule sinks_aux_subset)
moreover have "D y ∈ ?U"
by simp
ultimately show "D y ∈ sinks_aux I D ?U ys'" ..
next
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using N by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using O by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
O: "u ∈ sinks I D (D y) ?ws'" and
P: "(u, D None) ∈ I"
have "∃w ∈ set ?ws'. u = D w"
using O by (rule sinks_elem)
then obtain w where Q: "w ∈ set ?ws'" and R: "u = D w" ..
have S: "w ≠ None"
proof
assume "w = None"
hence "None ∈ set ?ws'"
using Q by simp
moreover have "None ∉ set ?ws'"
using N by simp
ultimately show False
by contradiction
qed
show ?thesis
proof (rule ipurge_ref_aux_empty [of u])
have "?U ⊆ sinks_aux I D ?U ys'"
by (rule sinks_aux_subset)
moreover have "u ∈ ?U"
using O by simp
ultimately show "u ∈ sinks_aux I D ?U ys'" ..
next
fix x
have "(D w, D None) ∈ I ∧ w ≠ None ⟶ (∀v ∈ range D. (D w, v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D w, D None) ∈ I"
using P and R by simp
ultimately have "∀v ∈ range D. (D w, v) ∈ I"
using S by simp
thus "(u, D x) ∈ I"
using R by simp
qed
qed
ultimately show ?thesis
proof simp
have "D None ∈ sinks I D (D y) (?ws' @ [None])"
using M by (simp only: sinks_interference_eq)
hence "(xs @ ipurge_tr I D (D y) ?ws', {}) ∈ failures Q"
using L by simp
moreover have "None ∉ set (xs @ ipurge_tr I D (D y) ?ws')"
proof -
show ?thesis
using N
proof (simp, (erule_tac conjE)+)
have "set (ipurge_tr I D (D y) ?ws') ⊆ set ?ws'"
by (rule ipurge_tr_set)
moreover assume "None ∉ set ?ws'"
ultimately show "None ∉ set (ipurge_tr I D (D y) ?ws')"
by (rule contra_subsetD)
qed
qed
ultimately show "(xs @ ipurge_tr I D (D y) ?ws', {})
∈ seq_comp_failures Q R"
by (rule SCF_R1 [OF J])
qed
next
assume "¬ ((D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ?ws'. (u, D None) ∈ I))"
hence "D None ∉ sinks I D (D y) (?ws' @ [None])"
by (simp only: sinks_interference_eq, simp)
hence "(xs @ ipurge_tr I D (D y) ?ws' @ [None], {}) ∈ failures Q"
using L by simp
hence "xs @ ipurge_tr I D (D y) ?ws' @ [None] ∈ traces Q"
by (rule failures_traces)
hence "xs @ ipurge_tr I D (D y) ?ws' ∈ sentences Q"
by (simp add: sentences_def)
thus ?thesis
using J by contradiction
qed
qed
next
case False
have "drop (length ws) (ws @ ys') = drop (length ws) (xs @ y # ys)"
using H by simp
hence "ys' = drop (length ws) xs @ y # ys"
(is "_ = ?xs' @ _")
using False by simp
hence "(?xs' @ y # ys, Y) ∈ failures R"
using G by simp
hence "(y # ys, Y) ∈ futures R ?xs'"
by (simp add: futures_def)
hence "(ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ futures R ?xs'"
using E by (simp add: secure_def)
hence I: "(?xs' @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ failures R"
by (simp add: futures_def)
have "xs = take (length ws) xs @ ?xs'"
by simp
hence "xs = take (length ws) (xs @ y # ys) @ ?xs'"
using False by simp
hence "xs = take (length ws) (ws @ ys') @ ?xs'"
using H by simp
hence J: "xs = ws @ ?xs'"
by simp
show ?thesis
proof (cases "?xs' @ ipurge_tr I D (D y) ys = []", insert I, subst J, simp)
have "(ws, {x. x ≠ None}) ∈ failures Q"
using B and C and F by (rule seq_sentences_ref)
moreover assume "([], ipurge_ref I D (D y) ys Y) ∈ failures R"
ultimately have "(ws, insert None {x. x ≠ None} ∩
ipurge_ref I D (D y) ys Y) ∈ seq_comp_failures Q R"
by (rule SCF_R2 [OF F])
moreover have "insert None {x. x ≠ None} ∩ ipurge_ref I D (D y) ys Y =
ipurge_ref I D (D y) ys Y"
by blast
ultimately show "(ws, ipurge_ref I D (D y) ys Y) ∈ seq_comp_failures Q R"
by simp
next
assume "?xs' @ ipurge_tr I D (D y) ys ≠ []"
with F and I have
"(ws @ ?xs' @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures Q R"
by (rule SCF_R3)
hence "((ws @ ?xs') @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures Q R"
by simp
thus ?thesis
using J by simp
qed
qed
lemma seq_comp_secure_aux_1 [rule_format]:
assumes
A: "secure_termination I D" and
B: "ref_union_closed P" and
C: "sequential P" and
D: "secure P I D" and
E: "secure Q I D"
shows "(ws, Y) ∈ seq_comp_failures P Q ⟹
ws = xs @ y # ys ⟶
(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
proof (erule seq_comp_failures.induct, rule_tac [!] impI, simp_all, (erule conjE)+)
fix X
assume
"xs @ y # ys ∉ sentences P" and
"(xs @ y # ys, X) ∈ failures P" and
"None ≠ y" and
"None ∉ set xs" and
"None ∉ set ys"
thus "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X)
∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_1_case_1 [OF A C D])
next
fix X Y
assume
"xs @ y # ys ∈ sentences P" and
"(xs @ y # ys, X) ∈ failures P" and
"([], Y) ∈ failures Q"
thus "(xs @ ipurge_tr I D (D y) ys,
ipurge_ref I D (D y) ys (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_1_case_2 [OF A C D E])
next
fix ws ys' Y
assume
"ws ∈ sentences P" and
"(ys', Y) ∈ failures Q" and
"ws @ ys' = xs @ y # ys"
thus "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_1_case_3 [OF A B C D E])
next
fix X Y
assume
"(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys X)
∈ seq_comp_failures P Q" and
"(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
hence "(xs @ ipurge_tr I D (D y) ys,
ipurge_ref I D (D y) ys X ∪ ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
by (rule SCF_R4)
thus "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys (X ∪ Y))
∈ seq_comp_failures P Q"
by (simp add: ipurge_ref_distrib_union)
qed
lemma seq_comp_secure_1:
assumes
A: "secure_termination I D" and
B: "ref_union_closed P" and
C: "sequential P" and
D: "secure P I D" and
E: "secure Q I D"
shows "(xs @ y # ys, Y) ∈ seq_comp_failures P Q ⟹
(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_1 [OF A B C D E, where ws = "xs @ y # ys"],
simp_all)
text ‹
\null
This completes the proof that the former requirement for noninterference security is satisfied, so
it is the turn of the latter one. Again, rule induction on set @{term seq_comp_failures} is applied,
and the closure of the failures of a secure process under intransitive purge is used to meet the
proof obligations arising from rule ‹SCF_R3›. In more detail, rule induction is applied to the
trace into which the event is inserted, and then a case distinction is performed on the trace from
which the event is extracted, using the expression of its refusal as union of a set of refusals
derived previously.
\null
›
lemma seq_comp_secure_aux_2_case_1:
assumes
A: "secure_termination I D" and
B: "sequential P" and
C: "secure P I D" and
D: "xs @ zs ∉ sentences P" and
E: "(xs @ zs, X) ∈ failures P" and
F: "None ∉ set xs" and
G: "None ∉ set zs" and
H: "(xs @ [y], {}) ∈ seq_comp_failures P Q"
shows "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X)
∈ seq_comp_failures P Q"
proof -
have "∃R. {} = (⋃n ∈ {..length (xs @ [y])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧ None ∉ set (xs @ [y]) ∧
(xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧ (∃U V. (xs @ [y], U) ∈ failures P ∧
([], V) ∈ failures Q ∧ W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [y])}. ∀W ∈ R n.
take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P ∧
(drop (length (xs @ [y]) - n) (xs @ [y]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [y])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using H by (rule seq_comp_refusals_1)
then obtain R where I: "?T R" ..
hence "∃n ∈ {..length (xs @ [y])}. ∃W. W ∈ R n"
by simp
moreover have "∀n ∈ {0<..length (xs @ [y])}. R n = {}"
proof (rule ballI, rule equals0I)
fix n W
assume J: "n ∈ {0<..length (xs @ [y])}"
hence "∀W ∈ R n. take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P"
using I by simp
moreover assume "W ∈ R n"
ultimately have "take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P" ..
moreover have "take (length (xs @ [y]) - n) (xs @ [y]) =
take (length (xs @ [y]) - n) (xs @ zs)"
using J by simp
ultimately have K: "take (length (xs @ [y]) - n) (xs @ zs) ∈ sentences P"
by simp
show False
proof (cases "drop (length (xs @ [y]) - n) (xs @ zs)")
case Nil
hence "xs @ zs ∈ sentences P"
using K by simp
thus False
using D by contradiction
next
case (Cons v vs)
moreover have "xs @ zs = take (length (xs @ [y]) - n) (xs @ zs) @
drop (length (xs @ [y]) - n) (xs @ zs)"
by (simp only: append_take_drop_id)
ultimately have L: "xs @ zs =
take (length (xs @ [y]) - n) (xs @ zs) @ v # vs"
by (simp del: take_append)
hence "(take (length (xs @ [y]) - n) (xs @ zs) @ v # vs, X)
∈ failures P"
using E by (simp del: take_append)
hence "take (length (xs @ [y]) - n) (xs @ zs) @ v # vs ∈ traces P"
by (rule failures_traces)
with B and K have "v = None"
by (rule seq_sentences_none)
moreover have "None ∉ set (xs @ zs)"
using F and G by simp
hence "None ∉ set (take (length (xs @ [y]) - n) (xs @ zs) @ v # vs)"
by (subst (asm) L)
hence "v ≠ None"
by (rule_tac not_sym, simp)
ultimately show False
by contradiction
qed
qed
ultimately have "∃W. W ∈ R 0"
proof simp
assume "∃n ∈ {..Suc (length xs)}. ∃W. W ∈ R n"
then obtain n where J: "n ∈ {..Suc (length xs)}" and K: "∃W. W ∈ R n" ..
assume L: "∀n ∈ {0<..Suc (length xs)}. R n = {}"
show ?thesis
proof (cases n)
case 0
thus ?thesis
using K by simp
next
case (Suc m)
obtain W where "W ∈ R n"
using K ..
moreover have "0 < n"
using Suc by simp
hence "n ∈ {0<..Suc (length xs)}"
using J by simp
with L have "R n = {}" ..
hence "W ∉ R n"
by (rule equals0D)
ultimately show ?thesis
by contradiction
qed
qed
then obtain W where J: "W ∈ R 0" ..
have "∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧
None ∉ set (xs @ [y]) ∧ (xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧
(∃U V. (xs @ [y], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "∀W ∈ R 0. ?T W")
using I by simp
hence "?T W" using J ..
hence K: "(xs @ [y], {}) ∈ failures P ∧ None ≠ y"
proof (cases "xs @ [y] ∈ sentences P", simp_all del: ex_simps,
(erule_tac exE)+, (erule_tac [!] conjE)+, simp_all)
case False
assume "(xs @ [y], W) ∈ failures P"
moreover have "{} ⊆ W" ..
ultimately show "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
next
fix U
case True
assume "(xs @ [y], U) ∈ failures P"
moreover have "{} ⊆ U" ..
ultimately have "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
moreover have "weakly_sequential P"
using B by (rule seq_implies_weakly_seq)
hence "None ∉ set (xs @ [y])"
using True by (rule weakly_seq_sentences_none)
hence "None ≠ y"
by simp
ultimately show ?thesis ..
qed
have "(zs, X) ∈ futures P xs"
using E by (simp add: futures_def)
moreover have "([y], {}) ∈ futures P xs"
using K by (simp add: futures_def)
ultimately have "(y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X) ∈
futures P xs"
using C by (simp add: secure_def)
hence L: "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X) ∈
failures P"
by (simp add: futures_def)
show ?thesis
proof (cases "xs @ y # ipurge_tr I D (D y) zs ∈ sentences P",
cases "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) zs. (u, D None) ∈ I)",
simp_all)
assume "xs @ y # ipurge_tr I D (D y) zs ∉ sentences P"
thus ?thesis using L
proof (rule SCF_R1, simp add: F K)
have "set (ipurge_tr I D (D y) zs) ⊆ set zs"
by (rule ipurge_tr_set)
thus "None ∉ set (ipurge_tr I D (D y) zs)"
using G by (rule contra_subsetD)
qed
next
assume
M: "xs @ y # ipurge_tr I D (D y) zs ∈ sentences P" and
N: "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) zs. (u, D None) ∈ I)"
have "ipurge_ref I D (D y) zs X = {}"
proof (rule disjE [OF N], erule_tac [2] bexE)
assume O: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_ref_empty [of "D y"], simp)
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using K by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using O by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
O: "u ∈ sinks I D (D y) zs" and
P: "(u, D None) ∈ I"
have "∃z ∈ set zs. u = D z"
using O by (rule sinks_elem)
then obtain z where Q: "z ∈ set zs" and R: "u = D z" ..
have S: "z ≠ None"
proof
assume "z = None"
hence "None ∈ set zs"
using Q by simp
thus False
using G by contradiction
qed
show ?thesis
proof (rule ipurge_ref_empty [of u], simp add: O)
fix x
have "(D z, D None) ∈ I ∧ z ≠ None ⟶ (∀v ∈ range D. (D z, v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D z, D None) ∈ I"
using P and R by simp
ultimately have "∀v ∈ range D. (D z, v) ∈ I"
using S by simp
thus "(u, D x) ∈ I"
using R by simp
qed
qed
thus ?thesis
proof simp
have "([], {}) ∈ failures Q"
by (rule process_rule_1)
with M and L have "(xs @ y # ipurge_tr I D (D y) zs,
insert None (ipurge_ref I D (D y) zs X) ∩ {}) ∈ seq_comp_failures P Q"
by (rule SCF_R2)
thus "(xs @ y # ipurge_tr I D (D y) zs, {}) ∈ seq_comp_failures P Q"
by simp
qed
next
assume
M: "xs @ y # ipurge_tr I D (D y) zs ∈ sentences P" and
N: "(D y, D None) ∉ I ∧ (∀u ∈ sinks I D (D y) zs. (u, D None) ∉ I)"
have "xs @ zs ∈ sentences P"
proof (simp add: sentences_def,
rule ipurge_tr_del_traces [OF C, where u = "D y"], simp add: N)
have "xs @ y # ipurge_tr I D (D y) zs @ [None] ∈ traces P"
using M by (simp add: sentences_def)
hence "(xs @ y # ipurge_tr I D (D y) zs @ [None], {}) ∈ failures P"
by (rule traces_failures)
hence "(y # ipurge_tr I D (D y) zs @ [None], {}) ∈ futures P xs"
by (simp add: futures_def)
hence "(ipurge_tr I D (D y) (ipurge_tr I D (D y) zs @ [None]),
ipurge_ref I D (D y) (ipurge_tr I D (D y) zs @ [None]) {}) ∈ futures P xs"
using C by (simp add: secure_def del: ipurge_tr.simps)
hence "(xs @ ipurge_tr I D (D y) (ipurge_tr I D (D y) zs @ [None]), {})
∈ failures P"
by (simp add: futures_def ipurge_ref_def)
moreover have "sinks I D (D y) (ipurge_tr I D (D y) zs) = {}"
by (rule sinks_idem)
hence "¬ ((D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) (ipurge_tr I D (D y) zs). (u, D None) ∈ I))"
using N by simp
hence "D None ∉ sinks I D (D y) (ipurge_tr I D (D y) zs @ [None])"
by (simp only: sinks_interference_eq, simp)
ultimately have "(xs @ ipurge_tr I D (D y) (ipurge_tr I D (D y) zs)
@ [None], {}) ∈ failures P"
by simp
hence "(xs @ ipurge_tr I D (D y) zs @ [None], {}) ∈ failures P"
by (simp add: ipurge_tr_idem)
thus "xs @ ipurge_tr I D (D y) zs @ [None] ∈ traces P"
by (rule failures_traces)
next
show "xs @ zs ∈ traces P"
using E by (rule failures_traces)
qed
thus ?thesis
using D by contradiction
qed
qed
lemma seq_comp_secure_aux_2_case_2:
assumes
A: "secure_termination I D" and
B: "sequential P" and
C: "secure P I D" and
D: "secure Q I D" and
E: "xs @ zs ∈ sentences P" and
F: "(xs @ zs, X) ∈ failures P" and
G: "([], Y) ∈ failures Q" and
H: "(xs @ [y], {}) ∈ seq_comp_failures P Q"
shows "(xs @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
proof -
have "∃R. {} = (⋃n ∈ {..length (xs @ [y])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧ None ∉ set (xs @ [y]) ∧
(xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧ (∃U V. (xs @ [y], U) ∈ failures P ∧
([], V) ∈ failures Q ∧ W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [y])}. ∀W ∈ R n.
take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P ∧
(drop (length (xs @ [y]) - n) (xs @ [y]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [y])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using H by (rule seq_comp_refusals_1)
then obtain R where I: "?T R" ..
hence "∃n ∈ {..length (xs @ [y])}. ∃W. W ∈ R n"
by simp
then obtain n where J: "n ∈ {..length (xs @ [y])}" and K: "∃W. W ∈ R n" ..
have "weakly_sequential P"
using B by (rule seq_implies_weakly_seq)
hence L: "None ∉ set (xs @ zs)"
using E by (rule weakly_seq_sentences_none)
have "n = 0 ∨ n ∈ {0<..length (xs @ [y])}"
using J by auto
thus ?thesis
proof
assume "n = 0"
hence "∃W. W ∈ R 0"
using K by simp
then obtain W where M: "W ∈ R 0" ..
have "∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧
None ∉ set (xs @ [y]) ∧ (xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧
(∃U V. (xs @ [y], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "∀W ∈ R 0. ?T W")
using I by simp
hence "?T W" using M ..
hence N: "(xs @ [y], {}) ∈ failures P ∧ None ∉ set xs ∧ None ≠ y"
proof (cases "xs @ [y] ∈ sentences P", simp_all del: ex_simps,
(erule_tac exE)+, (erule_tac [!] conjE)+, simp_all)
case False
assume "(xs @ [y], W) ∈ failures P"
moreover have "{} ⊆ W" ..
ultimately show "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
next
fix U
case True
assume "(xs @ [y], U) ∈ failures P"
moreover have "{} ⊆ U" ..
ultimately have "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
moreover have "weakly_sequential P"
using B by (rule seq_implies_weakly_seq)
hence "None ∉ set (xs @ [y])"
using True by (rule weakly_seq_sentences_none)
hence "None ∉ set xs ∧ None ≠ y"
by simp
ultimately show ?thesis ..
qed
have "(zs, X) ∈ futures P xs"
using F by (simp add: futures_def)
moreover have "([y], {}) ∈ futures P xs"
using N by (simp add: futures_def)
ultimately have "(y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X)
∈ futures P xs"
using C by (simp add: secure_def)
hence O: "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X)
∈ failures P"
by (simp add: futures_def)
show ?thesis
proof (cases "xs @ y # ipurge_tr I D (D y) zs ∈ sentences P",
case_tac [2] "(D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) zs. (u, D None) ∈ I)",
simp_all)
assume P: "xs @ y # ipurge_tr I D (D y) zs ∈ sentences P"
have "ipurge_ref I D (D y) zs Y ⊆ Y"
by (rule ipurge_ref_subset)
with G have "([], ipurge_ref I D (D y) zs Y) ∈ failures Q"
by (rule process_rule_3)
with P and O have "(xs @ y # ipurge_tr I D (D y) zs,
insert None (ipurge_ref I D (D y) zs X) ∩ ipurge_ref I D (D y) zs Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2)
moreover have
"ipurge_ref I D (D y) zs (insert None X) ∩ ipurge_ref I D (D y) zs Y ⊆
insert None (ipurge_ref I D (D y) zs X) ∩ ipurge_ref I D (D y) zs Y"
proof (rule subsetI, simp del: insert_iff, erule conjE)
fix x
have "ipurge_ref I D (D y) zs (insert None X) ⊆
insert None (ipurge_ref I D (D y) zs X)"
by (rule ipurge_ref_subset_insert)
moreover assume "x ∈ ipurge_ref I D (D y) zs (insert None X)"
ultimately show "x ∈ insert None (ipurge_ref I D (D y) zs X)" ..
qed
ultimately have "(xs @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs (insert None X) ∩ ipurge_ref I D (D y) zs Y)
∈ seq_comp_failures P Q"
by (rule seq_comp_prop_3)
thus ?thesis
by (simp add: ipurge_ref_distrib_inter)
next
assume
P: "xs @ y # ipurge_tr I D (D y) zs ∉ sentences P" and
Q: "(D y, D None) ∈ I ∨ (∃u ∈ sinks I D (D y) zs. (u, D None) ∈ I)"
have "ipurge_ref I D (D y) zs (insert None X ∩ Y) = {}"
proof (rule disjE [OF Q], erule_tac [2] bexE)
assume R: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_ref_empty [of "D y"], simp)
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using N by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using R by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
R: "u ∈ sinks I D (D y) zs" and
S: "(u, D None) ∈ I"
have "∃z ∈ set zs. u = D z"
using R by (rule sinks_elem)
then obtain z where T: "z ∈ set zs" and U: "u = D z" ..
have V: "z ≠ None"
proof
assume "z = None"
hence "None ∈ set zs"
using T by simp
moreover have "None ∉ set zs"
using L by simp
ultimately show False
by contradiction
qed
show ?thesis
proof (rule ipurge_ref_empty [of u], simp add: R)
fix x
have "(D z, D None) ∈ I ∧ z ≠ None ⟶ (∀v ∈ range D. (D z, v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D z, D None) ∈ I"
using S and U by simp
ultimately have "∀v ∈ range D. (D z, v) ∈ I"
using V by simp
thus "(u, D x) ∈ I"
using U by simp
qed
qed
thus ?thesis
proof simp
have "{} ⊆ ipurge_ref I D (D y) zs X" ..
with O have "(xs @ y # ipurge_tr I D (D y) zs, {}) ∈ failures P"
by (rule process_rule_3)
with P show "(xs @ y # ipurge_tr I D (D y) zs, {})
∈ seq_comp_failures P Q"
proof (rule SCF_R1, simp add: N)
have "set (ipurge_tr I D (D y) zs) ⊆ set zs"
by (rule ipurge_tr_set)
moreover have "None ∉ set zs"
using L by simp
ultimately show "None ∉ set (ipurge_tr I D (D y) zs)"
by (rule contra_subsetD)
qed
qed
next
assume
P: "xs @ y # ipurge_tr I D (D y) zs ∉ sentences P" and
Q: "(D y, D None) ∉ I ∧ (∀u ∈ sinks I D (D y) zs. (u, D None) ∉ I)"
have "xs @ zs @ [None] ∈ traces P"
using E by (simp add: sentences_def)
hence "(xs @ zs @ [None], {}) ∈ failures P"
by (rule traces_failures)
hence "(zs @ [None], {}) ∈ futures P xs"
by (simp add: futures_def)
moreover have "([y], {}) ∈ futures P xs"
using N by (simp add: futures_def)
ultimately have "(y # ipurge_tr I D (D y) (zs @ [None]),
ipurge_ref I D (D y) (zs @ [None]) {}) ∈ futures P xs"
(is "(_, ?Z) ∈ _")
using C by (simp add: secure_def del: ipurge_tr.simps)
hence "(xs @ y # ipurge_tr I D (D y) (zs @ [None]), ?Z) ∈ failures P"
by (simp add: futures_def)
hence "xs @ y # ipurge_tr I D (D y) (zs @ [None]) ∈ traces P"
by (rule failures_traces)
moreover have "¬ ((D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) zs. (u, D None) ∈ I))"
using Q by simp
hence "D None ∉ sinks I D (D y) (zs @ [None])"
by (simp only: sinks_interference_eq, simp)
ultimately have "xs @ y # ipurge_tr I D (D y) zs @ [None] ∈ traces P"
by simp
hence "xs @ y # ipurge_tr I D (D y) zs ∈ sentences P"
by (simp add: sentences_def)
thus ?thesis
using P by contradiction
qed
next
assume M: "n ∈ {0<..length (xs @ [y])}"
have "∀n ∈ {0<..length (xs @ [y])}. ∀W ∈ R n.
take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P ∧
(drop (length (xs @ [y]) - n) (xs @ [y]), W) ∈ failures Q"
(is "∀n ∈ _. ∀W ∈ _. ?T n W")
using I by simp
hence "∀W ∈ R n. ?T n W"
using M ..
moreover obtain W where "W ∈ R n"
using K ..
ultimately have N: "?T n W" ..
moreover have O: "take (length (xs @ [y]) - n) (xs @ [y]) =
take (length (xs @ [y]) - n) (xs @ zs)"
using M by simp
ultimately have P: "take (length (xs @ [y]) - n) (xs @ zs) ∈ sentences P"
by simp
have Q: "drop (length (xs @ [y]) - n) (xs @ zs) = []"
proof (cases "drop (length (xs @ [y]) - n) (xs @ zs)", simp)
case (Cons v vs)
moreover have "xs @ zs = take (length (xs @ [y]) - n) (xs @ zs) @
drop (length (xs @ [y]) - n) (xs @ zs)"
by (simp only: append_take_drop_id)
ultimately have R: "xs @ zs =
take (length (xs @ [y]) - n) (xs @ zs) @ v # vs"
by (simp del: take_append)
hence "(take (length (xs @ [y]) - n) (xs @ zs) @ v # vs, X)
∈ failures P"
using F by (simp del: take_append)
hence "take (length (xs @ [y]) - n) (xs @ zs) @ v # vs ∈ traces P"
by (rule failures_traces)
with B and P have "v = None"
by (rule seq_sentences_none)
moreover have
"None ∉ set (take (length (xs @ [y]) - n) (xs @ zs) @ v # vs)"
using L by (subst (asm) R)
hence "v ≠ None"
by (rule_tac not_sym, simp)
ultimately show ?thesis
by contradiction
qed
hence R: "zs = []"
using M by simp
moreover have "xs @ zs = take (length (xs @ [y]) - n) (xs @ zs) @
drop (length (xs @ [y]) - n) (xs @ zs)"
by (simp only: append_take_drop_id)
ultimately have "take (length (xs @ [y]) - n) (xs @ zs) = xs"
using Q by simp
hence "take (length (xs @ [y]) - n) (xs @ [y]) = xs"
using O by simp
moreover have "xs @ [y] = take (length (xs @ [y]) - n) (xs @ [y]) @
drop (length (xs @ [y]) - n) (xs @ [y])"
by (simp only: append_take_drop_id)
ultimately have "drop (length (xs @ [y]) - n) (xs @ [y]) = [y]"
by simp
hence S: "([y], W) ∈ failures Q"
using N by simp
show ?thesis using E and R
proof (rule_tac SCF_R3, simp_all)
have "∀xs y ys Y zs Z.
(y # ys, Y) ∈ futures Q xs ∧ (zs, Z) ∈ futures Q xs ⟶
(ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y) ∈ futures Q xs ∧
(y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Z) ∈ futures Q xs"
using D by (simp add: secure_def)
hence "([y], W) ∈ futures Q [] ∧ ([], Y) ∈ futures Q [] ⟶
(ipurge_tr I D (D y) [], ipurge_ref I D (D y) [] W) ∈ futures Q [] ∧
(y # ipurge_tr I D (D y) [], ipurge_ref I D (D y) [] Y) ∈ futures Q []"
by blast
moreover have "([y], W) ∈ futures Q []"
using S by (simp add: futures_def)
moreover have "([], Y) ∈ futures Q []"
using G by (simp add: futures_def)
ultimately have "([y], ipurge_ref I D (D y) [] Y) ∈ failures Q"
(is "(_, ?Y') ∈ _")
by (simp add: futures_def)
moreover have "ipurge_ref I D (D y) [] (insert None X) ∩ ?Y' ⊆ ?Y'"
by simp
ultimately have "([y], ipurge_ref I D (D y) [] (insert None X) ∩ ?Y')
∈ failures Q"
by (rule process_rule_3)
thus "([y], ipurge_ref I D (D y) [] (insert None X ∩ Y)) ∈ failures Q"
by (simp add: ipurge_ref_distrib_inter)
qed
qed
qed
lemma seq_comp_secure_aux_2_case_3:
assumes
A: "secure_termination I D" and
B: "ref_union_closed P" and
C: "sequential P" and
D: "secure P I D" and
E: "secure Q I D" and
F: "ws ∈ sentences P" and
G: "(ys, Y) ∈ failures Q" and
H: "ys ≠ []" and
I: "ws @ ys = xs @ zs" and
J: "(xs @ [y], {}) ∈ seq_comp_failures P Q"
shows "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Y)
∈ seq_comp_failures P Q"
proof -
have "∃R. {} = (⋃n ∈ {..length (xs @ [y])}. ⋃W ∈ R n. W) ∧
(∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧ None ∉ set (xs @ [y]) ∧
(xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧ (∃U V. (xs @ [y], U) ∈ failures P ∧
([], V) ∈ failures Q ∧ W = insert None U ∩ V)) ∧
(∀n ∈ {0<..length (xs @ [y])}. ∀W ∈ R n.
take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P ∧
(drop (length (xs @ [y]) - n) (xs @ [y]), W) ∈ failures Q) ∧
(∃n ∈ {..length (xs @ [y])}. ∃W. W ∈ R n)"
(is "∃R. ?T R")
using J by (rule seq_comp_refusals_1)
then obtain R where J: "?T R" ..
hence "∃n ∈ {..length (xs @ [y])}. ∃W. W ∈ R n"
by simp
then obtain n where K: "n ∈ {..length (xs @ [y])}" and L: "∃W. W ∈ R n" ..
have M: "n = 0 ∨ n ∈ {0<..length (xs @ [y])}"
using K by auto
show ?thesis
proof (cases "length xs < length ws")
case True
have "∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧
None ∉ set (xs @ [y]) ∧ (xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧
(∃U V. (xs @ [y], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "∀W ∈ _. ?T W")
using J by simp
moreover have "n ∉ {0<..length (xs @ [y])}"
proof
assume N: "n ∈ {0<..length (xs @ [y])}"
hence "∀W ∈ R n. take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P"
using J by simp
moreover obtain W where "W ∈ R n"
using L ..
ultimately have "take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P" ..
moreover have "take (length (xs @ [y]) - n) (xs @ [y]) =
take (length (xs @ [y]) - n) (xs @ zs)"
using N by simp
ultimately have "take (length (xs @ [y]) - n) (xs @ zs) ∈ sentences P"
by simp
hence "take (length (xs @ [y]) - n) (ws @ ys) ∈ sentences P"
using I by simp
moreover have "length (xs @ [y]) - n ≤ length xs"
using N by (simp, arith)
hence O: "length (xs @ [y]) - n < length ws"
using True by simp
ultimately have P: "take (length (xs @ [y]) - n) ws ∈ sentences P"
by simp
show False
proof (cases "drop (length (xs @ [y]) - n) ws")
case Nil
thus False
using O by simp
next
case (Cons v vs)
moreover have "ws = take (length (xs @ [y]) - n) ws @
drop (length (xs @ [y]) - n) ws"
by simp
ultimately have Q: "ws = take (length (xs @ [y]) - n) ws @ v # vs"
by simp
hence "take (length (xs @ [y]) - n) ws @ v # vs ∈ sentences P"
using F by simp
hence "(take (length (xs @ [y]) - n) ws @ v # vs) @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "take (length (xs @ [y]) - n) ws @ v # vs ∈ traces P"
by (rule process_rule_2_traces)
with C and P have "v = None"
by (rule seq_sentences_none)
moreover have "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
hence "None ∉ set ws"
using F by (rule weakly_seq_sentences_none)
hence "None ∉ set (take (length (xs @ [y]) - n) ws @ v # vs)"
by (subst (asm) Q)
hence "v ≠ None"
by (rule_tac not_sym, simp)
ultimately show False
by contradiction
qed
qed
hence "n = 0"
using M by blast
hence "∃W. W ∈ R 0"
using L by simp
then obtain W where "W ∈ R 0" ..
ultimately have "?T W" ..
hence N: "(xs @ [y], {}) ∈ failures P ∧ None ∉ set xs ∧ None ≠ y"
proof (cases "xs @ [y] ∈ sentences P", simp_all del: ex_simps,
(erule_tac exE)+, (erule_tac [!] conjE)+, simp_all)
case False
assume "(xs @ [y], W) ∈ failures P"
moreover have "{} ⊆ W" ..
ultimately show "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
next
fix U
case True
assume "(xs @ [y], U) ∈ failures P"
moreover have "{} ⊆ U" ..
ultimately have "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
moreover have "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
hence "None ∉ set (xs @ [y])"
using True by (rule weakly_seq_sentences_none)
hence "None ∉ set xs ∧ None ≠ y"
by simp
ultimately show ?thesis ..
qed
have "drop (length xs) (xs @ zs) = drop (length xs) (ws @ ys)"
using I by simp
hence O: "zs = drop (length xs) ws @ ys"
(is "_ = ?ws' @ _")
using True by simp
let ?U = "insert (D y) (sinks I D (D y) ?ws')"
have "ipurge_tr I D (D y) zs =
ipurge_tr I D (D y) ?ws' @ ipurge_tr_aux I D ?U ys"
using O by (simp add: ipurge_tr_append)
moreover have "ipurge_ref I D (D y) zs Y = ipurge_ref_aux I D ?U ys Y"
using O by (simp add: ipurge_ref_append)
ultimately show ?thesis
proof (cases "xs @ y # ipurge_tr I D (D y) ?ws' ∈ sentences P", simp_all)
assume P: "xs @ y # ipurge_tr I D (D y) ?ws' ∈ sentences P"
have Q: "(ipurge_tr_aux I D ?U ys, ipurge_ref_aux I D ?U ys Y) ∈ failures Q"
using E and G by (rule ipurge_tr_ref_aux_failures)
show "(xs @ y # ipurge_tr I D (D y) ?ws' @ ipurge_tr_aux I D ?U ys,
ipurge_ref_aux I D ?U ys Y) ∈ seq_comp_failures P Q"
proof (cases "ipurge_tr_aux I D ?U ys")
case Nil
have "(xs @ y # ipurge_tr I D (D y) ?ws', {x. x ≠ None}) ∈ failures P"
using B and C and P by (rule seq_sentences_ref)
moreover have "([], ipurge_ref_aux I D ?U ys Y) ∈ failures Q"
using Q and Nil by simp
ultimately have "(xs @ y # ipurge_tr I D (D y) ?ws',
insert None {x. x ≠ None} ∩ ipurge_ref_aux I D ?U ys Y)
∈ seq_comp_failures P Q"
by (rule SCF_R2 [OF P])
moreover have "insert None {x. x ≠ None} ∩
ipurge_ref_aux I D ?U ys Y = ipurge_ref_aux I D ?U ys Y"
by blast
ultimately show ?thesis
using Nil by simp
next
case Cons
hence "ipurge_tr_aux I D ?U ys ≠ []"
by simp
with P and Q have
"((xs @ y # ipurge_tr I D (D y) ?ws') @ ipurge_tr_aux I D ?U ys,
ipurge_ref_aux I D ?U ys Y) ∈ seq_comp_failures P Q"
by (rule SCF_R3)
thus ?thesis
by simp
qed
next
assume P: "xs @ y # ipurge_tr I D (D y) ?ws' ∉ sentences P"
have "ws = take (length xs) ws @ ?ws'"
by simp
moreover have "take (length xs) (ws @ ys) = take (length xs) (xs @ zs)"
using I by simp
hence "take (length xs) ws = xs"
using True by simp
ultimately have "xs @ ?ws' ∈ sentences P"
using F by simp
hence "xs @ ?ws' @ [None] ∈ traces P"
by (simp add: sentences_def)
hence "(xs @ ?ws' @ [None], {}) ∈ failures P"
by (rule traces_failures)
hence "(?ws' @ [None], {}) ∈ futures P xs"
by (simp add: futures_def)
moreover have "([y], {}) ∈ futures P xs"
using N by (simp add: futures_def)
ultimately have "(y # ipurge_tr I D (D y) (?ws' @ [None]),
ipurge_ref I D (D y) (?ws' @ [None]) {}) ∈ futures P xs"
using D by (simp add: secure_def del: ipurge_tr.simps)
hence Q: "(xs @ y # ipurge_tr I D (D y) (?ws' @ [None]), {}) ∈ failures P"
by (simp add: futures_def ipurge_ref_def)
have "set ?ws' ⊆ set ws"
by (rule set_drop_subset)
moreover have "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
hence "None ∉ set ws"
using F by (rule weakly_seq_sentences_none)
ultimately have R: "None ∉ set ?ws'"
by (rule contra_subsetD)
show "(xs @ y # ipurge_tr I D (D y) ?ws' @ ipurge_tr_aux I D ?U ys,
ipurge_ref_aux I D ?U ys Y) ∈ seq_comp_failures P Q"
proof (cases "(D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ?ws'. (u, D None) ∈ I)")
assume S: "(D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ?ws'. (u, D None) ∈ I)"
have "ipurge_tr_aux I D ?U ys = []"
proof (rule disjE [OF S], erule_tac [2] bexE)
assume T: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_tr_aux_nil [of "D y"], simp)
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using N by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using T by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
T: "u ∈ sinks I D (D y) ?ws'" and
U: "(u, D None) ∈ I"
have "∃w ∈ set ?ws'. u = D w"
using T by (rule sinks_elem)
then obtain w where V: "w ∈ set ?ws'" and W: "u = D w" ..
have X: "w ≠ None"
proof
assume "w = None"
hence "None ∈ set ?ws'"
using V by simp
moreover have "None ∉ set ?ws'"
using R by simp
ultimately show False
by contradiction
qed
show ?thesis
proof (rule ipurge_tr_aux_nil [of u], simp add: T)
fix x
have "(D w, D None) ∈ I ∧ w ≠ None ⟶
(∀v ∈ range D. (D w, v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D w, D None) ∈ I"
using U and W by simp
ultimately have "∀v ∈ range D. (D w, v) ∈ I"
using X by simp
thus "(u, D x) ∈ I"
using W by simp
qed
qed
moreover have "ipurge_ref_aux I D ?U ys Y = {}"
proof (rule disjE [OF S], erule_tac [2] bexE)
assume T: "(D y, D None) ∈ I"
show ?thesis
proof (rule ipurge_ref_aux_empty [of "D y"])
have "?U ⊆ sinks_aux I D ?U ys"
by (rule sinks_aux_subset)
moreover have "D y ∈ ?U"
by simp
ultimately show "D y ∈ sinks_aux I D ?U ys" ..
next
fix x
have "(D y, D None) ∈ I ∧ y ≠ None ⟶ (∀u ∈ range D. (D y, u) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "y ≠ None"
using N by (rule_tac not_sym, simp)
ultimately have "∀u ∈ range D. (D y, u) ∈ I"
using T by simp
thus "(D y, D x) ∈ I"
by simp
qed
next
fix u
assume
T: "u ∈ sinks I D (D y) ?ws'" and
U: "(u, D None) ∈ I"
have "∃w ∈ set ?ws'. u = D w"
using T by (rule sinks_elem)
then obtain w where V: "w ∈ set ?ws'" and W: "u = D w" ..
have X: "w ≠ None"
proof
assume "w = None"
hence "None ∈ set ?ws'"
using V by simp
moreover have "None ∉ set ?ws'"
using R by simp
ultimately show False
by contradiction
qed
show ?thesis
proof (rule ipurge_ref_aux_empty [of u])
have "?U ⊆ sinks_aux I D ?U ys"
by (rule sinks_aux_subset)
moreover have "u ∈ ?U"
using T by simp
ultimately show "u ∈ sinks_aux I D ?U ys" ..
next
fix x
have "(D w, D None) ∈ I ∧ w ≠ None ⟶
(∀v ∈ range D. (D w, v) ∈ I)"
using A by (simp add: secure_termination_def)
moreover have "(D w, D None) ∈ I"
using U and W by simp
ultimately have "∀v ∈ range D. (D w, v) ∈ I"
using X by simp
thus "(u, D x) ∈ I"
using W by simp
qed
qed
ultimately show ?thesis
proof simp
have "D None ∈ sinks I D (D y) (?ws' @ [None])"
using S by (simp only: sinks_interference_eq)
hence "(xs @ y # ipurge_tr I D (D y) ?ws', {}) ∈ failures P"
using Q by simp
moreover have "None ∉ set (xs @ y # ipurge_tr I D (D y) ?ws')"
proof (simp add: N)
have "set (ipurge_tr I D (D y) ?ws') ⊆ set ?ws'"
by (rule ipurge_tr_set)
thus "None ∉ set (ipurge_tr I D (D y) ?ws')"
using R by (rule contra_subsetD)
qed
ultimately show "(xs @ y # ipurge_tr I D (D y) ?ws', {})
∈ seq_comp_failures P Q"
by (rule SCF_R1 [OF P])
qed
next
assume "¬ ((D y, D None) ∈ I ∨
(∃u ∈ sinks I D (D y) ?ws'. (u, D None) ∈ I))"
hence "D None ∉ sinks I D (D y) (?ws' @ [None])"
by (simp only: sinks_interference_eq, simp)
hence "(xs @ y # ipurge_tr I D (D y) ?ws' @ [None], {}) ∈ failures P"
using Q by simp
hence "xs @ y # ipurge_tr I D (D y) ?ws' @ [None] ∈ traces P"
by (rule failures_traces)
hence "xs @ y # ipurge_tr I D (D y) ?ws' ∈ sentences P"
by (simp add: sentences_def)
thus ?thesis
using P by contradiction
qed
qed
next
case False
have "∀n ∈ {0<..length (xs @ [y])}. ∀W ∈ R n.
take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P ∧
(drop (length (xs @ [y]) - n) (xs @ [y]), W) ∈ failures Q"
(is "∀n ∈ _. ∀W ∈ _. ?T n W")
using J by simp
moreover have "n ≠ 0"
proof
have "∀W ∈ R 0.
xs @ [y] ∉ sentences P ∧
None ∉ set (xs @ [y]) ∧ (xs @ [y], W) ∈ failures P ∨
xs @ [y] ∈ sentences P ∧
(∃U V. (xs @ [y], U) ∈ failures P ∧ ([], V) ∈ failures Q ∧
W = insert None U ∩ V)"
(is "∀W ∈ _. ?T' W")
using J by blast
moreover assume "n = 0"
hence "∃W. W ∈ R 0"
using L by simp
then obtain W where "W ∈ R 0" ..
ultimately have "?T' W" ..
hence N: "xs @ [y] ∈ traces P ∧ None ∉ set (xs @ [y])"
proof (cases "xs @ [y] ∈ sentences P", simp_all del: ex_simps,
(erule_tac exE)+, (erule_tac [!] conjE)+, simp_all)
case False
assume "(xs @ [y], W) ∈ failures P"
moreover have "{} ⊆ W" ..
ultimately have "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
thus "xs @ [y] ∈ traces P"
by (rule failures_traces)
next
fix U
case True
assume "(xs @ [y], U) ∈ failures P"
moreover have "{} ⊆ U" ..
ultimately have "(xs @ [y], {}) ∈ failures P"
by (rule process_rule_3)
hence "xs @ [y] ∈ traces P"
by (rule failures_traces)
moreover have "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
hence "None ∉ set (xs @ [y])"
using True by (rule weakly_seq_sentences_none)
hence "None ≠ y ∧ None ∉ set xs"
by simp
ultimately show "xs @ [y] ∈ traces P ∧ None ≠ y ∧ None ∉ set xs" ..
qed
have "take (length xs) (xs @ zs) @ [y] = take (length xs) (ws @ ys) @ [y]"
using I by simp
hence "xs @ [y] = ws @ take (length xs - length ws) ys @ [y]"
using False by simp
moreover have "∃v vs. take (length xs - length ws) ys @ [y] = v # vs"
by (cases "take (length xs - length ws) ys @ [y]", simp_all)
then obtain v and vs where
"take (length xs - length ws) ys @ [y] = v # vs"
by blast
ultimately have O: "xs @ [y] = ws @ v # vs"
by simp
hence "ws @ v # vs ∈ traces P"
using N by simp
with C and F have "v = None"
by (rule seq_sentences_none)
moreover have "v ≠ None"
using N and O by (rule_tac not_sym, simp)
ultimately show False
by contradiction
qed
hence N: "n ∈ {0<..length (xs @ [y])}"
using M by blast
ultimately have "∀W ∈ R n. ?T n W" ..
moreover obtain W where "W ∈ R n"
using L ..
ultimately have O: "?T n W" ..
have P: "length (xs @ [y]) - n ≤ length xs"
using N by (simp, arith)
have "length (xs @ [y]) - n = length ws"
proof (rule ccontr, simp only: neq_iff, erule disjE)
assume Q: "length (xs @ [y]) - n < length ws"
moreover have "ws = take (length (xs @ [y]) - n) ws @
drop (length (xs @ [y]) - n) ws"
(is "_ = _ @ ?ws'")
by simp
ultimately have "ws = take (length (xs @ [y]) - n) (ws @ ys) @ ?ws'"
by simp
hence "ws = take (length (xs @ [y]) - n) (xs @ zs) @ ?ws'"
using I by simp
hence "ws = take (length (xs @ [y]) - n) (xs @ [y]) @ ?ws'"
using P by simp
moreover have "?ws' ≠ []"
using Q by simp
hence "∃v vs. ?ws' = v # vs"
by (cases ?ws', simp_all)
then obtain v and vs where "?ws' = v # vs"
by blast
ultimately have S: "ws = take (length (xs @ [y]) - n) (xs @ [y]) @ v # vs"
by simp
hence "(take (length (xs @ [y]) - n) (xs @ [y]) @ v # vs) @ [None]
∈ traces P"
using F by (simp add: sentences_def)
hence T: "take (length (xs @ [y]) - n) (xs @ [y]) @ v # vs ∈ traces P"
by (rule process_rule_2_traces)
have "take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P"
using O ..
with C have "v = None"
using T by (rule seq_sentences_none)
moreover have "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
hence "None ∉ set ws"
using F by (rule weakly_seq_sentences_none)
hence "v ≠ None"
using S by (rule_tac not_sym, simp)
ultimately show False
by contradiction
next
assume Q: "length ws < length (xs @ [y]) - n"
have "take (length (xs @ [y]) - n) (xs @ [y]) =
take (length (xs @ [y]) - n) (xs @ zs)"
using P by simp
also have "… = take (length (xs @ [y]) - n) (ws @ ys)"
using I by simp
also have "… = take (length (xs @ [y]) - n) ws @
take (length (xs @ [y]) - n - length ws) ys"
(is "_ = _ @ ?ys'")
by simp
also have "… = ws @ ?ys'"
using Q by simp
finally have "take (length (xs @ [y]) - n) (xs @ [y]) = ws @ ?ys'" .
moreover have "?ys' ≠ []"
using Q and H by simp
hence "∃v vs. ?ys' = v # vs"
by (cases ?ys', simp_all)
then obtain v and vs where "?ys' = v # vs"
by blast
ultimately have S: "take (length (xs @ [y]) - n) (xs @ [y]) = ws @ v # vs"
by simp
hence "(ws @ v # vs) @ [None] ∈ traces P"
using O by (simp add: sentences_def)
hence "ws @ v # vs ∈ traces P"
by (rule process_rule_2_traces)
with C and F have T: "v = None"
by (rule seq_sentences_none)
have "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
moreover have "take (length (xs @ [y]) - n) (xs @ [y]) ∈ sentences P"
using O ..
ultimately have "None ∉ set (take (length (xs @ [y]) - n) (xs @ [y]))"
by (rule weakly_seq_sentences_none)
hence "v ≠ None"
using S by (rule_tac not_sym, simp)
thus False
using T by contradiction
qed
hence "(drop (length ws) (xs @ [y]), W) ∈ failures Q"
using O by simp
hence "(drop (length ws) xs @ [y], W) ∈ failures Q"
(is "(?xs' @ _, _) ∈ _")
using False by simp
hence "([y], W) ∈ futures Q ?xs'"
by (simp add: futures_def)
moreover have "drop (length ws) (ws @ ys) = drop (length ws) (xs @ zs)"
using I by simp
hence "ys = ?xs' @ zs"
using False by simp
hence "(?xs' @ zs, Y) ∈ failures Q"
using G by simp
hence "(zs, Y) ∈ futures Q ?xs'"
by (simp add: futures_def)
ultimately have "(y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Y)
∈ futures Q ?xs'"
using E by (simp add: secure_def)
hence "(?xs' @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Y)
∈ failures Q"
by (simp add: futures_def)
moreover have "?xs' @ y # ipurge_tr I D (D y) zs ≠ []"
by simp
ultimately have "(ws @ ?xs' @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs Y) ∈ seq_comp_failures P Q"
by (rule SCF_R3 [OF F])
hence "((ws @ ?xs') @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs Y) ∈ seq_comp_failures P Q"
by simp
moreover have "xs = take (length ws) xs @ ?xs'"
by simp
hence "xs = take (length ws) (xs @ zs) @ ?xs'"
using False by simp
hence "xs = take (length ws) (ws @ ys) @ ?xs'"
using I by simp
hence "xs = ws @ ?xs'"
by simp
ultimately show ?thesis
by simp
qed
qed
lemma seq_comp_secure_aux_2 [rule_format]:
assumes
A: "secure_termination I D" and
B: "ref_union_closed P" and
C: "sequential P" and
D: "secure P I D" and
E: "secure Q I D"
shows "(ws, Z) ∈ seq_comp_failures P Q ⟹
ws = xs @ zs ⟶
(xs @ [y], {}) ∈ seq_comp_failures P Q ⟶
(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Z)
∈ seq_comp_failures P Q"
proof (erule seq_comp_failures.induct, (rule_tac [!] impI)+, simp_all, (erule conjE)+)
fix X
assume
"xs @ zs ∉ sentences P" and
"(xs @ zs, X) ∈ failures P" and
"None ∉ set xs" and
"None ∉ set zs" and
"(xs @ [y], {}) ∈ seq_comp_failures P Q"
thus "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X)
∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_2_case_1 [OF A C D])
next
fix X Y
assume
"xs @ zs ∈ sentences P" and
"(xs @ zs, X) ∈ failures P" and
"([], Y) ∈ failures Q" and
"(xs @ [y], {}) ∈ seq_comp_failures P Q"
thus "(xs @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs (insert None X ∩ Y)) ∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_2_case_2 [OF A C D E])
next
fix ws ys Y
assume
"ws ∈ sentences P" and
"(ys, Y) ∈ failures Q" and
"ys ≠ []" and
"ws @ ys = xs @ zs" and
"(xs @ [y], {}) ∈ seq_comp_failures P Q"
thus "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Y)
∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_2_case_3 [OF A B C D E])
next
fix X Y
assume
"(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs X)
∈ seq_comp_failures P Q" and
"(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Y)
∈ seq_comp_failures P Q"
hence "(xs @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs X ∪ ipurge_ref I D (D y) zs Y)
∈ seq_comp_failures P Q"
by (rule SCF_R4)
thus "(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs (X ∪ Y))
∈ seq_comp_failures P Q"
by (simp add: ipurge_ref_distrib_union)
qed
lemma seq_comp_secure_2:
assumes
A: "secure_termination I D" and
B: "ref_union_closed P" and
C: "sequential P" and
D: "secure P I D" and
E: "secure Q I D"
shows "(xs @ zs, Z) ∈ seq_comp_failures P Q ⟹
(xs @ [y], {}) ∈ seq_comp_failures P Q ⟹
(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Z)
∈ seq_comp_failures P Q"
by (rule seq_comp_secure_aux_2 [OF A B C D E, where ws = "xs @ zs"], simp_all)
text ‹
\null
Finally, the target security conservation theorem can be enunciated and proven, which is done here
below. The theorem states that for any two processes @{term P}, @{term Q} defined over the same
alphabet containing successful termination, to which the noninterference policy @{term I} and the
event-domain map @{term D} apply, if:
\begin{itemize}
\item
@{term I} and @{term D} enforce termination security,
\item
@{term P} is refusals union closed and sequential, and
\item
both @{term P} and @{term Q} are secure with respect to @{term I} and @{term D},
\end{itemize}
then @{term "P ; Q"} is secure as well.
\null
›
theorem seq_comp_secure:
assumes
A: "secure_termination I D" and
B: "ref_union_closed P" and
C: "sequential P" and
D: "secure P I D" and
E: "secure Q I D"
shows "secure (P ; Q) I D"
proof (simp add: secure_def seq_comp_futures seq_implies_weakly_seq [OF C],
(rule allI)+, rule impI, erule conjE)
fix xs y ys Y zs Z
assume
F: "(xs @ y # ys, Y) ∈ seq_comp_failures P Q" and
G: "(xs @ zs, Z) ∈ seq_comp_failures P Q"
show
"(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y)
∈ seq_comp_failures P Q ∧
(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Z)
∈ seq_comp_failures P Q"
(is "?A ∧ ?B")
proof
show ?A
by (rule seq_comp_secure_1 [OF A B C D E F])
next
have H: "weakly_sequential P"
using C by (rule seq_implies_weakly_seq)
hence "((xs @ [y]) @ ys, Y) ∈ failures (P ; Q)"
using F by (simp add: seq_comp_failures)
hence "(xs @ [y], {}) ∈ failures (P ; Q)"
by (rule process_rule_2_failures)
hence "(xs @ [y], {}) ∈ seq_comp_failures P Q"
using H by (simp add: seq_comp_failures)
thus ?B
by (rule seq_comp_secure_2 [OF A B C D E G])
qed
qed
subsection "Generalization of the security conservation theorem to lists of processes"
text ‹
The target security conservation theorem, in the basic version just proven, applies to the
sequential composition of a pair of processes. However, given an arbitrary list of processes where
each process satisfies its assumptions, the theorem could be orderly applied to the composition of
the first two processes in the list, then to the composition of the resulting process with the third
process in the list, and so on, until the last process is reached. The final outcome would be that
the sequential composition of all the processes in the list is secure.
Of course, this argument works provided that the assumptions of the theorem keep being satisfied by
the composed processes produced in each step of the recursion. But this is what indeed happens, by
virtue of the conservation of refusals union closure and sequentiality under sequential composition,
proven previously, and of the conservation of security under sequential composition, ensured by the
target theorem itself.
Therefore, the target security conservation theorem can be generalized to an arbitrary list of
processes, which is done here below. The resulting theorem states that for any nonempty list of
processes defined over the same alphabet containing successful termination, to which the
noninterference policy @{term I} and the event-domain map @{term D} apply, if:
\begin{itemize}
\item
@{term I} and @{term D} enforce termination security,
\item
each process in the list, with the possible exception of the last one, is refusals union closed and
sequential, and
\item
each process in the list is secure with respect to @{term I} and @{term D},
\end{itemize}
then the sequential composition of all the processes in the list is secure as well.
As a precondition, the above conservation lemmas for weak sequentiality, refusals union closure, and
sequentiality are generalized, too.
\null
›
lemma seq_comp_list_weakly_sequential [rule_format]:
"(∀X ∈ set (P # PS). weakly_sequential X) ⟶
weakly_sequential (foldl (;) P PS)"
proof (induction PS rule: rev_induct, simp, rule impI, simp, (erule conjE)+)
qed (rule seq_comp_weakly_sequential)
lemma seq_comp_list_ref_union_closed [rule_format]:
"(∀X ∈ set (butlast (P # PS)). weakly_sequential X) ⟶
(∀X ∈ set (P # PS). ref_union_closed X) ⟶
ref_union_closed (foldl (;) P PS)"
proof (induction PS rule: rev_induct, simp, (rule impI)+, simp, split if_split_asm,
simp, rule seq_comp_ref_union_closed, assumption+)
fix PS and Q :: "'a option process"
assume
A: "weakly_sequential P" and
B: "∀X ∈ set PS. weakly_sequential X" and
C: "ref_union_closed Q" and
D: "(∀X ∈ set (P # butlast PS). weakly_sequential X) ⟶
ref_union_closed (foldl (;) P PS)"
have "weakly_sequential (foldl (;) P PS)"
proof (rule seq_comp_list_weakly_sequential, simp, erule disjE, simp add: A)
fix X
assume "X ∈ set PS"
with B show "weakly_sequential X" ..
qed
moreover have "∀X ∈ set (P # butlast PS). weakly_sequential X"
proof (rule ballI, simp, erule disjE, simp add: A)
fix X
assume "X ∈ set (butlast PS)"
hence "X ∈ set PS"
by (rule in_set_butlastD)
with B show "weakly_sequential X" ..
qed
with D have "ref_union_closed (foldl (;) P PS)" ..
ultimately show "ref_union_closed (foldl (;) P PS ; Q)"
using C by (rule seq_comp_ref_union_closed)
qed
lemma seq_comp_list_sequential [rule_format]:
"(∀X ∈ set (P # PS). sequential X) ⟶
sequential (foldl (;) P PS)"
proof (induction PS rule: rev_induct, simp, rule impI, simp, (erule conjE)+)
qed (rule seq_comp_sequential)
theorem seq_comp_list_secure [rule_format]:
assumes A: "secure_termination I D"
shows
"(∀X ∈ set (butlast (P # PS)). ref_union_closed X ∧ sequential X) ⟶
(∀X ∈ set (P # PS). secure X I D) ⟶
secure (foldl (;) P PS) I D"
proof (induction PS rule: rev_induct, simp, (rule impI)+, simp, split if_split_asm,
simp, rule seq_comp_secure [OF A], assumption+)
fix PS Q
assume
B: "PS ≠ []" and
C: "ref_union_closed P" and
D: "sequential P" and
E: "∀X ∈ set PS. ref_union_closed X ∧ sequential X" and
F: "secure Q I D" and
G: "(∀X ∈ set (P # butlast PS). ref_union_closed X ∧ sequential X) ⟶
secure (foldl (;) P PS) I D"
have "ref_union_closed (foldl (;) P PS)"
proof (rule seq_comp_list_ref_union_closed, simp_all add: B, erule_tac [!] disjE,
simp_all add: C)
show "weakly_sequential P"
using D by (rule seq_implies_weakly_seq)
next
fix X
assume "X ∈ set (butlast PS)"
hence "X ∈ set PS"
by (rule in_set_butlastD)
with E have "ref_union_closed X ∧ sequential X" ..
hence "sequential X" ..
thus "weakly_sequential X"
by (rule seq_implies_weakly_seq)
next
fix X
assume "X ∈ set PS"
with E have "ref_union_closed X ∧ sequential X" ..
thus "ref_union_closed X" ..
qed
moreover have "sequential (foldl (;) P PS)"
proof (rule seq_comp_list_sequential, simp, erule disjE, simp add: D)
fix X
assume "X ∈ set PS"
with E have "ref_union_closed X ∧ sequential X" ..
thus "sequential X" ..
qed
moreover have "∀X ∈ set (P # butlast PS). ref_union_closed X ∧ sequential X"
proof (rule ballI, simp, erule disjE, simp add: C D)
fix X
assume "X ∈ set (butlast PS)"
hence "X ∈ set PS"
by (rule in_set_butlastD)
with E show "ref_union_closed X ∧ sequential X" ..
qed
with G have "secure (foldl (;) P PS) I D" ..
ultimately show "secure (foldl (;) P PS ; Q) I D"
using F by (rule seq_comp_secure [OF A])
qed
end