\documentclass[dvipsnames,14pt,t]{beamer}

\usepackage{proof}

\usepackage{beamerthemeplaincu}

\usepackage{mathpartir}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage[absolute,overlay]{textpos}

\usepackage{ifthen}

\usepackage{tikz}

\usepackage{courier}

\usepackage{listings}

\usetikzlibrary{arrows}

\usetikzlibrary{positioning}

\usetikzlibrary{calc}

\usepackage{graphicx} 

\usetikzlibrary{shapes}

\usetikzlibrary{shadows}

\usetikzlibrary{plotmarks}

\isabellestyle{rm}

\renewcommand{\isastyle}{\rm}%

\renewcommand{\isastyleminor}{\rm}%

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

\renewcommand{\isatagproof}{}

\renewcommand{\endisatagproof}{}

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

% 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}

% beamer stuff 

\renewcommand{\slidecaption}{APP 09, King's College London, 3 December 2013}

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

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

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}<1>[t]

\frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \\

  \LARGE Access Control and \\[-3mm] 

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

  \end{tabular}}\bigskip\bigskip\bigskip

  \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<presentation>{

\begin{frame}[c]

\frametitle{Review: Proofs}

Modify the formula

\begin{center}

\begin{tabular}{l}

\bl{$P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$}\\

\end{tabular}

\end{center}

using security levels so that it satisfies the {\it write rule} from the {\it

Bell-LaPadula} access policy.\bigskip 

Do the same again, but satisfy the {\it write rule}

from the {\it Biba} access policy.

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Review: Proofs}

Assume two security levels \bl{$\textit{S}$} and \bl{$\textit{TS}$}, 

which are ordered so that \bl{$slev(\textit{S}) < slev(\textit{TS})$}. 

Assume further the substitution rules

\begin{center}

\bl{\begin{tabular}{@{}c@{}}

$\Gamma \vdash slev(P) = l_1$ \hspace{2mm} $\Gamma \vdash slev(Q) = l_2$

\hspace{2mm} $\Gamma \vdash l_1 < l_2$\\\hline

$\Gamma \vdash slev(P) < slev(Q)$

\end{tabular}}

\end{center}

\begin{center}

\bl{\begin{tabular}{c}

$\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline

$\Gamma \vdash slev(P) = slev(Q)$

\end{tabular}}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Review: Proofs}\small

Let \bl{$\Gamma$} be the set containing the following six formulas

\begin{center}

\bl{\begin{tabular}{@{}l@{}}

$slev(\textit{S}) < slev(\textit{TS})$\smallskip\\

$slev(\textit{Agent}) = slev(\textit{TS})$\smallskip\\

$slev(\textit{File}_1) = slev(\textit{S})$\smallskip\\

$slev(\textit{File}_2) = slev(\textit{TS})$\smallskip\\

$\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow$\\ 

\hspace{30mm}$(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\

$\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow$\\ 

\hspace{30mm}$(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\

\end{tabular}}

\end{center}

Using the inference rules of access-control logic and the substitution rules shown above,

give proofs for the two judgements

\begin{center}

\bl{\begin{tabular}{@{}l@{}}

$\Gamma \vdash

(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1,

\textit{read})) \Rightarrow$\\

\hspace{50mm}$\textit{Permitted}(\textit{File}_1, \textit{read})$\\

\end{tabular}}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[t]

\frametitle{Checking Solutions}

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

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

want to tell Bob.\medskip

You use an English  dictionary:

\begin{itemize}

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

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

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

\only<3>{

\begin{quote}

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

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

\end{quote}}

\only<4>{

\begin{quote}

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

\end{quote}}

\only<5>{

\begin{quote}

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

\end{quote}}

\end{itemize}\bigskip\bigskip

\only<7->{

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

}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Zero-Knowledge Proofs}

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

\begin{itemize}

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

she can convince Bob that she knows the secret).\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<presentation>{

\begin{frame}[t]

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

\begin{center}

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

\\[-10mm]

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

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

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

\end{tabular}

\end{center}

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

The Alibaba cave:

\end{textblock}

\small

\only<2>{

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

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

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

\end{textblock}}

\only<3>{

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

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

\end{textblock}}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Applications of ZKPs}

\begin{itemize}

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

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

party to learn anything about this secret\bigskip

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

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

correct according to the protocol

\end{itemize}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Central Properties}

Zero-knowledge proof protocols should satisfy:\bigskip

\begin{itemize}

\item \alert{\bf Completeness} If Alice knows the secret, Bob accepts Alice ``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<presentation>{

\begin{frame}[c]

\frametitle{Graph Isomorphism}

\begin{center}

\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<presentation>{

\begin{frame}[c]

\frametitle{Graph Isomorphism Protocol}

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

\begin{enumerate}

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

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

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

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

\end{enumerate}\pause

these are called commitment algorithms

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Graph Isomorphism Protocol (2)}

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

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

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

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

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

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Graph Isomorphism Protocol (3)}

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

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

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

Anything Bob can compute using the information obtained from 

the transcript can be computed using only a forged transcript and 

therefore participation in such a communication does not increase 

Bob's capability  to perform any computation.

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Non-Interactive ZKPs}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Non-Interactive ZKPs (2)}

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

\begin{enumerate}

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

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

	the output will be)

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

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

\end{enumerate}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Problems of ZKPs}

\begin{itemize}

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

(person in the middle)\bigskip

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

\end{itemize}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Other Methods for ZKPs}

Essentially every NP-problem can be used for ZKPs

\begin{itemize}

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

\begin{center}

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

\end{center} 

\end{itemize}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Commitment Stage}

\begin{enumerate}

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

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

\begin{center}

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

\end{center}

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

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

\begin{center}

\begin{tabular}{ll}

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

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

\end{tabular}

\end{center}

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

\end{enumerate}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Confirmation Stage}

\begin{enumerate}

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

\begin{center}

\begin{tabular}{ll}

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

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

\end{tabular}

\end{center}\bigskip

Bob was send 

\begin{center}

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

\end{center}

where the corresponding bits were 

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

\end{enumerate}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Proving Stage}

\begin{enumerate}

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

she sends

\begin{center}

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

\end{center}

\item Bob confirms

\begin{center}

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

\end{center}

\end{enumerate}\bigskip\pause

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

chance. \\

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

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Random Number Generators}

\begin{itemize}

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