# HG changeset patch # User Christian Urban # Date 1506172749 -3600 # Node ID bd25d9f9d9dc6d519acfd3026e45a528a61cb5ec # Parent 06f91010fe1e6e269a44c175c7f6bb9c8ce09f9d updated diff -r 06f91010fe1e -r bd25d9f9d9dc coursework/cw01.pdf Binary file coursework/cw01.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc coursework/cw01.tex --- /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: diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho01.pdf Binary file handouts/ho01.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho02.pdf Binary file handouts/ho02.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho03.pdf Binary file handouts/ho03.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho04.pdf Binary file handouts/ho04.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho05.pdf Binary file handouts/ho05.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho06.pdf Binary file handouts/ho06.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho07.pdf Binary file handouts/ho07.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho08.pdf Binary file handouts/ho08.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc handouts/ho09.pdf Binary file handouts/ho09.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw01.pdf Binary file hws/hw01.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw02.pdf Binary file hws/hw02.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw03.pdf Binary file hws/hw03.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw04.pdf Binary file hws/hw04.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw05.pdf Binary file hws/hw05.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw06.pdf Binary file hws/hw06.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw07.pdf Binary file hws/hw07.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw08.pdf Binary file hws/hw08.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc hws/hw10.pdf Binary file hws/hw10.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/Dismantling_Megamos_Crypto.png Binary file pics/Dismantling_Megamos_Crypto.png has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/airbus.jpg Binary file pics/airbus.jpg has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/firefox1.png Binary file pics/firefox1.png has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/flight.jpg Binary file pics/flight.jpg has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/newyorktaxi.jpg Binary file pics/newyorktaxi.jpg has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/safari1.png Binary file pics/safari1.png has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/simple-b.png Binary file pics/simple-b.png has changed diff -r 06f91010fe1e -r bd25d9f9d9dc pics/simple.png Binary file pics/simple.png has changed diff -r 06f91010fe1e -r bd25d9f9d9dc progs/inter.scala --- /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()) +} diff -r 06f91010fe1e -r bd25d9f9d9dc slides/bak-slides06.tex --- 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{ -\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{ - \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{ -\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{ -\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{ -\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{ - \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{ -\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{ -\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{ -\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{ -\begin{frame}[c] -\frametitle{Sudoku} - -\begin{tikzpicture}[scale=.5] - \begin{scope} - \draw (0, 0) grid (9, 9); - \draw[very thick, scale=3] (0, 0) grid (3, 3); - - \setcounter{row}{1} - \setrow { }{2}{ } {5}{ }{1} { }{9}{ } - \setrow {8}{ }{ } {2}{ }{3} { }{ }{6} - \setrow { }{3}{ } { }{6}{ } { }{7}{ } - - \setrow { }{ }{1} { }{ }{ } {6}{ }{ } - \setrow {5}{4}{ } { }{ }{ } { }{1}{9} - \setrow { }{ }{2} { }{ }{ } {7}{ }{ } - - \setrow { }{9}{ } { }{3}{ } { }{8}{ } - \setrow {2}{ }{ } {8}{ }{4} { }{ }{7} - \setrow { }{1}{ } {9}{ }{7} { }{6}{ } - - \fill[red, fill opacity=0.4] (4,0) rectangle (5,9); - \fill[red, fill opacity=0.4] (0,5) rectangle (9,6); - \fill[red!50, fill opacity=0.4] (3,3) rectangle (4,5); - \fill[red!50, fill opacity=0.4] (5,3) rectangle (6,5); - \node[gray, anchor=center] at (4.5, -0.5) {columns}; - \node[gray, rotate=90, anchor=center] at (-0.6, 4.5, -0.5) {rows}; - \node[gray, anchor=center] at (4.5, 4.5) {box}; - \end{scope} - \end{tikzpicture} - -\small -\begin{textblock}{7}(9,3) -\begin{enumerate} -\item {\bf Row-Column:} each cell, must contain exactly one number -\item {\bf Row-Number:} each row must contain each number exactly once -\item {\bf Column-Number:} each column must contain each number exactly once -\item {\bf Box-Number:} each box must contain each number exactly once -\end{enumerate} -\end{textblock} - - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Solving Sudokus} - -\begin{tikzpicture}[scale=.5] - \begin{scope} - \draw (0, 0) grid (9, 9); - \draw[very thick, scale=3] (0, 0) grid (3, 3); - - \setcounter{row}{1} - \setrow { }{ }{ } {7}{ }{ } { }{5}{8} - \setrow {}{5}{6} {2}{1}{8} {7}{9}{3} - \setrow { }{ }{ } { }{ }{ } {1}{ }{ } - - \setrow { }{ }{ } { }{ }{ } { }{8}{1} - \setrow { }{ }{ } {3}{7}{6} { }{ }{ } - \setrow {9}{6}{ } { }{ }{ } { }{ }{ } - - \setrow { }{ }{5} { }{ }{ } { }{ }{ } - \setrow { }{ }{4} { }{2}{1} {8}{3}{ } - \setrow {8}{7}{ } { }{ }{3} { }{ }{ } - - \fill[red, fill opacity=0.4] (0,7) rectangle (1,8); - - \end{scope} - \end{tikzpicture} - -\small -\begin{textblock}{6}(9,6) -{\bf single position rules}\\ -\begin{center} -\bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}} -\end{center} - -\onslide<2->{ -\begin{center} -\bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one column}}}\medskip\\ -\bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one box}}} -\end{center}} -\end{textblock} - - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Solving Sudokus} - -\begin{tikzpicture}[scale=.5] - \begin{scope} - \draw (0, 0) grid (9, 9); - \draw[very thick, scale=3] (0, 0) grid (3, 3); - - \setcounter{row}{1} - \setrow { }{ }{ } {7}{ }{ } {\alert{\footnotesize 2}}{5}{8} - \setrow {}{5}{6} {2}{1}{8} {7}{9}{3} - \setrow { }{ }{ } { }{ }{ } {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}} - - \setrow { }{ }{ } { }{ }{ } { }{8}{1} - \setrow { }{ }{ } {3}{7}{6} { }{ }{ } - \setrow {9}{6}{ } { }{ }{ } { }{ }{ } - - \setrow { }{ }{5} { }{ }{ } { }{ }{ } - \setrow { }{ }{4} { }{2}{1} {8}{3}{ } - \setrow {8}{7}{ } { }{ }{3} { }{ }{ } - - \end{scope} - \end{tikzpicture} - -\small -\begin{textblock}{6}(7.5,6) -{\bf candidate rules}\\ -\begin{center} -\bl{\infer{x\;\text{candidate in empty positions}}{X - \{x\}\;\text{in one box} & X \subseteq \{1..9\}}} -\end{center} -\end{textblock} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Solving Sudokus} - -\begin{tikzpicture}[scale=.5] - \begin{scope} - \draw (0, 0) grid (9, 9); - \draw[very thick, scale=3] (0, 0) grid (3, 3); - - \setcounter{row}{1} - \setrow { }{ }{ } {7}{ }{ } {\alert{\footnotesize 2}}{5}{8} - \setrow {\alert{4}}{5}{6} {2}{1}{8} {7}{9}{3} - \setrow { }{ }{ } { }{ }{ } {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}} - - \setrow { }{ }{ } { }{ }{ } { }{8}{1} - \setrow { }{ }{ } {3}{7}{6} { }{ }{ } - \setrow {9}{6}{ } { }{ }{ } { }{ }{ } - - \setrow { }{ }{5} { }{ }{ } { }{ }{ } - \setrow { }{ }{4} { }{2}{1} {8}{3}{ } - \setrow {8}{7}{ } { }{ }{3} { }{ }{ } - - \end{scope} - \end{tikzpicture} - -\small -\begin{textblock}{6}(7.5,6) -\begin{center} -\bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}\bigskip\\ -\bl{\infer{2\;\text{candidate in empty positions}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}} -\end{center} -\end{textblock} - - -\begin{textblock}{3}(13.5,6.8) - \begin{tikzpicture} - \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};} - \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};} - \end{tikzpicture} -\end{textblock} - -\begin{textblock}{3}(14.5,9.3) - \begin{tikzpicture} - \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};} - \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};} - \end{tikzpicture} -\end{textblock} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{Solving Sudokus} - -\begin{tikzpicture}[scale=.5] - \begin{scope} - \draw (0, 0) grid (9, 9); - \draw[very thick, scale=3] (0, 0) grid (3, 3); - - \setcounter{row}{1} - \setrow { }{ }{ } {7}{ }{ } { }{5}{8} - \setrow { }{5}{6} {2}{1}{8} {7}{9}{3} - \setrow { }{ }{ } { }{ }{ } {1}{ }{ } - - \setrow { }{ }{ } { }{ }{ } { }{8}{1} - \setrow { }{ }{ } {3}{7}{6} { }{ }{ } - \setrow {9}{6}{ } { }{ }{ } { }{ }{ \alert{2}} - - \setrow { }{ }{5} { }{ }{ } { }{ }{ } - \setrow { }{ }{4} { }{2}{1} {8}{3}{ } - \setrow {8}{7}{ } { }{ }{3} { }{ }{ } - - \end{scope} - \end{tikzpicture} - -\small -\begin{textblock}{6}(7.5,6) -\begin{center} -\bl{\infer{2\;\text{candidate}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}} -\end{center} -\end{textblock} - -\begin{textblock}{3}(14.5,8.3) - \begin{tikzpicture} - \onslide<1>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};} - \end{tikzpicture} -\end{textblock} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{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{ -\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{ -\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{ -\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{ -\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{ -\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{ -\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{ -\begin{frame}[c] - -\begin{center} -\Large -\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} -\end{center} - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\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{ -\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{ -\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{ - \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{ -\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{ -\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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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: - diff -r 06f91010fe1e -r bd25d9f9d9dc slides/bak-slides06.tex-bak --- /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{ +\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{ + \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{ +\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{ +\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{ +\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{ + \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{ +\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{ +\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{ +\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{ +\begin{frame}[c] +\frametitle{Sudoku} + +\begin{tikzpicture}[scale=.5] + \begin{scope} + \draw (0, 0) grid (9, 9); + \draw[very thick, scale=3] (0, 0) grid (3, 3); + + \setcounter{row}{1} + \setrow { }{2}{ } {5}{ }{1} { }{9}{ } + \setrow {8}{ }{ } {2}{ }{3} { }{ }{6} + \setrow { }{3}{ } { }{6}{ } { }{7}{ } + + \setrow { }{ }{1} { }{ }{ } {6}{ }{ } + \setrow {5}{4}{ } { }{ }{ } { }{1}{9} + \setrow { }{ }{2} { }{ }{ } {7}{ }{ } + + \setrow { }{9}{ } { }{3}{ } { }{8}{ } + \setrow {2}{ }{ } {8}{ }{4} { }{ }{7} + \setrow { }{1}{ } {9}{ }{7} { }{6}{ } + + \fill[red, fill opacity=0.4] (4,0) rectangle (5,9); + \fill[red, fill opacity=0.4] (0,5) rectangle (9,6); + \fill[red!50, fill opacity=0.4] (3,3) rectangle (4,5); + \fill[red!50, fill opacity=0.4] (5,3) rectangle (6,5); + \node[gray, anchor=center] at (4.5, -0.5) {columns}; + \node[gray, rotate=90, anchor=center] at (-0.6, 4.5, -0.5) {rows}; + \node[gray, anchor=center] at (4.5, 4.5) {box}; + \end{scope} + \end{tikzpicture} + +\small +\begin{textblock}{7}(9,3) +\begin{enumerate} +\item {\bf Row-Column:} each cell, must contain exactly one number +\item {\bf Row-Number:} each row must contain each number exactly once +\item {\bf Column-Number:} each column must contain each number exactly once +\item {\bf Box-Number:} each box must contain each number exactly once +\end{enumerate} +\end{textblock} + + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Solving Sudokus} + +\begin{tikzpicture}[scale=.5] + \begin{scope} + \draw (0, 0) grid (9, 9); + \draw[very thick, scale=3] (0, 0) grid (3, 3); + + \setcounter{row}{1} + \setrow { }{ }{ } {7}{ }{ } { }{5}{8} + \setrow {}{5}{6} {2}{1}{8} {7}{9}{3} + \setrow { }{ }{ } { }{ }{ } {1}{ }{ } + + \setrow { }{ }{ } { }{ }{ } { }{8}{1} + \setrow { }{ }{ } {3}{7}{6} { }{ }{ } + \setrow {9}{6}{ } { }{ }{ } { }{ }{ } + + \setrow { }{ }{5} { }{ }{ } { }{ }{ } + \setrow { }{ }{4} { }{2}{1} {8}{3}{ } + \setrow {8}{7}{ } { }{ }{3} { }{ }{ } + + \fill[red, fill opacity=0.4] (0,7) rectangle (1,8); + + \end{scope} + \end{tikzpicture} + +\small +\begin{textblock}{6}(9,6) +{\bf single position rules}\\ +\begin{center} +\bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}} +\end{center} + +\onslide<2->{ +\begin{center} +\bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one column}}}\medskip\\ +\bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one box}}} +\end{center}} +\end{textblock} + + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Solving Sudokus} + +\begin{tikzpicture}[scale=.5] + \begin{scope} + \draw (0, 0) grid (9, 9); + \draw[very thick, scale=3] (0, 0) grid (3, 3); + + \setcounter{row}{1} + \setrow { }{ }{ } {7}{ }{ } {\alert{\footnotesize 2}}{5}{8} + \setrow {}{5}{6} {2}{1}{8} {7}{9}{3} + \setrow { }{ }{ } { }{ }{ } {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}} + + \setrow { }{ }{ } { }{ }{ } { }{8}{1} + \setrow { }{ }{ } {3}{7}{6} { }{ }{ } + \setrow {9}{6}{ } { }{ }{ } { }{ }{ } + + \setrow { }{ }{5} { }{ }{ } { }{ }{ } + \setrow { }{ }{4} { }{2}{1} {8}{3}{ } + \setrow {8}{7}{ } { }{ }{3} { }{ }{ } + + \end{scope} + \end{tikzpicture} + +\small +\begin{textblock}{6}(7.5,6) +{\bf candidate rules}\\ +\begin{center} +\bl{\infer{x\;\text{candidate in empty positions}}{X - \{x\}\;\text{in one box} & X \subseteq \{1..9\}}} +\end{center} +\end{textblock} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Solving Sudokus} + +\begin{tikzpicture}[scale=.5] + \begin{scope} + \draw (0, 0) grid (9, 9); + \draw[very thick, scale=3] (0, 0) grid (3, 3); + + \setcounter{row}{1} + \setrow { }{ }{ } {7}{ }{ } {\alert{\footnotesize 2}}{5}{8} + \setrow {\alert{4}}{5}{6} {2}{1}{8} {7}{9}{3} + \setrow { }{ }{ } { }{ }{ } {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}} + + \setrow { }{ }{ } { }{ }{ } { }{8}{1} + \setrow { }{ }{ } {3}{7}{6} { }{ }{ } + \setrow {9}{6}{ } { }{ }{ } { }{ }{ } + + \setrow { }{ }{5} { }{ }{ } { }{ }{ } + \setrow { }{ }{4} { }{2}{1} {8}{3}{ } + \setrow {8}{7}{ } { }{ }{3} { }{ }{ } + + \end{scope} + \end{tikzpicture} + +\small +\begin{textblock}{6}(7.5,6) +\begin{center} +\bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}\bigskip\\ +\bl{\infer{2\;\text{candidate in empty positions}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}} +\end{center} +\end{textblock} + + +\begin{textblock}{3}(13.5,6.8) + \begin{tikzpicture} + \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};} + \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};} + \end{tikzpicture} +\end{textblock} + +\begin{textblock}{3}(14.5,9.3) + \begin{tikzpicture} + \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};} + \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};} + \end{tikzpicture} +\end{textblock} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Solving Sudokus} + +\begin{tikzpicture}[scale=.5] + \begin{scope} + \draw (0, 0) grid (9, 9); + \draw[very thick, scale=3] (0, 0) grid (3, 3); + + \setcounter{row}{1} + \setrow { }{ }{ } {7}{ }{ } { }{5}{8} + \setrow { }{5}{6} {2}{1}{8} {7}{9}{3} + \setrow { }{ }{ } { }{ }{ } {1}{ }{ } + + \setrow { }{ }{ } { }{ }{ } { }{8}{1} + \setrow { }{ }{ } {3}{7}{6} { }{ }{ } + \setrow {9}{6}{ } { }{ }{ } { }{ }{ \alert{2}} + + \setrow { }{ }{5} { }{ }{ } { }{ }{ } + \setrow { }{ }{4} { }{2}{1} {8}{3}{ } + \setrow {8}{7}{ } { }{ }{3} { }{ }{ } + + \end{scope} + \end{tikzpicture} + +\small +\begin{textblock}{6}(7.5,6) +\begin{center} +\bl{\infer{2\;\text{candidate}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}} +\end{center} +\end{textblock} + +\begin{textblock}{3}(14.5,8.3) + \begin{tikzpicture} + \onslide<1>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};} + \end{tikzpicture} +\end{textblock} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{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{ +\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{ +\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{ +\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{ +\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{ +\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{ +\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{ +\begin{frame}[c] + +\begin{center} +\Large +\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\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{ +\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{ +\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{ + \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{ +\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{ +\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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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: + diff -r 06f91010fe1e -r bd25d9f9d9dc slides/bak-slides07.tex --- 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{ -\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{ - \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{ -\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{ -\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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ -\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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ - \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{ -\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{ -\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{ -\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{ -\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{ -\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: - diff -r 06f91010fe1e -r bd25d9f9d9dc slides/bak-slides07.tex-bak --- /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{ +\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{ + \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{ +\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{ +\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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ +\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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ +\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{ +\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{ +\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{ +\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{ +\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: + diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides01.pdf Binary file slides/slides01.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides02.pdf Binary file slides/slides02.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides03.pdf Binary file slides/slides03.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides04.pdf Binary file slides/slides04.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides05.pdf Binary file slides/slides05.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides06-zkp-old.tex --- 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{ -\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{ -\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{ -\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{ -\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: - diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides06-zkp-old.tex-bak --- /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{ +\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{ +\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{ +\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{ +\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: + diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides06.pdf Binary file slides/slides06.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides07.pdf Binary file slides/slides07.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides08.pdf Binary file slides/slides08.pdf has changed diff -r 06f91010fe1e -r bd25d9f9d9dc slides/slides08.tex --- 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} %