diff -r e1e314c1bb61 -r efcac3016613 hws/hw05.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw05.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,72 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+\usepackage{amssymb}
+
+\begin{document}
+
+\section*{Homework 5}
+
+\begin{enumerate}
+\item Access control is about deciding whether a principal that
+issues a request should be trusted on this request. Explain
+how such decision problems can be solved by using logic.
+
+\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 Explain what is meant by a {\it derived} inference rule.
+
+
+\item Give a justification for the derived rule
+\begin{center}
+\begin{tabular}{c}
+$\Gamma \vdash P\;\textit{controls}\;F$ \hspace{4mm} $\Gamma \vdash P\;\textit{says}\;F$\\\hline
+$\Gamma \vdash F$
+\end{tabular}
+\end{center}
+
+\item Give a justification for the derived rule
+\begin{center}
+\begin{tabular}{c}
+$\Gamma \vdash P\;\mapsto\;Q$ \hspace{4mm} $\Gamma \vdash P\;\textit{says}\;F$\\\hline
+$\Gamma \vdash Q\;\textit{says}\;F$
+\end{tabular}
+\end{center}
+
+\item Model formally the situation that a customer has bought a ticket and requests to see a
+movie. For this suppose three principals, {\it Ticket}, {\it Customer} and {\it Cinema},
+and suppose an authorization 
+\begin{center}
+$\textit{Permitted}(\textit{Customer}, \textit{sees\_movie})$.
+\end{center}
+Using access-control logic, give formulas for a {\it Customer}'s access
+request, an access-control policy of the {\it Cinema}, a trust assumption
+and a ticket rule.
+
+\item Assume $\Gamma$ is a set consisting of the three formulas:
+\begin{center}
+\begin{tabular}{l}
+\\
+$(\textit{Admin}\;\textit{says}\;\textit{del\_file})\;\Rightarrow\;\textit{del\_file}$\\
+$\textit{Admin}\;\textit{says}\;((\textit{Alice}\;\textit{says}\;\textit{del\_file})
+\Rightarrow \textit{del\_file})$\\
+$\textit{Alice}\;\textit{says}\;\textit{del\_file}$\\
+\\
+\end{tabular}
+\end{center}
+
+Give a proof of the judgement
+\begin{center}
+$\Gamma \vdash \textit{del\_file}$
+\end{center}
+
+
+\end{enumerate}
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: