\documentclass[twoside,11pt]{article}
\usepackage[margin=1.25in]{geometry}
\usepackage{amsmath,amsfonts,amsthm,amssymb}
\usepackage{lmodern}
\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, in typeset form, 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{1}{November 12, 2014}{November 19, 2014}
\problem{5} Consider executions over the alphabet $\{a,b,c\}$. Which
of the following are safety properties? For each safety property,
construct a corresponding security automata as defined by Schneider on
page 36 of the paper ``Enforceable Security Policies''. You may
present your automata in either of the two forms illustrated in
Fig.\ 1 and Fig.\ 2 of Schneider's paper.
\begin{enumerate}
\item $c$ never occurs after $a$ and $c$ never occurs after $b$.
\item Every $a$ is followed immediately by a $b$.
\item Every $a$ is followed by a $b$ (not necessarily immediately).
\item Every $a$ is followed by a $b$ within the next 7 steps.
\item In every prefix of the execution, the number of $c$'s is less
than the total number of $a$'s and $b$'s.
\end{enumerate}
\problem{5}
Recall Schneider's quote about Lamport's characterization of safety
properties.
\begin{center}
\begin{tabular}{p{0.8\textwidth}} A property $\Gamma$ is
defined in Lamport [1985] to be a safety property if and only if,
for any finite or infinite execution $\sigma$, $\sigma \not \in
\Gamma \Rightarrow (\exists i. (\forall \tau \in \Psi:
\sigma[..i]\tau \not \in \Gamma))$.
\end{tabular}
\end{center}
Assume that this quote is the definition of a safety property. Prove
that the following statement is an alternative characterization of
every safety property $\Gamma$ (that is, the statement above holds if
and only if the statement below holds).
\begin{center}
\begin{tabular}{p{0.8\textwidth}} There is a set $S$ of
\emph{finite} executions such that for any finite or infinite
execution $\sigma$, $\sigma \not \in \Gamma$ if and only if $\sigma
= \tau_1 \tau_2$ for some $\tau_1 \in S$ and $\tau_2 \in \Psi$.
\end{tabular}
\end{center}
\problem{5}
For each property of Problem 1-1 that is actually a safety property,
construct a suitable set $S$ that satisfies the characterization of
Problem 1-2.
\end{document}