# HG changeset patch # User Christian Urban # Date 1384221221 0 # Node ID b091e0abb8948bd06a0865edf4eda457b0c18030 # Parent 27103cafb2973f5142e001f488f288d8bec15424 added diff -r 27103cafb297 -r b091e0abb894 slides/slides06.pdf Binary file slides/slides06.pdf has changed 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{ -\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{ -\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{ -\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{ -\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{ -\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{ \begin{frame}[t] \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}} @@ -469,6 +386,271 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \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{ +\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{ +\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{ +\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{ +\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{ +\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{ +\begin{frame}[c] \frametitle{Protocol Specifications} The Needham-Schroeder Protocol: