# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1379954371 -3600
# Node ID efcac30166130be541900b5ed3f128a1f2edc464
# Parent  e1e314c1bb61450e2a62c9dcea4ebf23fd5bb2b6
added hws

diff -r e1e314c1bb61 -r efcac3016613 hw01.pdf
Binary file hw01.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw01.tex
--- a/hw01.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{hyperref}
-
-\begin{document}
-
-\section*{Homework 1}
-
-\begin{enumerate}
-\item {\bf (Optional)} If you want to have a look at the code presented in the lectures, install Scala available (for free) from
-\begin{center}
-\url{http://www.scala-lang.org}
-\end{center}
-
-\noindent
-The web-applications from the first lecture are written in Scala using the Play Framework available (also for free) from
-\begin{center}
-\url{http://www.playframework.org}
-\end{center}
-
-\item Practice thinking like an attacker. Assume the following situation:
-\begin{quote}\it
-Prof.~V.~Nasty gives the following final exam question (closed books, closed notes):\bigskip
-
-\noindent
-\begin{tabular}{@ {}l}
-Write the first 100 digits of pi:\\
-3.\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
-\end{tabular}
-\end{quote}
-
-\noindent
-Think of ways how you can cheat in this exam?
-
-\item Explain what hashes and salts are. Describe how they can be used for ensuring data integrity and
-storing password information.
-
-\item What are good uses of cookies (that is browser cookies)?
-
-\end{enumerate}
-
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hw02.pdf
Binary file hw02.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw02.tex
--- a/hw02.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{hyperref}
-
-\begin{document}
-
-\section*{Homework 2}
-
-\begin{enumerate}
-\item Assume format string attacks allow you to read out the stack. What can you do
-	with this information? (Hint: Consider what is stored in the stack.)
-
-\item Assume you can crash a program remotely. Why is this a problem?
-
-\item How can the choice of a programming language help with buffer overflow attacks?
-(Hint: Why are C-programs prone to such attacks, but not Java programs.)
-
-\item (Optional) How can a system that separates between \emph{users} and \emph{root} be of any help with buffer overflow attacks?
-\end{enumerate}
-
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hw03.pdf
Binary file hw03.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw03.tex
--- a/hw03.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{hyperref}
-
-\begin{document}
-
-\section*{Homework 3}
-
-\begin{enumerate}
-\item What does the principle of least privilege say?
-
-\item In which of the following situations can the access control mechanism of Unix
-file permissions be used?
-
-\begin{itemize}
-\item[(a)] Alice wants to have her files readable, except for her office mates.
-\item[(b)] Bob and Sam want to share some secret files.
-\item[(c)] Root wants some of her files to be public.
-\end{itemize}
-
-\item What should the architecture of a network application under Unix 
-be that processes potentially hostile data?
-
-\item How can you exploit the fact that every night root has a cron
-job that deletes the files in \texttt{/tmp}?
-
-\item What does it mean that the program \texttt{passwd} has the \texttt{setuid}
-bit set? Why is this necessary?
-
-\item What does the Bell --- La Padula model ensure? Similarly, what does the Biba model ensure?
-\end{enumerate}
-
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hw04.pdf
Binary file hw04.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw04.tex
--- a/hw04.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{hyperref}
-\usepackage{amssymb}
-
-\begin{document}
-
-\section*{Homework 4}
-
-\begin{enumerate}
-\item Voice voting is the method of casting a vote in the `open air' for everyone
-present to hear. Which of the following security requirements do paper ballots 
-satisfy better than voice voting? Check all that apply and give a brief explanation 
-for your decision.
-
-\begin{itemize}
-\item[$\Box$] Integrity\bigskip\bigskip
-\item[$\Box$] Enfranchisement\bigskip\bigskip
-\item[$\Box$] Ballot secrecy\bigskip\bigskip
-\item[$\Box$] Voter authentication\bigskip\bigskip
-\item[$\Box$] Availability\bigskip\bigskip
-\end{itemize}
-
-
-\item Explain how an attacker can use chain voting in order to influence the outcome of a 
-poll using paper ballots. 
-
-\item Which of the following mechanisms help with defending against chain voting? Check all 
-that apply. Give a brief reason for each defence that mitigates chain voting attacks.
-
-\begin{itemize}
-\item[$\Box$] Using a glass ballot box to make it clear there are no ballots in the box before the start of the election.
-\item[$\Box$] Distributing ballots publicly before the election.
-\item[$\Box$] Checking that a voter's ID (drivers license, passport) matches the voter.
-\item[$\Box$] Each ballot has a unique ID. When a voter is given a ballot, the ID is recorded. When the voter submits his or her ballot, this ID is checked against the record.
-\end{itemize}
-
-\end{enumerate}
-
-
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hw05.pdf
Binary file hw05.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw06.pdf
Binary file hw06.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw06.tex
--- a/hw06.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{hyperref}
-\usepackage{amssymb}
-
-\begin{document}
-
-\section*{Homework 6}
-
-\begin{enumerate}
-\item Access-control logic includes formulas of the form
-\begin{center}
-$P\;\textit{says}\;F$
-\end{center}
-
-where $P$ is a principal and $F$ a formula. Give two inference rules
-of access-control logic involving $\textit{says}$.
-
-\item (Removed) Was already used in HW 5
-
-\item 
-Assume an access control logic with security levels, say top secret ({\it TS}),
-secret ({\it S}) and public ({\it P}), with
-\begin{center}
-$slev(\textit{P}) < slev(\textit{S}) < slev(\textit{TS})$
-\end{center}
-
-(a) Modify the formula
-\begin{center}
-\begin{tabular}{l}
-$P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$\\
-\end{tabular}
-\end{center}
-using security levels so that it satisfies the {\it write rule} from the {\it
-Bell-LaPadula} access policy. Do the same again, but satisfy the {\it write rule}
-from the {\it Biba} access policy.
-
-(b)Modify the formula
-\begin{center}
-\begin{tabular}{l}
-$P\;\textit{controls}\;\textit{Permitted}(O, \textit{read})$\\
-\end{tabular}
-\end{center}
-using security levels so that it satisfies the {\it read rule} from the {\it
-Bell-LaPadula} access policy. Do the same again, but satisfy the {\it read rule}
-from the {\it Biba} access policy.
-
-\item Assume two security levels $\textit{S}$ and $\textit{TS}$, which are ordered so that $slev(\textit{S}) < slev(\textit{TS})$. 
-Assume further the substitution rules
-\begin{center}
-\begin{tabular}{c}
-$\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
-\hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
-$\Gamma \vdash slev(P) < slev(Q)$
-\end{tabular}
-\end{center}
-
-\begin{center}
-\begin{tabular}{c}
-$\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline
-$\Gamma \vdash slev(P) = slev(Q)$
-\end{tabular}
-\end{center}
-
-Let $\Gamma$ be the set containing the following six formulas
-\begin{center}
-\begin{tabular}{l}
-\\
-$slev(\textit{S}) < slev(\textit{TS})$\smallskip\\
-$slev(\textit{Agent}) = slev(\textit{TS})$\smallskip\\
-$slev(\textit{File}_1) = slev(\textit{S})$\smallskip\\
-$slev(\textit{File}_2) = slev(\textit{TS})$\smallskip\\
-$\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow 
-(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\
-$\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow 
-(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\
-\\
-\end{tabular}
-\end{center}
-Using the inference rules of access-control logic and the substitution rules shown above,
-give proofs for the two judgements
-\begin{center}
-\begin{tabular}{l}
-$\Gamma \vdash
-(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1,
-\textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_1, \textit{read})$\smallskip\\
-$\Gamma \vdash
-(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_2,
-\textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_2, \textit{read})$\\
-\end{tabular}
-\end{center}
-
-\end{enumerate}
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hw07.pdf
Binary file hw07.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hw07.tex
--- a/hw07.tex	Mon Sep 23 17:02:24 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-\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 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: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw01.pdf
Binary file hws/hw01.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw01.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw01.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,47 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+
+\begin{document}
+
+\section*{Homework 1}
+
+\begin{enumerate}
+\item {\bf (Optional)} If you want to have a look at the code presented in the lectures, install Scala available (for free) from
+\begin{center}
+\url{http://www.scala-lang.org}
+\end{center}
+
+\noindent
+The web-applications from the first lecture are written in Scala using the Play Framework available (also for free) from
+\begin{center}
+\url{http://www.playframework.org}
+\end{center}
+
+\item Practice thinking like an attacker. Assume the following situation:
+\begin{quote}\it
+Prof.~V.~Nasty gives the following final exam question (closed books, closed notes):\bigskip
+
+\noindent
+\begin{tabular}{@ {}l}
+Write the first 100 digits of pi:\\
+3.\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
+\end{tabular}
+\end{quote}
+
+\noindent
+Think of ways how you can cheat in this exam?
+
+\item Explain what hashes and salts are. Describe how they can be used for ensuring data integrity and
+storing password information.
+
+\item What are good uses of cookies (that is browser cookies)?
+
+\end{enumerate}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw02.pdf
Binary file hws/hw02.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw02.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw02.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,26 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+
+\begin{document}
+
+\section*{Homework 2}
+
+\begin{enumerate}
+\item Assume format string attacks allow you to read out the stack. What can you do
+	with this information? (Hint: Consider what is stored in the stack.)
+
+\item Assume you can crash a program remotely. Why is this a problem?
+
+\item How can the choice of a programming language help with buffer overflow attacks?
+(Hint: Why are C-programs prone to such attacks, but not Java programs.)
+
+\item (Optional) How can a system that separates between \emph{users} and \emph{root} be of any help with buffer overflow attacks?
+\end{enumerate}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw03.pdf
Binary file hws/hw03.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw03.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw03.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,38 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+
+\begin{document}
+
+\section*{Homework 3}
+
+\begin{enumerate}
+\item What does the principle of least privilege say?
+
+\item In which of the following situations can the access control mechanism of Unix
+file permissions be used?
+
+\begin{itemize}
+\item[(a)] Alice wants to have her files readable, except for her office mates.
+\item[(b)] Bob and Sam want to share some secret files.
+\item[(c)] Root wants some of her files to be public.
+\end{itemize}
+
+\item What should the architecture of a network application under Unix 
+be that processes potentially hostile data?
+
+\item How can you exploit the fact that every night root has a cron
+job that deletes the files in \texttt{/tmp}?
+
+\item What does it mean that the program \texttt{passwd} has the \texttt{setuid}
+bit set? Why is this necessary?
+
+\item What does the Bell --- La Padula model ensure? Similarly, what does the Biba model ensure?
+\end{enumerate}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw04.pdf
Binary file hws/hw04.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw04.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw04.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,46 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+\usepackage{amssymb}
+
+\begin{document}
+
+\section*{Homework 4}
+
+\begin{enumerate}
+\item Voice voting is the method of casting a vote in the `open air' for everyone
+present to hear. Which of the following security requirements do paper ballots 
+satisfy better than voice voting? Check all that apply and give a brief explanation 
+for your decision.
+
+\begin{itemize}
+\item[$\Box$] Integrity\bigskip\bigskip
+\item[$\Box$] Enfranchisement\bigskip\bigskip
+\item[$\Box$] Ballot secrecy\bigskip\bigskip
+\item[$\Box$] Voter authentication\bigskip\bigskip
+\item[$\Box$] Availability\bigskip\bigskip
+\end{itemize}
+
+
+\item Explain how an attacker can use chain voting in order to influence the outcome of a 
+poll using paper ballots. 
+
+\item Which of the following mechanisms help with defending against chain voting? Check all 
+that apply. Give a brief reason for each defence that mitigates chain voting attacks.
+
+\begin{itemize}
+\item[$\Box$] Using a glass ballot box to make it clear there are no ballots in the box before the start of the election.
+\item[$\Box$] Distributing ballots publicly before the election.
+\item[$\Box$] Checking that a voter's ID (drivers license, passport) matches the voter.
+\item[$\Box$] Each ballot has a unique ID. When a voter is given a ballot, the ID is recorded. When the voter submits his or her ballot, this ID is checked against the record.
+\end{itemize}
+
+\end{enumerate}
+
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw05.pdf
Binary file hws/hw05.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw05.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw05.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,72 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+\usepackage{amssymb}
+
+\begin{document}
+
+\section*{Homework 5}
+
+\begin{enumerate}
+\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: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw06.pdf
Binary file hws/hw06.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw06.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw06.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,99 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+\usepackage{amssymb}
+
+\begin{document}
+
+\section*{Homework 6}
+
+\begin{enumerate}
+\item Access-control logic includes formulas of the form
+\begin{center}
+$P\;\textit{says}\;F$
+\end{center}
+
+where $P$ is a principal and $F$ a formula. Give two inference rules
+of access-control logic involving $\textit{says}$.
+
+\item (Removed) Was already used in HW 5
+
+\item 
+Assume an access control logic with security levels, say top secret ({\it TS}),
+secret ({\it S}) and public ({\it P}), with
+\begin{center}
+$slev(\textit{P}) < slev(\textit{S}) < slev(\textit{TS})$
+\end{center}
+
+(a) Modify the formula
+\begin{center}
+\begin{tabular}{l}
+$P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$\\
+\end{tabular}
+\end{center}
+using security levels so that it satisfies the {\it write rule} from the {\it
+Bell-LaPadula} access policy. Do the same again, but satisfy the {\it write rule}
+from the {\it Biba} access policy.
+
+(b)Modify the formula
+\begin{center}
+\begin{tabular}{l}
+$P\;\textit{controls}\;\textit{Permitted}(O, \textit{read})$\\
+\end{tabular}
+\end{center}
+using security levels so that it satisfies the {\it read rule} from the {\it
+Bell-LaPadula} access policy. Do the same again, but satisfy the {\it read rule}
+from the {\it Biba} access policy.
+
+\item Assume two security levels $\textit{S}$ and $\textit{TS}$, which are ordered so that $slev(\textit{S}) < slev(\textit{TS})$. 
+Assume further the substitution rules
+\begin{center}
+\begin{tabular}{c}
+$\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
+\hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
+$\Gamma \vdash slev(P) < slev(Q)$
+\end{tabular}
+\end{center}
+
+\begin{center}
+\begin{tabular}{c}
+$\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline
+$\Gamma \vdash slev(P) = slev(Q)$
+\end{tabular}
+\end{center}
+
+Let $\Gamma$ be the set containing the following six formulas
+\begin{center}
+\begin{tabular}{l}
+\\
+$slev(\textit{S}) < slev(\textit{TS})$\smallskip\\
+$slev(\textit{Agent}) = slev(\textit{TS})$\smallskip\\
+$slev(\textit{File}_1) = slev(\textit{S})$\smallskip\\
+$slev(\textit{File}_2) = slev(\textit{TS})$\smallskip\\
+$\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow 
+(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\
+$\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow 
+(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\
+\\
+\end{tabular}
+\end{center}
+Using the inference rules of access-control logic and the substitution rules shown above,
+give proofs for the two judgements
+\begin{center}
+\begin{tabular}{l}
+$\Gamma \vdash
+(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1,
+\textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_1, \textit{read})$\smallskip\\
+$\Gamma \vdash
+(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_2,
+\textit{read})) \Rightarrow \textit{Permitted}(\textit{File}_2, \textit{read})$\\
+\end{tabular}
+\end{center}
+
+\end{enumerate}
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r e1e314c1bb61 -r efcac3016613 hws/hw07.pdf
Binary file hws/hw07.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 hws/hw07.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw07.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -0,0 +1,40 @@
+\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 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: 
diff -r e1e314c1bb61 -r efcac3016613 slides/pics/schneierbook3.jpg
Binary file slides/pics/schneierbook3.jpg has changed
diff -r e1e314c1bb61 -r efcac3016613 slides/slides01.pdf
Binary file slides/slides01.pdf has changed
diff -r e1e314c1bb61 -r efcac3016613 slides/slides01.tex
--- a/slides/slides01.tex	Mon Sep 23 17:02:24 2013 +0100
+++ b/slides/slides01.tex	Mon Sep 23 17:39:31 2013 +0100
@@ -217,7 +217,7 @@
 \begin{frame}[c]
 \frametitle{\begin{tabular}{@ {}c@ {}}Security Engineers\end{tabular}}
 
-\alert{\bf Security engineers} require a particular \alert{\bf mindset}:\bigskip
+\small\alert{\bf Security engineers} require a particular \alert{\bf mindset}:\bigskip
 
 \begin{tikzpicture}
 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
@@ -234,6 +234,7 @@
 \begin{flushright}
 \includegraphics[scale=0.0087]{pics/schneierbook1.jpg}\;
 \includegraphics[scale=0.0087]{pics/schneierbook2.jpg}\;
+\includegraphics[scale=0.23]{pics/schneierbook3.jpg}\;
 \includegraphics[scale=0.85]{pics/schneier.png}
 \end{flushright}