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)

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 (Enc(k,m)=m+k mod q\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 mm under key kk by sampling a random rr and outputting (r,  F(k,r)⊕m)(r,\; F(k, r) \oplus m), where FF 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 SS and TT where S.C=T.MS.\mathcal{C} = T.\mathcal{M}, the composed scheme encrypts as Σ.Enc((kS,kT),m)=T.Enc(kT,S.Enc(kS,m))\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 TT has IND-OT$, so does Σ\Sigma
GeneralDoubleSymEnc_INDCPA$_MultiChal If TT 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)
GapCDH_implies_GapCDH_NZ gap-CDH implies its non-zero-exponent variant (used as a lemma in the Hashed ElGamal KEM proof)

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: ss′=F(kF,ss∥c)\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
HashedElGamalKEM_INDCCA The Hashed ElGamal KEM is IND-CCA (multi-challenge, ROM) secure under gap-CDH in the random oracle model Rich example

Research Applications

CFRG Hybrid KEM Combiners (draft-irtf-cfrg-hybrid-kems-10)

A ProofFrog formalization of the four hybrid PQ/T KEM combiners specified in the IRTF CFRG draft Hybrid PQ/T Key Encapsulation Mechanisms. Each framework combines a post-quantum KEM with a “traditional” component — either another KEM or a nominal group — via a key-derivation function: UG and CG use a nominal group, UK and CK use a second KEM; U(niversal) and C(2PRI) name the two combiner constructions. Each is modelled in two variants (a seed-form matching the draft’s primary definition and an expanded-form cache), giving machine-checked proofs of correctness, IND-CCA security (for both the post-quantum and traditional branches), and the LEAK-BIND and HON-BIND binding properties.

This case study motivated much of the new lazy-map random-oracle and group-exponent machinery in the 0.5.0 engine. The full README documents the modelling choices, the mapping from draft sections to files, and the assumptions each proof relies on (including important caveats about implicit rejection and the absence of a quantum-attacker model).

See the applications/cfrg-hybrid-kems/ directory for all scheme definitions, games, and proofs.

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 (ss1,c1)(\mathit{ss}_1, c_1) and (ss2,c2)(\mathit{ss}_2, c_2), then derives the combined shared secret as ss=F(ss1,ss2,pk1∥c1∥pk2∥c2)\mathit{ss} = F(\mathit{ss}_1, \mathit{ss}_2, \mathit{pk}_1 \| c_1 \| \mathit{pk}_2 \| c_2) using a two-key PRF FF. 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.

This site uses Just the Docs, a documentation theme for Jekyll.