1 \documentclass{article}

     2 \usepackage{charter}

     3 \usepackage{hyperref}

     4 \usepackage{amssymb}

     5 

     6 \begin{document}

     7 

     8 \section*{Homework 5}

     9 

    10 \begin{enumerate}

    11 \item Access control is about deciding whether a principal that

    12 issues a request should be trusted on this request. Explain

    13 how such decision problems can be solved by using logic.

    14 

    15 \item The informal meaning of the formula $P\;\textit{controls}\;F$ is 

    16 `$P$ is entitled to do $F$'. Give a definition for this formula in terms 

    17 of $\textit{says}$. 

    18 

    19 \item Explain what is meant by a {\it derived} inference rule.

    20 

    21 

    22 \item Give a justification for the derived rule

    23 \begin{center}

    24 \begin{tabular}{c}

    25 $\Gamma \vdash P\;\textit{controls}\;F$ \hspace{4mm} $\Gamma \vdash P\;\textit{says}\;F$\\\hline

    26 $\Gamma \vdash F$

    27 \end{tabular}

    28 \end{center}

    29 

    30 \item Give a justification for the derived rule

    31 \begin{center}

    32 \begin{tabular}{c}

    33 $\Gamma \vdash P\;\mapsto\;Q$ \hspace{4mm} $\Gamma \vdash P\;\textit{says}\;F$\\\hline

    34 $\Gamma \vdash Q\;\textit{says}\;F$

    35 \end{tabular}

    36 \end{center}

    37 

    38 \item Model formally the situation that a customer has bought a ticket and requests to see a

    39 movie. For this suppose three principals, {\it Ticket}, {\it Customer} and {\it Cinema},

    40 and suppose an authorization 

    41 \begin{center}

    42 $\textit{Permitted}(\textit{Customer}, \textit{sees\_movie})$.

    43 \end{center}

    44 Using access-control logic, give formulas for a {\it Customer}'s access

    45 request, an access-control policy of the {\it Cinema}, a trust assumption

    46 and a ticket rule.

    47 

    48 \item Assume $\Gamma$ is a set consisting of the three formulas:

    49 \begin{center}

    50 \begin{tabular}{l}

    51 \\

    52 $(\textit{Admin}\;\textit{says}\;\textit{del\_file})\;\Rightarrow\;\textit{del\_file}$\\

    53 $\textit{Admin}\;\textit{says}\;((\textit{Alice}\;\textit{says}\;\textit{del\_file})

    54 \Rightarrow \textit{del\_file})$\\

    55 $\textit{Alice}\;\textit{says}\;\textit{del\_file}$\\

    56 \\

    57 \end{tabular}

    58 \end{center}

    59 

    60 Give a proof of the judgement

    61 \begin{center}

    62 $\Gamma \vdash \textit{del\_file}$

    63 \end{center}

    64 

    65 

    66 \end{enumerate}

    67 \end{document}

    68 

    69 %%% Local Variables: 

    70 %%% mode: latex

    71 %%% TeX-master: t

    72 %%% End: