Formalisations of proofs from The Joy of Cryptography in Coq, using SSProve.
Namely:
- Theorem 3.6 (Simple secret-sharing scheme)
- Theorems 3.8, 3.9, and 3.13 (Shamir's secret-sharing scheme)
- Claim 5.5 (Extending the Stretch of a PRG)
- Claim 5.10 (Symmetric Ratchet)
- Claim 6.3 (Constructing a PRG from a PRF)
- Claim 9.4 (CCA-secure encryption from a strong PRP)
- Claim 10.4 (A PRF is a MAC)
- Claim 10.10 (CCA-security from a MAC scheme)