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.

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 $\Sigma$ that composes two symmetric encryption schemes $S$ and $T$ where $S.C = T.M$, and $\Sigma.\mathrm{KeyGen}() = (S.\mathrm{KeyGen()}, T.\mathrm{KeyGen()})$ $\Sigma.\mathrm{Enc}((k_S, k_T), m) = T.\mathrm{Enc}(k_T, S.\mathrm{Enc}(k_S, m))$ $\Sigma.\mathrm{Dec}((k_S, k_T), c) = S.\mathrm{Dec}(k_S, T.\mathrm{Dec}(k_T, c))$

If $T$ has one-time uniform ciphertexts, then so does $\Sigma$. The proof file can be found here

Composing Two Symmetric Encryption Schemes for CPA$ security

This proof analyzes the same encryption scheme $\Sigma$ as in the prior heading. If $T$ is CPA$ secure, then so is $\Sigma$. 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.

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.