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

\begin{document}

\section*{Homework 7}

\begin{enumerate}
\item Suppose a judgement is of the form:
\begin{center}
$Alice\;\textit{says}\;S \wedge Bob\;\textit{says}\;S \vdash Bob\;\textit{says}\;S \wedge Alice\;\textit{says}\;S$
\end{center}

Assume you want to use the inference rule

\begin{center}
\mbox{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}
\end{center}

for constructing a proof of the judgement. What do the premises look like? 

\item What are the benefits of using Logic to describe protocols and access control problems?


%\item The informal meaning of the formula \mbox{$P\;\mapsto\;Q$} is `$P$ speaks for
%$Q$'. Give a definition for this formula in terms of $\textit{says}$.

%\item In Unix, what should be the general architecture of a network application that 
%processes potentially hostile data from the Internet? (Hint: Focus on the fact that in Unix
%you can give different privileges to processes.)

%\item Explain what are the differences between dictionary and brute forcing attacks  against  passwords.

\end{enumerate}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: