\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 rulesof 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 {\itBell-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 {\itBell-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: