\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 + −
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}) = slev(\textit{TS})$\smallskip\\+ −
$slev(\textit{File}_1) = slev(\textit{S})$\smallskip\\+ −
$slev(\textit{File}_2) = slev(\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: + −