
diff -r 27103cafb297 -r b091e0abb894 slides/slides06.tex
--- a/slides/slides06.tex	Tue Oct 29 12:18:43 2013 +0000
+++ b/slides/slides06.tex	Tue Nov 12 01:53:41 2013 +0000
@@ -1,8 +1,8 @@
 \documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{proof}
-\usepackage{beamerthemeplainculight}
-\usepackage[T1]{fontenc}
-\usepackage[latin1]{inputenc}
+\usepackage{beamerthemeplaincu}
+%\usepackage[T1]{fontenc}
+%\usepackage[latin1]{inputenc}
 \usepackage{mathpartir}
 \usepackage{isabelle}
 \usepackage{isabellesym}
@@ -14,6 +14,7 @@
 \usetikzlibrary{arrows}
 \usetikzlibrary{positioning}
 \usetikzlibrary{calc}
+\usetikzlibrary{shapes}
 \usepackage{graphicx} 
 
 \isabellestyle{rm}
@@ -35,6 +36,8 @@
 \renewcommand{\isasymsharp}{\isamath{\#}}
 \renewcommand{\isasymdots}{\isamath{...}}
 \renewcommand{\isasymbullet}{\act}
+\newcommand{\isaliteral}[1]{}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 
 
 
@@ -88,8 +91,24 @@
 	showspaces=false,
 	showstringspaces=false}
 
+%sudoku
+\newcounter{row}
+\newcounter{col}
+
+\newcommand\setrow[9]{
+        \setcounter{col}{1}
+        \foreach \n in {#1, #2, #3, #4, #5, #6, #7, #8, #9} {
+            \edef\x{\value{col} - 0.5}
+            \edef\y{9.5 - \value{row}}
+            \node[anchor=center] at (\x, \y) {\n};
+            \stepcounter{col}
+        }
+        \stepcounter{row}
+}
+
+
 % beamer stuff 
-\renewcommand{\slidecaption}{APP 06, King's College London, 29 October 2012}
+\renewcommand{\slidecaption}{APP 06, King's College London, 12 November 2013}
 
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
 \begin{document}
@@ -112,7 +131,7 @@
   \begin{center}
   \begin{tabular}{ll}
   Email:  & christian.urban at kcl.ac.uk\\
-  Of$\!$fice: & S1.27 (1st floor Strand Building)\\
+  Office: & S1.27 (1st floor Strand Building)\\
   Slides: & KEATS (also homework is there)\\
   \end{tabular}
   \end{center}
@@ -122,108 +141,6 @@
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{1st Week}
-
-\begin{itemize}
-\item What are hashes and salts?\bigskip\pause
-\item \ldots can be use to store securely data on a client, but
-you cannot make your protocol dependent on the
-presence of the data\bigskip\pause
-\item \ldots can be used to store and verify passwords
-
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{2nd Week}
-
-\begin{itemize}
-\item Buffer overflows\bigskip
-\item choice of programming language can mitigate or even eliminate this problem
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{3rd Week}
-
-\begin{itemize}
-\item defence in depth\bigskip
-\item privilege separation afforded by the OS
-\end{itemize}
-
-\begin{center}
-\begin{tikzpicture}[scale=1]
-  
-  \draw[line width=1mm] (0, 1.1) rectangle (1.2,2);
-  \draw (4.7,1) node {Internet};
-  \draw (0.6,1.7) node {\footnotesize Slave};
-  \draw[line width=1mm] (0, 0) rectangle (1.2,0.9);
-  \draw (0.6,1.7) node {\footnotesize Slave};
-  \draw (0.6,0.6) node {\footnotesize Slave};
-  \draw (0.6,-0.5) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] processes\end{tabular}};
-  \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}};
-  
-  \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2);
-  \draw (-2.9,1.7) node {\footnotesize Monitor};
-
-  \draw[white] (1.7,1) node (X) {};
-  \draw[white] (3.7,1) node (Y) {};
-  \draw[red, <->, line width = 2mm] (X) -- (Y);
- 
-  \draw[red, <->, line width = 1mm] (-0.4,1.4) -- (-1.4,1.1);
-  \draw[red, <->, line width = 1mm] (-0.4,0.6) -- (-1.4,0.9);
-
-  \end{tikzpicture}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{4th Week}
-
-\begin{itemize}
-\item voting\ldots has security requirements that are in tension with each other
-\begin{center}
-integrity vs ballot secrecy\\
-authentication vs enfranchisment 
-\end{center}\bigskip
-
-\item electronic voting makes `whole sale' fraud easier as opposed to `retail attacks' 
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{5th Week}
-
-\begin{itemize}
-\item access control logic\bigskip
-
-\item formulas
-\item judgements
-\item inference rules
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[t]
   \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
@@ -469,6 +386,271 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}[c]
+\frametitle{Sudoku}
+
+\begin{tikzpicture}[scale=.5]
+  \begin{scope}
+    \draw (0, 0) grid (9, 9);
+    \draw[very thick, scale=3] (0, 0) grid (3, 3);
+
+    \setcounter{row}{1}
+    \setrow { }{2}{ }  {5}{ }{1}  { }{9}{ }
+    \setrow {8}{ }{ }  {2}{ }{3}  { }{ }{6}
+    \setrow { }{3}{ }  { }{6}{ }  { }{7}{ }
+
+    \setrow { }{ }{1}  { }{ }{ }  {6}{ }{ }
+    \setrow {5}{4}{ }  { }{ }{ }  { }{1}{9}
+    \setrow { }{ }{2}  { }{ }{ }  {7}{ }{ }
+
+    \setrow { }{9}{ }  { }{3}{ }  { }{8}{ }
+    \setrow {2}{ }{ }  {8}{ }{4}  { }{ }{7}
+    \setrow { }{1}{ }  {9}{ }{7}  { }{6}{ }
+
+    \fill[red, fill opacity=0.4] (4,0) rectangle (5,9);
+    \fill[red, fill opacity=0.4] (0,5) rectangle (9,6);
+    \fill[red!50, fill opacity=0.4] (3,3) rectangle (4,5);
+    \fill[red!50, fill opacity=0.4] (5,3) rectangle (6,5);  
+    \node[gray, anchor=center] at (4.5, -0.5) {columns};
+    \node[gray, rotate=90, anchor=center] at (-0.6, 4.5, -0.5) {rows};
+    \node[gray, anchor=center] at (4.5, 4.5) {box};
+  \end{scope}
+  \end{tikzpicture}
+
+\small
+\begin{textblock}{7}(9,3)
+\begin{enumerate}
+\item {\bf Row-Column:} each cell, must contain exactly one number
+\item {\bf Row-Number:} each row must contain each number exactly once
+\item {\bf Column-Number:} each column must contain each number exactly once
+\item {\bf Box-Number:} each box must contain each number exactly once
+\end{enumerate}
+\end{textblock}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Solving Sudokus}
+
+\begin{tikzpicture}[scale=.5]
+  \begin{scope}
+    \draw (0, 0) grid (9, 9);
+    \draw[very thick, scale=3] (0, 0) grid (3, 3);
+
+    \setcounter{row}{1}
+    \setrow { }{ }{ }  {7}{ }{ }  { }{5}{8}
+    \setrow {}{5}{6}  {2}{1}{8}  {7}{9}{3}
+    \setrow { }{ }{ }  { }{ }{ }  {1}{ }{ }
+
+    \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}
+    \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }
+    \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }
+
+    \setrow { }{ }{5}  { }{3}{ }  { }{ }{ }
+    \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }
+    \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }
+
+    \fill[red, fill opacity=0.4] (0,7) rectangle (1,8);
+
+  \end{scope}
+  \end{tikzpicture}
+
+\small
+\begin{textblock}{6}(9,6)
+{\bf single position rules}\\
+\begin{center}
+\bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}
+\end{center}
+
+\onslide<2->{
+\begin{center}
+\bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one column}}}\medskip\\
+\bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one box}}}
+\end{center}}
+\end{textblock}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Solving Sudokus}
+
+\begin{tikzpicture}[scale=.5]
+  \begin{scope}
+    \draw (0, 0) grid (9, 9);
+    \draw[very thick, scale=3] (0, 0) grid (3, 3);
+
+    \setcounter{row}{1}
+    \setrow { }{ }{ }  {7}{ }{ }  {\alert{\footnotesize 2}}{5}{8}
+    \setrow {}{5}{6}  {2}{1}{8}  {7}{9}{3}
+    \setrow { }{ }{ }  { }{ }{ }  {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}}
+
+    \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}
+    \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }
+    \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }
+
+    \setrow { }{ }{5}  { }{3}{ }  { }{ }{ }
+    \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }
+    \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }
+
+  \end{scope}
+  \end{tikzpicture}
+
+\small
+\begin{textblock}{6}(7.5,6)
+{\bf candidate rules}\\
+\begin{center}
+\bl{\infer{x\;\text{candidate in empty positions}}{X - \{x\}\;\text{in one box} & X \subseteq \{1..9\}}}
+\end{center}
+\end{textblock}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Solving Sudokus}
+
+\begin{tikzpicture}[scale=.5]
+  \begin{scope}
+    \draw (0, 0) grid (9, 9);
+    \draw[very thick, scale=3] (0, 0) grid (3, 3);
+
+    \setcounter{row}{1}
+    \setrow { }{ }{ }  {7}{ }{ }  {\alert{\footnotesize 2}}{5}{8}
+    \setrow {\alert{4}}{5}{6}  {2}{1}{8}  {7}{9}{3}
+    \setrow { }{ }{ }  { }{ }{ }  {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}}
+
+    \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}
+    \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }
+    \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }
+
+    \setrow { }{ }{5}  { }{3}{ }  { }{ }{ }
+    \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }
+    \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }
+
+  \end{scope}
+  \end{tikzpicture}
+
+\small
+\begin{textblock}{6}(7.5,6)
+\begin{center}
+\bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}\bigskip\\
+\bl{\infer{2\;\text{candidate in empty positions}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}}
+\end{center}
+\end{textblock}
+
+
+\begin{textblock}{3}(13.5,6.8)
+  \begin{tikzpicture}
+  \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}
+  \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}
+  \end{tikzpicture}
+\end{textblock}
+
+\begin{textblock}{3}(14.5,9.3)
+  \begin{tikzpicture}
+  \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}
+  \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}
+  \end{tikzpicture}
+\end{textblock}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Solving Sudokus}
+
+\begin{tikzpicture}[scale=.5]
+  \begin{scope}
+    \draw (0, 0) grid (9, 9);
+    \draw[very thick, scale=3] (0, 0) grid (3, 3);
+
+    \setcounter{row}{1}
+    \setrow { }{ }{ }  {7}{ }{ }  { }{5}{8}
+    \setrow { }{5}{6}  {2}{1}{8}  {7}{9}{3}
+    \setrow { }{ }{ }  { }{ }{ }  {1}{ }{ }
+
+    \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}
+    \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }
+    \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ \alert{2}}
+
+    \setrow { }{ }{5}  { }{3}{ }  { }{ }{ }
+    \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }
+    \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }
+
+  \end{scope}
+  \end{tikzpicture}
+
+\small
+\begin{textblock}{6}(7.5,6)
+\begin{center}
+\bl{\infer{2\;\text{candidate}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}}
+\end{center}
+\end{textblock}
+
+\begin{textblock}{3}(14.5,8.3)
+  \begin{tikzpicture}
+  \onslide<1>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}
+  \end{tikzpicture}
+\end{textblock}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Sudoku}
+
+Are there sudokus that cannot be solved?\pause
+
+\begin{center}
+\begin{tikzpicture}[scale=.5]
+  \begin{scope}
+    \draw (0, 0) grid (9, 9);
+    \draw[very thick, scale=3] (0, 0) grid (3, 3);
+
+    \setcounter{row}{1}
+    \setrow {1}{2}{3}  {4}{5}{6}  {7}{8}{ }
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{2}
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{3}
+
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{4}
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{5}
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{6}
+
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{7}
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{8}
+    \setrow { }{ }{ }  { }{ }{ }  { }{ }{9}
+
+  \end{scope}
+  \end{tikzpicture}
+\end{center}
+
+Sometimes no rules apply at all....unsolvable sudoku.
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
 \frametitle{Protocol Specifications}
 
 The Needham-Schroeder Protocol:




