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

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

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

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

\item Alice only reveals the fact that she knows a secret, not the secret itself.\bigskip

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

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

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

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

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

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

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}

\begin{itemize}

\item ``grand chess master problem'' (person in the middle)

\item 

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{Other Methods for ZKPs}

\begin{itemize}

\item modular logarithms (you can 

\end{itemize}