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