Theory GenericUnwinding
section "The Generic Unwinding Theorem"
theory GenericUnwinding
imports Noninterference_Ipurge_Unwinding.DeterministicProcesses
begin
text ‹
\null
The classical definition of noninterference security for a deterministic state machine with outputs
requires to consider the outputs produced by machine actions after any trace, i.e. any indefinitely
long sequence of actions, of the machine. In order to render the verification of the security of
such a machine more straightforward, there is a need of some sufficient condition for security such
that just individual actions, rather than unbounded sequences of actions, have to be taken into
consideration.
By extending previous results applying to transitive noninterference policies, Rushby \<^cite>‹"R4"› has
proven an unwinding theorem that provides a sufficient condition of this kind in the general case of
a possibly intransitive policy. This condition consists of a combination of predicates, which have
to be satisfied by a generic function mapping security domains into equivalence relations over
machine states.
An analogous problem arises for CSP noninterference security, whose definition given in \<^cite>‹"R1"›
requires to consider any possible future, i.e. any indefinitely long sequence of subsequent events
and any indefinitely large set of refused events associated to that sequence, for each process
trace.
This paper provides a sufficient condition for CSP noninterference security, which indeed requires
to just consider individual accepted and refused events and applies to the general case of a
possibly intransitive policy. This condition follows Rushby's one for classical noninterference
security; in some detail, it consists of a combination of predicates, which are the translations of
Rushby's ones into Hoare's Communicating Sequential Processes model of computation \<^cite>‹"R3"›. These
predicates have to be satisfied by a generic function mapping security domains into equivalence
relations over process traces; hence the name given to the condition,
\emph{Generic Unwinding Theorem}. Variants of this theorem applying to deterministic processes and
trace set processes (cf. \<^cite>‹"R2"›) are also proven.
The sufficient condition for security expressed by the Generic Unwinding Theorem would be even more
valuable if it also provided a necessary condition, viz. if for any secure process, there existed
some domain-relation map satisfying the condition. Particularly, a constructive proof of such
proposition, showing that some specified domain-relation map satisfies the condition whatever secure
process is given, would permit to determine whether a process is secure or not by verifying whether
the condition is satisfied by that map or not. However, this paper proves by counterexample that the
Generic Unwinding Theorem does not express a necessary condition for security as well, viz. a
process and a noninterference policy for that process are constructed such that the process is
secure with respect to the policy, but no domain-relation map satisfying the condition exists.
The contents of this paper are based on those of \<^cite>‹"R1"› and \<^cite>‹"R2"›. The salient points of
definitions and proofs are commented; for additional information, cf. Isabelle documentation,
particularly \<^cite>‹"R5"›, \<^cite>‹"R6"›, \<^cite>‹"R7"›, and \<^cite>‹"R8"›.
For the sake of brevity, given a function ‹F› of type
‹'a⇩1 ⇒ … ⇒ 'a⇩m ⇒ 'a⇩m⇩+⇩1 ⇒ … ⇒ 'a⇩n ⇒ 'b›, the explanatory text may discuss of ‹F›
using attributes that would more exactly apply to a term of type ‹'a⇩m⇩+⇩1 ⇒ … ⇒ 'a⇩n ⇒ 'b›.
In this case, it shall be understood that strictly speaking, such attributes apply to a term
matching pattern ‹F a⇩1 … a⇩m›.
›
subsection "Propaedeutic definitions and lemmas"
text ‹
Here below are the translations of Rushby's predicates \emph{weakly step consistent} and
\emph{locally respects} \<^cite>‹"R4"›, applying to deterministic state machines, into Hoare's
Communicating Sequential Processes model of computation \<^cite>‹"R3"›.
The differences with respect to Rushby's original predicates are the following ones:
\begin{itemize}
\item
The relations in the range of the domain-relation map hold between event lists rather than machine
states.
\item
The domains appearing as inputs of the domain-relation map do not unnecessarily encompass all the
possible values of the data type of domains, but just the domains in the range of the event-domain
map.
\item
While every machine action is accepted in a machine state, not every process event is generally
accepted after a process trace. Thus, whenever an event is appended to an event list in the
consequent of an implication, the antecedent of the implication constrains the event list to be a
trace, and the event to be accepted after that trace. In this way, the predicates do not
unnecessarily impose that the relations in the range of the domain-relation map hold between event
lists not being process traces.
\end{itemize}
\null
›
definition weakly_step_consistent ::
"'a process ⇒ ('a ⇒ 'd) ⇒ ('a, 'd) dom_rel_map ⇒ bool" where
"weakly_step_consistent P D R ≡ ∀u ∈ range D. ∀xs ys x.
(xs, ys) ∈ R u ∩ R (D x) ∧ x ∈ next_events P xs ∩ next_events P ys ⟶
(xs @ [x], ys @ [x]) ∈ R u"
definition locally_respects ::
"'a process ⇒ ('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ ('a, 'd) dom_rel_map ⇒ bool" where
"locally_respects P I D R ≡ ∀u ∈ range D. ∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u"
text ‹
\null
In what follows, some lemmas propaedeutic for the proof of the Generic Unwinding Theorem are
demonstrated.
\null
›
lemma ipurge_tr_aux_single_event:
"ipurge_tr_aux I D U [x] = (if ∃v ∈ U. (v, D x) ∈ I
then []
else [x])"
proof (cases "∃v ∈ U. (v, D x) ∈ I")
case True
have "ipurge_tr_aux I D U [x] = ipurge_tr_aux I D U ([] @ [x])" by simp
also have "… = []" using True by (simp only: ipurge_tr_aux.simps, simp)
finally show ?thesis using True by simp
next
case False
have "ipurge_tr_aux I D U [x] = ipurge_tr_aux I D U ([] @ [x])" by simp
also have "… = [x]" using False by (simp only: ipurge_tr_aux.simps, simp)
finally show ?thesis using False by simp
qed
lemma ipurge_tr_aux_cons:
"ipurge_tr_aux I D U (x # xs) = (if ∃v ∈ U. (v, D x) ∈ I
then ipurge_tr_aux I D (insert (D x) U) xs
else x # ipurge_tr_aux I D U xs)"
proof (induction xs rule: rev_induct, case_tac [!] "∃v ∈ U. (v, D x) ∈ I",
simp_all add: ipurge_tr_aux_single_event del: ipurge_tr_aux.simps(2))
fix x' xs
assume A: "ipurge_tr_aux I D U (x # xs) =
ipurge_tr_aux I D (insert (D x) U) xs"
(is "?T = ?T'")
assume "∃v ∈ U. (v, D x) ∈ I"
hence B: "sinks_aux I D U (x # xs) = sinks_aux I D (insert (D x) U) xs"
(is "?S = ?S'")
by (simp add: sinks_aux_cons)
show "ipurge_tr_aux I D U (x # xs @ [x']) =
ipurge_tr_aux I D (insert (D x) U) (xs @ [x'])"
proof (cases "∃v ∈ ?S. (v, D x') ∈ I")
case True
hence "ipurge_tr_aux I D U ((x # xs) @ [x']) = ?T"
by (simp only: ipurge_tr_aux.simps, simp)
moreover have "∃v ∈ ?S'. (v, D x') ∈ I" using B and True by simp
hence "ipurge_tr_aux I D (insert (D x) U) (xs @ [x']) = ?T'" by simp
ultimately show ?thesis using A by simp
next
case False
hence "ipurge_tr_aux I D U ((x # xs) @ [x']) = ?T @ [x']"
by (simp only: ipurge_tr_aux.simps, simp)
moreover have "¬ (∃v ∈ ?S'. (v, D x') ∈ I)" using B and False by simp
hence "ipurge_tr_aux I D (insert (D x) U) (xs @ [x']) = ?T' @ [x']" by simp
ultimately show ?thesis using A by simp
qed
next
fix x' xs
assume A: "ipurge_tr_aux I D U (x # xs) = x # ipurge_tr_aux I D U xs"
(is "?T = ?T'")
assume "∀v ∈ U. (v, D x) ∉ I"
hence B: "sinks_aux I D U (x # xs) = sinks_aux I D U xs"
(is "?S = ?S'")
by (simp add: sinks_aux_cons)
show "ipurge_tr_aux I D U (x # xs @ [x']) =
x # ipurge_tr_aux I D U (xs @ [x'])"
proof (cases "∃v ∈ ?S. (v, D x') ∈ I")
case True
hence "ipurge_tr_aux I D U ((x # xs) @ [x']) = ?T"
by (simp only: ipurge_tr_aux.simps, simp)
moreover have "∃v ∈ ?S'. (v, D x') ∈ I" using B and True by simp
hence "x # ipurge_tr_aux I D U (xs @ [x']) = ?T'" by simp
ultimately show ?thesis using A by simp
next
case False
hence "ipurge_tr_aux I D U ((x # xs) @ [x']) = ?T @ [x']"
by (simp only: ipurge_tr_aux.simps, simp)
moreover have "¬ (∃v ∈ ?S'. (v, D x') ∈ I)" using B and False by simp
hence "x # ipurge_tr_aux I D U (xs @ [x']) = ?T' @ [x']" by simp
ultimately show ?thesis using A by simp
qed
qed
lemma unaffected_domains_subset:
assumes
A: "U ⊆ range D" and
B: "U ≠ {}"
shows "unaffected_domains I D U xs ⊆ range D ∩ (-I) `` range D"
proof (subst unaffected_domains_def, rule subsetI, simp, erule conjE)
fix v
have "U ⊆ sinks_aux I D U xs" by (rule sinks_aux_subset)
moreover have "∃u. u ∈ U" using B by (simp add: ex_in_conv)
then obtain u where C: "u ∈ U" ..
ultimately have D: "u ∈ sinks_aux I D U xs" ..
assume "∀u ∈ sinks_aux I D U xs. (u, v) ∉ I"
hence "(u, v) ∉ I" using D ..
hence "(u, v) ∈ -I" by simp
moreover have "u ∈ range D" using A and C ..
ultimately show "v ∈ (-I) `` range D" ..
qed
subsection "The Generic Unwinding Theorem: proof of condition sufficiency"
text ‹
Rushby's \emph{Unwinding Theorem for Intransitive Policies} \<^cite>‹"R4"› states that a sufficient
condition for a deterministic state machine with outputs to be secure is the existence of some
domain-relation map \emph{R} such that:
\begin{enumerate}
\item
\emph{R} is a \emph{view partition}, i.e. the relations over machine states in its range are
equivalence relations;
\item
\emph{R} is \emph{output consistent}, i.e. states equivalent with respect to the domain of an action
produce the same output as a result of that action;
\item
\emph{R} is weakly step consistent;
\item
\emph{R} locally respects the policy.
\end{enumerate}
The idea behind the theorem is that a machine is secure if its states can be partitioned, for each
domain \emph{u}, into equivalence classes (1), such that the states in any such class \emph{C} are
indistinguishable with respect to the actions in \emph{u} (2), transition into the same equivalence
class \emph{C'} as a result of an action (3), and transition remaining inside \emph{C} as a result
of an action not allowed to affect \emph{u} (4).
This idea can simply be translated into the realm of Communicating Sequential Processes \<^cite>‹"R3"› by
replacing the words "machine", "state", "action" with "process", "trace", "event", respectively, as
long as a clarification is provided of what it precisely means for a pair of traces to be
"indistinguishable" with respect to the events in a given domain. Intuitively, this happens just in
case the events in that domain being accepted or refused after either trace are the same, thus the
simplest choice would be to replace output consistency with \emph{future consistency} as defined in
\<^cite>‹"R2"›. However, indistinguishability between traces in the same equivalence class is not
required in the case of a domain allowed to be affected by any domain, since the policy puts no
restriction on the differences in process histories that may be detected by such a domain. Hence, it
is sufficient to replace output consistency with \emph{weak future consistency} \<^cite>‹"R2"›.
Furthermore, indistinguishability with respect to individual refused events does not imply
indistinguishability with respect to sets of refused events, i.e. refusals, unless for each trace,
the corresponding refusals set is closed under set union. Therefore, for the condition to be
sufficient for process security, the \emph{refusals union closure} of the process \<^cite>‹"R2"› is also
required. As remarked in \<^cite>‹"R2"›, this property holds for any process admitting a meaningful
interpretation, so that taking it as an additional assumption does not give rise to any actual
limitation on the applicability of the theorem.
As a result of these considerations, the Generic Unwinding Theorem, formalized in what follows as
theorem ‹generic_unwinding›, states that a sufficient condition for the CSP noninterference
security \<^cite>‹"R1"› of a process being refusals union closed \<^cite>‹"R2"› is the existence of some
domain-relation map \emph{R} such that:
\begin{enumerate}
\item
\emph{R} is a view partition \<^cite>‹"R2"›;
\item
\emph{R} is weakly future consistent \<^cite>‹"R2"›;
\item
\emph{R} is weakly step consistent;
\item
\emph{R} locally respects the policy.
\end{enumerate}
\null
›
lemma ruc_wfc_failures:
assumes
RUC: "ref_union_closed P" and
WFC: "weakly_future_consistent P I D R" and
A: "U ⊆ range D ∩ (-I) `` range D" and
B: "U ≠ {}" and
C: "∀u ∈ U. (xs, xs') ∈ R u" and
D: "(xs, X) ∈ failures P"
shows "(xs', X ∩ D -` U) ∈ failures P"
proof (cases "∃x. x ∈ X ∩ D -` U")
let ?A = "singleton_set (X ∩ D -` U)"
have "∀xs A. (∃X. X ∈ A) ⟶ (∀X ∈ A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ A. X) ∈ failures P"
using RUC by (simp add: ref_union_closed_def)
hence "(∃X. X ∈ ?A) ⟶ (∀X ∈ ?A. (xs', X) ∈ failures P) ⟶
(xs', ⋃X ∈ ?A. X) ∈ failures P"
by blast
moreover case True
hence "∃X. X ∈ ?A" by (simp add: singleton_set_some)
ultimately have "(∀X ∈ ?A. (xs', X) ∈ failures P) ⟶
(xs', ⋃X ∈ ?A. X) ∈ failures P" ..
moreover have "∀X ∈ ?A. (xs', X) ∈ failures P"
proof (simp add: singleton_set_def, rule allI, rule impI, erule bexE, erule IntE,
simp)
fix x
have "∀u ∈ range D ∩ (-I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
next_dom_events P D u xs = next_dom_events P D u ys ∧
ref_dom_events P D u xs = ref_dom_events P D u ys"
using WFC by (simp add: weakly_future_consistent_def)
moreover assume E: "D x ∈ U"
with A have "D x ∈ range D ∩ (- I) `` range D" ..
ultimately have "∀xs ys. (xs, ys) ∈ R (D x) ⟶
next_dom_events P D (D x) xs = next_dom_events P D (D x) ys ∧
ref_dom_events P D (D x) xs = ref_dom_events P D (D x) ys" ..
hence "(xs, xs') ∈ R (D x) ⟶
next_dom_events P D (D x) xs = next_dom_events P D (D x) xs' ∧
ref_dom_events P D (D x) xs = ref_dom_events P D (D x) xs'"
by blast
moreover have "(xs, xs') ∈ R (D x)" using C and E ..
ultimately have "ref_dom_events P D (D x) xs =
ref_dom_events P D (D x) xs'"
by simp
moreover assume "x ∈ X"
hence "{x} ⊆ X" by simp
with D have "(xs, {x}) ∈ failures P" by (rule process_rule_3)
hence "x ∈ ref_dom_events P D (D x) xs"
by (simp add: ref_dom_events_def refusals_def)
ultimately have "x ∈ ref_dom_events P D (D x) xs'" by simp
thus "(xs', {x}) ∈ failures P" by (simp add: ref_dom_events_def refusals_def)
qed
ultimately have "(xs', ⋃X ∈ ?A. X) ∈ failures P" ..
thus "(xs', X ∩ D -` U) ∈ failures P" by (simp only: singleton_set_union)
next
have "∃u. u ∈ U" using B by (simp add: ex_in_conv)
then obtain u where E: "u ∈ U" ..
with A have "u ∈ range D ∩ (- I) `` range D" ..
moreover have "(xs, xs') ∈ R u" using C and E ..
ultimately have "(xs ∈ traces P) = (xs' ∈ traces P)"
by (rule wfc_traces [OF WFC])
moreover have "xs ∈ traces P" using D by (rule failures_traces)
ultimately have "xs' ∈ traces P" by simp
hence "(xs', {}) ∈ failures P" by (rule traces_failures)
moreover case False
hence "X ∩ D -` U = {}" by (simp only: ex_in_conv, simp)
ultimately show "(xs', X ∩ D -` U) ∈ failures P" by simp
qed
lemma ruc_wfc_lr_failures_1:
assumes
RUC: "ref_union_closed P" and
WFC: "weakly_future_consistent P I D R" and
LR: "locally_respects P I D R" and
A: "(xs @ [y], Y) ∈ failures P"
shows "(xs, {x ∈ Y. (D y, D x) ∉ I}) ∈ failures P"
proof (cases "∃x. x ∈ {x ∈ Y. (D y, D x) ∉ I}")
let ?A = "singleton_set {x ∈ Y. (D y, D x) ∉ I}"
have "∀xs A. (∃X. X ∈ A) ⟶ (∀X ∈ A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ A. X) ∈ failures P"
using RUC by (simp add: ref_union_closed_def)
hence "(∃X. X ∈ ?A) ⟶ (∀X ∈ ?A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ ?A. X) ∈ failures P"
by blast
moreover case True
hence "∃X. X ∈ ?A" by (simp add: singleton_set_some)
ultimately have "(∀X ∈ ?A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ ?A. X) ∈ failures P" ..
moreover have "∀X ∈ ?A. (xs, X) ∈ failures P"
proof (rule ballI, simp add: singleton_set_def, erule exE, (erule conjE)+, simp)
fix x
have "∀u ∈ range D ∩ (-I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
next_dom_events P D u xs = next_dom_events P D u ys ∧
ref_dom_events P D u xs = ref_dom_events P D u ys"
using WFC by (simp add: weakly_future_consistent_def)
moreover assume B: "(D y, D x) ∉ I"
hence "D x ∈ range D ∩ (-I) `` range D" by (simp add: Image_iff, rule exI)
ultimately have "∀xs ys. (xs, ys) ∈ R (D x) ⟶
next_dom_events P D (D x) xs = next_dom_events P D (D x) ys ∧
ref_dom_events P D (D x) xs = ref_dom_events P D (D x) ys" ..
hence C: "(xs, xs @ [y]) ∈ R (D x) ⟶
ref_dom_events P D (D x) xs = ref_dom_events P D (D x) (xs @ [y])"
by simp
have "∀xs y. (D y, D x) ∉ I ∧ y ∈ next_events P xs ⟶
(xs, xs @ [y]) ∈ R (D x)"
using LR by (simp add: locally_respects_def)
hence "(D y, D x) ∉ I ∧ y ∈ next_events P xs ⟶ (xs, xs @ [y]) ∈ R (D x)"
by blast
moreover have "xs @ [y] ∈ traces P" using A by (rule failures_traces)
hence "y ∈ next_events P xs" by (simp add: next_events_def)
ultimately have "(xs, xs @ [y]) ∈ R (D x)" using B by simp
with C have "ref_dom_events P D (D x) xs =
ref_dom_events P D (D x) (xs @ [y])" ..
moreover assume D: "x ∈ Y"
have "x ∈ ref_dom_events P D (D x) (xs @ [y])"
proof (simp add: ref_dom_events_def refusals_def)
have "{x} ⊆ Y" using D by (simp add: ipurge_ref_def)
with A show "(xs @ [y], {x}) ∈ failures P" by (rule process_rule_3)
qed
ultimately have "x ∈ ref_dom_events P D (D x) xs" by simp
thus "(xs, {x}) ∈ failures P" by (simp add: ref_dom_events_def refusals_def)
qed
ultimately have "(xs, ⋃X ∈ ?A. X) ∈ failures P" ..
thus ?thesis by (simp only: singleton_set_union)
next
case False
hence "{x ∈ Y. (D y, D x) ∉ I} = {}" by simp
moreover have "(xs, {}) ∈ failures P" using A by (rule process_rule_2)
ultimately show ?thesis by (simp (no_asm_simp))
qed
lemma ruc_wfc_lr_failures_2:
assumes
RUC: "ref_union_closed P" and
WFC: "weakly_future_consistent P I D R" and
LR: "locally_respects P I D R" and
A: "(xs, Z) ∈ failures P" and
Y: "xs @ [y] ∈ traces P"
shows "(xs @ [y], {x ∈ Z. (D y, D x) ∉ I}) ∈ failures P"
proof (cases "∃x. x ∈ {x ∈ Z. (D y, D x) ∉ I}")
let ?A = "singleton_set {x ∈ Z. (D y, D x) ∉ I}"
have "∀xs A. (∃X. X ∈ A) ⟶ (∀X ∈ A. (xs, X) ∈ failures P) ⟶
(xs, ⋃X ∈ A. X) ∈ failures P"
using RUC by (simp add: ref_union_closed_def)
hence "(∃X. X ∈ ?A) ⟶ (∀X ∈ ?A. (xs @ [y], X) ∈ failures P) ⟶
(xs @ [y], ⋃X ∈ ?A. X) ∈ failures P"
by blast
moreover case True
hence "∃X. X ∈ ?A" by (simp add: singleton_set_some)
ultimately have "(∀X ∈ ?A. (xs @ [y], X) ∈ failures P) ⟶
(xs @ [y], ⋃X ∈ ?A. X) ∈ failures P" ..
moreover have "∀X ∈ ?A. (xs @ [y], X) ∈ failures P"
proof (rule ballI, simp add: singleton_set_def, erule exE, (erule conjE)+, simp)
fix x
have "∀u ∈ range D ∩ (-I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
next_dom_events P D u xs = next_dom_events P D u ys ∧
ref_dom_events P D u xs = ref_dom_events P D u ys"
using WFC by (simp add: weakly_future_consistent_def)
moreover assume B: "(D y, D x) ∉ I"
hence "D x ∈ range D ∩ (-I) `` range D" by (simp add: Image_iff, rule exI)
ultimately have "∀xs ys. (xs, ys) ∈ R (D x) ⟶
next_dom_events P D (D x) xs = next_dom_events P D (D x) ys ∧
ref_dom_events P D (D x) xs = ref_dom_events P D (D x) ys" ..
hence C: "(xs, xs @ [y]) ∈ R (D x) ⟶
ref_dom_events P D (D x) xs = ref_dom_events P D (D x) (xs @ [y])"
by simp
have "∀xs y. (D y, D x) ∉ I ∧ y ∈ next_events P xs ⟶
(xs, xs @ [y]) ∈ R (D x)"
using LR by (simp add: locally_respects_def)
hence "(D y, D x) ∉ I ∧ y ∈ next_events P xs ⟶ (xs, xs @ [y]) ∈ R (D x)"
by blast
moreover have "y ∈ next_events P xs" using Y by (simp add: next_events_def)
ultimately have "(xs, xs @ [y]) ∈ R (D x)" using B by simp
with C have "ref_dom_events P D (D x) xs =
ref_dom_events P D (D x) (xs @ [y])" ..
moreover assume D: "x ∈ Z"
have "x ∈ ref_dom_events P D (D x) xs"
proof (simp add: ref_dom_events_def refusals_def)
have "{x} ⊆ Z" using D by (simp add: ipurge_ref_def)
with A show "(xs, {x}) ∈ failures P" by (rule process_rule_3)
qed
ultimately have "x ∈ ref_dom_events P D (D x) (xs @ [y])" by simp
thus "(xs @ [y], {x}) ∈ failures P"
by (simp add: ref_dom_events_def refusals_def)
qed
ultimately have "(xs @ [y], ⋃X ∈ ?A. X) ∈ failures P" ..
thus ?thesis by (simp only: singleton_set_union)
next
case False
hence "{x ∈ Z. (D y, D x) ∉ I} = {}" by simp
moreover have "(xs @ [y], {}) ∈ failures P" using Y by (rule traces_failures)
ultimately show ?thesis by (simp (no_asm_simp))
qed
lemma gu_condition_imply_secure_aux [rule_format]:
assumes
VP: "view_partition P D R" and
WFC: "weakly_future_consistent P I D R" and
WSC: "weakly_step_consistent P D R" and
LR: "locally_respects P I D R"
shows "U ⊆ range D ⟶ U ≠ {} ⟶ xs @ ys ∈ traces P ⟶
(∀u ∈ unaffected_domains I D U []. (xs, xs') ∈ R u) ⟶
(∀u ∈ unaffected_domains I D U ys.
(xs @ ys, xs' @ ipurge_tr_aux I D U ys) ∈ R u)"
proof (induction ys arbitrary: xs xs' U, simp_all add: unaffected_domains_def,
((rule impI)+, (rule allI)?)+, erule conjE)
fix y ys xs xs' U u
assume
A: "⋀xs xs' U. U ⊆ range D ⟶ U ≠ {} ⟶ xs @ ys ∈ traces P ⟶
(∀u. u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶
(xs, xs') ∈ R u) ⟶
(∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D U ys. (v, u) ∉ I) ⟶
(xs @ ys, xs' @ ipurge_tr_aux I D U ys) ∈ R u)" and
B: "U ⊆ range D" and
C: "U ≠ {}" and
D: "xs @ y # ys ∈ traces P" and
E: "∀u. u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶ (xs, xs') ∈ R u" and
F: "u ∈ range D" and
G: "∀v ∈ sinks_aux I D U (y # ys). (v, u) ∉ I"
show "(xs @ y # ys, xs' @ ipurge_tr_aux I D U (y # ys)) ∈ R u"
proof (cases "∃v ∈ U. (v, D y) ∈ I",
simp_all (no_asm_simp) add: ipurge_tr_aux_cons)
case True
let ?U' = "insert (D y) U"
have "?U' ⊆ range D ⟶ ?U' ≠ {} ⟶ (xs @ [y]) @ ys ∈ traces P ⟶
(∀u. u ∈ range D ∧ (∀v ∈ ?U'. (v, u) ∉ I) ⟶
(xs @ [y], xs') ∈ R u) ⟶
(∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D ?U' ys. (v, u) ∉ I) ⟶
((xs @ [y]) @ ys, xs' @ ipurge_tr_aux I D ?U' ys) ∈ R u)"
using A .
hence
"(∀u. u ∈ range D ∧ (∀v ∈ ?U'. (v, u) ∉ I) ⟶
(xs @ [y], xs') ∈ R u) ⟶
(∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D ?U' ys. (v, u) ∉ I) ⟶
(xs @ y # ys, xs' @ ipurge_tr_aux I D ?U' ys) ∈ R u)"
using B and D by simp
moreover have
"∀u. u ∈ range D ∧ (∀v ∈ ?U'. (v, u) ∉ I) ⟶
(xs @ [y], xs') ∈ R u"
proof (rule allI, rule impI, erule conjE)
fix u
assume F: "u ∈ range D" and G: "∀v ∈ ?U'. (v, u) ∉ I"
moreover have "u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶ (xs, xs') ∈ R u"
using E ..
ultimately have H: "(xs, xs') ∈ R u" by simp
have "∀u ∈ range D. (D y, u) ∉ I ∧ y ∈ next_events P xs ⟶
(xs, xs @ [y]) ∈ R u"
using LR by (simp add: locally_respects_def)
hence "(D y, u) ∉ I ∧ y ∈ next_events P xs ⟶ (xs, xs @ [y]) ∈ R u"
using F ..
moreover have "D y ∈ ?U'" by simp
with G have "(D y, u) ∉ I" ..
moreover have "(xs @ [y]) @ ys ∈ traces P" using D by simp
hence "y ∈ next_events P xs"
by (simp (no_asm_simp) add: next_events_def, rule process_rule_2_traces)
ultimately have I: "(xs, xs @ [y]) ∈ R u" by simp
have "∀u ∈ range D. equiv (traces P) (R u)"
using VP by (simp add: view_partition_def)
hence J: "equiv (traces P) (R u)" using F ..
hence "trans (R u)" by (simp add: equiv_def)
moreover have "sym (R u)" using J by (simp add: equiv_def)
hence "(xs @ [y], xs) ∈ R u" using I by (rule symE)
ultimately show "(xs @ [y], xs') ∈ R u" using H by (rule transE)
qed
ultimately have
"∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D ?U' ys. (v, u) ∉ I) ⟶
(xs @ y # ys, xs' @ ipurge_tr_aux I D ?U' ys) ∈ R u" ..
hence
"u ∈ range D ∧ (∀v ∈ sinks_aux I D ?U' ys. (v, u) ∉ I) ⟶
(xs @ y # ys, xs' @ ipurge_tr_aux I D ?U' ys) ∈ R u" ..
moreover have "sinks_aux I D U (y # ys) = sinks_aux I D ?U' ys"
using Cons and True by (simp add: sinks_aux_cons)
hence "∀v ∈ sinks_aux I D ?U' ys. (v, u) ∉ I" using G by simp
with F have "u ∈ range D ∧ (∀v ∈ sinks_aux I D ?U' ys. (v, u) ∉ I)" ..
ultimately show "(xs @ y # ys, xs' @ ipurge_tr_aux I D ?U' ys) ∈ R u" ..
next
case False
have
"U ⊆ range D ⟶ U ≠ {} ⟶ (xs @ [y]) @ ys ∈ traces P ⟶
(∀u. u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶
(xs @ [y], xs' @ [y]) ∈ R u) ⟶
(∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D U ys. (v, u) ∉ I) ⟶
((xs @ [y]) @ ys, (xs' @ [y]) @ ipurge_tr_aux I D U ys) ∈ R u)"
using A .
hence
"(∀u. u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶
(xs @ [y], xs' @ [y]) ∈ R u) ⟶
(∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D U ys. (v, u) ∉ I) ⟶
(xs @ y # ys, xs' @ y # ipurge_tr_aux I D U ys) ∈ R u)"
using B and C and D by simp
moreover have
"∀u. u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶
(xs @ [y], xs' @ [y]) ∈ R u"
proof (rule allI, rule impI, erule conjE)
fix u
assume F: "u ∈ range D" and G: "∀v ∈ U. (v, u) ∉ I"
moreover have "u ∈ range D ∧ (∀v ∈ U. (v, u) ∉ I) ⟶ (xs, xs') ∈ R u"
using E ..
ultimately have "(xs, xs') ∈ R u" by simp
moreover have "D y ∈ range D ∧
(∀v ∈ U. (v, D y) ∉ I) ⟶ (xs, xs') ∈ R (D y)"
using E ..
hence "(xs, xs') ∈ R (D y)" using False by simp
ultimately have H: "(xs, xs') ∈ R u ∩ R (D y)" ..
have "∃v. v ∈ U" using C by (simp add: ex_in_conv)
then obtain v where I: "v ∈ U" ..
hence "(v, D y) ∈ -I" using False by simp
moreover have "v ∈ range D" using B and I ..
ultimately have "D y ∈ (-I) `` range D" ..
hence J: "D y ∈ range D ∩ (-I) `` range D" by simp
have "∀u ∈ range D ∩ (-I) `` range D. ∀xs ys. (xs, ys) ∈ R u ⟶
next_dom_events P D u xs = next_dom_events P D u ys ∧
ref_dom_events P D u xs = ref_dom_events P D u ys"
using WFC by (simp add: weakly_future_consistent_def)
hence "∀xs ys. (xs, ys) ∈ R (D y) ⟶
next_dom_events P D (D y) xs = next_dom_events P D (D y) ys ∧
ref_dom_events P D (D y) xs = ref_dom_events P D (D y) ys"
using J ..
hence "(xs, xs') ∈ R (D y) ⟶
next_dom_events P D (D y) xs = next_dom_events P D (D y) xs' ∧
ref_dom_events P D (D y) xs = ref_dom_events P D (D y) xs'"
by blast
hence "next_dom_events P D (D y) xs = next_dom_events P D (D y) xs'"
using H by simp
moreover have "(xs @ [y]) @ ys ∈ traces P" using D by simp
hence K: "y ∈ next_events P xs"
by (simp (no_asm_simp) add: next_events_def, rule process_rule_2_traces)
hence "y ∈ next_dom_events P D (D y) xs"
by (simp add: next_dom_events_def)
ultimately have "y ∈ next_events P xs'" by (simp add: next_dom_events_def)
with K have L: "y ∈ next_events P xs ∩ next_events P xs'" ..
have "∀u ∈ range D. ∀xs ys x.
(xs, ys) ∈ R u ∩ R (D x) ∧ x ∈ next_events P xs ∩ next_events P ys ⟶
(xs @ [x], ys @ [x]) ∈ R u"
using WSC by (simp add: weakly_step_consistent_def)
hence "∀xs ys x.
(xs, ys) ∈ R u ∩ R (D x) ∧ x ∈ next_events P xs ∩ next_events P ys ⟶
(xs @ [x], ys @ [x]) ∈ R u"
using F ..
hence
"(xs, xs') ∈ R u ∩ R (D y) ∧ y ∈ next_events P xs ∩ next_events P xs' ⟶
(xs @ [y], xs' @ [y]) ∈ R u"
by blast
thus "(xs @ [y], xs' @ [y]) ∈ R u" using H and L by simp
qed
ultimately have
"∀u. u ∈ range D ∧ (∀v ∈ sinks_aux I D U ys. (v, u) ∉ I) ⟶
(xs @ y # ys, xs' @ y # ipurge_tr_aux I D U ys) ∈ R u" ..
hence "u ∈ range D ∧ (∀v ∈ sinks_aux I D U ys. (v, u) ∉ I) ⟶
(xs @ y # ys, xs' @ y # ipurge_tr_aux I D U ys) ∈ R u" ..
moreover have "sinks_aux I D U (y # ys) = sinks_aux I D U ys"
using Cons and False by (simp add: sinks_aux_cons)
hence "∀v ∈ sinks_aux I D U ys. (v, u) ∉ I" using G by simp
with F have "u ∈ range D ∧ (∀v ∈ sinks_aux I D U ys. (v, u) ∉ I)" ..
ultimately show "(xs @ y # ys, xs' @ y # ipurge_tr_aux I D U ys) ∈ R u" ..
qed
qed
lemma gu_condition_imply_secure_1 [rule_format]:
assumes
RUC: "ref_union_closed P" and
VP: "view_partition P D R" and
WFC: "weakly_future_consistent P I D R" and
WSC: "weakly_step_consistent P D R" and
LR: "locally_respects P I D R"
shows "(xs @ y # ys, Y) ∈ failures P ⟶
(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y) ∈ failures P"
proof (induction ys arbitrary: Y rule: rev_induct, rule_tac [!] impI,
simp add: ipurge_ref_def)
fix Y
assume "(xs @ [y], Y) ∈ failures P"
with RUC and WFC and LR show
"(xs, {x ∈ Y. (D y, D x) ∉ I}) ∈ failures P"
by (rule ruc_wfc_lr_failures_1)
next
fix y' ys Y
assume
A: "⋀Y'. (xs @ y # ys, Y') ∈ failures P ⟶
(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y') ∈ failures P" and
B: "(xs @ y # ys @ [y'], Y) ∈ failures P"
show "(xs @ ipurge_tr I D (D y) (ys @ [y']), ipurge_ref I D (D y) (ys @ [y']) Y)
∈ failures P"
proof (cases "D y' ∈ sinks I D (D y) (ys @ [y'])", simp del: sinks.simps)
let ?Y' = "{x ∈ Y. (D y', D x) ∉ I}"
have "(xs @ y # ys, ?Y') ∈ failures P ⟶
(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys ?Y') ∈ failures P"
using A .
moreover have "((xs @ y # ys) @ [y'], Y) ∈ failures P" using B by simp
with RUC and WFC and LR have "(xs @ y # ys, ?Y') ∈ failures P"
by (rule ruc_wfc_lr_failures_1)
ultimately have
"(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys ?Y') ∈ failures P" ..
moreover case True
hence "ipurge_ref I D (D y) (ys @ [y']) Y = ipurge_ref I D (D y) ys ?Y'"
by (rule ipurge_ref_eq)
ultimately show
"(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) (ys @ [y']) Y) ∈ failures P"
by simp
next
case False
have "unaffected_domains I D {D y} (ys @ [y']) ⊆ range D ∩ (-I) `` range D"
(is "?U ⊆ _")
by (rule unaffected_domains_subset, simp_all)
moreover have "?U ≠ {}"
proof -
have "(D y, D y') ∉ I" using False by (rule_tac notI, simp)
moreover
have "¬ ((D y, D y') ∈ I ∨ (∃v ∈ sinks I D (D y) ys. (v, D y') ∈ I))"
using False by (simp only: sinks_interference_eq, simp)
then have "∀v ∈ sinks I D (D y) (ys @ [y']). (v, D y') ∉ I" by simp
ultimately show "?U ≠ {}"
apply (simp (no_asm_simp) add: unaffected_domains_def sinks_aux_single_dom set_eq_iff)
using ‹(D y, D y') ∉ I› by auto
qed
moreover have C: "xs @ y # ys @ [y'] ∈ traces P"
using B by (rule failures_traces)
have "∀u ∈ ?U. ((xs @ [y]) @ ys @ [y'],
xs @ ipurge_tr_aux I D {D y} (ys @ [y'])) ∈ R u"
proof (rule ballI, rule gu_condition_imply_secure_aux [OF VP WFC WSC LR],
simp_all add: unaffected_domains_def C, (erule conjE)+)
fix u
have "∀u ∈ range D. ∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u"
using LR by (simp add: locally_respects_def)
moreover assume D: "u ∈ range D"
ultimately have "∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u" ..
hence "(D y, u) ∉ I ∧ y ∈ next_events P xs ⟶
(xs, xs @ [y]) ∈ R u"
by blast
moreover assume "(D y, u) ∉ I"
moreover have "(xs @ [y]) @ ys @ [y'] ∈ traces P" using C 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 have E: "(xs, xs @ [y]) ∈ R u" by simp
have "∀u ∈ range D. equiv (traces P) (R u)"
using VP by (simp add: view_partition_def)
hence "equiv (traces P) (R u)" using D ..
hence "sym (R u)" by (simp add: equiv_def)
thus "(xs @ [y], xs) ∈ R u" using E by (rule symE)
qed
hence "∀u ∈ ?U. (xs @ y # ys @ [y'],
xs @ ipurge_tr I D (D y) (ys @ [y'])) ∈ R u"
by (simp only: ipurge_tr_aux_single_dom, simp)
ultimately have "(xs @ ipurge_tr I D (D y) (ys @ [y']), Y ∩ D -` ?U)
∈ failures P"
using B by (rule ruc_wfc_failures [OF RUC WFC])
moreover have
"Y ∩ D -` ?U = {x ∈ Y. D x ∈ unaffected_domains I D {D y} (ys @ [y'])}"
by (simp add: set_eq_iff)
ultimately show ?thesis by (simp only: unaffected_domains_single_dom)
qed
qed
lemma gu_condition_imply_secure_2 [rule_format]:
assumes
RUC: "ref_union_closed P" and
VP: "view_partition P D R" and
WFC: "weakly_future_consistent P I D R" and
WSC: "weakly_step_consistent P D R" and
LR: "locally_respects P I D R" and
Y: "xs @ [y] ∈ traces P"
shows "(xs @ zs, Z) ∈ failures P ⟶
(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Z) ∈ failures P"
proof (induction zs arbitrary: Z rule: rev_induct, rule_tac [!] impI,
simp add: ipurge_ref_def)
fix Z
assume "(xs, Z) ∈ failures P"
with RUC and WFC and LR show
"(xs @ [y], {x ∈ Z. (D y, D x) ∉ I}) ∈ failures P"
using Y by (rule ruc_wfc_lr_failures_2)
next
fix z zs Z
assume
A: "⋀Z'. (xs @ zs, Z') ∈ failures P ⟶
(xs @ y # ipurge_tr I D (D y) zs,
ipurge_ref I D (D y) zs Z') ∈ failures P" and
B: "(xs @ zs @ [z], Z) ∈ failures P"
show "(xs @ y # ipurge_tr I D (D y) (zs @ [z]),
ipurge_ref I D (D y) (zs @ [z]) Z) ∈ failures P"
proof (cases "D z ∈ sinks I D (D y) (zs @ [z])", simp del: sinks.simps)
let ?Z' = "{x ∈ Z. (D z, D x) ∉ I}"
have "(xs @ zs, ?Z') ∈ failures P ⟶
(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs ?Z') ∈ failures P"
using A .
moreover have "((xs @ zs) @ [z], Z) ∈ failures P" using B by simp
with RUC and WFC and LR have "(xs @ zs, ?Z') ∈ failures P"
by (rule ruc_wfc_lr_failures_1)
ultimately have
"(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs ?Z') ∈ failures P" ..
moreover case True
hence "ipurge_ref I D (D y) (zs @ [z]) Z = ipurge_ref I D (D y) zs ?Z'"
by (rule ipurge_ref_eq)
ultimately show
"(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) (zs @ [z]) Z)
∈ failures P"
by simp
next
case False
have "unaffected_domains I D {D y} (zs @ [z]) ⊆ range D ∩ (-I) `` range D"
(is "?U ⊆ _")
by (rule unaffected_domains_subset, simp_all)
moreover have "?U ≠ {}"
proof -
have "(D y, D z) ∉ I" using False by (rule_tac notI, simp)
moreover
have "¬ ((D y, D z) ∈ I ∨ (∃v ∈ sinks I D (D y) zs. (v, D z) ∈ I))"
using False by (simp only: sinks_interference_eq, simp)
then have "∀v ∈ sinks I D (D y) (zs @ [z]). (v, D z) ∉ I" by simp
ultimately show "?U ≠ {}"
apply (simp (no_asm_simp) add: unaffected_domains_def sinks_aux_single_dom set_eq_iff)
using ‹(D y, D z) ∉ I› by auto
qed
moreover have C: "xs @ zs @ [z] ∈ traces P" using B by (rule failures_traces)
have "∀u ∈ ?U. (xs @ zs @ [z],
(xs @ [y]) @ ipurge_tr_aux I D {D y} (zs @ [z])) ∈ R u"
proof (rule ballI, rule gu_condition_imply_secure_aux [OF VP WFC WSC LR],
simp_all add: unaffected_domains_def C, (erule conjE)+)
fix u
have "∀u ∈ range D. ∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u"
using LR by (simp add: locally_respects_def)
moreover assume D: "u ∈ range D"
ultimately have "∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u" ..
hence "(D y, u) ∉ I ∧ y ∈ next_events P xs ⟶ (xs, xs @ [y]) ∈ R u" by blast
moreover assume "(D y, u) ∉ I"
moreover have "y ∈ next_events P xs" using Y by (simp add: next_events_def)
ultimately show "(xs, xs @ [y]) ∈ R u" by simp
qed
hence "∀u ∈ ?U. (xs @ zs @ [z],
xs @ y # ipurge_tr I D (D y) (zs @ [z])) ∈ R u"
by (simp only: ipurge_tr_aux_single_dom, simp)
ultimately have "(xs @ y # ipurge_tr I D (D y) (zs @ [z]), Z ∩ D -` ?U)
∈ failures P"
using B by (rule ruc_wfc_failures [OF RUC WFC])
moreover have
"Z ∩ D -` ?U = {x ∈ Z. D x ∈ unaffected_domains I D {D y} (zs @ [z])}"
by (simp add: set_eq_iff)
ultimately show ?thesis by (simp only: unaffected_domains_single_dom)
qed
qed
theorem generic_unwinding:
assumes
RUC: "ref_union_closed P" and
VP: "view_partition P D R" and
WFC: "weakly_future_consistent P I D R" and
WSC: "weakly_step_consistent P D R" and
LR: "locally_respects P I D R"
shows "secure P I D"
proof (simp add: secure_def futures_def, (rule allI)+, rule impI, erule conjE)
fix xs y ys Y zs Z
assume
A: "(xs @ y # ys, Y) ∈ failures P" and
B: "(xs @ zs, Z) ∈ failures P"
show "(xs @ ipurge_tr I D (D y) ys, ipurge_ref I D (D y) ys Y) ∈ failures P ∧
(xs @ y # ipurge_tr I D (D y) zs, ipurge_ref I D (D y) zs Z) ∈ failures P"
(is "?P ∧ ?Q")
proof
show ?P using RUC and VP and WFC and WSC and LR and A
by (rule gu_condition_imply_secure_1)
next
have "((xs @ [y]) @ ys, Y) ∈ failures P" using A by simp
hence "(xs @ [y], {}) ∈ failures P" by (rule process_rule_2_failures)
hence "xs @ [y] ∈ traces P" by (rule failures_traces)
with RUC and VP and WFC and WSC and LR show ?Q using B
by (rule gu_condition_imply_secure_2)
qed
qed
text ‹
\null
It is interesting to observe that unlike symmetry and transitivity, the assumed reflexivity of the
relations in the range of the domain-relation map is never used in the proof of the Generic
Unwinding Theorem. Nonetheless, by assuming that such relations be equivalence relations over
process traces rather than just symmetric and transitive ones, reflexivity has been kept among
assumptions for both historical reasons -- Rushby's Unwinding Theorem for deterministic state
machines deals with equivalence relations -- and practical reasons -- predicate
@{term "refl_on (traces P)"} may only be verified by a relation included in
@{term "traces P × traces P"}, thus ensuring that traces be not correlated with non-trace event
lists, which is a necessary condition for weak future consistency (cf. \<^cite>‹"R2"›).
Here below are convenient variants of the Generic Unwinding Theorem applying to deterministic
processes and trace set processes (cf. \<^cite>‹"R2"›).
\null
›
theorem d_generic_unwinding:
"deterministic P ⟹
view_partition P D R ⟹
d_weakly_future_consistent P I D R ⟹
weakly_step_consistent P D R ⟹
locally_respects P I D R ⟹
secure P I D"
proof (rule generic_unwinding, rule d_implies_ruc, simp_all)
qed (drule d_wfc_equals_dwfc [of P I D R], simp)
theorem ts_generic_unwinding:
"trace_set T ⟹
view_partition (ts_process T) D R ⟹
d_weakly_future_consistent (ts_process T) I D R ⟹
weakly_step_consistent (ts_process T) D R ⟹
locally_respects (ts_process T) I D R ⟹
secure (ts_process T) I D"
proof (rule d_generic_unwinding, simp_all)
qed (rule ts_process_d)
subsection "The Generic Unwinding Theorem: counterexample to condition necessity"
text ‹
At a first glance, it seems reasonable to hypothesize that the Generic Unwinding Theorem expresses
a necessary, as well as sufficient, condition for security, viz. that whenever a process is secure
with respect to a policy, there should exist a set of "views" of process traces, one per domain,
satisfying the apparently simple assumptions of the theorem.
It can thus be surprising to discover that this hypothesis is false, as proven in what follows by
constructing a counterexample. The key observation for attaining this result is that symmetry,
transitivity, weak step consistency, and local policy respect permit to infer the correlation of
pairs of traces, and can then be given the form of introduction rules in the inductive definition of
a set. In this way, a "minimum" domain-relation map ‹rel_induct› is obtained, viz. a map such
that, for each domain ‹u›, the image of ‹u› under this map is included in the image of
‹u› under any map which has the aforesaid properties -- particularly, which satisfies the
assumptions of the Generic Unwinding Theorem.
Although reflexivity can be given the form of an introduction rule, too, it has been omitted from
the inductive definition. This has been done in order to ensure that the "minimum" domain-relation
map, and consequently the counterexample as well, still remain such even if reflexivity, being
unnecessary (cf. above), were removed from the assumptions of the Generic Unwinding Theorem.
\null
›
inductive_set rel_induct_aux ::
"'a process ⇒ ('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ ('d × 'a list × 'a list) set"
for P :: "'a process" and I :: "('d × 'd) set" and D :: "'a ⇒ 'd" where
rule_sym: "(u, xs, ys) ∈ rel_induct_aux P I D ⟹
(u, ys, xs) ∈ rel_induct_aux P I D" |
rule_trans: "⟦(u, xs, ys) ∈ rel_induct_aux P I D;
(u, ys, zs) ∈ rel_induct_aux P I D⟧ ⟹
(u, xs, zs) ∈ rel_induct_aux P I D" |
rule_WSC: "⟦(u, xs, ys) ∈ rel_induct_aux P I D;
(D x, xs, ys) ∈ rel_induct_aux P I D;
x ∈ next_events P xs ∩ next_events P ys⟧ ⟹
(u, xs @ [x], ys @ [x]) ∈ rel_induct_aux P I D" |
rule_LR: "⟦u ∈ range D; (D x, u) ∉ I; x ∈ next_events P xs⟧ ⟹
(u, xs, xs @ [x]) ∈ rel_induct_aux P I D"
definition rel_induct ::
"'a process ⇒ ('d × 'd) set ⇒ ('a ⇒ 'd) ⇒ ('a, 'd) dom_rel_map" where
"rel_induct P I D u ≡ rel_induct_aux P I D `` {u}"
lemma rel_induct_subset:
assumes
VP: "view_partition P D R" and
WSC: "weakly_step_consistent P D R" and
LR: "locally_respects P I D R"
shows "rel_induct P I D u ⊆ R u"
proof (rule subsetI, simp add: rel_induct_def split_paired_all,
erule rel_induct_aux.induct)
fix u xs ys
have "∀u ∈ range D. equiv (traces P) (R u)"
using VP by (simp add: view_partition_def)
moreover assume "(u, xs, ys) ∈ rel_induct_aux P I D"
hence "u ∈ range D" by (rule rel_induct_aux.induct)
ultimately have "equiv (traces P) (R u)" ..
hence "sym (R u)" by (simp add: equiv_def)
moreover assume "(xs, ys) ∈ R u"
ultimately show "(ys, xs) ∈ R u" by (rule symE)
next
fix u xs ys zs
have "∀u ∈ range D. equiv (traces P) (R u)"
using VP by (simp add: view_partition_def)
moreover assume "(u, xs, ys) ∈ rel_induct_aux P I D"
hence "u ∈ range D" by (rule rel_induct_aux.induct)
ultimately have "equiv (traces P) (R u)" ..
hence "trans (R u)" by (simp add: equiv_def)
moreover assume "(xs, ys) ∈ R u" and "(ys, zs) ∈ R u"
ultimately show "(xs, zs) ∈ R u" by (rule transE)
next
fix u xs ys x
have "∀u ∈ range D. ∀xs ys x.
(xs, ys) ∈ R u ∩ R (D x) ∧ x ∈ next_events P xs ∩ next_events P ys ⟶
(xs @ [x], ys @ [x]) ∈ R u"
using WSC by (simp add: weakly_step_consistent_def)
moreover assume "(u, xs, ys) ∈ rel_induct_aux P I D"
hence "u ∈ range D" by (rule rel_induct_aux.induct)
ultimately have "∀xs ys x.
(xs, ys) ∈ R u ∩ R (D x) ∧ x ∈ next_events P xs ∩ next_events P ys ⟶
(xs @ [x], ys @ [x]) ∈ R u" ..
hence "(xs, ys) ∈ R u ∩ R (D x) ∧ x ∈ next_events P xs ∩ next_events P ys ⟶
(xs @ [x], ys @ [x]) ∈ R u"
by blast
moreover assume
"(xs, ys) ∈ R u" and
"(xs, ys) ∈ R (D x)" and
"x ∈ next_events P xs ∩ next_events P ys"
ultimately show "(xs @ [x], ys @ [x]) ∈ R u" by simp
next
fix u xs x
have "∀u ∈ range D. ∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u"
using LR by (simp add: locally_respects_def)
moreover assume "u ∈ range D"
ultimately have "∀xs x.
(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u" ..
hence "(D x, u) ∉ I ∧ x ∈ next_events P xs ⟶ (xs, xs @ [x]) ∈ R u" by blast
moreover assume "(D x, u) ∉ I" and "x ∈ next_events P xs"
ultimately show "(xs, xs @ [x]) ∈ R u" by simp
qed
text ‹
\null
The next step consists of the definition of a trace set ‹T⇩c›, the corresponding trace set
process ‹P⇩c› (cf. \<^cite>‹"R2"›), and a reflexive, intransitive noninterference policy ‹I⇩c›
for this process, where subscript "c" stands for "counterexample". As event-domain map, the identity
function is used, which explains why the policy is defined over events themselves.
\null
›