Commit 2aeee5da authored by Stanley Clark's avatar Stanley Clark
Browse files

Added old latex resources to the archive

parent 5bad0950
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
%!TEX root = ../paper.tex
%============================================================================%
\begin{table}[!t]
\centering
\small
\caption{Results of running $C \difference (C \semijoin O)$ on $\database$ and $\secd{\database}$.}
\label{tab:a_priori_not_sound}
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\database}{C \semijoin O}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
1 & EU \\\hline
\end{tabular}
\end{subtable}%
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\database}{ C \difference (C \semijoin O)}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
2 & US \\\hline
\end{tabular}
\end{subtable}%
\newline
\vspace*{1mm}
\newline
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\secd{\database}}{C \semijoin O}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
1 & NULL \\\hline
\end{tabular}
\end{subtable}%
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\secd{\database}}{ C \difference (C \semijoin O)}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
1 & NULL \\\hline
2 & US \\\hline
\end{tabular}
\end{subtable}
\end{table}
% $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
% Macros for Fitch-style formal proofs
% Johan W. Klüwer, June 10, 2001
% EDITS (Alexander W. Kocurek, June 8, 2019)
% %\RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
% - too many fonts were loading
% - removed mdwtab, which redefines tabular, causing several conflicts such as overriding color in tabular cells and redefining \hline so that \hline without arguments no longer works
\RequirePackage{mathtools,amsmath,ifthen}
% Line height in proofs
\newlength{\fitchlineht}
\setlength{\fitchlineht}{1.5\baselineskip}
% Horizontal indent between proof levels
\newlength{\fitchindent}
\setlength{\fitchindent}{0.7em}
% Indent to comment
\newlength{\fitchcomind}
\setlength{\fitchcomind}{2em}
% Line number width
\newlength{\fitchnumwd}
\setlength{\fitchnumwd}{1em}
% Altered from mdwtab.sty: shorter vline, for start of subproof
\makeatletter
\newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
\makeatother
% Ordinary vertical line
\newcommand{\fa}{\vline\hspace*{\fitchindent}}
% Vertical line, shorter: Use at start of (sub)proof
\newcommand{\fb}{\fvline\hspace*{\fitchindent}}
% Hypothesis
\newcommand{\fh}{\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Hypothesis, with longer vert line: for >1 hypothesis
\newcommand{\fj}{\vline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Modal subproof: takes argument = operator
\newcommand{\fitchmodal}[1]{%
\makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
\newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
\newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
% Modal subproof with hypothesis in first line (as in Fitch)
\newcommand{\fitchmodalh}[1]{%
\makebox[0pt][r]{${}^{\footnotesize #1}$\,}%
\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
\newcommand{\fm}{\fitchmodalh{\Box}}% Box subproof with hypothesis
\newcommand{\fq}{\fitchmodalh{\Diamond}}% Diamond subproof with hypothesis
% Rule: formula introduction marker. \fr with line, \fs without line
\newcommand{\fr}{%
\makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
\newcommand{\fs}{%
\makebox[0pt][r]{${\rhd}$\,\,}}
% Box around argument, like new variable in ql
\newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
%
\newcounter{fitchcounter}
\setcounter{fitchcounter}{0}
%To avoid starting from 1, \setboolean{resetfitchcounter}{false}
\newboolean{resetfitchcounter}
\setboolean{resetfitchcounter}{true}
%To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
\newboolean{increasefitchcounter}
\setboolean{increasefitchcounter}{true}
%\formatfitchcounter can be altered if need be, though only once per proof
\newcommand{\formatfitchcounter}[1]{\scriptsize \arabic{#1}}
%Typeset the counter
\newcommand{\fitchcounter}{%
\ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
\formatfitchcounter{fitchcounter}}
%A line with a special number -- a tag, e.g. \ftag{\vdots}{}
\newcommand{\ftag}[2]{\multicolumn{1}%
{!{\makebox[\fitchnumwd][r]{\footnotesize $#1$}\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}}%
{#2}} % Arc put the tag in math mode by default
% Main environments
% Arc modified the next two environments by replacing Ml (which is supposed to force math mode, left aligned in mdwtab) with >{$}l<{$}, which has the same effect in tabular
\newenvironment{fitchnum}%
{\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
\begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter }\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitchunum}%
{\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
\begin{fitchnum}}{\end{fitchnum}}
\newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
\begin{fitchunum}}{\end{fitchunum}}
% The following is useful for giving a numbered formula, then the proof.
\newenvironment{flem}[2]%
{\begin{eqnarray}
&#1\label{#2}\\
&\begin{fitch}}%
{\end{fitch}\notag\end{eqnarray}}
%To write comment field for two consecutive lines, with brace
\newcommand{\ftwocom}[1]{%
\parbox[t]{3cm}{
\raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
$\left.
\begin{aligned}
\,\\ \,
\end{aligned}
\right\}$\quad #1}
}}
\ No newline at end of file
%!TEX root = ../paper.tex
%============================================================================%
\section{Future Work}
\label{appendix:future_work}
In this appendix, we list all proofs and theory related to exploring soundness, security and maximality under conditions other than incomplete databases and inference-based property definitions.
Under the approach which allows inference of data outside of that permitted by the policy, the following set of implication rules can be derived:
%
\begin{itemize}
\item Soundness: $\tone \in \evalnormal{\database}{\secq} \implies \ttwo \in \evalnormal{\database}{\query} \wedge \tone \subsumed \ttwo$
\item Security: $\tone \in \evalnormal{\database}{\secq} \implies \tone \in \maskeddbprojection$
\item Maximality: $\tone \in \maskeddbprojection \wedge \ttwo \in \evalnormal{\database}{\query} \wedge \tone \subsumed \ttwo \implies \tone \in \evalnormal{\database}{\secq}$
\end{itemize}
%
Soundness is the same as for the anti-inference definitions.
However, both approaches are now secure since a different set of tuples is permitted.
The next question is: is the new definition of security contained in the old definition, i.e.\ does $ \forall_{\done \in \equivalentD}[\tone \in \evalnormal{\done}{\secq}] \implies (\tone \in \evalnormal{\database}{\secq} \implies \tone \in \secd{\database})$ hold?
Given a database $\database$ we have $\tone \in \evalnormal{\database}{\secq}$ by for-all elimination.
Further, we know that $\secd{\database}$ must be in the set $\equivalentD$.
So we have $\tone \in \evalnormal{\secd{\database}}{\secq}$, which in turn means that $\tone \in \secd{\database}$.
It is interesting to see how the old and new definitions relate to each other.
Essentially, in the new definition, due to weaker security, maximality allows more tuples, even those that you could infer something from; therefore a-priori filters out too many tuples to begin with.
In the old definitions, the notion of security is that of non-inference, and therefore a-posteriori applies predicates too late, whereby we are able to infer contents of the database.
\begin{proposition}
A-priori, new, complete, incomplete $\rightarrow$ secure.
\end{proposition}
\begin{proof}
We prove that $\forall_{\database, \policy, \query, \tuple}[\tuple \in \evalnormal{\secd{\database}}{\query} \implies \tuple \in \maskeddbprojection]$.
Because $\evalnormal{\secd{\database}}{\query} \subseteq \maskeddbprojection$, this trivially holds.
Therefore, security holds.
\end{proof}
\begin{proposition}
A-priori, new, complete, incomplete $\rightarrow$ not maximal.
\end{proposition}
\begin{proof}
We prove by counterexample that $\exists_{\database, \policy, \query, \tone}[\tone \in \maskeddbprojection \wedge \ttwo \in \evalnormal{\database}{\query} \wedge \tone \subsumed \ttwo \implies \tone \not\in \evalnormal{\database}{\secq}]$.
Let $\schema = \{\,\rel\,\}$ with $\headerof{\rel} = \{\,\attname\,\}$, $\relinstance = \{\,\{\,(\attname, 0)\,\}\,\}$, $\database = \{\,\relinstance\,\}$, $\rowpolicy = \{\,(\rel, true)\,\}$, $\cellpolicy = \{\,(\rel.\attname, false)\,\}$, $\query = \sigma_{\rel.\attname = \rel.\attname}(\rel)$ and $\nameof{\relinstance} = \rel$.
%
Take the tuple $\tone = \{\,(\attname, \textnull)\,\} \in \maskeddbprojection$.
We know that $\{\,(\attname, 0)\,\} \in \evalnormal{\database}{\query}$ since a comparison of a non-\textnull{} value to itself is true.
Therefore we have $\tone \subsumed \ttwo$.
However, $\evalnormal{\secd{\database}}{\query} = \emptyset$ since $\textnull \neq \textnull$.
The tuple $\tone$ is therefore not in $\evalnormal{\secd{\database}}{\query}$ and so maximality does not hold.
\end{proof}
\begin{proposition}
A-priori, old, complete $\rightarrow$ not maximal.
\end{proposition}
\begin{proof}
% --- Non-tuple-based proof ---
% We prove by counterexample. Let $\schema = \{\,\rel\,\}$ with $\headerof{\rel} = \{\,\attname\,\}$, $\relinstance = \{\,\{\,(\attname, 0)\,\}\,\}$, $\database = \{\,\relinstance\,\}$, $\rowpolicy = \{\,(\rel, true)\,\}$, $\cellpolicy = \{\,(\rel.\attname, false)\,\}$, $\query = \sigma_{\rel.\attname = \rel.\attname}(\rel)$ and $\nameof{\relinstance} = \rel$.
% The desired output is $\evalnormal{\database}{\secq} = \{\{\,(\attname, \textnull)\,\}\}$, since a comparison of a value to itself does not allow us to distinguish between two database instances.
% We know that $d{\database} = \{\,\{\,\{\,(\attname, \textnull)\,\}\,\}\,\}$.
% The certain answer to the query is then $\{\,\{\,(\attname, \textnull)\,\}\,\}$ since for any valuation $v(\{\,(\attname, \textnull)\,\})$, it is evident that the chosen constant is equal to itself.
% However, we have $\evalnormal{\database}{\secq} = \emptyset$ since $\textnull \neq \textnull$.
% The certain answer is not subsumed by the answer given by the ordering, and so \propertythree\ does not hold.
% --- Tuple-based proof ---
We prove by counterexample that $\exists_{\database, \policy, \query, \tone}[\tone \in \maskeddbprojection \wedge \forall_{\done \in \equivalentD}[\ttwo \in \evalnormal{\done}{\query} \wedge \tone \subsumed \ttwo] \implies \tone \not\in \evalnormal{\database}{\secq}]$.
Let $\schema = \{\,\rel\,\}$ with $\headerof{\rel} = \{\,\attname\,\}$, $\relinstance = \{\,\{\,(\attname, 0)\,\}\,\}$, $\database = \{\,\relinstance\,\}$, $\rowpolicy = \{\,(\rel, true)\,\}$, $\cellpolicy = \{\,(\rel.\attname, false)\,\}$, $\query = \sigma_{\rel.\attname = \rel.\attname}(\rel)$ and $\nameof{\relinstance} = \rel$.
%
Take the tuple $\tone = \{\,(\attname, \textnull)\,\} \in \maskeddbprojection$.
For any database instance in $\equivalentD$, by replacing the value of $\attname$ with any other value, that value will be equal to itself.
However, we have $\evalnormal{\database}{\secq} = \emptyset$ since $\textnull \neq \textnull$.
The tuple $\tone$ is therefore not in $\evalnormal{\database}{\secq}$ and so maximality does not hold.
\end{proof}
\begin{proposition}
A-posteriori, new, complete, incomplete $\rightarrow$ secure.
\end{proposition}
\begin{proof}
$\tone \in \evalnormal{\database}{\relsec{\query}} \implies \tone \in \maskeddbprojection$.
There is a $\ttwo \in \evalnormal{\database}{\query}$.
From the definition of $\relsec{\query}$ we know that $\tone \subsumed \ttwo$.
We also know that $\ttwo \in \database$.
This means that for the combination of selection conditions in $\query$, $\eval{\condition}{\ttwo} = 1$.
We know that $\tuple \in \rione \wedge \tuple \in \ritwo \implies (\tuple \in \relsec{\rione} \iff \tuple \in \relsec{\ritwo})$.
From this we conclude that $\tone \in \secd{\database}$ and a-posteriori is secure.
\end{proof}
\begin{proposition}
A-posteriori, new, complete, incomplete $\rightarrow$ maximal.
\end{proposition}
\begin{proof}
We prove that a-posteriori is maximal by proving $\ttwo \in \evalnormal{\database}{\query} \wedge \tone \in \secd{\database} \wedge \tone \subsumed \ttwo \implies \tone \in \evalnormal{\database}{\relsec{\query}}$.
Once again, this is proved by taking $\tuple \in \rione \wedge \tuple \in \ritwo \implies (\tuple \in \relsec{\rione} \iff \tuple \in \relsec{\ritwo})$.
\end{proof}
\begin{table}
\centering
\caption{Properties of the orderings under SPJR/named algebra, (in)complete databases, and (non-)inference security}
\begin{tabular}{ccccccc}
order & algebra & type & I/C & sound & secure & maximal \\
\toprule
a-pos & SPJR & old & C & $\checkmark$ & $\times$ & $\times$ \\
a-priori & SPJR & old & C & $\checkmark$ & $\checkmark$ & $\times$ \\
\midrule
a-pos & SPJR & old & I & $\checkmark$ & $\times$ & $\checkmark$ \\
a-priori & SPJR & old & I & $\checkmark$ & $\checkmark$ & $\checkmark$ \\
\midrule
a-pos & SPJR & new & I/C & $\checkmark$ & $\checkmark$ & $\checkmark$ \\
a-priori & SPJR & new & I/C & $\checkmark$ & $\checkmark$ & $\times$ \\
\midrule
a-priori & named & o/n & C & $\times$ & $\checkmark$ & $\times$ \\
a-priori & named & new & I & $\times$ & $\checkmark$ & $\times$ \\
a-priori & named & old & I & $\times$ & $\checkmark$ & $\checkmark$ \\
\bottomrule
\end{tabular}
\end{table}
All this is only possible under the assumption that we operate under incomplete databases.
If one were to take away the possibility of \textnull{} values in the original database, then maximality behaves in a different way, as well as the containment of the new definitions within the old being questioned as well.
\paragraph{Complete Databases}
In case of a complete database, the old inference based definition of security (and with it maximality) can lead to unexpected results.
First, the tuple based definition of $\rmax$ which we saw earlier, is based on an incomplete database.
Therefore, to give the counter example, we assume a database instance where $|\equivalentD| = 1$.
In this way $\rmax$ is always $\evalnormal{\database}{\query}$.
Assume a database schema $\schema = \{\, \rel \,\}$, policy $\policy$ masking cells where $b = 0$, a database $\database$ with $\relinstance = \evalnormal{\database}{\rel} = \{\{\,(a, 0), (b, 0)\,\}\}$ and a query $\query = \selection_{a=b}(\rel)$.
Then, $\equivalentD = \{\,\relinstance\,\}$.
From this, we get $\rmax = \relinstance$, which does not contain a masked value even though the policy says that it should be masked.
This means that the new definition of security is not contained within the old one for complete databases.
It also means that maximality cannot be achieved over a complete database by either algorithm.
One can argue that we cannot infer anything about external database contents this way, so this is the desired outcome, but is this really intuitive?
We argue that this is not.\nztodoin{This may be given in the discussion. (see also below)}
%!TEX root = ../paper.tex
%============================================================================%
\begin{figure}[!t]
\centering
\small
\fbox{
\begin{minipage}[c]{\columnwidth-2\fboxsep-2\fboxrule}
\centering
\begin{tabbing}
\hspace*{0.3cm}\=\hspace*{0.3cm}\=\hspace*{0.3cm}\=\hspace*{0.3cm}\=\hspace*{0.3cm}\= \kill
(\textsf{employee.role} $=$ `clerk' $\wedge$ \textsf{action\_id} = `read',\\
\> \textsf{pov}(\\
\>\> (\textsf{object} $=$ `customer', 1)\\
\>\> (\textsf{object} $=$ `order',\\
\>\>\> \textsf{fa}( \\
\>\>\>\> ($\textsf{order.customer.region} = \textsf{employee.region}$, 1)\\
\>\>\>\> ($\textsf{order.amount} < 500$, 1)\\
\>\>\> )\\
\>\> )\\
\>\> \textsf{dov}(\\
\>\>\> (\textsf{object} $=$ `order.amount' $\wedge$ $\textsf{order.amount} > 100$), 0)\\
\>\>\>(\textsf{object} $=$ `customer.region' $\wedge$ $\textsf{customer.region} = \textsf{EU}$, 0)\\
\>\>\> 1\\
\>\> )\\
\>\> 0\\
\> )\\
)
\end{tabbing}
\end{minipage}
}\\
\bigskip
\fbox{
\begin{minipage}[c]{0.91\columnwidth}
\begin{flushleft}
\textsf{employee.role} $=$ `clerk'
$\wedge$ \textsf{action\_id} = `read'
$\wedge$ (
\textsf{object} $=$ `customer'
$\vee$
(
\textsf{object} $=$ `order'
$\wedge$
(
\textsf{order.customer.region} $=$ \textsf{employee.region}
$\vee$
(
$\neg$\,(\textsf{order.customer.region} $=$ \textsf{employee.region})
$\wedge$
\textsf{order.amount} $<$ 500
)
)
)
$\vee$ (
$\neg$\,(
(
\textsf{object} $=$ `customer.region'
$\wedge$
$\textsf{customer.region} = \text{`EU'}$
)
$\vee$
(
\textsf{object} $=$ `order.amount'
$\wedge$
$\neg\,(\textsf{order.amount} <= 100)$
)
)
)
)
\end{flushleft}
\end{minipage}
}
\caption{ABAC policy}
\label{fig:policy}
\end{figure}
%!TEX root = ../paper.tex
%============================================================================%
\begin{proof}[Proof of \ref{rw:sec_assoc}]
We prove that for any relation instance $\relinstance \in \relationinstanceset$, attribute name $ \attname \in \headerof{\relinstance}$, security formulas $\sczero$ and $\scone$, and tuple $\tuple$, it holds that $\relinstance.\attname \notin \attributesin{\scone} \implies (\tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance)) \iff \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)))$.
\begin{fitch}
\fa \relinstance \in \relationinstanceset,\ \attname \in \headerof{\relinstance},\ \sczero,\ \scone,\ \tuple\\
\fj \relinstance.\attname \notin \attributesin{\scone}\\
\fa \fh \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance))\\
\fa \fa \fw{\ttwo \in \rowop_{\scone}(\relinstance)} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \tuple[\anone] = \ttwo[\anone]] \wedge \tuple[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (F) + $\exists^{*}$-Elim (3)\\
\fa \fa \ttwo \in \relinstance & \Cref{lemma:row_level_subset} (4)\\
\fa \fa \cellmask{\ttwo}{\attname}{\sczero} = \cellmask{\ttwo}{\attname}{\sczero} & ????? (4, 5)\\
\fa \fa \fw{\tfour \in \cellop_{\sczero, \attname}(\relinstance)} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \ttwo[\anone] = \tfour[\anone]] \wedge \tfour[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (R) + $\exists^{*}$-Elim (5)\\
\fa \fa \tuple[\attname] = \tfour[\attname] & (4, 6, 7)\\
\fa \fa \fh (\antwo, \vone) \in \ttwo : \antwo \neq \attname & \\
\fa \fa \fa \antwo \neq \attname \implies \tuple[\antwo] = \tfour[\antwo] & $\forall$-Elim (4, 7, 9)\\
\fa \fa \forall_{(\antwo, \vone) \in \ttwo}[\antwo \neq \attname \implies \tuple[\antwo] = \tfour[\antwo]] & $\forall$-Intro (9, 10))\\
\fa \fa \tuple = \tfour & (8, 11)\\
\fa \fa \tuple \in \cellop_{\sczero, \attname}(\relinstance) & (7, 12)\\
\fa \fa \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) & \Cref{lemma:row_filter_equality} (3, 4, 13)\\
\fa \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance)) \implies \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) & $\implies$-Intro (3, 14)\\
\fa \fh \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance))\\
\fa \fa \tuple \in \cellop_{\sczero, \attname}(\relinstance) & \Cref{lemma:row_level_subset} (16)\\
\fa \fa \fw{\ttwo \in \relinstance} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \tuple[\anone] = \ttwo[\anone]] \wedge \tuple[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (F) + $\exists^{*}$-Elim (17)\\
\fa \fa \ttwo \in \rowop_{\scone}(\relinstance) & ????? (2, 18) \\
\fa \fa \cellmask{\ttwo}{\attname}{\sczero} = \cellmask{\ttwo}{\attname}{\sczero} & ????? (18, 19) \\
\fa \fa \fw{\tfour \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance))} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \tfour[\anone] = \ttwo[\anone]] \wedge \tfour[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (R) + $\exists^{*}$-Elim (19)\\
\fa \fa \tuple[\attname] = \tfour[\attname] & (18, 20, 21)\\
\fa \fa \fh (\antwo, \vone) \in \ttwo : \antwo \neq \attname & \\
\fa \fa \fa \antwo \neq \attname \implies \tuple[\antwo] = \tfour[\antwo] & $\forall$-Elim (18, 21, 23)\\
\fa \fa \forall_{(\antwo, \vone) \in \ttwo}[\antwo \neq \attname \implies \tuple[\antwo] = \tfour[\antwo]] & $\forall$-Intro (23, 24)\\
\fa \fa \tuple = \tfour & (22, 25)\\
\fa \fa \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance)) & (21, 26)\\
\fa \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) \implies \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance)) & $\implies$-Intro (16, 27)\\
\fa \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) \iff \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance))) & $\iff$-Intro (15, 28)\\
\relinstance.\attname \notin \attributesin{\scone} \implies (\tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) \iff \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance))) & $\implies$-Intro (2, 29)\\
\end{fitch}
\end{proof}
\ No newline at end of file
%!TEX root = ../paper.tex
%============================================================================%
\newcommand{\betainstanceforward}[6]{
\fw{#1 \in #2} : \forall_{#3 \in \headerof{#1}}[#3 \neq #6 \implies #5[#3] = #1[#3]] \wedge #5[#6] = \cellmask{#1}{#6}{#4}
}
\newcommand{\betainstancereverse}[7]{
\fw{#1 \in #2} : \forall_{#3 \in \headerof{#5}}[#3 \neq #6 \implies #1[#3] = #5[#3]] \wedge #1[#6] = \cellmask{#5}{#6}{#4}
}
\begin{proof}[Proof of \ref{rw:beta_comm}]
We prove that, given two security formulas $\scone$ and $\sctwo$, two attribute names $\anone$ and $\antwo$ and a relation instance $\relinstance$, it holds that $\relinstance.\anone \notin \attributesin{\sctwo} \wedge \relinstance.\antwo \notin \attributesin{\scone} \implies (\tuple \in \cellop_{\secform_{1}, \anone}(\cellop_{\secform_{2}, \antwo}(\relinstance)) \iff \tuple \in \cellop_{\secform_{2}, \antwo}(\cellop_{\secform_{1}, \anone}(\relinstance)))$
\begin{fitch}
\fa \scone,\ \sctwo,\ \anone,\ \antwo,\ \relinstance\\
\fj \relinstance.\anone \notin \attributesin{\sctwo} \wedge \relinstance.\antwo \notin \attributesin{\scone}\\
\fa \fh \tuple \in \cellop_{\scone, \anone}(\cellop_{\sctwo, \antwo}(\relinstance)) \\
\fa \fa \betainstanceforward{\tone}{\cellop_{\sctwo, \antwo}(\relinstance)}{\anthree}{\scone}{\tuple}{\anone} & $\cellop$-Def (F) (3)\\
\fa \fa \betainstanceforward{\ttwo}{\relinstance}{\anthree}{\sctwo}{\tone}{\antwo} & $\cellop$-Def (F) (4)\\
\fa \fa \betainstancereverse{\tthree}{\cellop_{\scone, \anone}(\relinstance)}{\anthree}{\scone}{\ttwo}{\anone}{\relinstance} & $\cellop$-Def (R) (5)\\
\fa \fa \betainstancereverse{\tfour}{\cellop_{\sctwo, \antwo}(\cellop_{\scone, \anone}(\relinstance))}{\anthree}{\sctwo}{\tthree}{\antwo}{\cellop_{\scone, \anone}(\relinstance)} & $\cellop$-Def (R) (6)\\
\fa \fa \headerof{\tuple} = \headerof{\tone} = \headerof{\ttwo} = \headerof{\tthree} = \headerof{\tfour} = \headerof{\relinstance} & \\
\fa \fa \fh \anfour \in \headerof{\relinstance} : \anfour \neq \anone \wedge \anfour \neq \antwo \\
\fa \fa \fa \anfour \neq \anone \wedge \anfour \neq \antwo \implies \tuple[\anfour] = \tfour[\anfour] & $\forall$-Elim (4, 5, 6, 7)\\
\fa \fa \forall_{\anthree \in \headerof{\relinstance}}[\anthree \neq \anone \wedge \anthree \neq \antwo \implies \tuple[\anthree] = \tfour[\anthree]] & $\forall$-Intro (9, 10)\\
\fa \fa \tuple[\antwo] = \tone[\antwo] & $\forall$-Elim (4)\\
\fa \fa \ttwo[\antwo] = \tthree[\antwo] & $\forall$-Elim (6)\\
\fa \fa \ldots & \\
\fa \fa \tuple[\antwo] = \tfour[\antwo] & GOAL 1\\
\fa \fa \ldots & \\
\fa \fa \tuple[\anone] = \tfour[\anone] & GOAL 2\\
\fa \fa \tuple = \tfour & () \\
\fa \fa \tuple \in \cellop_{\sctwo, \antwo}(\cellop_{\scone, \anone}(\relinstance)) & (7, )\\
\fa \tuple \in \cellop_{\secform_{1}, \anone}(\cellop_{\secform_{2}, \antwo}(\relinstance)) \implies \tuple \in \cellop_{\secform_{2}, \antwo}(\cellop_{\secform_{1}, \anone}(\relinstance)) & $\implies$-Intro (3,) \\
\fa \fh \tuple \in \cellop_{\secform_{2}, \antwo}(\cellop_{\secform_{1}, \anone}(\relinstance)) \\
\fa \fa \betainstanceforward{\tone}{\cellop_{\scone, \anone}(\relinstance)}{\anthree}{\attval}{\sctwo}{\tuple}{\attname} & $\cellop$-Def (F) ()\\
\fa \fa \ldots & \\
\fa \fa \tuple \in \cellop_{\scone, \anone}(\cellop_{\sctwo, \antwo}(\relinstance)) & \\
\fa \tuple \in \cellop_{\secform_{2}, \antwo}(\cellop_{\secform_{1}, \anone}(\relinstance)) \implies \tuple \in \cellop_{\scone, \anone}(\cellop_{\sctwo, \antwo}(\relinstance)) & $\implies$-Intro (,)\\
\fa \tuple \in \cellop_{\secform_{1}, \anone}(\cellop_{\secform_{2}, \antwo}(\relinstance)) \iff \tuple \in \cellop_{\secform_{2}, \antwo}(\cellop_{\secform_{1}, \anone}(\relinstance)) & $\iff$-Intro (,)\\
\relinstance.\anone \notin \attributesin{\sctwo} \wedge \relinstance.\antwo \notin \attributesin{\scone} \implies (\tuple \in \cellop_{\secform_{1}, \anone}(\cellop_{\secform_{2}, \antwo}(\relinstance)) \iff \tuple \in \cellop_{\secform_{2}, \antwo}(\cellop_{\secform_{1}, \anone}(\relinstance))) & $\implies$-Intro (2,)\\
\end{fitch}
\end{proof}
\ No newline at end of file
%!TEX root = ../paper.tex
%============================================================================%
%!TEX root = ../paper.tex
%============================================================================%
%!TEX root = ../paper.tex
%============================================================================%
\newcommand{\rwfiveproj}{\projection_{\attributenames}}
\newcommand{\rwfivebeta}{\cellop_{\secform, \attname}}
\begin{proof}[Proof of \ref{rw:cell_pi}]
Cell-level enforcement is commutative with projection $\attributenames \subseteq \headerof{\relinstance} \wedge \attname \notin \attributenames \wedge \nexists_{\anone \in \attributenames}[\relinstance.\anone \in \attributesin{\secform}] \implies (\tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \iff \tuple \in \rwfivebeta(\rwfiveproj(\relinstance)))$.
\begin{fitch}
\fa \attributenames \wedge \relinstance \wedge \attname \wedge \secform \\
\fj \attributenames \subseteq \headerof{\relinstance} \wedge \attname \notin \attributenames \wedge \nexists_{\anone \in \attributenames}[\relinstance.\anone \in \attributesin{\secform}] \\
\fa \fh \tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \\
\fa \fa \tone \in \rwfivebeta(\relinstance) : \headerof{\tone} \subseteq \headerof{\tuple} \\
\fa \fa \betainstanceforward{\ttwo}{\relinstance}{\anone}{\secform}{\tuple}{\attname} \\
\fa \fa \tuple \in \rwfivebeta(\rwfiveproj(\relinstance)) \\
\fa \tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \implies \tuple \in \rwfivebeta(\rwfiveproj(\relinstance)) \\
\fa \fh \tuple \in \rwfivebeta(\rwfiveproj(\relinstance)) \\
\fa \fa \tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \\
\fa \tuple \in \rwfivebeta(\rwfiveproj(\relinstance)) \implies \tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \\
\fa \tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \iff \tuple \in \rwfivebeta(\rwfiveproj(\relinstance)) \\
\attributenames \subseteq \headerof{\relinstance} \wedge \attname \notin \attributenames \wedge \nexists_{\anone \in \attributenames}[\relinstance.\anone \in \attributesin{\secform}] \implies (\tuple \in \rwfiveproj(\rwfivebeta(\relinstance)) \iff \tuple \in \rwfivebeta(\rwfiveproj(\relinstance))) \\
\end{fitch}
\end{proof}
%!TEX root = ../paper.tex