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