\documentclass[twoside,11pt]{article}

\usepackage[margin=1.25in]{geometry}
\usepackage{amsmath,amsfonts,amsthm,amssymb,graphicx}
\usepackage{lmodern}
\usepackage{hyperref}
\usepackage{enumerate}
\usepackage{courier}
\usepackage{mathpartir}

\newcommand{\pred}[1]{\ensuremath{{\sf #1}}}
\newcommand{\rname}[1]{\mbox{\small #1}}
\setlength{\parindent}{0 in}

\newcounter{lecnum}
\renewcommand{\thepage}{\thelecnum-\arabic{page}}

\newcounter{pbcounter}
\newcommand{\problem}[1]{\stepcounter{pbcounter}\vspace{12pt}{\Large\bf Problem \thelecnum-\arabic{pbcounter} (#1 points)}\\[3pt]}

\newcommand{\lecture}[3]{
\pagestyle{myheadings}
\thispagestyle{plain}
\newpage
\setcounter{lecnum}{#1}
\setcounter{page}{1}
\noindent
\begin{center}
	\textbf{\large Logics in Security} \hfill \textbf{\large Winter 2014}\\[9pt]
	{\LARGE Homework for Module #1}\\[9pt]
	Instructor: Deepak Garg \hfill TA: Iulia Bolo\c steanu\\
	\texttt{dg@mpi-sws.org} \hfill \texttt{iulia\_mb@mpi-sws.org}\\[-6pt]
	\rule{\textwidth}{0.2mm}\\
	{\it Release date: #2 \hfill Due date: #3}\\[-6pt]
	\rule{\textwidth}{0.2mm}
\end{center}

\vspace{-18pt}

\paragraph{General instructions:}
Attempt all questions. Submit your homework via email to both the
instructor and the TA before midnight on the due date. The {\LaTeX} source for this homework will
be provided to help you typeset. You can also typeset using any other
means, including simple ASCII.

\vspace{6pt}
}

\begin{document}
\lecture{3}{13.12.2014}{20.12.2014}

\problem{$2+3+1+2+2=10$} {\bf Authorization policies in SecPAL.}
%
Saarland University, \texttt{UnivSaarland}, has bachelors students,
graduate students and professors, all of whom need access to a
specific door in the university. \texttt{UnivSaarland} uses SecPAL to
manage the door's authorization system. Let the predicate ``$x$
\textsf{has access}'' mean that principal $x$ has access to this
door. Saarland University has created credentials that establish the
following judgments:

\begin{center}
\begin{tabular}{l}
\texttt{UnivSaarland} \textsf{says} $x$ \textsf{has access} if $x$ \textsf{is a bachelors student}\\
\texttt{UnivSaarland} \textsf{says} $x$ \textsf{has access} if $x$ \textsf{is a graduate student}\\
\texttt{UnivSaarland} \textsf{says} $x$ \textsf{has access} if $x$ \textsf{is a professor}
\end{tabular}
\end{center}

\begin{enumerate}[A.]
\item Assume that \texttt{Alice} is a bachelors student and
  \texttt{Bob} is a professor, so the following judgments hold:

\begin{center}
\begin{tabular}{l}
\texttt{UnivSaarland} \textsf{says} \texttt{Alice} \textsf{is a bachelors student}\\
\texttt{UnivSaarland} \textsf{says} \texttt{Bob} \textsf{is a professor}
\end{tabular}
\end{center}

What judgment in SecPAL corresponds to the informal assertion ``Alice
can access the door''? Write down a proof using the rules of SecPAL
(paragraph ``Semantics'' in Section~3 of the paper) that establishes
this judgment. Now do the same for Bob instead of Alice.

\item \texttt{UnivSaarland} gives every professor the right to decide
  who is a graduate student (this makes sense because graduate
  students are usually associated with a professor). Accordingly,
  \texttt{UnivSaarland} issues the following credential:
%
\begin{equation}
\mbox{\texttt{UnivSaarland} \textsf{says} $x$ \textsf{can say}$_\infty$ $y$
\textsf{is a graduate student} if $x$ \textsf{is a professor}}
\label{eq:saardeleg}
\end{equation}

\texttt{Bob} decides to take \texttt{Charlie} as a graduate student,
so \texttt{Bob} issues the following credential:
%
\begin{center}
\texttt{Bob} \textsf{says} \texttt{Charlie} \textsf{is a graduate student}
\end{center}

Write a formal SecPAL proof to show that \texttt{Charlie} is allowed
access to the university's door.

\item Professor \texttt{Bob} wants to delegate administrative
  responsibility to his student \texttt{Charlie}. Accordingly, he
  wants to issue a credential that will allow \texttt{Charlie} to
  state who is a graduate student. What SecPAL judgment would this
  credential establish?

\item \texttt{Charlie} decides to misuse the authority he received
  from Professor \texttt{Bob} in the previous step. He decides to
  designate his wife \texttt{Mary} a graduate student so that she can
  access the university's door (\texttt{Mary} is not really a graduate
  student). \texttt{Charlie} issues the credential:
%
\begin{center}
\texttt{Charlie} \textsf{says} \texttt{Mary} \textsf{is a graduate
  student}
\end{center} 

Write a SecPAL proof to show that \texttt{Mary} has access to the the
university's door.

\item Clearly, something has gone wrong. One way to fix this problem
  is for \texttt{UnivSaarland} to delegate to \texttt{Bob} the right
  to decide graduate students but \emph{without} allowing him to
  delegate this right further. What credential should
  \texttt{UnivSaarland} have issued in place of
  credential~(\ref{eq:saardeleg}) of step B in order to ensure this
  property?  Explain why with this revised credential (and keeping all
  other credentials the same) \texttt{Mary} will \emph{not} get access
  to the university's door. 
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{$2.5\times4=10$} {\bf Intuitionistic logic.}
%
Construct proofs of the following judgments in intuitionistic
logic. The proof rules are listed in Figure~1 for your reference. Note
that the judgment $\vdash \varphi$ is an abbreviation for $\emptyset
\vdash \varphi$. Further, $\neg \varphi$ is an abbreviation for
$\varphi \supset \bot$.

\begin{enumerate}[a.]
\item $\vdash A \supset (B \supset (A \land B))$

\item $\vdash (A \supset B) \supset ((A \supset \neg B) \supset \neg
  A)$

\item $\vdash (\neg \neg (A \supset B)) \supset (A \supset \neg \neg
  B)$

\item $\vdash \neg \neg (\neg \neg A \supset A)$
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\problem{$0$} This is a practice exercise to help you understand
reduction semantics better. If you turn in a solution, we will check
it to provide you feedback, but not for points. We strongly encourage
you to solve this exercise before the lecture on Wednesday, December
17, 2014. \\

{\bf Reduction semantics.}
%
Consider the following program $p$ with the initial memory $\mu = \{x
\mapsto 5; y \mapsto \mathit{false}; z \mapsto 2\}$:

\begin{center}
\begin{tabular}{cl}
 & $x:=0;$ \\
 & $\mathsf{if}~ (y == \mathit{true})~ \mathsf{then}$ \\
	& \quad $x : = 1;$\\
	& $\mathsf{else}$\\
 & \quad $\mathsf{while}~ (z > 0) ~\mathsf{do}$\\
	& \qquad $x := x + 1;$\\
	& \qquad $z := z - 1;$
\end{tabular}
\end{center}

Specify the first four steps of the reduction of this program and the
memory corresponding to the result of each of them. For the first and
fourth steps of the reduction write down complete derivation trees
following the rules of the reduction judgment. You may want to
introduce names for parts of the program to abbreviate your
proofs. The rules of the reduction judgment are shown in Figure~2 for
your reference.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage

\begin{figure}[t]
\begin{mathpar}
\inferrule{\Gamma \vdash A \and \Gamma \vdash B}{\Gamma \vdash A \land B}\rname{$\land$I}

\inferrule{\Gamma \vdash A \land B}{\Gamma \vdash A}\rname{$\land E_1$}  

\inferrule{\Gamma \vdash A \land B}{\Gamma \vdash B}\rname{$\land E_2$}\\

\inferrule{\Gamma \vdash A}{\Gamma \vdash A \lor B}\rname{$\lor I_1$}

\inferrule{\Gamma \vdash B}{\Gamma \vdash A \lor B}\rname{$\lor I_2$}

\inferrule{\Gamma \vdash A \lor B \and \Gamma, A \vdash C \and \Gamma, B \vdash C}{\Gamma \vdash C}\rname{$\lor E$}\\

\inferrule{\Gamma, A \vdash B}{\Gamma \vdash A \supset B}\rname{$\supset$I} 

\inferrule{\Gamma \vdash A \supset B \and \Gamma \vdash A}{\Gamma \vdash B}\rname{$\supset$E}

\inferrule{\Gamma \vdash \bot}{\Gamma \vdash A}\rname{$\bot$E} 

\inferrule{ }{\Gamma \vdash \top}\rname{$\top$I} 
\end{mathpar}

\caption{Intuitionistic logic introduction and elimination rules.}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}
Syntax:

\[\begin{array}{llll}
\mbox{Values} & v & ::= & 0 \mid 1 \mid 2 \ldots \mid \mathit{true}
\mid \mathit{false}\\

\mbox{Expressions} & e & ::= & v \mid \ell \mid e_1 + e_2 \mid e_1 -
e_2 \mid e_1 == e_2 \mid e_1 > e_2\\

\mbox{Commands} & p & ::= & \mathsf{skip} \mid \ell := e \mid p_1;p_2 \mid \mathsf{if}~ (e)~ \mathsf{then}~ p_1~ \mathsf{else}~ p_2 \mid \mathsf{while}~ (e)~ \mathsf{do}
\end{array} \]

\medskip

Semantic rules for expressions:\\

{\bf Note:} For any connective $o$ in $\{+, -, ==, >\}$, $\hat{o}$
denotes the underlying arithmetic operator.
%
\begin{mathpar}
\inferrule{ }{\mu, v \Downarrow v}

\inferrule{ }{\mu, \ell \Downarrow \mu(\ell)}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  v_1 \hat{+} v_2 = v}{\mu, e_1 + e_2 \Downarrow \mu, v}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  v_1 \hat{-} v_2 = v}{\mu, e_1 - e_2 \Downarrow \mu, v}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  (v_1 \hat{==} v_2) = v}{\mu, e_1 == e_2 \Downarrow \mu, v}

\inferrule{\mu, e_1 \Downarrow v_1 \and \mu, e_2 \Downarrow v_2 \and
  (v_1 \hat{>} v_2) = v}{\mu, e_1 > e_2 \Downarrow \mu, v}
\end{mathpar}

\medskip

Semantic rules for commands:
%
\begin{mathpar}
\inferrule{\mu, e \Downarrow v }{\mu, \ell := e \rightarrow \mu[\ell \mapsto v], \mathsf{skip}}

\inferrule{\mu, p_1 \rightarrow \mu', p'_1}{\mu, p_1; p_2 \rightarrow \mu', p_1';p_2}

\inferrule{ }{\mu, \mathsf{skip}; p \rightarrow \mu, p}

\inferrule{\mu, e \Downarrow \mathit{true}}{\mu, \mathsf{if}~ (e)~ \mathsf{then}~ p_1 ~\mathsf{else}~ p_2 \rightarrow \mu, p_1} 

\inferrule{\mu, e \Downarrow \mathit{false}}{\mu, \mathsf{if}~ (e)~ \mathsf{then}~ p_1 ~\mathsf{else}~ p_2 \rightarrow \mu, p_2}

\inferrule{\mu, e \Downarrow \mathit{true}}{\mu, \mathsf{while}~ (e)~ \mathsf{do}~ p \rightarrow \mu, p; \mathsf{while}~ (e)~ \mathsf{do}~ p}

\inferrule{\mu, e \Downarrow \mathit{false}}{\mu, \mathsf{while}~ (e)~ \mathsf{do}~ p \rightarrow \mu, \mathsf{skip}}

\end{mathpar}
\caption{Reduction semantics.}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}





