Source Files: nicodemus Tutorial
These are the input files for the nicodemus tutorial.
main.tex
\documentclass{article}
\usepackage[margin=1in,letterpaper]{geometry}
\usepackage{amsfonts,amsmath,amsthm}
\usepackage{xcolor}
\usepackage{nicodemus}
\usepackage[package=nicodemus]{texfrog}
\input{macros.tex}
\newtheorem{theorem}{Theorem}
%%% Game registration
\tfgames{indcpa}{G0, G1, Red1, G2, G3}
\tfgamename{indcpa}{G0}{G_0}
\tfgamename{indcpa}{G1}{G_1}
\tfgamename{indcpa}{Red1}{\Bdversary_1}
\tfgamename{indcpa}{G2}{G_2}
\tfgamename{indcpa}{G3}{G_3}
\tfdescription{indcpa}{G0}{$\INDCPA_\Enc^\Adversary()$: The IND-CPA game. The LR oracle encrypts using the actual PRF.}
\tfdescription{indcpa}{G1}{Replace $\mathrm{PRF}(k, r)$ with a truly random function $\RF(r)$.}
\tfdescription{indcpa}{Red1}{Reduction against PRF security, simulating Games \tfgamename{indcpa}{G0} and \tfgamename{indcpa}{G1} via an external PRF challenger.}
\tfdescription{indcpa}{G2}{Replace $\RF(r)$ with independently sampled randomness.}
\tfdescription{indcpa}{G3}{Ciphertext is uniformly random, independent of $m_b$.}
\tfreduction{indcpa}{Red1}
\tfrelatedgames{indcpa}{Red1}{G0, G1}
\tfmacrofile{macros.tex}
\tfmacrofile{nicodemus.sty}
\tfcommentary{indcpa}{G0}{commentary/G0.tex}
\tfcommentary{indcpa}{G1}{commentary/G1.tex}
\tfcommentary{indcpa}{Red1}{commentary/Red1.tex}
\tfcommentary{indcpa}{G2}{commentary/G2.tex}
\tfcommentary{indcpa}{G3}{commentary/G3.tex}
\tffigure{indcpa}[Games $\tfgamename{indcpa}{G0}$--$\tfgamename{indcpa}{G3}$, Reduction $\tfgamename{indcpa}{Red1}$]{all_games}{G0,G1,G2,G3,Red1}
%%% Proof source
\begin{tfsource}{indcpa}
\begin{tabular}[t]{l}
\nicodemusboxNew{250pt}{%
\tfonly*{G0}{\nicodemusheader{$\INDCPA_\Enc^\Adversary()$}}
\tfonly*{G1}{\nicodemusheader{Game~$\tfgamename{G1}$}}
\tfonly*{G2}{\nicodemusheader{Game~$\tfgamename{G2}$}}
\tfonly*{G3}{\nicodemusheader{Game~$\tfgamename{G3}$}}
\tfonly*{Red1}{\nicodemusheader{Reduction $\Bdversary_1^{\OPRF}$}}
\tffigonly{\nicodemusheader{Games $\tfgamename{G0}$--$\tfgamename{G3}$}}
\begin{nicodemus}
\tfonly{G0}{\item $k \getsr \{0,1\}^\lambda$}
\item $b \getsr \{0,1\}$
\item $b' \gets \Adversary^{\mathsf{LR}}()$
\item Return $(b' = b)$
\end{nicodemus}%
\medskip
\nicodemusheader{Oracle $\mathsf{LR}(m_0, m_1)$}
\begin{nicodemus}
\item $r \getsr \{0,1\}^\lambda$
\tfonly{G0}{\item $y \gets \mathrm{PRF}(k, r)$}
\tfonly{G1}{\item $y \gets \RF(r)$}
\tfonly{G2}{\item $y \getsr \{0,1\}^\lambda$}
\tfonly{Red1}{\item $y \gets \OPRF(r)$}
\tfonly{G0-G2}{\item $c \gets y \oplus m_b$}
\tfonly{G3}{\item $c \getsr \{0,1\}^\lambda$}
\item Return $(r, c)$
\end{nicodemus}%
}%
\end{tabular}%
\end{tfsource}
\title{IND-CPA Security of PRF-Based Symmetric Encryption\\
{\large A TeXFrog Tutorial (using the \texttt{nicodemus} package)}}
\author{}
\date{}
\begin{document}
\maketitle
\section{Construction}
Let $\mathrm{PRF}\colon \{0,1\}^\lambda \times \{0,1\}^\lambda \to \{0,1\}^\lambda$
be a pseudorandom function.
Define a symmetric encryption scheme $\Pi = (\mathsf{KeyGen}, \mathsf{Enc}, \mathsf{Dec})$ as follows:
\begin{itemize}
\item $\mathsf{KeyGen}()$: sample $k \getsr \{0,1\}^\lambda$ and return $k$.
\item $\mathsf{Enc}(k, m)$: sample $r \getsr \{0,1\}^\lambda$, compute
$c \gets \mathrm{PRF}(k, r) \oplus m$, and return $(r, c)$.
\item $\mathsf{Dec}(k, (r, c))$: return $\mathrm{PRF}(k, r) \oplus c$.
\end{itemize}
\section{Security}
\begin{theorem}
If\/ $\mathrm{PRF}$ is a secure pseudorandom function, then $\Pi$ is IND-CPA secure.
Concretely, for any adversary $\mathcal{A}$ making $q$ queries to the
left-or-right oracle,
\[
\mathbf{Adv}^{\mathrm{IND\text{-}CPA}}_\Pi(\mathcal{A})
\;\leq\;
\mathbf{Adv}^{\mathrm{PRF}}_{\mathrm{PRF}}(\mathcal{B}_1)
\;+\; \frac{q^2}{2^{\lambda+1}} \,.
\]
\end{theorem}
\noindent\textit{Proof.}\quad
We proceed via a sequence of games. Figure~\ref{fig:all-games} shows all the games, and the games are also shown individually in subsequent figures.
\begin{figure}[ht]
\centering
\tfrenderfigure{indcpa}{G0,G1,G2,G3,Red1}
\caption{Consolidated figure showing games $\tfgamename{indcpa}{G0}$--$\tfgamename{indcpa}{G3}$ and Reduction $\tfgamename{indcpa}{Red1}$.}
\label{fig:all-games}
\end{figure}
\paragraph{Game~$\tfgamename{indcpa}{G0}$.}
\input{commentary/G0.tex}
\begin{figure}[ht]
\centering
\tfrendergame{indcpa}{G0}
\caption{Game~$\tfgamename{indcpa}{G0}$: $\INDCPA_\Enc^\Adversary()$: The IND-CPA game. The LR oracle encrypts using the actual PRF.}
\label{fig:G0}
\end{figure}
...
\end{document}