Examples

All examples compile directly with pdflatex — no Python needed. Just place texfrog.sty in the same directory.

TeXFrog ships with tutorials that implement the same IND-CPA game-hopping proof using different pseudocode packages. Comparing them side by side shows the syntax differences between cryptocode and nicodemus.

Both tutorials prove IND-CPA security of a PRF-based symmetric encryption scheme via a three-hop game sequence with 4 games and 1 reduction.

We also have a demo of TeXFrog for a key exchange model, specifically a signed-Diffie–Hellman key exchange protocol. This is extracted from Section 3.1 of a technical report by Doreen Riepel and Paul Rösler for the proof-ladders project.

Example	Pseudocode Package	Source Files	Live Demo
Tutorial: cryptocode quickstart	cryptocode	N/A	N/A
Tutorial: cryptocode	cryptocode	Source	View demo
Tutorial: nicodemus	nicodemus	Source	View demo
Multiple proofs	cryptocode	N/A	N/A
Signed DH proof	nicodemus	N/A	View demo

Warning

The TeXFrog version of the Signed DH proof was generated automatically by having an LLM extract the metadata about which lines belong in which games/reductions from the LaTeX source code in the authors’ paper. On the one hand, it’s awesome that this can be done automatically. On the other hand, this extraction has not been checked for correctness against the original authors’ paper, so don’t rely on it for scientific purposes; it’s here solely for visual demonstration purposes.