examples.md

title	layout	nav_order
Examples	default	4

Examples

Below are a list of examples that ProofFrog can currently verify. Many are adapted from The Joy of Cryptography. In such cases, we will indicate which claim in the textbook is being proved. References and examples are from the old PDF preview version, and need to be updated to the final print edition.

One-Time Uniform Ciphertexts implies One-Time Secrecy

This proves Theorem 2.15.

The proof file can be found here.

CPA$ Security implies CPA Security

This proves Claim 7.3.

The proof file can be found here.

Composing Two Symmetric Encryption Schemes for One-Time Uniform Ciphertexts

This proof analyzes a symmetric encryption scheme {% katex %}\Sigma{% endkatex %} that composes two symmetric encryption schemes {% katex %}S{% endkatex %} and {% katex %}T{% endkatex %} where {% katex %}S.C = T.M{% endkatex %}, and {% katex display %} \Sigma.\mathrm{KeyGen}() = (S.\mathrm{KeyGen()}, T.\mathrm{KeyGen()}) {% endkatex %} {% katex display %} \Sigma.\mathrm{Enc}((k_S, k_T), m) = T.\mathrm{Enc}(k_T, S.\mathrm{Enc}(k_S, m)) {% endkatex %} {% katex display %} \Sigma.\mathrm{Dec}((k_S, k_T), c) = S.\mathrm{Dec}(k_S, T.\mathrm{Dec}(k_T, c)) {% endkatex %}

If {% katex %}T{% endkatex %} has one-time uniform ciphertexts, then so does {% katex %}\Sigma{% endkatex %}. The proof file can be found here.

OTUC implies Double OTUC

If a symmetric encryption scheme has one-time uniform ciphertexts, then the double encryption scheme (composing two copies of it) also has one-time uniform ciphertexts. The proof file can be found here.

Composing Two Symmetric Encryption Schemes for CPA$ security

This proof analyzes the same encryption scheme {% katex %}\Sigma{% endkatex %} as in the prior heading. If {% katex %}T{% endkatex %} is CPA$ secure, then so is {% katex %}\Sigma{% endkatex %}. The proof file can be found here.

Double One-Time Pad has One-Time Uniform Ciphertexts

This proves Claim 2.13.

The proof file can be found here.

Pseudo One-Time Pad has One-Time Uniform Ciphertexts

This proves Claim 5.4.

The proof file can be found here.

Pseudorandomness of a length-tripling PRG

This proves Claim 5.5.

The proof file can be found here.

One-Time Secrecy implies CPA Security for Public Key Encryption Schemes

This proves Claim 15.5.

The proof file can be found here.

KEM-DEM Hybrid Encryption is CPA secure

This proves CPA security of the hybrid public key encryption scheme constructed via the KEM-DEM paradigm, assuming CPA security of the KEM and one-time secrecy of the symmetric encryption scheme.

The proof file can be found here.

Hybrid Encryption is CPA secure

This proves Claim 15.9.

The proof file can be found here.

Encrypt-then-MAC is CCA secure

This proves Claim 10.10.

The proof file can be found here.

Textbook Exercises

The following are ProofFrog proofs of exercises from The Joy of Cryptography.

Exercise 2.13

One-time secrecy of the double symmetric encryption scheme. The proof file can be found here.

Exercise 2.14

An alternative characterization of one-time secrecy. Proved in both directions: forward and backward.

Exercise 2.15

Another alternative characterization of one-time secrecy. Proved in both directions: forward and backward.

Exercise 5.8

Security of various PRG constructions. Parts: a, b, e, f. Also, Pseudo-OTP has OTUC (used in part e).

Exercise 5.10

Security of a PRG construction. The proof file can be found here.

Exercise 7.13

An alternative characterization of CPA security. Proved in both directions: forward and backward.

Exercise 9.6

CCA$ security implies CCA security. The proof file can be found here.