Binary file coursework/cw01.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/coursework/cw01.tex Sat Sep 23 14:19:09 2017 +0100
@@ -0,0 +1,39 @@
+\documentclass{article}
+\usepackage{../style}
+\usepackage{array}
+
+
+\begin{document}
+\newcolumntype{C}[1]{>{\centering}m{#1}}
+
+\section*{Coursework 7CCSMSEN}
+
+This coursework is worth 4\% and is due on 19 October at
+16:00. You are asked to implement a regular expression matcher
+and submit a document containing the answers for the questions
+below. You can do the implementation in any programming
+language you like, but you need to submit the source code with
+which you answered the questions, otherwise a mark of 0\% will
+be awarded. You can submit your answers in a txt-file or pdf.
+Code send as code.
+
+
+
+\subsubsection*{Disclaimer}
+
+It should be understood that the work you submit represents
+your own effort. You have not copied from anyone else. An
+exception is the Scala code I showed during the lectures or
+uploaded to KEATS, which you can freely use.\bigskip
+
+
+\subsection*{Task}
+
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
Binary file handouts/ho01.pdf has changed
Binary file handouts/ho02.pdf has changed
Binary file handouts/ho03.pdf has changed
Binary file handouts/ho04.pdf has changed
Binary file handouts/ho05.pdf has changed
Binary file handouts/ho06.pdf has changed
Binary file handouts/ho07.pdf has changed
Binary file handouts/ho08.pdf has changed
Binary file handouts/ho09.pdf has changed
Binary file hws/hw01.pdf has changed
Binary file hws/hw02.pdf has changed
Binary file hws/hw03.pdf has changed
Binary file hws/hw04.pdf has changed
Binary file hws/hw05.pdf has changed
Binary file hws/hw06.pdf has changed
Binary file hws/hw07.pdf has changed
Binary file hws/hw08.pdf has changed
Binary file hws/hw10.pdf has changed
Binary file pics/Dismantling_Megamos_Crypto.png has changed
Binary file pics/airbus.jpg has changed
Binary file pics/firefox1.png has changed
Binary file pics/flight.jpg has changed
Binary file pics/newyorktaxi.jpg has changed
Binary file pics/safari1.png has changed
Binary file pics/simple-b.png has changed
Binary file pics/simple.png has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/progs/inter.scala Sat Sep 23 14:19:09 2017 +0100
@@ -0,0 +1,48 @@
+abstract class Exp
+abstract class Stmt
+
+case class Plus(e1: Exp, e2: Exp) extends Exp
+case class Times(e1: Exp, e2: Exp) extends Exp
+case class Equ(e1: Exp, e2: Exp) extends Exp
+case class Num(n: Int) extends Exp
+case class Var(x: String) extends Exp
+
+case class Label(l: String) extends Stmt
+case class Assign(x: String, e: Exp) extends Stmt
+case class Goto(l: String) extends Stmt
+case class Jmp(e: Exp, l: String) extends Stmt
+
+type Stmts = List[Stmt]
+type Env = Map[String, Int]
+type Snips = Map[String, Stmts]
+
+def preproc(sts: Stmts) : Snips = sts match {
+ case Nil => Map()
+ case Label(l)::rest => preproc(rest) + (l -> rest)
+ case _::rest => preproc(rest)
+}
+
+def Prog(sts: Stmt*) = preproc(Label("")::sts.toList)
+
+def eval_exp(e: Exp, env: Env) : Int = e match {
+ case Var(x) => env(x)
+ case Num(n) => n
+ case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env)
+ case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env)
+ case Equ(e1, e2) =>
+ if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0
+}
+
+def eval(sn: Snips) : Env = {
+ def eval_stmts(sts: Stmts, env: Env): Env = sts match {
+ case Nil => env
+ case Label(l)::rest => eval_stmts(rest, env)
+ case Assign(x, e)::rest =>
+ eval_stmts(rest, env + (x -> eval_exp(e, env)))
+ case Goto(l)::rest => eval_stmts(sn(l), env)
+ case Jmp(b, l)::rest =>
+ if (eval_exp(b, env) == 1) eval_stmts(sn(l), env)
+ else eval_stmts(rest, env)
+ }
+ eval_stmts(sn(""), Map())
+}
--- a/slides/bak-slides06.tex Sat Sep 23 13:36:20 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1484 +0,0 @@
-\documentclass[dvipsnames,14pt,t]{beamer}
-\usepackage{proof}
-\usepackage{beamerthemeplaincu}
-%\usepackage[T1]{fontenc}
-%\usepackage[latin1]{inputenc}
-\usepackage{mathpartir}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage[absolute,overlay]{textpos}
-\usepackage{ifthen}
-\usepackage{tikz}
-\usepackage{courier}
-\usepackage{listings}
-\usetikzlibrary{arrows}
-\usetikzlibrary{positioning}
-\usetikzlibrary{calc}
-\usetikzlibrary{shapes}
-\usepackage{graphicx}
-\setmonofont[Scale=MatchLowercase]{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}
-\newcommand{\isaliteral}[1]{}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-
-
-
-\definecolor{javared}{rgb}{0.6,0,0} % for strings
-\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
-\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
-\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
-
-\lstset{language=Java,
- basicstyle=\ttfamily,
- keywordstyle=\color{javapurple}\bfseries,
- stringstyle=\color{javagreen},
- commentstyle=\color{javagreen},
- morecomment=[s][\color{javadocblue}]{/**}{*/},
- numbers=left,
- numberstyle=\tiny\color{black},
- stepnumber=1,
- numbersep=10pt,
- tabsize=2,
- showspaces=false,
- showstringspaces=false}
-
-\lstdefinelanguage{scala}{
- morekeywords={abstract,case,catch,class,def,%
- do,else,extends,false,final,finally,%
- for,if,implicit,import,match,mixin,%
- new,null,object,override,package,%
- private,protected,requires,return,sealed,%
- super,this,throw,trait,true,try,%
- type,val,var,while,with,yield},
- otherkeywords={=>,<-,<\%,<:,>:,\#,@},
- sensitive=true,
- morecomment=[l]{//},
- morecomment=[n]{/*}{*/},
- morestring=[b]",
- morestring=[b]',
- morestring=[b]"""
-}
-
-\lstset{language=Scala,
- basicstyle=\ttfamily,
- keywordstyle=\color{javapurple}\bfseries,
- stringstyle=\color{javagreen},
- commentstyle=\color{javagreen},
- morecomment=[s][\color{javadocblue}]{/**}{*/},
- numbers=left,
- numberstyle=\tiny\color{black},
- stepnumber=1,
- numbersep=10pt,
- tabsize=2,
- 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}
-}
-
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
-
-% beamer stuff
-\renewcommand{\slidecaption}{APP 06, King's College London, 12 November 2013}
-
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}
-\begin{document}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>[t]
-\frametitle{%
- \begin{tabular}{@ {}c@ {}}
- \\
- \LARGE Access Control and \\[-3mm]
- \LARGE Privacy Policies (6)\\[-6mm]
- \end{tabular}}\bigskip\bigskip\bigskip
-
- %\begin{center}
- %\includegraphics[scale=1.3]{pics/barrier.jpg}
- %\end{center}
-
-\normalsize
- \begin{center}
- \begin{tabular}{ll}
- Email: & christian.urban at kcl.ac.uk\\
- Office: & N7.07 (North Wing, Bush House)\\
- Slides: & KEATS (also homework is there)\\
- \end{tabular}
- \end{center}
-
-
-\end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
-
- Formulas
-
- \begin{itemize}
- \item[]
-
- \begin{center}\color{blue}
- \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
- \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\
- \end{tabular}
- \end{center}
-
- \end{itemize}
-
-Judgements
-
-\begin{itemize}
-\item[] \mbox{\hspace{9mm}}\bl{$\Gamma \vdash \text{F}$}
-\end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Judgements}
-
-\begin{center}
-\begin{tikzpicture}[scale=1]
-
- \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
- \onslide<2->{
- \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{Inference Rules}
-
-\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}
-
-\only<2>{
-\begin{textblock}{11}(1,13)
-\small
-\bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}
-\end{textblock}}
-\only<3>{
-\begin{textblock}{11}(1,13)
-\small
-\bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge
- \underbrace{P \,\text{says}\, G}_{F_2} $}
-\end{textblock}}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Inference Rules}
-
-\begin{center}
-\bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\
-
-\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}}
-\qquad
-\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\
-
-\bl{\infer{\Gamma \vdash P\,\text{says}\, F}{\Gamma \vdash F}}\medskip\\
-
-\bl{\infer{\Gamma \vdash P \,\text{says}\, F_2}
- {\Gamma \vdash P \,\text{says}\, (F_1\Rightarrow F_2) \quad
- \Gamma \vdash P \,\text{says}\, F_1}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Sending Messages}
-
- \begin{itemize}
- \item Alice sends a message \bl{$m$}
- \begin{center}
- \bl{Alice says $m$}
- \end{center}\medskip\pause
-
- \item Alice sends an encrypted message \bl{$m$} with key \bl{$K$}
- (\bl{$\{m\}_K \dn K \Rightarrow m$})
- \begin{center}
- \bl{Alice says $\{m\}_K$}
- \end{center}\medskip\pause
-
- \item Decryption of Alice's message\smallskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
- {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Proofs}
-
-\begin{center}
-\bl{
-\infer{\Gamma \vdash F}
- {\infer{\hspace{1cm}:\hspace{1cm}}
- {\infer{\hspace{1cm}:\hspace{1cm}}{:}
- &
- \infer{\hspace{1cm}:\hspace{1cm}}{:\quad :}
- }}
-}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{The Access Control Problem}
-
-
-\begin{center}
- \begin{tikzpicture}[scale=1]
-
- \draw[line width=1mm] (-.3, -0.5) 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}provable/\\not provable\end{tabular}};
- \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\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}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Proofs}
-
-\begin{center}
-\includegraphics[scale=0.4]{pics/river-stones.jpg}
-\end{center}
-
-\begin{textblock}{5}(11.7,5)
-goal
-\end{textblock}
-
-\begin{textblock}{5}(11.7,14)
-start
-\end{textblock}
-
-\begin{textblock}{5}(0,7)
-\begin{center}
-\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]
-\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]
-\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}
-\end{center}
-\end{textblock}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\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} { }{ }{ } { }{ }{ }
- \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} { }{ }{ } { }{ }{ }
- \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} { }{ }{ } { }{ }{ }
- \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} { }{ }{ } { }{ }{ }
- \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{BTW}
-
-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{Example Proof}
-
-\begin{center}
-\bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}
- {\raisebox{2mm}{\text{\LARGE $?$}}}}
-\end{center}
-
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Example Proof}
-
-\begin{tabular}{@{\hspace{-6mm}}l}
-\begin{minipage}{1.1\textwidth}
-We have (by axiom)
-
-\begin{center}
-\begin{tabular}{@{}ll@{}}
-(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}
-\end{tabular}
-\end{center}
-
-From (1) we get
-
-\begin{center}
-\begin{tabular}{@{}ll@{}}
-(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
-(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
-\end{tabular}
-\end{center}
-
-From (3) and (2) we get
-
-\begin{center}
-\begin{tabular}{@{}ll@{}}
-\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
-\end{tabular}
-\end{center}
-
-Done.
-\end{minipage}
-\end{tabular}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Other Direction}
-
-\begin{tabular}{@{\hspace{-6mm}}l}
-\begin{minipage}{1.1\textwidth}
-We want to prove
-
-\begin{center}
-\begin{tabular}{@{}ll@{}}
-\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
-\end{tabular}
-\end{center}
-
-We better be able to prove:
-
-\begin{center}
-\begin{tabular}{@{}ll@{}}
-(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
-(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
-\end{tabular}
-\end{center}
-
-For (1): If we can prove
-
-\begin{center}
-\begin{tabular}{@{}ll@{}}
-\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
-\end{tabular}
-\end{center}
-
-then (1) is fine. Similarly for (2).
-\end{minipage}
-\end{tabular}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[t]
-
-I want to prove
-
-\begin{center}
-\bl{$\Gamma \vdash \text{del\_file}$}
-\end{center}\pause
-
-There is an inference rule
-
-\begin{center}
-\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
-\end{center}\pause
-
-So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause
-
-\bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\
-So I can use the rule
-
-\begin{center}
-\bl{\infer{\Gamma, F \vdash F}{}}
-\end{center}
-
-\onslide<5>{\bf\alert{What is wrong with this?}}
-\hfill{\bf Done. Qed.}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Program}
-
-How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip
-
-\begin{center}
-\Large \bl{\infer{\Gamma, F\vdash F}{}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad
-\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{center}
-\Large
-\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[t]
-\frametitle{Program: \texttt{prove2}}
-
-I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause
-
-\begin{enumerate}
-\item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause
-\item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove
-\begin{center}
-\bl{$\Gamma \vdash F_2$}
-\end{center}\bigskip\pause
-
-\item So I am able to try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption
-\bl{$F_2$}.\bigskip
-\begin{center}
-\bl{$F_2, \Gamma \vdash \text{Pred}$}
-\end{center}
-\end{enumerate}
-
-\only<4>{
-\begin{textblock}{11}(1,10.5)
-\bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}
-\end{textblock}}
-
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{}
-
- Recall the following scenario:
-
- \begin{itemize}
- \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}}
- should be deleted, then this file must be deleted.
- \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
- \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.
- \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.
- \end{itemize}\bigskip
-
- \small
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
- \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\
- \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
- \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
- \end{tabular}}\medskip
-
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{itemize}
-\item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or
-can make a statement \bl{$F$}\bigskip
-
-\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
-\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
-
-\begin{center}
-\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
-\end{center}
-
-
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Trusted Third Party}
-
-Simple protocol for establishing a secure connection via a mutually
-trusted 3rd party (server):
-
-\begin{center}
-\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
-Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
-Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
-Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
-Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
-\end{tabular}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Sending Rule}
-
- \bl{\begin{center}
- \mbox{\infer{\Gamma \vdash Q \;\text{says}\; F}
- {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}}
- \end{center}}\bigskip\pause
-
- \bl{$P \,\text{sends}\, Q : F \dn$}\\
- \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Trusted Third Party}
-
- \begin{center}
- \bl{\begin{tabular}{l}
- $A$ sends $S$ : $\text{Connect}(A,B)$\\
- \bl{$S \,\text{says}\, (\text{Connect}(A,B) \Rightarrow$}\\
- \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
- \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
- $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
- $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
- $A$ sends $B$ : $\{m\}_{K_{AB}}$
- \end{tabular}}
- \end{center}\bigskip\pause
-
-
- \bl{$\Gamma \vdash B \,\text{says} \, m$}?
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Public/Private Keys}
-
- \begin{itemize}
- \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
- {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
- \Gamma \vdash K_{Bob}^{priv}}}}
- \end{center}\bigskip\pause
-
- \item this is {\bf not} a derived rule!
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Security Levels}
- \small
-
- \begin{itemize}
- \item Top secret (\bl{$T\!S$})
- \item Secret (\bl{$S$})
- \item Public (\bl{$P$})
- \end{itemize}
-
- \begin{center}
- \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
- \end{center}
-
- \begin{itemize}
- \item Bob has a clearance for ``secret''
- \item Bob can read documents that are public or sectret, but not top secret
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
- \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\only<2->{\\}
- \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
- \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
- \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
- \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Substitution Rule}
- \small
-
- \bl{\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}}\bigskip\pause
-
- \begin{itemize}
- \item \bl{$slev($Bob$)$ $=$ $S$}
- \item \bl{$slev($File$)$ $=$ $P$}
- \item \bl{$slev(P) < slev(S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ $P$\\
- $slev($Bob$)$ $=$ $T\!S$\\
- \only<1>{\textcolor{red}{$?$}}%
- \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
- \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Transitivity Rule}
- \small
-
- \bl{\begin{center}
- \begin{tabular}{c}
- $\Gamma \vdash l_1 < l_2$
- \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
- $\Gamma \vdash l_1 < l_3$
- \end{tabular}
- \end{center}}\bigskip
-
- \begin{itemize}
- \item \bl{$slev(P) < slev (S)$}
- \item \bl{$slev(S) < slev (T\!S)$}
- \item[] \bl{$slev(P) < slev (T\!S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading Files}
-
- \begin{itemize}
- \item Access policy for reading
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
- $slev($Bob$)$ $=$ $T\!S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Writing Files}
-
- \begin{itemize}
- \item Access policy for \underline{writing}
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
- Bob says Permitted $($File, write$)$\\
- $slev($File$)$ $=$ $T\!S$\\
- $slev($Bob$)$ $=$ $S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, write$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-\end{document}
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Encryption}
-
- \begin{itemize}
- \item Encryption of a message\smallskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
- {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Public/Private Keys}
-
- \begin{itemize}
- \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
- {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
- \Gamma \vdash K_{Bob}^{priv}}}}
- \end{center}\bigskip\pause
-
- \item this is {\bf not} a derived rule!
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Trusted Third Party}
-
- \begin{itemize}
- \item Alice calls Sam for a key to communicate with Bob
- \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
- \item Alice sends the message encrypted with the key and the second key it recieved
- \end{itemize}\bigskip
-
- \begin{center}
- \bl{\begin{tabular}{lcl}
- $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\
- $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
- $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\
- $A$ sends $B$ &:& $\{m\}_{K_{AB}}$
- \end{tabular}}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Controls}
- \small
-
- \begin{itemize}
- \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}
-
- \item its meaning ``\bl{P} is entitled to do \bl{F}''
- \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- }}
- \end{center}\pause
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- }}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Security Levels}
- \small
-
- \begin{itemize}
- \item Top secret (\bl{$T\!S$})
- \item Secret (\bl{$S$})
- \item Public (\bl{$P$})
- \end{itemize}
-
- \begin{center}
- \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
- \end{center}
-
- \begin{itemize}
- \item Bob has a clearance for ``secret''
- \item Bob can read documents that are public or sectret, but not top secret
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
- \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\only<2->{\\}
- \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
- \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
- \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
- \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Substitution Rule}
- \small
-
- \bl{\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}}\bigskip\pause
-
- \begin{itemize}
- \item \bl{$slev($Bob$)$ $=$ $S$}
- \item \bl{$slev($File$)$ $=$ $P$}
- \item \bl{$slev(P) < slev(S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ $P$\\
- $slev($Bob$)$ $=$ $T\!S$\\
- \only<1>{\textcolor{red}{$?$}}%
- \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
- \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Transitivity Rule}
- \small
-
- \bl{\begin{center}
- \begin{tabular}{c}
- $\Gamma \vdash l_1 < l_2$
- \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
- $\Gamma \vdash l_1 < l_3$
- \end{tabular}
- \end{center}}\bigskip
-
- \begin{itemize}
- \item \bl{$slev(P) < slev (S)$}
- \item \bl{$slev(S) < slev (T\!S)$}
- \item[] \bl{$slev(P) < slev (T\!S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading Files}
-
- \begin{itemize}
- \item Access policy for reading
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
- $slev($Bob$)$ $=$ $T\!S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Writing Files}
-
- \begin{itemize}
- \item Access policy for \underline{writing}
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
- Bob says Permitted $($File, write$)$\\
- $slev($File$)$ $=$ $T\!S$\\
- $slev($Bob$)$ $=$ $S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, write$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Sending Rule}
-
- \bl{\begin{center}
- \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
- {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
- \end{center}}\bigskip\pause
-
- \bl{$P \,\text{sends}\, Q : F \dn$}\\
- \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Trusted Third Party}
-
- \begin{center}
- \bl{\begin{tabular}{l}
- $A$ sends $S$ : $\textit{Connect}(A,B)$\\
- \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\
- \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
- \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
- $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
- $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
- $A$ sends $B$ : $\{m\}_{K_{AB}}$
- \end{tabular}}
- \end{center}\bigskip\pause
-
-
- \bl{$\Gamma \vdash B \,\text{says} \, m$}?
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/bak-slides06.tex-bak Sat Sep 23 14:19:09 2017 +0100
@@ -0,0 +1,1484 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{proof}
+\usepackage{beamerthemeplaincu}
+%\usepackage[T1]{fontenc}
+%\usepackage[latin1]{inputenc}
+\usepackage{mathpartir}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage[absolute,overlay]{textpos}
+\usepackage{ifthen}
+\usepackage{tikz}
+\usepackage{courier}
+\usepackage{listings}
+\usetikzlibrary{arrows}
+\usetikzlibrary{positioning}
+\usetikzlibrary{calc}
+\usetikzlibrary{shapes}
+\usepackage{graphicx}
+\setmonofont[Scale=MatchLowercase]{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}
+\newcommand{\isaliteral}[1]{}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+
+
+
+\definecolor{javared}{rgb}{0.6,0,0} % for strings
+\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
+\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
+\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
+
+\lstset{language=Java,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+\lstdefinelanguage{scala}{
+ morekeywords={abstract,case,catch,class,def,%
+ do,else,extends,false,final,finally,%
+ for,if,implicit,import,match,mixin,%
+ new,null,object,override,package,%
+ private,protected,requires,return,sealed,%
+ super,this,throw,trait,true,try,%
+ type,val,var,while,with,yield},
+ otherkeywords={=>,<-,<\%,<:,>:,\#,@},
+ sensitive=true,
+ morecomment=[l]{//},
+ morecomment=[n]{/*}{*/},
+ morestring=[b]",
+ morestring=[b]',
+ morestring=[b]"""
+}
+
+\lstset{language=Scala,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ 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}
+}
+
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+
+% beamer stuff
+\renewcommand{\slidecaption}{APP 06, King's College London, 12 November 2013}
+
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1>[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\
+ \LARGE Access Control and \\[-3mm]
+ \LARGE Privacy Policies (6)\\[-6mm]
+ \end{tabular}}\bigskip\bigskip\bigskip
+
+ %\begin{center}
+ %\includegraphics[scale=1.3]{pics/barrier.jpg}
+ %\end{center}
+
+\normalsize
+ \begin{center}
+ \begin{tabular}{ll}
+ Email: & christian.urban at kcl.ac.uk\\
+ Office: & N7.07 (North Wing, Bush House)\\
+ Slides: & KEATS (also homework is there)\\
+ \end{tabular}
+ \end{center}
+
+
+\end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
+
+ Formulas
+
+ \begin{itemize}
+ \item[]
+
+ \begin{center}\color{blue}
+ \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
+ \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+Judgements
+
+\begin{itemize}
+\item[] \mbox{\hspace{9mm}}\bl{$\Gamma \vdash \text{F}$}
+\end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Judgements}
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+
+ \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
+ \onslide<2->{
+ \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{Inference Rules}
+
+\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}
+
+\only<2>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}
+\end{textblock}}
+\only<3>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge
+ \underbrace{P \,\text{says}\, G}_{F_2} $}
+\end{textblock}}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Inference Rules}
+
+\begin{center}
+\bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\
+
+\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}}
+\qquad
+\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\
+
+\bl{\infer{\Gamma \vdash P\,\text{says}\, F}{\Gamma \vdash F}}\medskip\\
+
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F_2}
+ {\Gamma \vdash P \,\text{says}\, (F_1\Rightarrow F_2) \quad
+ \Gamma \vdash P \,\text{says}\, F_1}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Messages}
+
+ \begin{itemize}
+ \item Alice sends a message \bl{$m$}
+ \begin{center}
+ \bl{Alice says $m$}
+ \end{center}\medskip\pause
+
+ \item Alice sends an encrypted message \bl{$m$} with key \bl{$K$}
+ (\bl{$\{m\}_K \dn K \Rightarrow m$})
+ \begin{center}
+ \bl{Alice says $\{m\}_K$}
+ \end{center}\medskip\pause
+
+ \item Decryption of Alice's message\smallskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Proofs}
+
+\begin{center}
+\bl{
+\infer{\Gamma \vdash F}
+ {\infer{\hspace{1cm}:\hspace{1cm}}
+ {\infer{\hspace{1cm}:\hspace{1cm}}{:}
+ &
+ \infer{\hspace{1cm}:\hspace{1cm}}{:\quad :}
+ }}
+}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{The Access Control Problem}
+
+
+\begin{center}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[line width=1mm] (-.3, -0.5) 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}provable/\\not provable\end{tabular}};
+ \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\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}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Proofs}
+
+\begin{center}
+\includegraphics[scale=0.4]{pics/river-stones.jpg}
+\end{center}
+
+\begin{textblock}{5}(11.7,5)
+goal
+\end{textblock}
+
+\begin{textblock}{5}(11.7,14)
+start
+\end{textblock}
+
+\begin{textblock}{5}(0,7)
+\begin{center}
+\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]
+\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]
+\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}
+\end{center}
+\end{textblock}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\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} { }{ }{ } { }{ }{ }
+ \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} { }{ }{ } { }{ }{ }
+ \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} { }{ }{ } { }{ }{ }
+ \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} { }{ }{ } { }{ }{ }
+ \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{BTW}
+
+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{Example Proof}
+
+\begin{center}
+\bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}
+ {\raisebox{2mm}{\text{\LARGE $?$}}}}
+\end{center}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Example Proof}
+
+\begin{tabular}{@{\hspace{-6mm}}l}
+\begin{minipage}{1.1\textwidth}
+We have (by axiom)
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}
+\end{tabular}
+\end{center}
+
+From (1) we get
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
+(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+\end{tabular}
+\end{center}
+
+From (3) and (2) we get
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+Done.
+\end{minipage}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Other Direction}
+
+\begin{tabular}{@{\hspace{-6mm}}l}
+\begin{minipage}{1.1\textwidth}
+We want to prove
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+We better be able to prove:
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
+\end{tabular}
+\end{center}
+
+For (1): If we can prove
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+then (1) is fine. Similarly for (2).
+\end{minipage}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+I want to prove
+
+\begin{center}
+\bl{$\Gamma \vdash \text{del\_file}$}
+\end{center}\pause
+
+There is an inference rule
+
+\begin{center}
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}\pause
+
+So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause
+
+\bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\
+So I can use the rule
+
+\begin{center}
+\bl{\infer{\Gamma, F \vdash F}{}}
+\end{center}
+
+\onslide<5>{\bf\alert{What is wrong with this?}}
+\hfill{\bf Done. Qed.}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Program}
+
+How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip
+
+\begin{center}
+\Large \bl{\infer{\Gamma, F\vdash F}{}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad
+\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{Program: \texttt{prove2}}
+
+I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause
+
+\begin{enumerate}
+\item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause
+\item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove
+\begin{center}
+\bl{$\Gamma \vdash F_2$}
+\end{center}\bigskip\pause
+
+\item So I am able to try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption
+\bl{$F_2$}.\bigskip
+\begin{center}
+\bl{$F_2, \Gamma \vdash \text{Pred}$}
+\end{center}
+\end{enumerate}
+
+\only<4>{
+\begin{textblock}{11}(1,10.5)
+\bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}
+\end{textblock}}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+
+ Recall the following scenario:
+
+ \begin{itemize}
+ \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}}
+ should be deleted, then this file must be deleted.
+ \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
+ \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.
+ \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.
+ \end{itemize}\bigskip
+
+ \small
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
+ \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\
+ \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
+ \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
+ \end{tabular}}\medskip
+
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{itemize}
+\item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or
+can make a statement \bl{$F$}\bigskip
+
+\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
+\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
+
+\begin{center}
+\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
+\end{center}
+
+
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Trusted Third Party}
+
+Simple protocol for establishing a secure connection via a mutually
+trusted 3rd party (server):
+
+\begin{center}
+\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
+Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
+Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
+Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
+Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
+\end{tabular}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Rule}
+
+ \bl{\begin{center}
+ \mbox{\infer{\Gamma \vdash Q \;\text{says}\; F}
+ {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}}
+ \end{center}}\bigskip\pause
+
+ \bl{$P \,\text{sends}\, Q : F \dn$}\\
+ \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $A$ sends $S$ : $\text{Connect}(A,B)$\\
+ \bl{$S \,\text{says}\, (\text{Connect}(A,B) \Rightarrow$}\\
+ \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
+ \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
+ $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ : $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}\bigskip\pause
+
+
+ \bl{$\Gamma \vdash B \,\text{says} \, m$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Public/Private Keys}
+
+ \begin{itemize}
+ \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
+ \Gamma \vdash K_{Bob}^{priv}}}}
+ \end{center}\bigskip\pause
+
+ \item this is {\bf not} a derived rule!
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Security Levels}
+ \small
+
+ \begin{itemize}
+ \item Top secret (\bl{$T\!S$})
+ \item Secret (\bl{$S$})
+ \item Public (\bl{$P$})
+ \end{itemize}
+
+ \begin{center}
+ \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
+ \end{center}
+
+ \begin{itemize}
+ \item Bob has a clearance for ``secret''
+ \item Bob can read documents that are public or sectret, but not top secret
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
+ \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\only<2->{\\}
+ \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
+ \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
+ \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
+ \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Substitution Rule}
+ \small
+
+ \bl{\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}}\bigskip\pause
+
+ \begin{itemize}
+ \item \bl{$slev($Bob$)$ $=$ $S$}
+ \item \bl{$slev($File$)$ $=$ $P$}
+ \item \bl{$slev(P) < slev(S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ $P$\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ \only<1>{\textcolor{red}{$?$}}%
+ \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
+ \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Transitivity Rule}
+ \small
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ $\Gamma \vdash l_1 < l_2$
+ \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
+ $\Gamma \vdash l_1 < l_3$
+ \end{tabular}
+ \end{center}}\bigskip
+
+ \begin{itemize}
+ \item \bl{$slev(P) < slev (S)$}
+ \item \bl{$slev(S) < slev (T\!S)$}
+ \item[] \bl{$slev(P) < slev (T\!S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading Files}
+
+ \begin{itemize}
+ \item Access policy for reading
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Writing Files}
+
+ \begin{itemize}
+ \item Access policy for \underline{writing}
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
+ Bob says Permitted $($File, write$)$\\
+ $slev($File$)$ $=$ $T\!S$\\
+ $slev($Bob$)$ $=$ $S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, write$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+\end{document}
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Encryption}
+
+ \begin{itemize}
+ \item Encryption of a message\smallskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Public/Private Keys}
+
+ \begin{itemize}
+ \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
+ \Gamma \vdash K_{Bob}^{priv}}}}
+ \end{center}\bigskip\pause
+
+ \item this is {\bf not} a derived rule!
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{itemize}
+ \item Alice calls Sam for a key to communicate with Bob
+ \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
+ \item Alice sends the message encrypted with the key and the second key it recieved
+ \end{itemize}\bigskip
+
+ \begin{center}
+ \bl{\begin{tabular}{lcl}
+ $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\
+ $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ &:& $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Controls}
+ \small
+
+ \begin{itemize}
+ \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}
+
+ \item its meaning ``\bl{P} is entitled to do \bl{F}''
+ \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause
+
+ \begin{center}
+ \bl{\mbox{
+ \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
+ {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
+ }}
+ \end{center}\pause
+
+ \begin{center}
+ \bl{\mbox{
+ \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
+ {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
+ }}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Security Levels}
+ \small
+
+ \begin{itemize}
+ \item Top secret (\bl{$T\!S$})
+ \item Secret (\bl{$S$})
+ \item Public (\bl{$P$})
+ \end{itemize}
+
+ \begin{center}
+ \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
+ \end{center}
+
+ \begin{itemize}
+ \item Bob has a clearance for ``secret''
+ \item Bob can read documents that are public or sectret, but not top secret
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
+ \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\only<2->{\\}
+ \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
+ \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
+ \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
+ \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Substitution Rule}
+ \small
+
+ \bl{\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}}\bigskip\pause
+
+ \begin{itemize}
+ \item \bl{$slev($Bob$)$ $=$ $S$}
+ \item \bl{$slev($File$)$ $=$ $P$}
+ \item \bl{$slev(P) < slev(S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ $P$\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ \only<1>{\textcolor{red}{$?$}}%
+ \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
+ \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Transitivity Rule}
+ \small
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ $\Gamma \vdash l_1 < l_2$
+ \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
+ $\Gamma \vdash l_1 < l_3$
+ \end{tabular}
+ \end{center}}\bigskip
+
+ \begin{itemize}
+ \item \bl{$slev(P) < slev (S)$}
+ \item \bl{$slev(S) < slev (T\!S)$}
+ \item[] \bl{$slev(P) < slev (T\!S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading Files}
+
+ \begin{itemize}
+ \item Access policy for reading
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Writing Files}
+
+ \begin{itemize}
+ \item Access policy for \underline{writing}
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
+ Bob says Permitted $($File, write$)$\\
+ $slev($File$)$ $=$ $T\!S$\\
+ $slev($Bob$)$ $=$ $S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, write$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Rule}
+
+ \bl{\begin{center}
+ \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
+ {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
+ \end{center}}\bigskip\pause
+
+ \bl{$P \,\text{sends}\, Q : F \dn$}\\
+ \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $A$ sends $S$ : $\textit{Connect}(A,B)$\\
+ \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\
+ \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
+ \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
+ $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ : $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}\bigskip\pause
+
+
+ \bl{$\Gamma \vdash B \,\text{says} \, m$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+
--- a/slides/bak-slides07.tex Sat Sep 23 13:36:20 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,739 +0,0 @@
-\documentclass[dvipsnames,14pt,t]{beamer}
-\usepackage{proof}
-\usepackage{beamerthemeplaincu}
-%\usepackage[T1]{fontenc}
-%\usepackage[latin1]{inputenc}
-\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}
-
-
-\isabellestyle{rm}
-\renewcommand{\isastyle}{\rm}%
-\renewcommand{\isastyleminor}{\rm}%
-\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
-\renewcommand{\isatagproof}{}
-\renewcommand{\endisatagproof}{}
-\renewcommand{\isamarkupcmt}[1]{#1}
-\newcommand{\isaliteral}[1]{}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#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}
-
-
-
-\definecolor{javared}{rgb}{0.6,0,0} % for strings
-\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
-\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
-\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
-
-\lstset{language=Java,
- basicstyle=\ttfamily,
- keywordstyle=\color{javapurple}\bfseries,
- stringstyle=\color{javagreen},
- commentstyle=\color{javagreen},
- morecomment=[s][\color{javadocblue}]{/**}{*/},
- numbers=left,
- numberstyle=\tiny\color{black},
- stepnumber=1,
- numbersep=10pt,
- tabsize=2,
- showspaces=false,
- showstringspaces=false}
-
-\lstdefinelanguage{scala}{
- morekeywords={abstract,case,catch,class,def,%
- do,else,extends,false,final,finally,%
- for,if,implicit,import,match,mixin,%
- new,null,object,override,package,%
- private,protected,requires,return,sealed,%
- super,this,throw,trait,true,try,%
- type,val,var,while,with,yield},
- otherkeywords={=>,<-,<\%,<:,>:,\#,@},
- sensitive=true,
- morecomment=[l]{//},
- morecomment=[n]{/*}{*/},
- morestring=[b]",
- morestring=[b]',
- morestring=[b]"""
-}
-
-\lstset{language=Scala,
- basicstyle=\ttfamily,
- keywordstyle=\color{javapurple}\bfseries,
- stringstyle=\color{javagreen},
- commentstyle=\color{javagreen},
- morecomment=[s][\color{javadocblue}]{/**}{*/},
- numbers=left,
- numberstyle=\tiny\color{black},
- stepnumber=1,
- numbersep=10pt,
- tabsize=2,
- showspaces=false,
- showstringspaces=false}
-
-% beamer stuff
-\renewcommand{\slidecaption}{APP 07, King's College London, 19 November 2013}
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}
-
-
-
-\begin{document}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>[t]
-\frametitle{%
- \begin{tabular}{@ {}c@ {}}
- \\
- \LARGE Access Control and \\[-3mm]
- \LARGE Privacy Policies (7)\\[-6mm]
- \end{tabular}}\bigskip\bigskip\bigskip
-
- %\begin{center}
- %\includegraphics[scale=1.3]{pics/barrier.jpg}
- %\end{center}
-
-\normalsize
- \begin{center}
- \begin{tabular}{ll}
- Email: & christian.urban at kcl.ac.uk\\
- Office: & N7.07 (North Wing, Bush House)\\
- Slides: & KEATS (also homework is there)\\
- \end{tabular}
- \end{center}
-
-
-\end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{}
-
- Recall the following scenario:
-
- \begin{itemize}
- \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file}}
- should be deleted, then this file must be deleted.
- \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
- \textcolor{blue}{\isa{file}} should be deleted (delegation).
- \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file}}.
- \end{itemize}\bigskip
-
- \small
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
- \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\
- \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
- \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
- \end{tabular}}\medskip
-
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{\begin{tabular}{@ {\hspace{-2mm}}c@ {}}The Access Control Problem\end{tabular}}
-
-
-\begin{center}
- \begin{tikzpicture}[scale=1]
-
- \draw[line width=1mm] (-.3, -0.5) 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}provable/\\not provable\end{tabular}};
- \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\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 (\boldmath\bl{$\Gamma$})\end{tabular}};
-
- \end{tikzpicture}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\begin{itemize}
-\item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or
-can make a ``statement'' \bl{$F$}\bigskip\pause
-
-\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
-\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
-
-\begin{center}
-\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
-\end{center}
-
-
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Security Levels}
- \small
-
- \begin{itemize}
- \item Top secret (\bl{$T\!S$})
- \item Secret (\bl{$S$})
- \item Public (\bl{$P$})
- \end{itemize}
-
- \begin{center}
- \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
- \end{center}
-
- \begin{itemize}
- \item Bob has a clearance for ``secret''
- \item Bob can read documents that are public or sectret, but not top secret
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
- \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\only<2->{\\}
- \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
- \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
- \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
- \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Substitution Rule}
- \small
-
- \bl{\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}}\bigskip\pause
-
- \begin{itemize}
- \item \bl{$slev($Bob$)$ $=$ $S$}
- \item \bl{$slev($File$)$ $=$ $P$}
- \item \bl{$slev(P) < slev(S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ $P$\\
- $slev($Bob$)$ $=$ $T\!S$\\
- \only<1>{\textcolor{red}{$?$}}%
- \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
- \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Transitivity Rule}
- \small
-
- \bl{\begin{center}
- \begin{tabular}{c}
- $\Gamma \vdash l_1 < l_2$
- \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
- $\Gamma \vdash l_1 < l_3$
- \end{tabular}
- \end{center}}\bigskip
-
- \begin{itemize}
- \item \bl{$slev(P) < slev (S)$}
- \item \bl{$slev(S) < slev (T\!S)$}
- \item[] \bl{$slev(P) < slev (T\!S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading Files}
-
- \begin{itemize}
- \item Access policy for Bob for reading
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
- $slev($Bob$)$ $=$ $T\!S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Writing Files}
-
- \begin{itemize}
- \item Access policy for Bob for {\bf writing}
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
- Bob says Permitted $($File, write$)$\\
- $slev($File$)$ $=$ $T\!S$\\
- $slev($Bob$)$ $=$ $S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, write$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Encrypted Messages}
-
- \begin{itemize}
- \item Alice sends a message \bl{$m$}
- \begin{center}
- \bl{Alice says $m$}
- \end{center}\medskip\pause
-
- \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})
- \begin{center}
- \bl{Alice says $\{m\}_K$}
- \end{center}\medskip\pause
-
- \item Decryption of Alice's message\smallskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
- {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Encryption}
-
- \begin{itemize}
- \item Encryption of a message\smallskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
- {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Trusted Third Party}
-
-Simple protocol for establishing a secure connection via a mutually
-trusted 3rd party (server):
-
-\begin{center}
-\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
-Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
-Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
-Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
-Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
-\end{tabular}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Sending Rule}
-
- \bl{\begin{center}
- \mbox{$\infer{\Gamma \vdash Q \;\text{says}\; F}
- {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}$}
- \end{center}}\bigskip\pause
-
- \bl{$P \,\text{sends}\, Q : F \dn$}\\
- \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Trusted Third Party}
-
- \begin{center}
- \bl{\begin{tabular}{l}
- $A$ sends $S$ : $\text{Connect}(A,B)$\\
- \bl{$S \,\text{says}\, (\text{Connect}(A,B) \Rightarrow$}\\
- \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
- \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
- $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
- $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
- $A$ sends $B$ : $\{m\}_{K_{AB}}$
- \end{tabular}}
- \end{center}\bigskip\pause
-
-
- \bl{$\Gamma \vdash B \,\text{says} \, m$}?
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Public/Private Keys}
-
- \begin{itemize}
- \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
- \begin{center}
- \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
- {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
- \Gamma \vdash K_{Bob}^{priv}}}}
- \end{center}\bigskip\pause
-
- \item this is {\bf not} a derived rule!
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-% \begin{itemize}
-% \item Alice calls Sam for a key to communicate with Bob
-% \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
- % \item Alice sends the message encrypted with the key and the second key it recieved
- % \end{itemize}\bigskip
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Sending Rule}
-
-
- \bl{\begin{center}
- \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
- {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
- \end{center}}\bigskip\pause
-
- \bl{$P \,\text{sends}\, Q : F \dn$}\\
- \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Trusted Third Party}
-
- \begin{center}
- \bl{\begin{tabular}{l}
- $A$ sends $S$ : $\textit{Connect}(A,B)$\\
- \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\
- \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
- \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
- $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
- $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
- $A$ sends $B$ : $\{m\}_{K_{AB}}$
- \end{tabular}}
- \end{center}\bigskip\pause
-
-
- \bl{$\Gamma \vdash B \,\text{says} \, m$}?
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Challenge-Response Protocol}
-
- \begin{itemize}
- \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip
- \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip
- \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip
- \item if \bl{$E$} receives \bl{$\{N\}_K$} from \bl{$T$}, it starts engine
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Challenge-Response Protocol}
-
- \begin{center}
- \bl{\begin{tabular}{l}
- $E \;\text{says}\; N$\hfill(start)\\
- $E \;\text{sends}\; T : N$\hfill(challenge)\\
- $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\
- \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\
- $T \;\text{says}\; K$\hfill(key)\\
- $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\
- $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\
- \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\
- \end{tabular}}
- \end{center}\bigskip
-
- \bl{$\Gamma \vdash \text{start\_engine}(T)$}?
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Exchange of a Fresh Key}
-
-\bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key
-
- \begin{itemize}
- \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip
- \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$}
- \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
- \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
- \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}
- \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}
- \end{itemize}\bigskip
-
- Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{The Attack}
-
-An intruder \bl{$I$} convinces \bl{$A$} to accept the compromised key \bl{$K^{new}_{AB}$}\medskip
-
-\begin{minipage}{1.1\textwidth}
-\begin{itemize}
- \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$}
- \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
- \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
- \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause
- \item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$}
- \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$}
- \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$}
- \item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$}
- \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause
- \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also
- \end{itemize}
- \end{minipage}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-A Man-in-the-middle attack in real life:
-
-\begin{itemize}
-\item the card only says yes or no to the terminal if the PIN is correct
-\item trick the card in thinking transaction is verified by signature
-\item trick the terminal in thinking the transaction was verified by PIN
-\end{itemize}
-
-\begin{minipage}{1.1\textwidth}
-\begin{center}
-\mbox{}\hspace{-6mm}\includegraphics[scale=0.5]{pics/chip-attack.png}
-\includegraphics[scale=0.3]{pics/chipnpinflaw.png}
-\end{center}
-\end{minipage}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Problems with EMV}
-
-\begin{itemize}
-\item it is a wrapper for many protocols
-\item specification by consensus (resulted unmanageable complexity)
-\item its specification is 700 pages in English plus 2000+ pages for testing, additionally some
-further parts are secret
-\item other attacks have been found
-
-\item one solution might be to require always online verification of the PIN with the bank
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{\begin{tabular}{c}Problems with WEP (Wifi)\end{tabular}}
-
-\begin{itemize}
-\item a standard ratified in 1999
-\item the protocol was designed by a committee not including cryptographers
-\item it used the RC4 encryption algorithm which is a stream cipher requiring a unique nonce
-\item WEP did not allocate enough bits for the nonce
-\item for authenticating packets it used CRC checksum which can be easily broken
-\item the network password was used to directly encrypt packages (instead of a key negotiation protocol)\bigskip
-\item encryption was turned off by default
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Protocols are Difficult}
-
-\begin{itemize}
-\item even the systems designed by experts regularly fail\medskip
-\item try to make everything explicit (you need to authenticate all data you might rely on)\medskip
-\item the one who can fix a system should also be liable for the losses\medskip
-\item cryptography is often not {\bf the} answer\bigskip\bigskip
-\end{itemize}
-
-logic is one way protocols are studied in academia
-(you can use computers to search for attacks)
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Public-Key Infrastructure}
-
-\begin{itemize}
-\item the idea is to have a certificate authority (CA)
-\item you go to the CA to identify yourself
-\item CA: ``I, the CA, have verified that public key \bl{$P^{pub}_{Bob}$} belongs to Bob''\bigskip
-\item CA must be trusted by everybody
-\item What happens if CA issues a false certificate? Who pays in case of loss? (VeriSign
-explicitly limits liability to \$100.)
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-
-
-
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/bak-slides07.tex-bak Sat Sep 23 14:19:09 2017 +0100
@@ -0,0 +1,739 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{proof}
+\usepackage{beamerthemeplaincu}
+%\usepackage[T1]{fontenc}
+%\usepackage[latin1]{inputenc}
+\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}
+
+
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\renewcommand{\isatagproof}{}
+\renewcommand{\endisatagproof}{}
+\renewcommand{\isamarkupcmt}[1]{#1}
+\newcommand{\isaliteral}[1]{}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#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}
+
+
+
+\definecolor{javared}{rgb}{0.6,0,0} % for strings
+\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
+\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
+\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
+
+\lstset{language=Java,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+\lstdefinelanguage{scala}{
+ morekeywords={abstract,case,catch,class,def,%
+ do,else,extends,false,final,finally,%
+ for,if,implicit,import,match,mixin,%
+ new,null,object,override,package,%
+ private,protected,requires,return,sealed,%
+ super,this,throw,trait,true,try,%
+ type,val,var,while,with,yield},
+ otherkeywords={=>,<-,<\%,<:,>:,\#,@},
+ sensitive=true,
+ morecomment=[l]{//},
+ morecomment=[n]{/*}{*/},
+ morestring=[b]",
+ morestring=[b]',
+ morestring=[b]"""
+}
+
+\lstset{language=Scala,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+% beamer stuff
+\renewcommand{\slidecaption}{APP 07, King's College London, 19 November 2013}
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
+
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1>[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\
+ \LARGE Access Control and \\[-3mm]
+ \LARGE Privacy Policies (7)\\[-6mm]
+ \end{tabular}}\bigskip\bigskip\bigskip
+
+ %\begin{center}
+ %\includegraphics[scale=1.3]{pics/barrier.jpg}
+ %\end{center}
+
+\normalsize
+ \begin{center}
+ \begin{tabular}{ll}
+ Email: & christian.urban at kcl.ac.uk\\
+ Office: & N7.07 (North Wing, Bush House)\\
+ Slides: & KEATS (also homework is there)\\
+ \end{tabular}
+ \end{center}
+
+
+\end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+
+ Recall the following scenario:
+
+ \begin{itemize}
+ \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file}}
+ should be deleted, then this file must be deleted.
+ \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
+ \textcolor{blue}{\isa{file}} should be deleted (delegation).
+ \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file}}.
+ \end{itemize}\bigskip
+
+ \small
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
+ \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\
+ \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
+ \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
+ \end{tabular}}\medskip
+
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{\begin{tabular}{@ {\hspace{-2mm}}c@ {}}The Access Control Problem\end{tabular}}
+
+
+\begin{center}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[line width=1mm] (-.3, -0.5) 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}provable/\\not provable\end{tabular}};
+ \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\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 (\boldmath\bl{$\Gamma$})\end{tabular}};
+
+ \end{tikzpicture}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{itemize}
+\item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or
+can make a ``statement'' \bl{$F$}\bigskip\pause
+
+\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
+\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
+
+\begin{center}
+\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
+\end{center}
+
+
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Security Levels}
+ \small
+
+ \begin{itemize}
+ \item Top secret (\bl{$T\!S$})
+ \item Secret (\bl{$S$})
+ \item Public (\bl{$P$})
+ \end{itemize}
+
+ \begin{center}
+ \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
+ \end{center}
+
+ \begin{itemize}
+ \item Bob has a clearance for ``secret''
+ \item Bob can read documents that are public or sectret, but not top secret
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
+ \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\only<2->{\\}
+ \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
+ \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
+ \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
+ \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Substitution Rule}
+ \small
+
+ \bl{\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}}\bigskip\pause
+
+ \begin{itemize}
+ \item \bl{$slev($Bob$)$ $=$ $S$}
+ \item \bl{$slev($File$)$ $=$ $P$}
+ \item \bl{$slev(P) < slev(S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading a File}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $($File, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ $P$\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ \only<1>{\textcolor{red}{$?$}}%
+ \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
+ \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Transitivity Rule}
+ \small
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ $\Gamma \vdash l_1 < l_2$
+ \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
+ $\Gamma \vdash l_1 < l_3$
+ \end{tabular}
+ \end{center}}\bigskip
+
+ \begin{itemize}
+ \item \bl{$slev(P) < slev (S)$}
+ \item \bl{$slev(S) < slev (T\!S)$}
+ \item[] \bl{$slev(P) < slev (T\!S)$}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Reading Files}
+
+ \begin{itemize}
+ \item Access policy for Bob for reading
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
+ Bob says Permitted $($File, read$)$\\
+ $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
+ $slev($Bob$)$ $=$ $T\!S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, read$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Writing Files}
+
+ \begin{itemize}
+ \item Access policy for Bob for {\bf writing}
+ \end{itemize}
+
+ \bl{\begin{center}
+ \begin{tabular}{c}
+ \begin{tabular}{@ {}l@ {}}
+ $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
+ \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
+ Bob says Permitted $($File, write$)$\\
+ $slev($File$)$ $=$ $T\!S$\\
+ $slev($Bob$)$ $=$ $S$\\
+ $slev(P) < slev(S)$\\
+ $slev(S) < slev(T\!S)$
+ \end{tabular}\\
+ \hline
+ Permitted $($File, write$)$
+ \end{tabular}
+ \end{center}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Encrypted Messages}
+
+ \begin{itemize}
+ \item Alice sends a message \bl{$m$}
+ \begin{center}
+ \bl{Alice says $m$}
+ \end{center}\medskip\pause
+
+ \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})
+ \begin{center}
+ \bl{Alice says $\{m\}_K$}
+ \end{center}\medskip\pause
+
+ \item Decryption of Alice's message\smallskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Encryption}
+
+ \begin{itemize}
+ \item Encryption of a message\smallskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Trusted Third Party}
+
+Simple protocol for establishing a secure connection via a mutually
+trusted 3rd party (server):
+
+\begin{center}
+\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
+Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
+Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
+Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
+Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
+\end{tabular}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Rule}
+
+ \bl{\begin{center}
+ \mbox{$\infer{\Gamma \vdash Q \;\text{says}\; F}
+ {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}$}
+ \end{center}}\bigskip\pause
+
+ \bl{$P \,\text{sends}\, Q : F \dn$}\\
+ \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $A$ sends $S$ : $\text{Connect}(A,B)$\\
+ \bl{$S \,\text{says}\, (\text{Connect}(A,B) \Rightarrow$}\\
+ \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
+ \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
+ $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ : $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}\bigskip\pause
+
+
+ \bl{$\Gamma \vdash B \,\text{says} \, m$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Public/Private Keys}
+
+ \begin{itemize}
+ \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
+ \begin{center}
+ \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+ {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
+ \Gamma \vdash K_{Bob}^{priv}}}}
+ \end{center}\bigskip\pause
+
+ \item this is {\bf not} a derived rule!
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+% \begin{itemize}
+% \item Alice calls Sam for a key to communicate with Bob
+% \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
+ % \item Alice sends the message encrypted with the key and the second key it recieved
+ % \end{itemize}\bigskip
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Sending Rule}
+
+
+ \bl{\begin{center}
+ \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
+ {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
+ \end{center}}\bigskip\pause
+
+ \bl{$P \,\text{sends}\, Q : F \dn$}\\
+ \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Trusted Third Party}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $A$ sends $S$ : $\textit{Connect}(A,B)$\\
+ \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\
+ \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge
+ \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
+ $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+ $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
+ $A$ sends $B$ : $\{m\}_{K_{AB}}$
+ \end{tabular}}
+ \end{center}\bigskip\pause
+
+
+ \bl{$\Gamma \vdash B \,\text{says} \, m$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Challenge-Response Protocol}
+
+ \begin{itemize}
+ \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip
+ \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip
+ \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip
+ \item if \bl{$E$} receives \bl{$\{N\}_K$} from \bl{$T$}, it starts engine
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Challenge-Response Protocol}
+
+ \begin{center}
+ \bl{\begin{tabular}{l}
+ $E \;\text{says}\; N$\hfill(start)\\
+ $E \;\text{sends}\; T : N$\hfill(challenge)\\
+ $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\
+ \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\
+ $T \;\text{says}\; K$\hfill(key)\\
+ $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\
+ $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\
+ \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\
+ \end{tabular}}
+ \end{center}\bigskip
+
+ \bl{$\Gamma \vdash \text{start\_engine}(T)$}?
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Exchange of a Fresh Key}
+
+\bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key
+
+ \begin{itemize}
+ \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip
+ \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$}
+ \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
+ \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}
+ \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}
+ \end{itemize}\bigskip
+
+ Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{The Attack}
+
+An intruder \bl{$I$} convinces \bl{$A$} to accept the compromised key \bl{$K^{new}_{AB}$}\medskip
+
+\begin{minipage}{1.1\textwidth}
+\begin{itemize}
+ \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$}
+ \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
+ \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause
+ \item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$}
+ \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$}
+ \item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$}
+ \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause
+ \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also
+ \end{itemize}
+ \end{minipage}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+A Man-in-the-middle attack in real life:
+
+\begin{itemize}
+\item the card only says yes or no to the terminal if the PIN is correct
+\item trick the card in thinking transaction is verified by signature
+\item trick the terminal in thinking the transaction was verified by PIN
+\end{itemize}
+
+\begin{minipage}{1.1\textwidth}
+\begin{center}
+\mbox{}\hspace{-6mm}\includegraphics[scale=0.5]{pics/chip-attack.png}
+\includegraphics[scale=0.3]{pics/chipnpinflaw.png}
+\end{center}
+\end{minipage}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Problems with EMV}
+
+\begin{itemize}
+\item it is a wrapper for many protocols
+\item specification by consensus (resulted unmanageable complexity)
+\item its specification is 700 pages in English plus 2000+ pages for testing, additionally some
+further parts are secret
+\item other attacks have been found
+
+\item one solution might be to require always online verification of the PIN with the bank
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}Problems with WEP (Wifi)\end{tabular}}
+
+\begin{itemize}
+\item a standard ratified in 1999
+\item the protocol was designed by a committee not including cryptographers
+\item it used the RC4 encryption algorithm which is a stream cipher requiring a unique nonce
+\item WEP did not allocate enough bits for the nonce
+\item for authenticating packets it used CRC checksum which can be easily broken
+\item the network password was used to directly encrypt packages (instead of a key negotiation protocol)\bigskip
+\item encryption was turned off by default
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Protocols are Difficult}
+
+\begin{itemize}
+\item even the systems designed by experts regularly fail\medskip
+\item try to make everything explicit (you need to authenticate all data you might rely on)\medskip
+\item the one who can fix a system should also be liable for the losses\medskip
+\item cryptography is often not {\bf the} answer\bigskip\bigskip
+\end{itemize}
+
+logic is one way protocols are studied in academia
+(you can use computers to search for attacks)
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Public-Key Infrastructure}
+
+\begin{itemize}
+\item the idea is to have a certificate authority (CA)
+\item you go to the CA to identify yourself
+\item CA: ``I, the CA, have verified that public key \bl{$P^{pub}_{Bob}$} belongs to Bob''\bigskip
+\item CA must be trusted by everybody
+\item What happens if CA issues a false certificate? Who pays in case of loss? (VeriSign
+explicitly limits liability to \$100.)
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+
+
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+
Binary file slides/slides01.pdf has changed
Binary file slides/slides02.pdf has changed
Binary file slides/slides03.pdf has changed
Binary file slides/slides04.pdf has changed
Binary file slides/slides05.pdf has changed
--- a/slides/slides06-zkp-old.tex Sat Sep 23 13:36:20 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,505 +0,0 @@
-\documentclass[dvipsnames,14pt,t]{beamer}
-\usepackage{../slides}
-\usepackage{../graphics}
-
-\setmonofont[Scale=.88]{Consolas}
-\newfontfamily{\consolas}{Consolas}
-
-\hfuzz=220pt
-
-% beamer stuff
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}
-\renewcommand{\slidecaption}{SEN 06, King's College London}
-
-\begin{document}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t]
-\frametitle{%
- \begin{tabular}{@ {}c@ {}}
- \\
- \LARGE Security Engineering (6)\\[-3mm]
- \end{tabular}}\bigskip\bigskip\bigskip
-
- \normalsize
- \begin{center}
- \begin{tabular}{ll}
- Email: & christian.urban at kcl.ac.uk\\
- Office: & N7.07 (North Wing, Bush House)\\
- Slides: & KEATS (also homework is there)\\
- \end{tabular}
- \end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Hashes for History}
-
-Q: What is the hash for?
-
-\begin{center}
-\includegraphics[scale=0.4]{../pics/Dismantling_Megamos_Crypto.png}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t]
-\frametitle{Checking Solutions}
-
-How can you check somebody's solution without revealing the solution?\pause\bigskip
-
-Alice and Bob solve crosswords. Alice knows the answer for 21D (folio) but doesn't
-want to tell Bob.\medskip
-
-You use an English dictionary:
-
-\begin{itemize}
-\item folio \onslide<4->{$\stackrel{1}{\rightarrow}$ individual }
- \onslide<5->{$\stackrel{2}{\rightarrow}$ human}
- \onslide<6->{$\stackrel{3}{\rightarrow}$ or \ldots}
-\only<3>{
-\begin{quote}
-``an \alert{individual} leaf of paper or parchment, either loose as one of a series or
-forming part of a bound volume, which is numbered on the recto or front side only.''
-\end{quote}}
-\only<4>{
-\begin{quote}
-``a single \alert{human} being as distinct from a group''
-\end{quote}}
-\only<5>{
-\begin{quote}
-``relating to \alert{or} characteristic of humankind''
-\end{quote}}
-\end{itemize}\bigskip\bigskip
-
-\only<7->{
-this is essentially a hash function...but Bob can only check once he has also found the solution
-}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Zero-Knowledge Proofs}
-
-Two remarkable properties of \alert{Zero-Knowledge
-Proofs}:\bigskip
-
-\begin{itemize}
-
-\item Alice only reveals the fact that she knows a secret, not
- the secret itself (meaning she can convince Bob that she
- knows the secret, but does not give it to him).\bigskip
-\item Having been convinced, Bob cannot use the evidence in
- order to convince Carol that Alice knows the secret.
-
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Interactive Protocols}
-
-Q: How to cut a cake into two equal slices?
-
-\begin{center}
-\includegraphics[scale=0.15]{../pics/cake.jpg}
-\end{center}\pause\bigskip
-
-\small
-Solves the problem of communication when both parties
-distrust each other.
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t]
-\frametitle{The Idea}
-
-\begin{center}
-\begin{tabular}{l@{\hspace{10mm}}r}
-\\[-10mm]
-\raisebox{10mm}{\large 1.} & \includegraphics[scale=0.1]{../pics/alibaba1.png}\\
-\raisebox{10mm}{\large 2.} & \includegraphics[scale=0.1]{../pics/alibaba2.png}\\
-\raisebox{10mm}{\large 3.} & \includegraphics[scale=0.1]{../pics/alibaba3.png}
-\end{tabular}
-\end{center}
-
-\begin{textblock}{7}(1,2)
-The Alibaba cave protocol:
-\end{textblock}
-
-\small
-\only<2>{
-\begin{textblock}{12}(2,13.3)
-Even if Bob has a hidden camera, a recording will not be
-convincing to anyone else (Alice and Bob could have made it
-all up).
-\end{textblock}}
-\only<3>{
-\begin{textblock}{12}(2,13.3)
-Even worse, an observer present at the experiment would not be
-convinced.
-\end{textblock}}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Applications of ZKPs}
-
-\begin{itemize}
-\item authentication, where one party wants to prove its
- identity to a second party via some secret information,
- but doesn't want the second party to learn anything
- about this secret\bigskip
-\item to enforce honest behaviour while maintaining privacy:
- the idea is to force users to prove, using a
- zero-knowledge proof, that their behaviour is correct
- according to the protocol
-\end{itemize}\bigskip
-
-\small
-digital currencies, smart cards, id cards
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Central Properties}
-
-Zero-knowledge proof protocols should satisfy:\bigskip
-
-\begin{itemize}
-\item \alert{\bf Completeness} If Alice knows the secret, Bob
- accepts Alice's ``proof'' for sure.\bigskip
-\item \alert{\bf Soundness} If Alice does not know the secret,
- Bob accepts her ``proof'' with a very small probability.
-
-\item \alert{\bf Zero-Knowledge} Even if Bob accepts
- the proof by Alice, he cannot convince anybody else.
-
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Graph Isomorphism}
-\mbox{}\\[-20mm]\mbox{}
-
-\begin{center}
-\begin{tabular}{@{}ccc}
-\raisebox{-18mm}{\includegraphics[scale=0.4]{../pics/simple.png}} &
-\raisebox{-18mm}{\includegraphics[scale=0.4]{../pics/simple-b.png}}&
-
-\footnotesize
-\begin{tabular}{rl}
-Graph A & Graph B\\
-Graph $G_1$ & Graph $G_2$\\
-a & 1\\
-b & 6\\
-c & 8\\
-d & 3\\
-g & 5\\
-h & 2\\
-i & 4\\
-j & 7\\
-\end{tabular}
-\end{tabular}
-\end{center}
-
-Finding an isomorphism between two graphs is an NP problem.
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\begin{center}
-\includegraphics[scale=0.8]{../pics/graphs.png}
-\end{center}
-
-Creating a new isomorphic graph is easy; finding an
-isomorphism is hard; checking an isomorphism is easy again
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{\Large Graph Isomorphism Protocol}
-
-Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip
-
-\begin{enumerate}
-\item Alice generates an isomorphic graph \bl{$H$} which she sends to Bob
-\item Bob asks either for an isomorphism between \bl{$G_1$} and \bl{$H$}, or
-\bl{$G_2$} and \bl{$H$}
-\item Alice and Bob repeat this procedure \bl{$n$} times
-\end{enumerate}\pause
-
-these are called commitment algorithms
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{\Large Graph Isomorphism Protocol (2)}
-
-If Alice knows the isomorphism, she can always calculate
-\bl{$\sigma$}.\bigskip
-
-If she doesn't, she can only correctly respond if Bob's choice
-of index is the same as the one she used to form \bl{$H$}. The
-probability of this happening is \bl{$\frac{1}{2}$}, so after
-\bl{$n$} rounds the probability of her always responding
-correctly is only \bl{$\frac{1}{2}^n$}.
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t]
-\frametitle{Plot of $\frac{1}{2}^n$}
-
-\begin{center}
-\begin{tikzpicture}
-\begin{axis}[
- enlargelimits=true,
- xtick={0,1,...,10},
- xmax=11,
- ymax=1.1,
- ytick={0,0.1,...,1.1},
- scaled ticks=false,
- axis lines=left,
- width=11cm,
- height=7cm]
-\addplot[blue,mark=*, mark options={fill=white}]
- coordinates {
- (0, 1) (1, 0.5) (2, 0.25) (3, 0.125)
- (4, 0.0625) (5, 0.03125) (6, 0.015625)
- (7, 0.0078125) (8, 0.00390625)
- (9, 0.001953125) (10, 0.0009765625)
- };
-\end{axis}
-\end{tikzpicture}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{\Large Graph Isomorphism Protocol (3)}
-
-Why is the GI-protocol zero-knowledge?\bigskip\pause
-
-A: We can generate a fake transcript of a conversation, which
-cannot be distinguished from a ``real'' conversation.\bigskip
-
-Anything Bob can compute using the information obtained from
-the transcript can be computed using only a forged transcript
-and therefore participation in such a communication does not
-increase Bob's capability to perform any computation.
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Non-Interactive ZKPs}
-
-This is amazing: This can all be done ``offline'':
-\bigskip
-
-Alice can publish some data that contains no data about her
-secret, but this data can be used to convince anyone of the
-secret's existence (whether Alice knows it, must be
-established my other means).
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Non-Interactive ZKPs (2)}
-
-Alice starts with knowing an isomorphism \bl{$\sigma$} between
-graphs \bl{$G_1$} and \bl{$G_2$}\medskip
-
-\begin{enumerate}
-\item Alice generates \bl{$n$} isomorphic graphs
- \bl{$H_{1..n}$} which she makes public
-\item she feeds the \bl{$H_{1..n}$} into a hashing function
- (she has no control over what the output will be)
-\item Alice takes the first \bl{$n$} bits of the output:
- whenever output is \bl{$0$}, she shows an isomorphism
- with \bl{$G_1$} ; for \bl{$1$} she shows an isomorphism
- with \bl{$G_2$}
-\end{enumerate}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Problems of ZKPs}
-
-\begin{itemize}
-\item ``grand chess master problem''\\ (person in the
- middle again)\bigskip
-
-\item Alice can have multiple identities; once she committed a
- fraud with one, she stops using one
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Other Methods for ZKPs}
-
-Essentially every NP-problem can be used for ZKPs
-
-\begin{itemize}
-\item modular logarithms: Alice chooses public \bl{$A$}, \bl{$B$}, \bl{$p$}; and private \bl{$x$}
-
-\begin{center}
-\bl{$A^x \equiv B\; mod\; p$}
-\end{center}
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Commitment Stage}
-
-\begin{enumerate}
-\item Alice generates \bl{$z$} random numbers \bl{$r_1$}, ..., \bl{$r_z$}, all less than \bl{$p - 1$}.
-\item Alice sends Bob for all \bl{$1..z$}
-\begin{center}
-\bl{$h_i = A^{r_i} \;mod\; p$}
-\end{center}
-\item Bob generates random bits \bl{$b_1$}, ..., \bl{$b_z$} by flipping a coin
-\item For each bit \bl{$b_i$}, Alice sends Bob an \bl{$s_i$} where
-
-\begin{center}
-\begin{tabular}{ll}
-\bl{$b_i = 0$}: & \bl{$s_i = r_i$}\\
-\bl{$b_i = 1$}: & \bl{$s_i = (r_i - r_j) \;mod\; (p -1)$}\\
-\end{tabular}
-\end{center}
-where \bl{$r_j$} is the lowest \bl{$j$} where \bl{$b_j = 1$}
-
-\end{enumerate}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Confirmation Stage}
-
-\begin{enumerate}
-\item For each \bl{$b_i$} Bob checks whether \bl{$s_i$} conforms to the protocol
-
-\begin{center}
-\begin{tabular}{ll}
-\bl{$b_i = 0$}: & \bl{$A^{s_i} \equiv h_i\;mod\;p$}\\
-\bl{$b_i = 1$}: & \bl{$A^{s_i} \equiv h_i * h_j^{-1} \;mod\; p$}\\
-\end{tabular}
-\end{center}\bigskip
-
-Bob was sent
-
-\begin{center}
-\bl{$r_j - r_j$}, \bl{$r_m - r_j$}, \ldots, \bl{$r_p - r_j \;mod \;p - 1$}
-\end{center}
-
-where the corresponding bits were
-\bl{$1$}; Bob does not know \bl{$r_j$}, he does not know any \bl{$r_i$} where the bit was \bl{$1$}
-\end{enumerate}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Proving Stage}
-
-\begin{enumerate}
-\item Alice proves she knows \bl{$x$}, the discrete log of \bl{$B$}\\
-she sends
-
-\begin{center}
-\bl{$s_{z+1} = (x - r_j)$}
-\end{center}
-
-\item Bob confirms
-
-\begin{center}
-\bl{$A^{s_{z+1}} \equiv B * h_j^{-1} \;mod \; p$}
-\end{center}
-\end{enumerate}\bigskip\pause
-
-In order to cheat, Alice has to guess all bits in advance. She
-has only \bl{$\frac{1}{2}^z$} chance of doing so.\bigskip\\
-
-\small\hspace{7mm}
-\textcolor{gray}{(explanation $\rightarrow$ \url{http://goo.gl/irL9GK})}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Take Home Points}
-
-\begin{itemize}
-\item this is pretty old work (in theory); seems
- little used in practice (surprising)\bigskip
-
-\item for use in privacy, the incentives are
- not yet right\bigskip
-
-\item most likely applied with digital cash
- (Bitcoins are not yet good enough, Zerocoins)
-
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/slides06-zkp-old.tex-bak Sat Sep 23 14:19:09 2017 +0100
@@ -0,0 +1,505 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{../slides}
+\usepackage{../graphics}
+
+\setmonofont[Scale=.88]{Consolas}
+\newfontfamily{\consolas}{Consolas}
+
+\hfuzz=220pt
+
+% beamer stuff
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+\renewcommand{\slidecaption}{SEN 06, King's College London}
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\
+ \LARGE Security Engineering (6)\\[-3mm]
+ \end{tabular}}\bigskip\bigskip\bigskip
+
+ \normalsize
+ \begin{center}
+ \begin{tabular}{ll}
+ Email: & christian.urban at kcl.ac.uk\\
+ Office: & N7.07 (North Wing, Bush House)\\
+ Slides: & KEATS (also homework is there)\\
+ \end{tabular}
+ \end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Hashes for History}
+
+Q: What is the hash for?
+
+\begin{center}
+\includegraphics[scale=0.4]{../pics/Dismantling_Megamos_Crypto.png}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{Checking Solutions}
+
+How can you check somebody's solution without revealing the solution?\pause\bigskip
+
+Alice and Bob solve crosswords. Alice knows the answer for 21D (folio) but doesn't
+want to tell Bob.\medskip
+
+You use an English dictionary:
+
+\begin{itemize}
+\item folio \onslide<4->{$\stackrel{1}{\rightarrow}$ individual }
+ \onslide<5->{$\stackrel{2}{\rightarrow}$ human}
+ \onslide<6->{$\stackrel{3}{\rightarrow}$ or \ldots}
+\only<3>{
+\begin{quote}
+``an \alert{individual} leaf of paper or parchment, either loose as one of a series or
+forming part of a bound volume, which is numbered on the recto or front side only.''
+\end{quote}}
+\only<4>{
+\begin{quote}
+``a single \alert{human} being as distinct from a group''
+\end{quote}}
+\only<5>{
+\begin{quote}
+``relating to \alert{or} characteristic of humankind''
+\end{quote}}
+\end{itemize}\bigskip\bigskip
+
+\only<7->{
+this is essentially a hash function...but Bob can only check once he has also found the solution
+}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Zero-Knowledge Proofs}
+
+Two remarkable properties of \alert{Zero-Knowledge
+Proofs}:\bigskip
+
+\begin{itemize}
+
+\item Alice only reveals the fact that she knows a secret, not
+ the secret itself (meaning she can convince Bob that she
+ knows the secret, but does not give it to him).\bigskip
+\item Having been convinced, Bob cannot use the evidence in
+ order to convince Carol that Alice knows the secret.
+
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Interactive Protocols}
+
+Q: How to cut a cake into two equal slices?
+
+\begin{center}
+\includegraphics[scale=0.15]{../pics/cake.jpg}
+\end{center}\pause\bigskip
+
+\small
+Solves the problem of communication when both parties
+distrust each other.
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{The Idea}
+
+\begin{center}
+\begin{tabular}{l@{\hspace{10mm}}r}
+\\[-10mm]
+\raisebox{10mm}{\large 1.} & \includegraphics[scale=0.1]{../pics/alibaba1.png}\\
+\raisebox{10mm}{\large 2.} & \includegraphics[scale=0.1]{../pics/alibaba2.png}\\
+\raisebox{10mm}{\large 3.} & \includegraphics[scale=0.1]{../pics/alibaba3.png}
+\end{tabular}
+\end{center}
+
+\begin{textblock}{7}(1,2)
+The Alibaba cave protocol:
+\end{textblock}
+
+\small
+\only<2>{
+\begin{textblock}{12}(2,13.3)
+Even if Bob has a hidden camera, a recording will not be
+convincing to anyone else (Alice and Bob could have made it
+all up).
+\end{textblock}}
+\only<3>{
+\begin{textblock}{12}(2,13.3)
+Even worse, an observer present at the experiment would not be
+convinced.
+\end{textblock}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Applications of ZKPs}
+
+\begin{itemize}
+\item authentication, where one party wants to prove its
+ identity to a second party via some secret information,
+ but doesn't want the second party to learn anything
+ about this secret\bigskip
+\item to enforce honest behaviour while maintaining privacy:
+ the idea is to force users to prove, using a
+ zero-knowledge proof, that their behaviour is correct
+ according to the protocol
+\end{itemize}\bigskip
+
+\small
+digital currencies, smart cards, id cards
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Central Properties}
+
+Zero-knowledge proof protocols should satisfy:\bigskip
+
+\begin{itemize}
+\item \alert{\bf Completeness} If Alice knows the secret, Bob
+ accepts Alice's ``proof'' for sure.\bigskip
+\item \alert{\bf Soundness} If Alice does not know the secret,
+ Bob accepts her ``proof'' with a very small probability.
+
+\item \alert{\bf Zero-Knowledge} Even if Bob accepts
+ the proof by Alice, he cannot convince anybody else.
+
+\end{itemize}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Graph Isomorphism}
+\mbox{}\\[-20mm]\mbox{}
+
+\begin{center}
+\begin{tabular}{@{}ccc}
+\raisebox{-18mm}{\includegraphics[scale=0.4]{../pics/simple.png}} &
+\raisebox{-18mm}{\includegraphics[scale=0.4]{../pics/simple-b.png}}&
+
+\footnotesize
+\begin{tabular}{rl}
+Graph A & Graph B\\
+Graph $G_1$ & Graph $G_2$\\
+a & 1\\
+b & 6\\
+c & 8\\
+d & 3\\
+g & 5\\
+h & 2\\
+i & 4\\
+j & 7\\
+\end{tabular}
+\end{tabular}
+\end{center}
+
+Finding an isomorphism between two graphs is an NP problem.
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\begin{center}
+\includegraphics[scale=0.8]{../pics/graphs.png}
+\end{center}
+
+Creating a new isomorphic graph is easy; finding an
+isomorphism is hard; checking an isomorphism is easy again
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Graph Isomorphism Protocol}
+
+Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip
+
+\begin{enumerate}
+\item Alice generates an isomorphic graph \bl{$H$} which she sends to Bob
+\item Bob asks either for an isomorphism between \bl{$G_1$} and \bl{$H$}, or
+\bl{$G_2$} and \bl{$H$}
+\item Alice and Bob repeat this procedure \bl{$n$} times
+\end{enumerate}\pause
+
+these are called commitment algorithms
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Graph Isomorphism Protocol (2)}
+
+If Alice knows the isomorphism, she can always calculate
+\bl{$\sigma$}.\bigskip
+
+If she doesn't, she can only correctly respond if Bob's choice
+of index is the same as the one she used to form \bl{$H$}. The
+probability of this happening is \bl{$\frac{1}{2}$}, so after
+\bl{$n$} rounds the probability of her always responding
+correctly is only \bl{$\frac{1}{2}^n$}.
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{Plot of $\frac{1}{2}^n$}
+
+\begin{center}
+\begin{tikzpicture}
+\begin{axis}[
+ enlargelimits=true,
+ xtick={0,1,...,10},
+ xmax=11,
+ ymax=1.1,
+ ytick={0,0.1,...,1.1},
+ scaled ticks=false,
+ axis lines=left,
+ width=11cm,
+ height=7cm]
+\addplot[blue,mark=*, mark options={fill=white}]
+ coordinates {
+ (0, 1) (1, 0.5) (2, 0.25) (3, 0.125)
+ (4, 0.0625) (5, 0.03125) (6, 0.015625)
+ (7, 0.0078125) (8, 0.00390625)
+ (9, 0.001953125) (10, 0.0009765625)
+ };
+\end{axis}
+\end{tikzpicture}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Graph Isomorphism Protocol (3)}
+
+Why is the GI-protocol zero-knowledge?\bigskip\pause
+
+A: We can generate a fake transcript of a conversation, which
+cannot be distinguished from a ``real'' conversation.\bigskip
+
+Anything Bob can compute using the information obtained from
+the transcript can be computed using only a forged transcript
+and therefore participation in such a communication does not
+increase Bob's capability to perform any computation.
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Non-Interactive ZKPs}
+
+This is amazing: This can all be done ``offline'':
+\bigskip
+
+Alice can publish some data that contains no data about her
+secret, but this data can be used to convince anyone of the
+secret's existence (whether Alice knows it, must be
+established my other means).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Non-Interactive ZKPs (2)}
+
+Alice starts with knowing an isomorphism \bl{$\sigma$} between
+graphs \bl{$G_1$} and \bl{$G_2$}\medskip
+
+\begin{enumerate}
+\item Alice generates \bl{$n$} isomorphic graphs
+ \bl{$H_{1..n}$} which she makes public
+\item she feeds the \bl{$H_{1..n}$} into a hashing function
+ (she has no control over what the output will be)
+\item Alice takes the first \bl{$n$} bits of the output:
+ whenever output is \bl{$0$}, she shows an isomorphism
+ with \bl{$G_1$} ; for \bl{$1$} she shows an isomorphism
+ with \bl{$G_2$}
+\end{enumerate}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Problems of ZKPs}
+
+\begin{itemize}
+\item ``grand chess master problem''\\ (person in the
+ middle again)\bigskip
+
+\item Alice can have multiple identities; once she committed a
+ fraud with one, she stops using one
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Other Methods for ZKPs}
+
+Essentially every NP-problem can be used for ZKPs
+
+\begin{itemize}
+\item modular logarithms: Alice chooses public \bl{$A$}, \bl{$B$}, \bl{$p$}; and private \bl{$x$}
+
+\begin{center}
+\bl{$A^x \equiv B\; mod\; p$}
+\end{center}
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Commitment Stage}
+
+\begin{enumerate}
+\item Alice generates \bl{$z$} random numbers \bl{$r_1$}, ..., \bl{$r_z$}, all less than \bl{$p - 1$}.
+\item Alice sends Bob for all \bl{$1..z$}
+\begin{center}
+\bl{$h_i = A^{r_i} \;mod\; p$}
+\end{center}
+\item Bob generates random bits \bl{$b_1$}, ..., \bl{$b_z$} by flipping a coin
+\item For each bit \bl{$b_i$}, Alice sends Bob an \bl{$s_i$} where
+
+\begin{center}
+\begin{tabular}{ll}
+\bl{$b_i = 0$}: & \bl{$s_i = r_i$}\\
+\bl{$b_i = 1$}: & \bl{$s_i = (r_i - r_j) \;mod\; (p -1)$}\\
+\end{tabular}
+\end{center}
+where \bl{$r_j$} is the lowest \bl{$j$} where \bl{$b_j = 1$}
+
+\end{enumerate}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Confirmation Stage}
+
+\begin{enumerate}
+\item For each \bl{$b_i$} Bob checks whether \bl{$s_i$} conforms to the protocol
+
+\begin{center}
+\begin{tabular}{ll}
+\bl{$b_i = 0$}: & \bl{$A^{s_i} \equiv h_i\;mod\;p$}\\
+\bl{$b_i = 1$}: & \bl{$A^{s_i} \equiv h_i * h_j^{-1} \;mod\; p$}\\
+\end{tabular}
+\end{center}\bigskip
+
+Bob was sent
+
+\begin{center}
+\bl{$r_j - r_j$}, \bl{$r_m - r_j$}, \ldots, \bl{$r_p - r_j \;mod \;p - 1$}
+\end{center}
+
+where the corresponding bits were
+\bl{$1$}; Bob does not know \bl{$r_j$}, he does not know any \bl{$r_i$} where the bit was \bl{$1$}
+\end{enumerate}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Proving Stage}
+
+\begin{enumerate}
+\item Alice proves she knows \bl{$x$}, the discrete log of \bl{$B$}\\
+she sends
+
+\begin{center}
+\bl{$s_{z+1} = (x - r_j)$}
+\end{center}
+
+\item Bob confirms
+
+\begin{center}
+\bl{$A^{s_{z+1}} \equiv B * h_j^{-1} \;mod \; p$}
+\end{center}
+\end{enumerate}\bigskip\pause
+
+In order to cheat, Alice has to guess all bits in advance. She
+has only \bl{$\frac{1}{2}^z$} chance of doing so.\bigskip\\
+
+\small\hspace{7mm}
+\textcolor{gray}{(explanation $\rightarrow$ \url{http://goo.gl/irL9GK})}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Take Home Points}
+
+\begin{itemize}
+\item this is pretty old work (in theory); seems
+ little used in practice (surprising)\bigskip
+
+\item for use in privacy, the incentives are
+ not yet right\bigskip
+
+\item most likely applied with digital cash
+ (Bitcoins are not yet good enough, Zerocoins)
+
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+
Binary file slides/slides06.pdf has changed
Binary file slides/slides07.pdf has changed
Binary file slides/slides08.pdf has changed
--- a/slides/slides08.tex Sat Sep 23 13:36:20 2017 +0100
+++ b/slides/slides08.tex Sat Sep 23 14:19:09 2017 +0100
@@ -906,10 +906,11 @@
% \begin{center}\small
% \begin{tabular}{lp{7cm}}
% Time Allowed & Two hours\\
-% Rubric & ANSWER ALL QUESTIONS\\
+% Rubric & ANSWER ALL QUESTIONS\\
% Calculators & Calculators are not permitted\\
% Notes & Books, notes or other written material
-% may not be brought into this examination\\
\end{tabular}
+% may not be brought into this examination\\
+% \end{tabular}
% \end{center}
%\end{itemize}
%
