Skip to content

examples.md

Latest commit

 

History

History
195 lines (134 loc) · 20.3 KB

examples.md

File metadata and controls

195 lines (134 loc) · 20.3 KB
title Examples
layout default
nav_order 3

Examples Catalogue

{: .no_toc }

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
  • TOC {:toc}

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
{: .table-labels }

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
{: .table-labels }

Basic constructions

Proof Description
ModOTP_INDOT The modular one-time pad ({% katex %}\mathrm{Enc}(k, m) = m + k \bmod q{% endkatex %}) has IND-OT Beginner
{: .table-labels }

PRF-based encryption

The PRF-based symmetric encryption scheme {% katex %}\Sigma{% endkatex %} encrypts a message {% katex %}m{% endkatex %} under key {% katex %}k{% endkatex %} by sampling a random {% katex %}r{% endkatex %} and outputting {% katex %}(r,; F(k, r) \oplus m){% endkatex %}, where {% katex %}F{% endkatex %} 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
{: .table-labels }

Composition of encryption schemes

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

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 {% katex %}T{% endkatex %} has IND-OT$, so does {% katex %}\Sigma{% endkatex %}
GeneralDoubleSymEnc_INDCPA$_MultiChal If {% katex %}T{% endkatex %} is IND-CPA$ (multi-challenge) secure, so is {% katex %}\Sigma{% endkatex %}

Authenticated encryption

Proof Description
EncryptThenMAC_INDCCA_MultiChal Encrypt-then-MAC is IND-CCA (multi-challenge) secure Rich example
{: .table-labels }

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
{: .table-labels }

KEM constructions

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

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
{: .table-labels }

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 {% katex %}(\mathit{ss}_1, c_1){% endkatex %} and {% katex %}(\mathit{ss}_2, c_2){% endkatex %}, then derives the combined shared secret as {% katex %}\mathit{ss} = F(\mathit{ss}_1, \mathit{ss}_2, \mathit{pk}_1 | c_1 | \mathit{pk}_2 | c_2){% endkatex %} using a two-key PRF {% katex %}F{% endkatex %}. 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
{: .table-labels }

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]({% link researchers/external-uses.md %}).