\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

The informal meaning of the formula $P\;\textit{controls}\;F$ is `$P$ is entitled

to do $F$'. Give a definition for this formula in terms of $\textit{says}$. 

\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: