diff -r e1e314c1bb61 -r efcac3016613 hw06.tex
--- a/hw06.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-\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 (Removed) Was already used in HW 5
-
-\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: