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