diff -r e8071a3f13b2 -r bcdcdb422813 hw06.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hw06.tex	Thu Nov 01 20:15:02 2012 +0000
@@ -0,0 +1,101 @@
+\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: