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