% !TeX root = easycrypt.tex

\chapter{Advanced Examples}

\section{Building a PRG from a PRF}
\input{prg}


%\section{Public Key Encryption Schemes}
%\subsection{A first glance at \citet{Bellare:1993}\label{sec:tutorial}}
%\input{br93}

%%\subsection{Another Look at \citet{Bellare:1993}}
%%In this Section, we return on the example proof discussed in
%%Section~\ref{sec:tutorial} and rewrite it making use of the standard library and
%%advanced features of \EasyCrypt presented in this manual. The corresponding
%%\EasyCrypt \href{file:../examples/br93.ec}{proof script} can be found in the
%%public repository.

\subsection{El Gamal}
A security \href{file:../examples/elgamal.ec}{proof} for the El Gamal encryption scheme is available in the public
repository.

\subsection{Hashed El Gamal}
A security \href{file:../examples/hashed_elgamal.ec}{proof} for the hashed El Gamal encryption scheme is available in the
public repository. \href{file:../examples/hashed_elgamal_generic.ec}{Another version} illustrates the use of some generic game transformations.
%\subsection{OAEP}

%\section{Public Key Signature Schemes}
%\subsection{FDH}
%\subsection{PSS}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "easycrypt"
%%% End: