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