--- 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: