Examples Catalogue

The ProofFrog/examples repository contains a growing collection of cryptographic proofs verified by ProofFrog. This page organizes them by topic.

• Beginner denotes a proof that is a good starting point for learning ProofFrog
• Rich example denotes a substantial proof with multiple hops or techniques

---

• Joy of Cryptography (MIT Press Edition)
• Symmetric Encryption
  • Security notion implications
  • Basic constructions
  • PRF-based encryption
  • Composition of encryption schemes
  • Authenticated encryption
• Pseudorandom Generators
• Pseudorandom Functions
• Group-Based Assumptions
• Public-Key Encryption
  • Security notion implications
  • ElGamal
  • Hybrid public-key encryption
  • KEM constructions
• Research Applications
  • KEM Combiner (GHP18)
• Proof Ladders
• Old Joy of Cryptography Exercises (PDF Preview Edition)
• External Uses of ProofFrog

---

Joy of Cryptography (MIT Press Edition)

The examples/joy directory contains ProofFrog formulations of constructions from Chapters 1 and 2 of The Joy of Cryptography by Mike Rosulek. These are designed to be read alongside the textbook and are the best place to start learning ProofFrog.

Proof	Description
OTPCorrectness	One-time pad is correct (Claim 1.2.3)	Beginner
OTPSecure	One-time pad has one-time secrecy (Example 2.5.4)	Beginner
OTPSecureLR	One-time pad has left-or-right one-time secrecy	Beginner
ChainedEncryptionSecure	Chained encryption has one-time secrecy (Claim 2.6.2)	Beginner

Joy of Cryptography exercises. The README file about the Joy of Cryptography examples also lists exercises from Chapter 2 that are doable in ProofFrog — try them yourself! Solutions are not publicly available, but instructors can contact Douglas Stebila to obtain a copy.

---

Symmetric Encryption

Security notion implications

Proof	Description
INDOT$_implies_INDOT	IND-OT$ implies IND-OT	Beginner
INDCPA$_MultiChal_implies_INDCPA_MultiChal	IND-CPA$ (multi-challenge) security implies IND-CPA (multi-challenge) security

Basic constructions

Proof	Description
ModOTP_INDOT	The modular one-time pad ($\mathrm{Enc}(k, m) = m + k \bmod q$) has IND-OT	Beginner

PRF-based encryption

The PRF-based symmetric encryption scheme $\Sigma$ encrypts a message $m$ under key $k$ by sampling a random $r$ and outputting $(r,\; F(k, r) \oplus m)$, where $F$ is a PRF.

Proof	Description
SymEncPRF_INDOT$	PRF-based symmetric encryption has IND-OT$
SymEncPRF_INDCPA$_MultiChal	PRF-based symmetric encryption is IND-CPA$ (multi-challenge) secure	Rich example

Composition of encryption schemes

Given two symmetric encryption schemes $S$ and $T$ where $S.\mathcal{C} = T.\mathcal{M}$, the composed scheme encrypts as $\Sigma.\mathrm{Enc}((k_S, k_T), m) = T.\mathrm{Enc}(k_T, S.\mathrm{Enc}(k_S, m))$.

Proof	Description
INDOT$_implies_DoubleSymEnc_INDOT$	If a scheme has IND-OT$, then double-encrypting with two copies of it also has IND-OT$
GeneralDoubleSymEnc_INDOT$	If $T$ has IND-OT$, so does $\Sigma$
GeneralDoubleSymEnc_INDCPA$_MultiChal	If $T$ is IND-CPA$ (multi-challenge) secure, so is $\Sigma$

Authenticated encryption

Proof	Description
EncryptThenMAC_INDCCA_MultiChal	Encrypt-then-MAC is IND-CCA (multi-challenge) secure	Rich example

---

Pseudorandom Generators

Proof	Description
TriplingPRG_PRGSecurity	A length-tripling PRG built by applying a length-doubling PRG twice is secure
CounterPRG_PRGSecurity	A counter-mode PRG built from a PRF is secure

---

Pseudorandom Functions

Proof	Description
PRFSecurity_implies_PRFSecurity_MultiKey	Multi-key PRF security follows from single-key PRF security via a hybrid argument

---

Group-Based Assumptions

These proofs establish implications between Diffie–Hellman-type assumptions.

Proof	Description
DDH_implies_CDH	DDH implies CDH
DDH_implies_HashedDDH	DDH implies Hashed DDH (standard model)
CDH_implies_HashedDDH	CDH implies Hashed DDH (random oracle model)
DDHMultiChal_implies_HashedDDHMultiChal	DDH (multi-challenge) implies Hashed DDH (multi-challenge) (random oracle model)

---

Public-Key Encryption

Security notion implications

Proof	Description
INDCPA_implies_INDCPA_MultiChal	IND-CPA implies IND-CPA (multi-challenge) for public-key encryption

ElGamal

Proof	Description
ElGamal_Correctness	ElGamal encryption is correct
ElGamal_INDCPA_MultiChal	ElGamal is IND-CPA (multi-challenge) secure under DDH (multi-challenge)
HashedElGamal_INDCPA_MultiChal	Hashed ElGamal is IND-CPA (multi-challenge) secure under Hashed DDH (multi-challenge) (standard model)
HashedElGamal_INDCPA_ROM_MultiChal	Hashed ElGamal is IND-CPA (multi-challenge) secure under DDH (multi-challenge) (random oracle model)

Hybrid public-key encryption

Proof	Description
HybridKEMDEM_INDCPA_MultiChal	KEM-DEM hybrid public-key encryption is IND-CPA (multi-challenge) secure	Rich example
HybridPKEDEM_INDCPA_MultiChal	PKE+SymEnc hybrid public-key encryption is IND-CPA (multi-challenge) secure	Rich example

KEM constructions

The KEMPRF construction derives the shared secret by applying a PRF to the underlying KEM’s shared secret and ciphertext: $\mathit{ss'} = F(k_F, \mathit{ss} \| c)$.

Proof	Description
KEMPRF_Correctness	KEMPRF is correct
KEMPRF_INDCPA	KEMPRF is IND-CPA (multi-challenge) secure
KEMPRF_INDCCA	KEMPRF is IND-CCA (multi-challenge) secure	Rich example

---

Research Applications

KEM Combiner (GHP18)

A ProofFrog formalization of the KEM combiner from Giacon, Heuer, and Poettering (PKC 2018). The combiner encapsulates with two KEMs independently, obtaining $(\mathit{ss}_1, c_1)$ and $(\mathit{ss}_2, c_2)$, then derives the combined shared secret as $\mathit{ss} = F(\mathit{ss}_1, \mathit{ss}_2, \mathit{pk}_1 \| c_1 \| \mathit{pk}_2 \| c_2)$ using a two-key PRF $F$. The combined KEM is secure as long as at least one of the component KEMs is secure.

See the full README for construction details and a list of all files.

Proof	Description
GHP18_Correctness	The KEM combiner is correct
GHP18_INDCPA1	IND-CPA (multi-challenge) security from security of the first component KEM	Rich example
GHP18_INDCPA2	IND-CPA (multi-challenge) security from security of the second component KEM	Rich example

---

Proof Ladders

The Proof Ladders project includes an example showing CPA security of KEM-DEM in both ProofFrog and EasyCrypt, which is helpful for seeing how proofs in ProofFrog compare to proofs in more advanced formal verification tools like EasyCrypt. Note that that version of the ProofFrog KEM-DEM proof uses a slightly different formulation compared to the example linked earlier on this page.

---

Old Joy of Cryptography Exercises (PDF Preview Edition)

The examples/joy_old directory contains ProofFrog proofs of selected exercises from the older PDF preview edition of The Joy of Cryptography. These use an older syntax; for new work, prefer the examples in examples/joy above.

Exercise	Description	Proof
Claim 2.13	Double one-time pad has OTUC	2_13
Claim 5.4	Pseudo one-time pad has OTUC	5_3
Exercise 2.13	One-time secrecy of the double symmetric encryption scheme	2_13
Exercise 2.14	Alternative characterization of one-time secrecy	forward, backward
Exercise 2.15	Another alternative characterization of one-time secrecy	forward, backward
Exercise 5.8	Security of PRG constructions	a, b, e, f; also Pseudo-OTP OTUC
Exercise 5.10	Security of a PRG construction	5_10
Exercise 7.13	Alternative characterization of CPA security	forward, backward
Exercise 9.6	CCA$ security implies CCA security	9_6

---

External Uses of ProofFrog

A list of external projects and papers using ProofFrog is maintained on the external uses page.