Source Files: cryptocode Tutorial

These are the input files for the cryptocode tutorial.

main.tex

\documentclass{article}

\usepackage[margin=1in,letterpaper]{geometry}
\usepackage[n,advantage,operators,sets,adversary,landau,probability,notions,logic,ff,mm,primitives,events,complexity,oracles,asymptotics,keys]{cryptocode}
\usepackage{amsfonts,amsmath,amsthm}
\usepackage[package=cryptocode]{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}

\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{pcvstack}[boxed]
  \procedure[linenumbering]{%
    \tfonly*{G0}{Game $\tfgamename{G0} = \INDCPA_\Enc^\Adversary()$}%
    \tfonly*{G1}{Game $\tfgamename{G1}$}%
    \tfonly*{G2}{Game $\tfgamename{G2}$}%
    \tfonly*{G3}{Game $\tfgamename{G3}$}%
    \tfonly*{Red1}{Reduction $\Bdversary_1^{\OPRF}$}%
    \tffigonly{Games $\tfgamename{G0}$--$\tfgamename{G3}$}%
  }{
    \tfonly{G0}{k \getsr \{0,1\}^\lambda \\}
    b \getsr \{0,1\} \\
    b' \gets \Adversary^{\mathsf{LR}}() \\
    \pcreturn (b' = b)
  }
  \pclb
  \procedure[linenumbering]{$\mathsf{LR}(m_0, m_1)$}{
    r \getsr \{0,1\}^\lambda \\
    \tfonly{G0}{y \gets \mathrm{PRF}(k, r) \\}
    \tfonly{G1}{y \gets \RF(r) \\}
    \tfonly{G2}{y \getsr \{0,1\}^\lambda \\}
    \tfonly{Red1}{y \gets \OPRF(r) \\}
    \tfonly{G0-G2}{c \gets y \oplus m_b \\}
    \tfonly{G3}{c \getsr \{0,1\}^\lambda \\}
    \pcreturn (r, c)
  }
\end{pcvstack}
\end{tfsource}

\title{IND-CPA Security of PRF-Based Symmetric Encryption\\
{\large A TeXFrog Tutorial (using the \texttt{cryptocode} 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}