# HG changeset patch # User Christian Urban # Date 1415020560 0 # Node ID d6dc6f0e355608467501537f11a94c628a86bb0f # Parent d7109c6e721d87d093a0a4ab08b5fa23b0bbbea2 updated diff -r d7109c6e721d -r d6dc6f0e3556 slides/slides06-bak.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/slides06-bak.tex Mon Nov 03 13:16:00 2014 +0000 @@ -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: & S1.27 (1st floor Strand Building)\\ + 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 d7109c6e721d -r d6dc6f0e3556 slides/slides06.pdf Binary file slides/slides06.pdf has changed diff -r d7109c6e721d -r d6dc6f0e3556 slides/slides06.tex --- a/slides/slides06.tex Mon Nov 03 03:22:41 2014 +0000 +++ b/slides/slides06.tex Mon Nov 03 13:16:00 2014 +0000 @@ -1,135 +1,28 @@ \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 +\usepackage{../slides} +\usepackage{../graphics} -\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]""" -} +\setmonofont[Scale=.88]{Consolas} +\newfontfamily{\consolas}{Consolas} -\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 +\hfuzz=220pt % beamer stuff -\renewcommand{\slidecaption}{APP 06, King's College London, 12 November 2013} +\newcommand{\bl}[1]{\textcolor{blue}{#1}} +\renewcommand{\slidecaption}{APP 06, King's College London} -\newcommand{\bl}[1]{\textcolor{blue}{#1}} \begin{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}<1>[t] +\begin{frame}[t] \frametitle{% \begin{tabular}{@ {}c@ {}} \\ \LARGE Access Control and \\[-3mm] - \LARGE Privacy Policies (6)\\[-6mm] + \LARGE Privacy Policies (9)\\[-6mm] \end{tabular}}\bigskip\bigskip\bigskip - %\begin{center} - %\includegraphics[scale=1.3]{pics/barrier.jpg} - %\end{center} - -\normalsize + \normalsize \begin{center} \begin{tabular}{ll} Email: & christian.urban at kcl.ac.uk\\ @@ -138,518 +31,46 @@ \end{tabular} \end{center} - -\end{frame}} +\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{frame}[t] +\frametitle{Checking Solutions} -\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}{ } +How can you check somebody's solution without revealing the solution?\pause\bigskip - \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}{ }{ } +Alice and Bob solve crosswords. Alice knows the answer for 21D (folio) but doesn't +want to tell Bob.\medskip - \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}} +You use an English dictionary: - \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{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 -\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} - +\only<7->{ +this is essentially a hash function...but Bob can only check once he has also found the solution +} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -657,122 +78,48 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] -\frametitle{Example Proof} - -\begin{tabular}{@{\hspace{-6mm}}l} -\begin{minipage}{1.1\textwidth} -We have (by axiom) +\frametitle{Zero-Knowledge Proofs} -\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 +Two remarkable properties of \alert{Zero-Knowledge Proofs}:\bigskip -\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} +\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).\bigskip +\item Having been convinced, Bob cannot use the evidence in order to convince Carol +that Alice knows the secret. +\end{itemize} \end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ -\begin{frame}[c] -\frametitle{Other Direction} - -\begin{tabular}{@{\hspace{-6mm}}l} -\begin{minipage}{1.1\textwidth} -We want to prove +\begin{frame}[t] +\frametitle{\begin{tabular}{@{}c@{}}The Idea \end{tabular}} \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$} +\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} -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{textblock}{7}(1,2.5) +The Alibaba cave: +\end{textblock} -\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} +\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}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -780,701 +127,294 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \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] +\frametitle{Applications of ZKPs} -\begin{center} -\Large -\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} -\end{center} - +\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 a user to prove, using a zero-knowledge proof, that its behaviour is +correct according to the protocol +\end{itemize} \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} +\frametitle{Central Properties} -\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] +Zero-knowledge proof protocols should satisfy:\bigskip \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} - - +\item \alert{\bf Completeness} If Alice knows the secret, Bob accepts Alice ``proof'' for sure.\bigskip +\item \alert{\bf Soundness} If Alice does not know the secret, Bob accepts her ``proof'' with a very +small probability. \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): +\frametitle{Graph Isomorphism} \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}}$}\\ +\begin{tabular}{l@{\hspace{10mm}}r} +\includegraphics[scale=0.8]{../pics/graphs.png}\\ \end{tabular} \end{center} +Finding an isomorphism between two graphs is an NP complete problem. \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)$} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Graph Isomorphism Protocol} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Trusted Third Party} +Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip - \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}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\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 - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Public/Private Keys} +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Graph Isomorphism Protocol (2)} - \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 +If Alice knows the isomorphism, she can always calculate \bl{$\sigma$}.\bigskip - \item this is {\bf not} a derived rule! - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Security Levels} - \small + 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$}. - \begin{itemize} - \item Top secret (\bl{$T\!S$}) - \item Secret (\bl{$S$}) - \item Public (\bl{$P$}) - \end{itemize} +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{center} - \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause - \end{center} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Graph Isomorphism Protocol (3)} - \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} +Why is the GI-protocol zero-knowledge?\bigskip\pause - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading a File} +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. - \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}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Non-Interactive ZKPs} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \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 +\bigskip +This is amazing: Alison 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. +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \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} +\mode{ +\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 - \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}} +\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}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\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 +\mode{ +\begin{frame}[c] +\frametitle{Problems of ZKPs} - \begin{itemize} - \item \bl{$slev(P) < slev (S)$} - \item \bl{$slev(S) < slev (T\!S)$} - \item[] \bl{$slev(P) < slev (T\!S)$} - \end{itemize} +\begin{itemize} +\item ``grand chess master problem''\\ +(person in the middle)\bigskip - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\item Alice can have multiple identities; once she committed a fraud she stops using one +\end{itemize} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading Files} +\mode{ +\begin{frame}[c] +\frametitle{Other Methods for ZKPs} - \begin{itemize} - \item Access policy for reading - \end{itemize} +Essentially every NP-problem can be used for ZKPs - \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}} +\begin{itemize} +\item modular logarithms: Alice chooses public \bl{$A$}, \bl{$B$}, \bl{$p$}; and private \bl{$x$} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\begin{center} +\bl{$A^x \equiv B\; mod\; p$} +\end{center} +\end{itemize} +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Writing Files} - - \begin{itemize} - \item Access policy for \underline{writing} - \end{itemize} +\mode{ +\begin{frame}[c] +\frametitle{Commitment Stage} - \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}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\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 - -\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} +\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{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 +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \item this is {\bf not} a derived rule! - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Trusted Third Party} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Confirmation Stage} - \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} +\begin{enumerate} +\item For each \bl{$b_i$} Bob checks whether \bl{$s_i$} conforms to the protocol - \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}} +\begin{center} +\begin{tabular}{ll} +\bl{$b_i = 0$}: & \bl{$A^{s_i} \equiv B\;mod\;p$}\\ +\bl{$b_i = 1$}: & \bl{$A^{s_i} \equiv h_i * h_j^{-1} \;mod\; p$}\\ +\end{tabular} +\end{center}\bigskip - \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 +Bob was send - \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{$r_j - r _j$}, \bl{$r_m - r _j$}, \ldots, \bl{$r_p - r _j$ \;mod \;p} +\end{center} - \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} +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}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Security Levels} - \small +\mode{ +\begin{frame}[c] +\frametitle{Proving Stage} - \begin{itemize} - \item Top secret (\bl{$T\!S$}) - \item Secret (\bl{$S$}) - \item Public (\bl{$P$}) - \end{itemize} +\begin{enumerate} +\item Alice proves she knows \bl{$x$}, the discrete log of \bl{$B$}\\ +she sends - \begin{center} - \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause - \end{center} +\begin{center} +\bl{$s_{z+1} = (x - r_j)$} +\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} +\item Bob confirms - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading a File} +\begin{center} +\bl{$A^{s_{z+1}} \equiv B * h_j^{-1} \;mod \; p$} +\end{center} +\end{enumerate}\bigskip\pause - \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}} +In order to cheat, Alice has to guess all bits in advance. She has only \bl{$1$} to \bl{$2^z$} +chance. \\ +\small\hspace{7mm}\textcolor{gray}{(explanation $\rightarrow$ \url{http://goo.gl/irL9GK})} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% +\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 +\mode{ +\begin{frame}[c] +\frametitle{Random Number Generators} - \begin{itemize} - \item \bl{$slev($Bob$)$ $=$ $S$} - \item \bl{$slev($File$)$ $=$ $P$} - \item \bl{$slev(P) < slev(S)$} - \end{itemize} +\begin{itemize} +\item Computers are deterministic. How do they generate random numbers?\bigskip\pause - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Reading a File} +\item The most popular method to generate random numbers between \bl{$0$} and \bl{$m$} is: choose +three integers - \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}} +\begin{center} +\begin{tabular}{ll} +\bl{$a$} & multiplier\\ +\bl{$c$} & increment\\ +\bl{$X_0$} & start value +\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} +and calculate - \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} +\begin{center} +\bl{$X_{n+1} = (a * X_n + c) \;mod\; m$} +\end{center} +\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} +\only<3->{ +\begin{textblock}{7}(10,2) +\begin{tikzpicture} +\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] +{\begin{minipage}{3.8cm} +\begin{tabular}{ll|l} +\bl{$m =$} & \bl{$16$} & \bl{$16$}\\ +\bl{$X_0 =$} & \bl{$1$} & \bl{$1$}\\ +\bl{$a = $} & \bl{$5$} & \bl{$5$}\\ +\bl{$c =$} & \bl{$1$} & \bl{$0$}\\ +\end{tabular} +\end{minipage}}; +\end{tikzpicture} +\end{textblock}} - \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{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \end{document} %%% Local Variables: