30 \item Give a justification for the derived rule

    30 %\item Give a justification for the derived rule

    31 \begin{center}

    31 %\begin{center}

    32 \begin{tabular}{c}

    32 %\begin{tabular}{c}

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

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

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

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

    35 \end{tabular}

    35 %\end{tabular}

    36 \end{center}

    36 %\end{center}

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

    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},

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

    40 and suppose an authorization 

    40 %and suppose an authorization 

    41 \begin{center}

    41 %\begin{center}

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

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

    43 \end{center}

    43 %\end{center}

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

    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

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

    46 and a ticket rule.

    46 %and a ticket rule.