\documentclass{article}
\usepackage{charter}
\usepackage{hyperref}
\usepackage{amssymb}

\begin{document}

\section*{Homework 5}

\begin{enumerate}
\item Consider the following simple mutual authentication protocol:

\begin{center}
\begin{tabular}{ll}
$A \rightarrow B$: & $N_a$\\  
$B \rightarrow A$: & $\{N_a, N_b\}_{K_{ab}}$\\
$A \rightarrow B$: & $N_b$\\
\end{tabular}
\end{center}

Explain how an attacker $B'$ can launch an impersonation attack by 
intercepting all messages for $B$ and make $A$ decrypt her own challenges.


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