TeXFrog Tutorial (nicodemus)

View interactive demo

Package

This tutorial uses nicodemus. For the same proof using cryptocode (the default, with a more detailed walkthrough), see Tutorial: cryptocode.

This tutorial contains the same IND-CPA proof as the cryptocode tutorial, rewritten for the nicodemus pseudocode package. Comparing the two shows the key syntax differences.

The Proof Scenario

Scheme. A symmetric encryption scheme:

Enc(k, m)  =  (r, PRF(k, r) XOR m)    where r is fresh per call
Dec(k, (r, c))  =  PRF(k, r) XOR c

Theorem. Enc is IND-CPA secure if PRF is a secure pseudorandom function.

Proof. Via a three-hop game sequence:

G0 (Real)  ~_PRF  G1  ~_birthday  G2  =  G3 (Ideal)
Game What changes
G0 Oracle computes y <- PRF(k, r), returns (r, y XOR m_b)
G1 Oracle computes y <- RF(r) (truly random function), returns (r, y XOR m_b)
G2 Oracle samples y at random, returns (r, y XOR m_b)
G3 Oracle samples c directly (message not used)
Red1 Reduction: replaces PRF call by querying an external challenger

G0 to G1 is by PRF security (via Red1). G1 to G2 is by a birthday bound on nonce collisions. G2 to G3 is a perfect equivalence.

Files

File Purpose
main.tex Single source file: declares games, contains pseudocode with \tfonly tags, and renders output
macros.tex Short macro definitions (no external dependencies)
nicodemus.sty The nicodemus pseudocode package
commentary/*.tex Per-game commentary files (LaTeX)

See the Source Files page for the full contents of main.tex.

Key Differences from the cryptocode Tutorial

The .tex file structure is the same (game registration, tfsource environment, rendering commands). The main differences are in the pseudocode syntax:

  1. \usepackage[package=nicodemus]{texfrog} selects the nicodemus package profile.
  2. nicodemus.sty is listed via \tfmacrofile{nicodemus.sty} (.sty files are copied to the build directory for \usepackage but are not \input-ed).

The source syntax differs substantially:

cryptocode nicodemus
\begin{pcvstack}[boxed] \begin{tabular}[t]{l} + \nicodemusboxNew{250pt}{%
\procedure[linenumbering]{Name}{ \nicodemusheader{Name}
k \getsr \{0,1\}^\lambda \\ \item $k \getsr \{0,1\}^\lambda$
\pcreturn (b' = b) \item Return $(b' = b)$
} (closing procedure) \end{nicodemus}%

Key points:

  • Text mode: nicodemus environments are text-mode, so math content needs explicit $...$.
  • \item prefix: Each pseudocode line starts with \item (nicodemus uses enumerate). The \item is kept outside \tfchanged{} to preserve list structure.
  • No \\ separators: List items are naturally separated.
  • \nicodemusheader: Procedure headers use \nicodemusheader{...} above \begin{nicodemus} blocks. Like cryptocode’s \procedure{...}{ syntax, \nicodemusheader lines are never wrapped in \tfchanged.

The Proof Source (main.tex)

Lines with no tag appear in every game 

\item $b \getsr \{0,1\}$
\item $b' \gets \Adversary^{\mathsf{LR}}()$
\item Return $(b' = b)$

Lines with a tag appear only in named games 

\tfonly{G0,G1-G3}{\item $k \getsr \{0,1\}^\lambda$}

Consecutive variant lines encode “slots”

The y computation is a four-way slot:

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

For each game, at most one of these lines survives filtering. They are consecutive, so the chosen line always appears at the right position.

Procedure headers

In nicodemus, procedure headers use \nicodemusheader{...} above \begin{nicodemus} environments:

\tfonly*{G0}{\nicodemusheader{$\INDCPA_\Enc^\Adversary()$}}
\tfonly*{G1}{\nicodemusheader{Game~$\tfgamename{G1}$}}

Running the Tutorial

Compiling with pdflatex (no Python needed)

The .tex file compiles directly with pdflatex. You just need texfrog.sty and nicodemus.sty in the same directory:

cd examples/tutorial-nicodemus
pdflatex main.tex

This also works on Overleaf — upload texfrog.sty, nicodemus.sty, main.tex, macros.tex, and the commentary/ files to a project and compile.

Building the HTML viewer (requires Python CLI)

If you have the Python CLI installed, you can also build an interactive HTML viewer:

# Build an interactive HTML viewer
texfrog html build examples/tutorial-nicodemus/main.tex -o /tmp/tf_tutorial_nic_html

# Or build and open in your browser with live reload
texfrog html serve examples/tutorial-nicodemus/main.tex

Or view the pre-built interactive demo.

What \tfchanged Looks Like

The default highlight macro for nicodemus:

\providecommand{\tfchanged}[1]{\colorbox{blue!15}{#1}}

No $...$ wrapping — unlike cryptocode, nicodemus content is text-mode. The \item prefix is kept outside \tfchanged:

\item \tfchanged{$y \getsr \{0,1\}^\lambda$}

Next Steps

Table of contents