Binary file handouts/ho08.pdf has changed

--- a/handouts/ho08.tex	Mon Dec 01 06:50:25 2014 +0000
+++ b/handouts/ho08.tex	Tue Dec 02 02:29:37 2014 +0000
@@ -44,7 +44,7 @@
 \noindent is signed by Satoshi Nakamoto, which however is
 likely only a pen name. There is a lot of speculation who
 could be the inventor, or inventors, but we simply do not
-know. This part of Bitcoins is definitely anonymous. The paper
+know. This part of Bitcoins is definitely anonymous so far. The paper
 above is from the end of 2008; the first Bitcoin transaction
 was made in January 2009. The rules in Bitcoin are set up so
 that there will only ever be 21 Million Bitcoins with the
@@ -77,8 +77,8 @@
 already used addresses. If you start with a random number to
 generate a public-private key pair it is very unlikely that
 you step on somebody else's shoes. Compare this with the
-email-addresses you always wanted to register with, say
-Gmail, but which are already taken.
+email-addresses you wanted to register with, say
+Gmail, but which are always already taken.
 
 One major difference between Bitcoins and traditional banking
 is that you do not have a place, or places, that record the
@@ -143,7 +143,7 @@
 \noindent But for this banks would need to be trusted and
 would also be an easy target for any government interference,
 for example. Think of the early days of music sharing where
-the company Napster was the single point of ``failure'' which
+the company Napster was the trusted third-party but also the single point of ``failure'' which
 was taken offline by law enforcement. Bitcoins is more like a
 system such as BitTorrent without a single central entity that
 can be taken offline.\footnote{There is some Bitcoin
@@ -151,9 +151,9 @@
 for example Bitcoin exchanges, HQs of Bitcoin mining pools,
 Bitcoin developers and so on.}
 
-Bitcoin solves the problem of not being able to rely on a bank
+Bitcoins solve the problem of not being able to rely on a bank
 by making everybody the ``bank''. Everybody who cares can have
-the entire transactions history starting with the first
+the entire transaction history starting with the first
 transaction made in January 2009. This history of transactions
 is called the \emph{blockchain}. Bob, for example, can use his
 copy of the blockchain for determining whether Alice owned the
@@ -220,7 +220,7 @@
 Consider again the rightmost transactions in
 Figure~\ref{txngraph} and suppose Alice is a coffeeshop owner
 selling coffees for 1 Bitcoin. Charles received a transaction
-from Zack over 5 Bitcoins, say. How does he pay for the
+from Zack over 5 Bitcoins, say. How does Charles pay for the
 coffee? There is no explicit notion of \emph{change} in the
 Bitcoin system. What Charles has to do instead is to make one
 single transaction with 1 Bitcoin to Alice and with 4 Bitcoins
@@ -252,7 +252,7 @@
 
 I think this is a good time for you to pause to let this
 concept of transactions to really sink in\ldots{}You should
-see that there is really no need for a central ledger and no
+come to the conclusion that there is really no need for a central ledger and no
 need for an account balance as familiar from traditional
 banking. The closest what Bitcoin has to offer for the notion
 of a balance in a bank account are the unspend transactions

--- a/slides/slides05.tex	Mon Dec 01 06:50:25 2014 +0000
+++ b/slides/slides05.tex	Tue Dec 02 02:29:37 2014 +0000
@@ -424,12 +424,12 @@
 \frametitle{Car Transponder (HiTag2)}
 
 \begin{enumerate}
-\item \bl{$C$} generates a random number \bl{$r$}
-\item \bl{$C$} calculates \bl{$(F,G) = \{r\}_K$}
-\item \bl{$C \to T$}: \bl{$r, F$}
-\item \bl{$T$} calculates \bl{$(F',G') = \{r\}_K$}
+\item \bl{$C$} generates a random number \bl{$N$}
+\item \bl{$C$} calculates \bl{$(F,G) = \{N\}_K$}
+\item \bl{$C \to T$}: \bl{$N, F$}
+\item \bl{$T$} calculates \bl{$(F',G') = \{N\}_K$}
 \item \bl{$T$} checks that \bl{$F = F'$}
-\item \bl{$T \to C$}: \bl{$r, G'$}
+\item \bl{$T \to C$}: \bl{$N, G'$}
 \item \bl{$C$} checks that \bl{$G = G'$}
 \end{enumerate}\pause
 

Binary file slides/slides10.pdf has changed

--- a/slides/slides10.tex	Mon Dec 01 06:50:25 2014 +0000
+++ b/slides/slides10.tex	Tue Dec 02 02:29:37 2014 +0000
@@ -1,47 +1,10 @@
 \documentclass[dvipsnames,14pt,t]{beamer}
-\usepackage{proof}
-\usepackage{beamerthemeplaincu}
-\usepackage{mathpartir}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage[absolute,overlay]{textpos}
-\usepackage{ifthen}
-\usepackage{tikz}
-\usepackage{courier}
-\usepackage{listings}
-\usetikzlibrary{arrows}
-\usetikzlibrary{positioning}
-\usetikzlibrary{calc}
-\usepackage{graphicx} 
-\usetikzlibrary{shapes}
-\usetikzlibrary{shadows}
-\usetikzlibrary{plotmarks}
-\setmonofont[Scale=MatchLowercase]{Consolas}
-\newfontfamily{\consolas}{Consolas}
-
-\isabellestyle{rm}
-\renewcommand{\isastyle}{\rm}%
-\renewcommand{\isastyleminor}{\rm}%
-\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
-\renewcommand{\isatagproof}{}
-\renewcommand{\endisatagproof}{}
-\renewcommand{\isamarkupcmt}[1]{#1}
-
-% Isabelle characters
-\renewcommand{\isacharunderscore}{\_}
-\renewcommand{\isacharbar}{\isamath{\mid}}
-\renewcommand{\isasymiota}{}
-\renewcommand{\isacharbraceleft}{\{}
-\renewcommand{\isacharbraceright}{\}}
-\renewcommand{\isacharless}{$\langle$}
-\renewcommand{\isachargreater}{$\rangle$}
-\renewcommand{\isasymsharp}{\isamath{\#}}
-\renewcommand{\isasymdots}{\isamath{...}}
-\renewcommand{\isasymbullet}{\act}
+\usepackage{../slides}
+\usepackage{../langs}
+\usepackage{../graphics}
 
 % beamer stuff 
-\renewcommand{\slidecaption}{APP 09, King's College London, 10 December 2013}
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\renewcommand{\slidecaption}{APP 10, King's College London}
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
 
 \begin{document}
@@ -302,155 +265,6 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile,t]
-\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}
-
-Bell-LaPadula access model:
-
- \begin{itemize}
-  \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if
-  \bl{$P$}'s security level is at least as high as \bl{$O$}'s.
-  \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if
-  \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip
-
-  \item Meta-Rule: All principals in a system should have a sufficiently high security level
-  in order to access an object.
-  \end{itemize}\bigskip
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile,t]
-\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}
-
-Biba (data integrity)
-
-  \begin{itemize}
-  \item Biba: {\bf `no read down'} - {\bf `no write up'}
-  \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if
-  \bl{$P$}'s security level is lower or equal than \bl{$O$}'s.
-  \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if
-  \bl{$O$}'s security level is lower or equal than \bl{$P$}'s.
-  \end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile,t]
-\frametitle{\begin{tabular}{c}4th Lecture:\\ Protocols\end{tabular}}
-
-A mutual authentication protocol
-
-\begin{center}
-\begin{tabular}{ll}
-\bl{$A \rightarrow B$:} & \bl{$N_a$}\\  
-\bl{$B \rightarrow A$:} & \bl{$\{N_a, N_b\}_{K_{ab}}$}\\
-\bl{$A \rightarrow B$:} & \bl{$N_b$}\\
-\end{tabular}
-\end{center}
-
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile,t]
-\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}
-
-
-\begin{itemize}
-\item formulas
-\item judgements
-\end{itemize}\pause
-
-\begin{center}
-  \begin{tikzpicture}[scale=1]
-  
-  \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
-  \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
-  \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}};
-  \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}};
- 
-  \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); 
-  \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
-  \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); 
-  
-  \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};
-
-  \end{tikzpicture}
-\end{center}
-
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile,t]
-\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}
-
-\begin{center}
-\begin{tikzpicture}[scale=1]
-  
-  \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
-  \onslide<1->{
-  \draw (-1,-0.3) node (X) {};
-  \draw (-2.0,-2.0) node (Y) {};
-  \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};
-  \draw[red, ->, line width = 2mm] (Y) -- (X);
- 
-  \draw (1.2,-0.1) node (X1) {};
-  \draw (2.8,-0.1) node (Y1) {};
-  \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};
-  \draw[red, ->, line width = 2mm] (Y1) -- (X1);
-
-  \draw (-0.1,0.1) node (X2) {};
-  \draw (0.5,1.5) node (Y2) {};
-  \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};
-  \draw[red, ->, line width = 2mm] (Y2) -- (X2);}
-  
-  \end{tikzpicture}
-\end{center}
-
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{\begin{tabular}{c}5th Lecture:\\ Inference Rules\end{tabular}}
-
-
-\begin{center}
-\begin{tikzpicture}[scale=1]
-  
-  \draw (0.0,0.0) node 
-  {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};
- 
-  \draw (-0.1,-0.7) node (X) {};
-  \draw (-0.1,-1.9) node (Y) {};
-  \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};
-  \draw[red, ->, line width = 2mm] (Y) -- (X);
- 
-  \draw (-1,0.6) node (X2) {};
-  \draw (0.0,1.6) node (Y2) {};
-  \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};
-  \draw[red, ->, line width = 2mm] (Y2) -- (X2);
-   \draw (1,0.6) node (X3) {};
-  \draw (0.0,1.6) node (Y3) {};
-  \draw[red, ->, line width = 2mm] (Y3) -- (X3);
-  \end{tikzpicture}
-\end{center}
-
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}[c]
 \frametitle{\begin{tabular}{c}8th Lecture: Privacy\end{tabular}}