\documentclass{article}
\usepackage{charter}
\usepackage{hyperref}
\usepackage{amssymb}

\begin{document}

\section*{Homework 6}

\begin{enumerate}
\item Access-control logic includes formulas of the form
\begin{center}
$P\;\textit{says}\;F$
\end{center}

where $P$ is a principal and $F$ a formula. Give two inference rules
of access-control logic involving $\textit{says}$.

\item (Removed) Was already used in HW 5

\item 
Assume an access control logic with security levels, say top secret ({\it TS}),
secret ({\it S}) and public ({\it P}), with
\begin{center}
$slev(\textit{P}) < slev(\textit{S}) < slev(\textit{TS})$
\end{center}

(a) Modify the formula
\begin{center}
\begin{tabular}{l}
$P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$\\
\end{tabular}
\end{center}
using security levels so that it satisfies the {\it write rule} from the {\it
Bell-LaPadula} access policy. Do the same again, but satisfy the {\it write rule}
from the {\it Biba} access policy.

(b)Modify the formula
\begin{center}
\begin{tabular}{l}
$P\;\textit{controls}\;\textit{Permitted}(O, \textit{read})$\\
\end{tabular}
\end{center}
using security levels so that it satisfies the {\it read rule} from the {\it
Bell-LaPadula} access policy. Do the same again, but satisfy the {\it read rule}
from the {\it Biba} access policy.

\item Assume two security levels $\textit{S}$ and $\textit{TS}$, which are ordered so that $slev(\textit{S}) < slev(\textit{TS})$. 
Assume further the substitution rules
\begin{center}
\begin{tabular}{c}
$\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
\hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
$\Gamma \vdash slev(P) < slev(Q)$
\end{tabular}
\end{center}

\begin{center}
\begin{tabular}{c}
$\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline
$\Gamma \vdash slev(P) = slev(Q)$
\end{tabular}
\end{center}

Let $\Gamma$ be the set containing the following six formulas
\begin{center}
\begin{tabular}{l}
\\
$slev(\textit{S}) < slev(\textit{TS})$\smallskip\\
$slev(\textit{Agent}) = \textit{TS}$\smallskip\\
$slev(\textit{File}_1) = \textit{S}$\smallskip\\
$slev(\textit{File}_2) = \textit{TS}$\smallskip\\
$\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow 
(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\
$\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow 
(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\
\\
\end{tabular}
\end{center}
Using the inference rules of access-control logic and the substitution rules shown above,
give proofs for the two judgements
\begin{center}
\begin{tabular}{l}
$\Gamma \vdash
(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1,
\textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_1, \textit{read})$\smallskip\\
$\Gamma \vdash
(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_2,
\textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_2, \textit{read})$\\
\end{tabular}
\end{center}

\end{enumerate}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: