2 \usepackage{proof}

     2 \usepackage{../slides}

     3 \usepackage{beamerthemeplaincu}

     3 \usepackage{../graphics}

     4 %\usepackage[T1]{fontenc}

     4 

     5 %\usepackage[latin1]{inputenc}

     5 \setmonofont[Scale=.88]{Consolas}

     6 \usepackage{mathpartir}

     6 \newfontfamily{\consolas}{Consolas}

     7 \usepackage{isabelle}

     7 

     8 \usepackage{isabellesym}

     8 \hfuzz=220pt 

     9 \usepackage[absolute,overlay]{textpos}

    10 \usepackage{ifthen}

    11 \usepackage{tikz}

    12 \usepackage{courier}

    13 \usepackage{listings}

    14 \usetikzlibrary{arrows}

    15 \usetikzlibrary{positioning}

    16 \usetikzlibrary{calc}

    17 \usetikzlibrary{shapes}

    18 \usepackage{graphicx} 

    19 \setmonofont[Scale=MatchLowercase]{Consolas}

    20 

    21 \isabellestyle{rm}

    22 \renewcommand{\isastyle}{\rm}%

    23 \renewcommand{\isastyleminor}{\rm}%

    24 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}%

    25 \renewcommand{\isatagproof}{}

    26 \renewcommand{\endisatagproof}{}

    27 \renewcommand{\isamarkupcmt}[1]{#1}

    28 

    29 % Isabelle characters

    30 \renewcommand{\isacharunderscore}{\_}

    31 \renewcommand{\isacharbar}{\isamath{\mid}}

    32 \renewcommand{\isasymiota}{}

    33 \renewcommand{\isacharbraceleft}{\{}

    34 \renewcommand{\isacharbraceright}{\}}

    35 \renewcommand{\isacharless}{$\langle$}

    36 \renewcommand{\isachargreater}{$\rangle$}

    37 \renewcommand{\isasymsharp}{\isamath{\#}}

    38 \renewcommand{\isasymdots}{\isamath{...}}

    39 \renewcommand{\isasymbullet}{\act}

    40 \newcommand{\isaliteral}[1]{}

    41 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}

    42 

    43 

    44 

    45 \definecolor{javared}{rgb}{0.6,0,0} % for strings

    46 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments

    47 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords

    48 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc

    49 

    50 \lstset{language=Java,

    51 	basicstyle=\ttfamily,

    52 	keywordstyle=\color{javapurple}\bfseries,

    53 	stringstyle=\color{javagreen},

    54 	commentstyle=\color{javagreen},

    55 	morecomment=[s][\color{javadocblue}]{/**}{*/},

    56 	numbers=left,

    57 	numberstyle=\tiny\color{black},

    58 	stepnumber=1,

    59 	numbersep=10pt,

    60 	tabsize=2,

    61 	showspaces=false,

    62 	showstringspaces=false}

    63 

    64 \lstdefinelanguage{scala}{

    65   morekeywords={abstract,case,catch,class,def,%

    66     do,else,extends,false,final,finally,%

    67     for,if,implicit,import,match,mixin,%

    68     new,null,object,override,package,%

    69     private,protected,requires,return,sealed,%

    70     super,this,throw,trait,true,try,%

    71     type,val,var,while,with,yield},

    72   otherkeywords={=>,<-,<\%,<:,>:,\#,@},

    73   sensitive=true,

    74   morecomment=[l]{//},

    75   morecomment=[n]{/*}{*/},

    76   morestring=[b]",

    77   morestring=[b]',

    78   morestring=[b]"""

    79 }

    80 

    81 \lstset{language=Scala,

    82 	basicstyle=\ttfamily,

    83 	keywordstyle=\color{javapurple}\bfseries,

    84 	stringstyle=\color{javagreen},

    85 	commentstyle=\color{javagreen},

    86 	morecomment=[s][\color{javadocblue}]{/**}{*/},

    87 	numbers=left,

    88 	numberstyle=\tiny\color{black},

    89 	stepnumber=1,

    90 	numbersep=10pt,

    91 	tabsize=2,

    92 	showspaces=false,

    93 	showstringspaces=false}

    94 

    95 %sudoku

    96 \newcounter{row}

    97 \newcounter{col}

    98 

    99 \newcommand\setrow[9]{

   100         \setcounter{col}{1}

   101         \foreach \n in {#1, #2, #3, #4, #5, #6, #7, #8, #9} {

   102             \edef\x{\value{col} - 0.5}

   103             \edef\y{9.5 - \value{row}}

   104             \node[anchor=center] at (\x, \y) {\n};

   105             \stepcounter{col}

   106         }

   107         \stepcounter{row}

   108 }

   109 

   110 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions

   113 \renewcommand{\slidecaption}{APP 06, King's College London, 12 November 2013}

    11 \newcommand{\bl}[1]{\textcolor{blue}{#1}}  

   114 

    12 \renewcommand{\slidecaption}{APP 06, King's College London}

   115 \newcommand{\bl}[1]{\textcolor{blue}{#1}}

    13 

   119 \mode<presentation>{

    17 \begin{frame}[t]

   120 \begin{frame}<1>[t]

   125   \LARGE Privacy Policies (6)\\[-6mm] 

    22   \LARGE Privacy Policies (9)\\[-6mm] 

   128   %\begin{center}

    25   \normalsize

   129   %\includegraphics[scale=1.3]{pics/barrier.jpg}

   130   %\end{center}

   131 

   132 \normalsize

   141 

    34 \end{frame}

   142 \end{frame}}

   145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    37 

   146   \mode<presentation>{

    38 

   147   \begin{frame}[t]

    39 

   148   \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}

    40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   149   

    41 \mode<presentation>{

   150   Formulas

    42 \begin{frame}[t]

   151   

    43 \frametitle{Checking Solutions}

   152   \begin{itemize}

    44 

   153   \item[]

    45 How can you check somebody's solution without revealing the solution?\pause\bigskip

   154   

    46 

   155   \begin{center}\color{blue}

    47 Alice and Bob solve crosswords. Alice knows the answer for 21D (folio) but doesn't 

   156   \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}

    48 want to tell Bob.\medskip

   157   \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\

    49 

   158             & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\

    50 You use an English  dictionary:

   159             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\

    51 

   160             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\

    52 \begin{itemize}

   161             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\

    53 \item folio \onslide<4->{$\stackrel{1}{\rightarrow}$ individual }

   162             & \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}}} \\  

    54                 \onslide<5->{$\stackrel{2}{\rightarrow}$ human}

   163             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ 

    55                 \onslide<6->{$\stackrel{3}{\rightarrow}$ or \ldots}

   164   \end{tabular}

    56 \only<3>{

   165   \end{center}

    57 \begin{quote}

   166   

    58 ``an \alert{individual} leaf of paper or parchment, either loose as one of a series or 

   167   \end{itemize}

    59 forming part of a bound volume, which is numbered on the recto or front side only.''	

   168   

    60 \end{quote}}

   169 Judgements

    61 \only<4>{

   170 

    62 \begin{quote}

   171 \begin{itemize}

    63 ``a single \alert{human} being as distinct from a group''

   172 \item[] \mbox{\hspace{9mm}}\bl{$\Gamma \vdash \text{F}$}

    64 \end{quote}}

   173 \end{itemize}

    65 \only<5>{

   174   

    66 \begin{quote}

   175   \end{frame}}

    67 ``relating to \alert{or} characteristic of humankind''

   176   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    68 \end{quote}}

   177   

    69 \end{itemize}\bigskip\bigskip

   178 

    70 

   179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    71 \only<7->{

   180 \mode<presentation>{

    72 this is essentially a hash function...but Bob can only check once he has also found the solution

   181 \begin{frame}[c]

    73 }

   182 \frametitle{Judgements}

    74 

   183 

    75 \end{frame}}

   184 \begin{center}

    76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   185 \begin{tikzpicture}[scale=1]

    77 

   186   

    78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   187   \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};

    79 \mode<presentation>{

   188   \onslide<2->{

    80 \begin{frame}[c]

   189   \draw (-1,-0.3) node (X) {};

    81 \frametitle{Zero-Knowledge Proofs}

   190   \draw (-2.0,-2.0) node (Y) {};

    82 

   191   \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};

    83 Two remarkable properties of \alert{Zero-Knowledge Proofs}:\bigskip

   192   \draw[red, ->, line width = 2mm] (Y) -- (X);

    84 

   193  

    85 \begin{itemize}

   194   \draw (1.2,-0.1) node (X1) {};

    86 \item Alice only reveals the fact that she knows a secret, not the secret itself (meaning 

   195   \draw (2.8,-0.1) node (Y1) {};

    87 she can convince Bob that she knows the secret).\bigskip

   196   \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};

    88 \item Having been convinced, Bob cannot use the evidence in order to convince Carol 

   197   \draw[red, ->, line width = 2mm] (Y1) -- (X1);

    89 that Alice knows the secret.

   198 

    90 \end{itemize}

   199   \draw (-0.1,0.1) node (X2) {};

    91 

   200   \draw (0.5,1.5) node (Y2) {};

    92 \end{frame}}

   201   \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};

    93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   202   \draw[red, ->, line width = 2mm] (Y2) -- (X2);}

    94 

   203   

    95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   204   \end{tikzpicture}

    96 \mode<presentation>{

   205 \end{center}

    97 \begin{frame}[t]

   206 

    98 \frametitle{\begin{tabular}{@{}c@{}}The Idea \end{tabular}}

   207 \end{frame}}

    99 

   208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   100 \begin{center}

   209   

   101 \begin{tabular}{l@{\hspace{10mm}}r}

   210 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   102 \\[-10mm]

   211 \mode<presentation>{

   103 \raisebox{10mm}{\large 1.} & \includegraphics[scale=0.1]{../pics/alibaba1.png}\\

   212 \begin{frame}[c]

   104 \raisebox{10mm}{\large 2.} & \includegraphics[scale=0.1]{../pics/alibaba2.png}\\

   213 \frametitle{Inference Rules}

   105 \raisebox{10mm}{\large 3.} & \includegraphics[scale=0.1]{../pics/alibaba3.png}

   214 

   106 \end{tabular}

   215 \begin{center}

   107 \end{center}

   216 \begin{tikzpicture}[scale=1]

   108 

   217   

   109 \begin{textblock}{7}(1,2.5)

   218   \draw (0.0,0.0) node 

   110 The Alibaba cave:

   219   {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};

   111 \end{textblock}

   220  

   112 

   221   \draw (-0.1,-0.7) node (X) {};

   113 \small

   222   \draw (-0.1,-1.9) node (Y) {};

   223   \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};

   224   \draw[red, ->, line width = 2mm] (Y) -- (X);

   225  

   226   \draw (-1,0.6) node (X2) {};

   227   \draw (0.0,1.6) node (Y2) {};

   228   \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};

   229   \draw[red, ->, line width = 2mm] (Y2) -- (X2);

   230    \draw (1,0.6) node (X3) {};

   231   \draw (0.0,1.6) node (Y3) {};

   232   \draw[red, ->, line width = 2mm] (Y3) -- (X3);

   233   \end{tikzpicture}

   234 \end{center}

   235 

   237 \begin{textblock}{11}(1,13)

   115 \begin{textblock}{12}(2,13.3)

   238 \small

   116 Even if Bob has a hidden camera, a recording will not be convincing to anyone else 

   239 \bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}

   117 (Alice and Bob could have made it all up).

   242 \begin{textblock}{11}(1,13)

   120 \begin{textblock}{12}(2,13.3)

   243 \small

   121 Even worse, an observer present at the experiment would not be convinced.

   244 \bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge

   245         \underbrace{P \,\text{says}\, G}_{F_2} $}

   321 

   127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   322 

   128 \mode<presentation>{

   323 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   129 \begin{frame}[c]

   324 \mode<presentation>{

   130 \frametitle{Applications of ZKPs}

   325 \begin{frame}[c]

   131 

   326 \frametitle{The Access Control Problem}

   132 \begin{itemize}

   327 

   133 \item authentication, where one party wants to prove its identity to a 

   328 

   134 second party via some secret information,  but doesn't want the second 

   329 \begin{center}

   135 party to learn anything about this secret\bigskip

   330   \begin{tikzpicture}[scale=1]

   136 \item to enforce honest behaviour while maintaining privacy: the idea is to 

   331   

   137 force a user to prove, using a zero-knowledge proof, that its behaviour is 

   332   \draw[line width=1mm] (-.3, -0.5) rectangle (1.5,2);

   138 correct according to the protocol

   333   \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};

   139 \end{itemize}

   334   \draw (4.2,1) node {\begin{tabular}{l}provable/\\not provable\end{tabular}};

   140 \end{frame}}

   335   \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}};

   141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   142 

   143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   144 \mode<presentation>{

   145 \begin{frame}[c]

   146 \frametitle{Central Properties}

   147 

   148 Zero-knowledge proof protocols should satisfy:\bigskip

   149 

   150 \begin{itemize}

   151 \item \alert{\bf Completeness} If Alice knows the secret, Bob accepts Alice ``proof'' for sure.\bigskip

   152 \item \alert{\bf Soundness} If Alice does not know the secret, Bob accepts her ``proof'' with a very 

   153 small probability.

   154 \end{itemize}

   155 \end{frame}}

   156 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   157 

   158 

   159 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   160 \mode<presentation>{

   161 \begin{frame}[c]

   162 \frametitle{Graph Isomorphism}

   163 

   164 \begin{center}

   165 \begin{tabular}{l@{\hspace{10mm}}r}

   166 \includegraphics[scale=0.8]{../pics/graphs.png}\\

   167 \end{tabular}

   168 \end{center}

   169 

   170 Finding an isomorphism between two graphs is an NP complete problem.

   171 \end{frame}}

   172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   173 

   174 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   175 \mode<presentation>{

   176 \begin{frame}[c]

   177 \frametitle{Graph Isomorphism Protocol}

   178 

   179 Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip

   180 

   181 \begin{enumerate}

   182 \item Alice generates an isomorphic graph \bl{$H$} which she sends to Bob 

   183 \item Bob asks either for an isomorphism between \bl{$G_1$} and \bl{$H$}, or

   184 \bl{$G_2$} and \bl{$H$}	

   185 \item Alice and Bob repeat this procedure \bl{$n$} times	

   186 \end{enumerate}\pause

   187 

   188 these are called commitment algorithms

   189 

   190 \end{frame}}

   191 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

   192    

   193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   194 \mode<presentation>{

   195 \begin{frame}[c]

   196 \frametitle{Graph Isomorphism Protocol (2)}

   197 

   198 If Alice knows the isomorphism, she can always calculate \bl{$\sigma$}.\bigskip

   199 

   200  If she doesn't, she can only correctly respond if Bob's 

   201  choice of index is the same as the one she used to form \bl{$H$}. The probability 

   202  of this happening is \bl{$\frac{1}{2}$}, so after \bl{$n$} rounds the probability of her 

   203  always responding correctly is only \bl{$\frac{1}{2}^n$}.

   204 

   205 \end{frame}}

   206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

   207 

   208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   209 \mode<presentation>{

   210 \begin{frame}[c]

   211 \frametitle{Graph Isomorphism Protocol (3)}

   212 

   213 Why is the GI-protocol zero-knowledge?\bigskip\pause

   214 

   215 A: We can generate a fake transcript of a conversation, which 

   216 cannot be distinguished from a ``real'' conversation.\bigskip

   217 

   218 Anything Bob can compute using the information obtained from 

   219 the transcript can be computed using only a forged transcript and 

   220 therefore participation in such a communication does not increase 

   221 Bob's capability  to perform any computation.

   222 

   223 \end{frame}}

   224 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

   225    

   226    

   227    

   228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   229 \mode<presentation>{

   230 \begin{frame}[c]

   231 \frametitle{Non-Interactive ZKPs}

   232 

   233 

   234 \bigskip

   235 This is amazing: Alison can publish some data that contains no data about her secret,

   236 but this data can be used to convince anyone of the secret's existence.

   237 \end{frame}}

   238 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   239 

   240 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   241 \mode<presentation>{

   242 \begin{frame}[c]

   243 \frametitle{Non-Interactive ZKPs (2)}

   244 

   245 Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip

   246 

   247 \begin{enumerate}

   248 \item Alice generates \bl{$n$} isomorphic graphs \bl{$H_{1..n}$} which she makes public 

   249 \item she feeds the \bl{$H_{1..n}$} into a hashing function (she has no control over what

   250 	the output will be)

   251 \item Alice takes the first \bl{$n$} bits of the output: whenever output is \bl{$0$}, she shows 

   252 an isomorphism with \bl{$G_1$} ; for \bl{$1$} she shows an isomorphism with \bl{$G_2$}

   253 \end{enumerate}

   254 

   255 \end{frame}}

   256 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   257 

   258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   259 \mode<presentation>{

   260 \begin{frame}[c]

   261 \frametitle{Problems of ZKPs}

   262 

   263 \begin{itemize}

   264 \item ``grand chess master problem''\\ 

   265 (person in the middle)\bigskip

   266 

   267 \item Alice can have multiple identities; once she committed a fraud she stops using one

   268 \end{itemize}

   269 

   270 \end{frame}}

   271 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   272 

   273 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   274 \mode<presentation>{

   275 \begin{frame}[c]

   276 \frametitle{Other Methods for ZKPs}

   277 

   278 Essentially every NP-problem can be used for ZKPs

   279 

   280 \begin{itemize}

   281 \item modular logarithms: Alice chooses public \bl{$A$},  \bl{$B$}, \bl{$p$}; and private \bl{$x$}

   282 

   283 \begin{center}

   284 \bl{$A^x \equiv B\; mod\; p$}

   285 \end{center} 

   286 \end{itemize}

   287 

   288 \end{frame}}

   289 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   290 

   291 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   292 \mode<presentation>{

   293 \begin{frame}[c]

   294 \frametitle{Commitment Stage}

   295 

   296 \begin{enumerate}

   297 \item Alice generates \bl{$z$} random numbers \bl{$r_1$}, ..., \bl{$r_z$}, all less than \bl{$p - 1$}.

   298 \item Alice sends Bob for all \bl{$1..z$} 

   299 \begin{center}

   300 \bl{$h_i = A^{r_i} \;mod\; p$}

   301 \end{center}

   302 \item Bob generates random bits   \bl{$b_1$}, ..., \bl{$b_z$} by flipping a coin

   303 \item For each bit \bl{$b_i$}, Alice sends Bob an \bl{$s_i$} where

   304 

   305 \begin{center}

   306 \begin{tabular}{ll}

   307 \bl{$b_i = 0$}: & \bl{$s_i = r_i$}\\

   308 \bl{$b_i = 1$}: & \bl{$s_i = (r_i - r_j) \;mod\; (p -1)$}\\

   309 \end{tabular}

   310 \end{center}

   311 where \bl{$r_j$} is the lowest \bl{$j$} where \bl{$b_j = 1$}

   337   \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); 

   313 \end{enumerate}

   338   \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);

   314 

   339   \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); 

   315 \end{frame}}

   340   

   316 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   341   \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};

   317 

   342 

   318 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   343   \end{tikzpicture}

   319 \mode<presentation>{

   344 \end{center}

   320 \begin{frame}[c]

   345 

   321 \frametitle{Confirmation Stage}

   346 \end{frame}}

   322 

   347 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   348 

   349 

   350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   351 \mode<presentation>{

   352 \begin{frame}[c]

   353 \frametitle{Proofs}

   354 

   355 \begin{center}

   356 \includegraphics[scale=0.4]{pics/river-stones.jpg}

   357 \end{center}

   358 

   359 \begin{textblock}{5}(11.7,5)

   360 goal

   361 \end{textblock}

   362 

   363 \begin{textblock}{5}(11.7,14)

   364 start

   365 \end{textblock}

   366 

   367 \begin{textblock}{5}(0,7)

   368 \begin{center}

   369 \bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]

   370 \bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]

   371 \bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}

   372 \end{center}

   373 \end{textblock}

   374 

   375 \end{frame}}

   376 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   377 

   378 

   379 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   380 \mode<presentation>{

   381 \begin{frame}[c]

   382 \frametitle{Sudoku}

   383 

   384 \begin{tikzpicture}[scale=.5]

   385   \begin{scope}

   386     \draw (0, 0) grid (9, 9);

   387     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   388 

   389     \setcounter{row}{1}

   390     \setrow { }{2}{ }  {5}{ }{1}  { }{9}{ }

   391     \setrow {8}{ }{ }  {2}{ }{3}  { }{ }{6}

   392     \setrow { }{3}{ }  { }{6}{ }  { }{7}{ }

   393 

   394     \setrow { }{ }{1}  { }{ }{ }  {6}{ }{ }

   395     \setrow {5}{4}{ }  { }{ }{ }  { }{1}{9}

   396     \setrow { }{ }{2}  { }{ }{ }  {7}{ }{ }

   397 

   398     \setrow { }{9}{ }  { }{3}{ }  { }{8}{ }

   399     \setrow {2}{ }{ }  {8}{ }{4}  { }{ }{7}

   400     \setrow { }{1}{ }  {9}{ }{7}  { }{6}{ }

   401 

   402     \fill[red, fill opacity=0.4] (4,0) rectangle (5,9);

   403     \fill[red, fill opacity=0.4] (0,5) rectangle (9,6);

   404     \fill[red!50, fill opacity=0.4] (3,3) rectangle (4,5);

   405     \fill[red!50, fill opacity=0.4] (5,3) rectangle (6,5);  

   406     \node[gray, anchor=center] at (4.5, -0.5) {columns};

   407     \node[gray, rotate=90, anchor=center] at (-0.6, 4.5, -0.5) {rows};

   408     \node[gray, anchor=center] at (4.5, 4.5) {box};

   409   \end{scope}

   410   \end{tikzpicture}

   411 

   412 \small

   413 \begin{textblock}{7}(9,3)

   415 \item {\bf Row-Column:} each cell, must contain exactly one number

   324 \item For each \bl{$b_i$} Bob checks whether \bl{$s_i$} conforms to the protocol

   416 \item {\bf Row-Number:} each row must contain each number exactly once

   325 

   417 \item {\bf Column-Number:} each column must contain each number exactly once

   326 \begin{center}

   418 \item {\bf Box-Number:} each box must contain each number exactly once

   327 \begin{tabular}{ll}

   328 \bl{$b_i = 0$}: & \bl{$A^{s_i} \equiv B\;mod\;p$}\\

   329 \bl{$b_i = 1$}: & \bl{$A^{s_i}  \equiv h_i * h_j^{-1}  \;mod\; p$}\\

   330 \end{tabular}

   331 \end{center}\bigskip

   332 

   333 Bob was send 

   334 

   335 \begin{center}

   336 \bl{$r_j - r _j$},  \bl{$r_m - r _j$}, \ldots, \bl{$r_p - r _j$ \;mod \;p} 

   337 \end{center}

   338 

   339 where the corresponding bits were 

   340 \bl{$1$}; Bob does not know \bl{$r_j$}, he does not know any \bl{$r_i$} where the bit was \bl{$1$}

   420 \end{textblock}

   342 

   421 

   343 \end{frame}}

   422 

   344 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   423 \end{frame}}

   345 

   424 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   346 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   425 

   347 \mode<presentation>{

   426 

   348 \begin{frame}[c]

   427 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   349 \frametitle{Proving Stage}

   428 \mode<presentation>{

   350 

   429 \begin{frame}[c]

   351 \begin{enumerate}

   430 \frametitle{Solving Sudokus}

   352 \item Alice proves she knows \bl{$x$}, the discrete log of \bl{$B$}\\

   431 

   353 she sends

   432 \begin{tikzpicture}[scale=.5]

   354 

   433   \begin{scope}

   355 \begin{center}

   434     \draw (0, 0) grid (9, 9);

   356 \bl{$s_{z+1} = (x - r_j)$}

   435     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   357 \end{center}

   436 

   358 

   437     \setcounter{row}{1}

   359 \item Bob confirms

   438     \setrow { }{ }{ }  {7}{ }{ }  { }{5}{8}

   360 

   439     \setrow {}{5}{6}  {2}{1}{8}  {7}{9}{3}

   361 \begin{center}

   440     \setrow { }{ }{ }  { }{ }{ }  {1}{ }{ }

   362 \bl{$A^{s_{z+1}} \equiv B * h_j^{-1} \;mod \; p$}

   441 

   363 \end{center}

   442     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   364 \end{enumerate}\bigskip\pause

   443     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   365 

   444     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }

   366 In order to cheat, Alice has to guess all bits in advance. She has only \bl{$1$} to \bl{$2^z$}

   445 

   367 chance. \\

   446     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   368 \small\hspace{7mm}\textcolor{gray}{(explanation $\rightarrow$ \url{http://goo.gl/irL9GK})}

   447     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   369 

   448     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   370 \end{frame}}

   449 

   371 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   450     \fill[red, fill opacity=0.4] (0,7) rectangle (1,8);

   372 

   451 

   373  

   452   \end{scope}

   374 

   453   \end{tikzpicture}

   375 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   454 

   376 \mode<presentation>{

   455 \small

   377 \begin{frame}[c]

   456 \begin{textblock}{6}(9,6)

   378 \frametitle{Random Number Generators}

   457 {\bf single position rules}\\

   379 

   458 \begin{center}

   380 \begin{itemize}

   459 \bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}

   381 \item Computers are deterministic. How do they generate random numbers?\bigskip\pause

   460 \end{center}

   382 

   461 

   383 \item The most popular method to generate random numbers between \bl{$0$} and \bl{$m$} is: choose

   462 \onslide<2->{

   384 three integers

   463 \begin{center}

   385 

   464 \bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one column}}}\medskip\\

   386 \begin{center}

   465 \bl{\infer{x\;\text{in empty position}}{\{1..9\} - \{x\}\;\text{in one box}}}

   387 \begin{tabular}{ll}

   466 \end{center}}

   388 \bl{$a$} & multiplier\\

   467 \end{textblock}

   389 \bl{$c$} & increment\\

   468 

   390 \bl{$X_0$} & start value

   469 

   470 \end{frame}}

   471 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   472 

   473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   474 \mode<presentation>{

   475 \begin{frame}[c]

   476 \frametitle{Solving Sudokus}

   477 

   478 \begin{tikzpicture}[scale=.5]

   479   \begin{scope}

   480     \draw (0, 0) grid (9, 9);

   481     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   482 

   483     \setcounter{row}{1}

   484     \setrow { }{ }{ }  {7}{ }{ }  {\alert{\footnotesize 2}}{5}{8}

   485     \setrow {}{5}{6}  {2}{1}{8}  {7}{9}{3}

   486     \setrow { }{ }{ }  { }{ }{ }  {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}}

   487 

   488     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   489     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   490     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }

   491 

   492     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   493     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   494     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   495 

   496   \end{scope}

   497   \end{tikzpicture}

   498 

   499 \small

   500 \begin{textblock}{6}(7.5,6)

   501 {\bf candidate rules}\\

   502 \begin{center}

   503 \bl{\infer{x\;\text{candidate in empty positions}}{X - \{x\}\;\text{in one box} & X \subseteq \{1..9\}}}

   504 \end{center}

   505 \end{textblock}

   506 

   507 \end{frame}}

   508 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   509 

   510 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   511 \mode<presentation>{

   512 \begin{frame}[c]

   513 \frametitle{Solving Sudokus}

   514 

   515 \begin{tikzpicture}[scale=.5]

   516   \begin{scope}

   517     \draw (0, 0) grid (9, 9);

   518     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   519 

   520     \setcounter{row}{1}

   521     \setrow { }{ }{ }  {7}{ }{ }  {\alert{\footnotesize 2}}{5}{8}

   522     \setrow {\alert{4}}{5}{6}  {2}{1}{8}  {7}{9}{3}

   523     \setrow { }{ }{ }  { }{ }{ }  {1}{\alert{\footnotesize 2}}{\alert{\footnotesize 2}}

   524 

   525     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   526     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   527     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ }

   528 

   529     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   530     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   531     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   532 

   533   \end{scope}

   534   \end{tikzpicture}

   535 

   536 \small

   537 \begin{textblock}{6}(7.5,6)

   538 \begin{center}

   539 \bl{\infer{4\;\text{in empty position}}{\{1..9\} - \{4\}\;\text{in one row}}}\bigskip\\

   540 \bl{\infer{2\;\text{candidate in empty positions}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}}

   541 \end{center}

   542 \end{textblock}

   543 

   544 

   545 \begin{textblock}{3}(13.5,6.8)

   546   \begin{tikzpicture}

   547   \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}

   548   \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}

   549   \end{tikzpicture}

   550 \end{textblock}

   551 

   552 \begin{textblock}{3}(14.5,9.3)

   553   \begin{tikzpicture}

   554   \onslide<1>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}

   555   \onslide<2>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}

   556   \end{tikzpicture}

   557 \end{textblock}

   558 

   559 \end{frame}}

   560 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   561 

   562 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   563 \mode<presentation>{

   564 \begin{frame}[c]

   565 \frametitle{Solving Sudokus}

   566 

   567 \begin{tikzpicture}[scale=.5]

   568   \begin{scope}

   569     \draw (0, 0) grid (9, 9);

   570     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   571 

   572     \setcounter{row}{1}

   573     \setrow { }{ }{ }  {7}{ }{ }  { }{5}{8}

   574     \setrow { }{5}{6}  {2}{1}{8}  {7}{9}{3}

   575     \setrow { }{ }{ }  { }{ }{ }  {1}{ }{ }

   576 

   577     \setrow { }{ }{ }  { }{ }{ }  { }{8}{1}

   578     \setrow { }{ }{ }  {3}{7}{6}  { }{ }{ }

   579     \setrow {9}{6}{ }  { }{ }{ }  { }{ }{ \alert{2}}

   580 

   581     \setrow { }{ }{5}  { }{ }{ }  { }{ }{ }

   582     \setrow { }{ }{4}  { }{2}{1}  {8}{3}{ }

   583     \setrow {8}{7}{ }  { }{ }{3}  { }{ }{ }

   584 

   585   \end{scope}

   586   \end{tikzpicture}

   587 

   588 \small

   589 \begin{textblock}{6}(7.5,6)

   590 \begin{center}

   591 \bl{\infer{2\;\text{candidate}}{X - \{2\}\;\text{in one box} & X \subseteq \{1..9\}}}

   592 \end{center}

   593 \end{textblock}

   594 

   595 \begin{textblock}{3}(14.5,8.3)

   596   \begin{tikzpicture}

   597   \onslide<1>{\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=white]{\mbox{\alert{a}}};}

   598   \end{tikzpicture}

   599 \end{textblock}

   600 

   601 \end{frame}}

   602 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   603 

   604 

   605 

   606 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   607 \mode<presentation>{

   608 \begin{frame}[c]

   609 \frametitle{BTW}

   610 

   611 Are there sudokus that cannot be solved?\pause

   612 

   613 \begin{center}

   614 \begin{tikzpicture}[scale=.5]

   615   \begin{scope}

   616     \draw (0, 0) grid (9, 9);

   617     \draw[very thick, scale=3] (0, 0) grid (3, 3);

   618 

   619     \setcounter{row}{1}

   620     \setrow {1}{2}{3}  {4}{5}{6}  {7}{8}{ }

   621     \setrow { }{ }{ }  { }{ }{ }  { }{ }{2}

   622     \setrow { }{ }{ }  { }{ }{ }  { }{ }{3}

   623 

   624     \setrow { }{ }{ }  { }{ }{ }  { }{ }{4}

   625     \setrow { }{ }{ }  { }{ }{ }  { }{ }{5}

   626     \setrow { }{ }{ }  { }{ }{ }  { }{ }{6}

   627 

   628     \setrow { }{ }{ }  { }{ }{ }  { }{ }{7}

   629     \setrow { }{ }{ }  { }{ }{ }  { }{ }{8}

   630     \setrow { }{ }{ }  { }{ }{ }  { }{ }{9}

   631 

   632   \end{scope}

   633   \end{tikzpicture}

   634 \end{center}

   635 

   636 Sometimes no rules apply at all....unsolvable sudoku.

   637 

   638 

   639 \end{frame}}

   640 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   641 

   642 

   643 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   644 \mode<presentation>{

   645 \begin{frame}[c]

   646 \frametitle{Example Proof}

   647 

   648 \begin{center}

   649 \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}

   650          {\raisebox{2mm}{\text{\LARGE $?$}}}}

   651 \end{center}

   652 

   653 

   654 \end{frame}}

   655 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   656 

   657 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   658 \mode<presentation>{

   659 \begin{frame}[c]

   660 \frametitle{Example Proof}

   661 

   662 \begin{tabular}{@{\hspace{-6mm}}l}

   663 \begin{minipage}{1.1\textwidth}

   664 We have (by axiom)

   665 

   666 \begin{center}

   667 \begin{tabular}{@{}ll@{}}

   668 (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$}

   672 From (1) we get

   394 and calculate

   673 

   395 

   674 \begin{center}

   396 \begin{center}

   675 \begin{tabular}{@{}ll@{}}

   397 \bl{$X_{n+1} = (a * X_n + c) \;mod\; m$}

   676 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\

   398 \end{center}

   677 (3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\

   399 \end{itemize}

   678 \end{tabular}

   400 

   679 \end{center}

   401 \only<3->{

   680 

   402 \begin{textblock}{7}(10,2)

   681 From (3) and (2) we get

   403 \begin{tikzpicture}

   682 

   404 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   683 \begin{center}

   405 {\begin{minipage}{3.8cm}

   684 \begin{tabular}{@{}ll@{}}

   406 \begin{tabular}{ll|l}

   685 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

   407 \bl{$m =$}    & \bl{$16$} & \bl{$16$}\\

   686 \end{tabular}

   408 \bl{$X_0 =$} &  \bl{$1$} & \bl{$1$}\\

   687 \end{center}

   409 \bl{$a = $}    & \bl{$5$} & \bl{$5$}\\

   688 

   410 \bl{$c =$}     & \bl{$1$} & \bl{$0$}\\

   689 Done.

   411 \end{tabular} 

   690 \end{minipage}

   412 \end{minipage}};

   691 \end{tabular}

   413 \end{tikzpicture}

   692 

   693 \end{frame}}

   694 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   695 

   696 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   697 \mode<presentation>{

   698 \begin{frame}[c]

   699 \frametitle{Other Direction}

   700 

   701 \begin{tabular}{@{\hspace{-6mm}}l}

   702 \begin{minipage}{1.1\textwidth}

   703 We want to prove

   704 

   705 \begin{center}

   706 \begin{tabular}{@{}ll@{}}

   707 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

   708 \end{tabular}

   709 \end{center}

   710 

   711 We better be able to prove:

   712 

   713 \begin{center}

   714 \begin{tabular}{@{}ll@{}}

   715 (1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\

   716 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\

   717 \end{tabular}

   718 \end{center}

   719 

   720 For (1): If we can prove

   721 

   722 \begin{center}

   723 \begin{tabular}{@{}ll@{}}

   724 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

   725 \end{tabular}

   726 \end{center}

   727 

   728 then (1) is fine. Similarly for (2).

   729 \end{minipage}

   730 \end{tabular}

   731 

   732 \end{frame}}

   733 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      

   734      

   735 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   736 \mode<presentation>{

   737 \begin{frame}[t]

   738 

   739 I want to prove

   740 

   741 \begin{center}

   742 \bl{$\Gamma \vdash \text{del\_file}$}

   743 \end{center}\pause

   744 

   745 There is an inference rule

   746 

   747 \begin{center}

   748 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}

   749 \end{center}\pause

   750 

   751 So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause

   752 

   753 \bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\

   754 So I can use the rule

   755 

   756 \begin{center}

   757 \bl{\infer{\Gamma, F \vdash F}{}}

   758 \end{center}

   759 

   760 \onslide<5>{\bf\alert{What is wrong with this?}}

   761 \hfill{\bf Done. Qed.}

   762 

   763 \end{frame}}

   764 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%        

   765 

   766 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   767 \mode<presentation>{

   768 \begin{frame}[c]

   769 \frametitle{Program}

   770 

   771 How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip

   772 

   773 \begin{center}

   774 \Large \bl{\infer{\Gamma, F\vdash F}{}}

   775 \end{center}

   776 

   777 \end{frame}}

   778 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   779 

   780 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   781 \mode<presentation>{

   782 \begin{frame}[c]

   783 

   784 \begin{center}

   785 \Large 

   786 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}

   787 \end{center}

   788 

   789 \end{frame}}

   790 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   791 

   792 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   793 \mode<presentation>{

   794 \begin{frame}[c]

   795 

   796 \begin{center}

   797 \Large 

   798 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}

   799 \end{center}

   800 

   801 \end{frame}}

   802 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   803 

   804 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   805 \mode<presentation>{

   806 \begin{frame}[c]

   807 

   808 \begin{center}

   809 \Large 

   810 \bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad

   811 \bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\

   812 \end{center}

   813 

   814 \end{frame}}

   815 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   816 

   817 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   818 \mode<presentation>{

   819 \begin{frame}[c]

   820 

   821 \begin{center}

   822 \Large 

   823 \bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}

   824 \end{center}

   825 

   826 \end{frame}}

   827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   828 

   829 

   830      

   831 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   832 \mode<presentation>{

   833 \begin{frame}[t]

   834 \frametitle{Program: \texttt{prove2}}

   835 

   836 I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause

   837 

   838 \begin{enumerate}

   839 \item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause

   840 \item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove

   841 \begin{center}

   842 \bl{$\Gamma \vdash F_2$}

   843 \end{center}\bigskip\pause

   844 

   845 \item So I am able to try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption

   846 \bl{$F_2$}.\bigskip

   847 \begin{center}

   848 \bl{$F_2, \Gamma \vdash \text{Pred}$}

   849 \end{center}

   850 \end{enumerate}

   851 

   852 \only<4>{

   853 \begin{textblock}{11}(1,10.5)

   854 \bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}

   857 

   416 \end{frame}}

   858 \end{frame}}

   417 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   859 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%       

   860      

   861 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   862   \mode<presentation>{

   863   \begin{frame}[c]

   864   \frametitle{}

   865 

   866   Recall the following scenario:

   867 

   868   \begin{itemize}

   869   \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}} 

   870   should be deleted, then this file must be deleted.

   871   \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether 

   872   \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.

   873   \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.

   874   \end{itemize}\bigskip

   875 

   876   \small

   877   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}

   878   \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}{}},\\

   879   \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}}},\\

   880   \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\

   881   \end{tabular}}\medskip

   882 

   883   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}

   884   \end{frame}}

   885   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   886 

   887 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   888 \mode<presentation>{

   889 \begin{frame}[c]

   890 

   891 \begin{itemize}

   892 \item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or

   893 can make a statement \bl{$F$}\bigskip

   894 

   895 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ 

   896 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip

   897 

   898 \begin{center}

   899 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}

   900 \end{center}

   901 

   902 

   903 \end{itemize}

   904 

   905 \end{frame}}

   906 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   907 

   908 

   909 

   910 

   911 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   912 \mode<presentation>{

   913 \begin{frame}[c]

   914 \frametitle{Trusted Third Party}

   915 

   916 Simple protocol for establishing a secure connection via a mutually

   917 trusted 3rd party (server):

   918 

   919 \begin{center}

   920 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}

   921 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\

   922 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\

   923 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\

   924 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\

   925 \end{tabular}

   926 \end{center}

   927 

   928 \end{frame}}

   929 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   930 

   931    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   932   \mode<presentation>{

   933   \begin{frame}[c]

   934   \frametitle{Sending Rule}

   935 

   936   \bl{\begin{center}

   937   \mbox{\infer{\Gamma \vdash Q \;\text{says}\; F}

   938               {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}}

   939   \end{center}}\bigskip\pause

   940   

   941   \bl{$P \,\text{sends}\, Q : F \dn$}\\

   942   \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}

   943 

   944   \end{frame}}

   945   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   946   

   947     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   948   \mode<presentation>{

   949   \begin{frame}[c]

   950   \frametitle{Trusted Third Party}

   951 

   952   \begin{center}