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