This directory (examples/joy) contains ProofFrog versions of constructions from Chapters 1 and 2 of The Joy of Cryptography by Mike Rosulek. Those aiming to learn how to do provable security proofs using ProofFrog may find it helpful to read those two chapters of Joy of Cryptography in parallel with the corresponding ProofFrog files.
| Book reference | Description | ProofFrog File |
|---|---|---|
| Chapter 1 | One-Time Pad and the Provable Security Mindset | |
| Construction 1.2.1 | One-Time Pad | examples/joy/Schemes/SymEnc/OTP.scheme |
| Claim 1.2.3 | OTP correctness | examples/joy/Games/SymEnc/Correctness.game, examples/joy/Proofs/Ch1/OTPCorrectness.proof |
| Chapter 2 | Rudiments of Provable Security | |
| Definition 2.5.1 | Symmetric-key encryption | examples/joy/Primitives/SymEnc.primitive |
| Definition 2.5.3 | One-time secrecy (real-or-random) | examples/joy/Games/SymEnc/OneTimeSecrecy.game |
| Example 2.5.4 | OTP has one-time secrecy | examples/joy/Proofs/Ch2/OTPSecure.proof |
| Construction 2.6.1 | Chained encryption | examples/joy/Schemes/SymEnc/ChainedEncryption.scheme |
| Claim 2.6.2 | Chained encryption has one-time secrecy | examples/joy/Proofs/Ch2/ChainedEncryptionSecure.proof |
| Definition 2.7.1 | One-time secrecy (left-or-right) | examples/joy/Games/SymEnc/OneTimeSecrecyLR.game |
| – | OTP has one-time secrecy (left-or-right) | examples/joy/Proofs/Ch2/OTPSecureLR.proof |
The following exercises from Joy of Cryptography are doable in ProofFrog. Solutions are not publicly available, but instructors can contact Douglas Stebila to get a copy.
| Book reference | Description |
|---|---|
| Chapter 2 | |
| Exercise 2.6 | Sampling difference of two uniform ModInt<q> values is uniform |
| Exercise 2.7 | Bitwise complement of a uniform bitstring is uniform |
| Exercise 2.8 | A || (A XOR B) is interchangeable with a uniform 2n-bit string |
| Exercise 2.9b | (A XOR B) || (B XOR C) is interchangeable with a uniform 2n-bit string |
| Exercise 2.17 | Chained encryption is correct |
| Exercise 2.21 | Encrypt-twice has one-time secrecy |
| Exercise 2.22 | Encrypt-halves has one-time secrecy |
| Exercise 2.23 | Double encryption has one-time secrecy |
| Exercise 2.24 | Real-or-random OTS implies left-or-right OTS |
| Exercise 2.25b | Append-zero scheme has left-or-right OTS |
| Exercise 2.26b | Double-ciphertext scheme has left-or-right OTS |
| Exercise 2.27 | Encrypt-then-ignore-input characterization of left-or-right OTS (both directions) |
| Exercise 2.28 | Swap-ciphertext characterization of left-or-right OTS (both directions) |