Joclean

The (very) starter code for formalizing the Joy of Cryptography in Lean4, made as a final project for the PROOF101 course led by Daniel Dia.

Overview

Current state of repository contains single proof of Claim 1.4.1 from the book which claims that the OTP encryption is uniformly distributed over the n-bit strings.

Unfortunatelly I did not manage to complete the general library abstraction implementation (Interface, Library, Adversary), but it is defined in the Future Work section.

Design Choices

Currently there are 2 primary design choices:

• Use of BitVec - the Lean4 builtin for working over bit strings, with isomorphism to the Fin 2^n type.
• Use of PMF to describe the uniform distribution over the BitVec n, defined as PMFBitVec.

Main Theorems

The single main theorem proven in this chapter is the Claim 1.4.1 which states that output of the OTP encryption is uniformly distributed.

Proof Strategies

Following key steps were used to prove the Claim 1.4.1:

• Rewriting the PMF: PMF.ext_iff and PMF.map_apply to convert the monadic PMF type into a tsum object with if-then-else expression
• Definiting a k' = m ^^^ c as the "valid" key, that matches plaintext m and ciphertext c with let and have to obtain a useful simplification hypthesis.
• Solving goal #1: the case when k = k', we have the "right" valid key which encrypted the ciphertext
• Solving goal #2: the case when k != k', we prove by contradiction obtaining both k = k' and k != k' in our state, finishing with the exfalso tactic, to turn our goal to False.
• For both #1 and #2 we use BitVec.xor useful theorems like xor_comm, xor_assoc and xor_right_inj.

Challenges

The primary challenge was to getting started with the PMF object - it was new for me, it is a monadic type and it was hard to deteremine what could I really "use" for the proofs. There are also not many resources that explain how to use this structure in the proofs, except for the [4]. The important chaning moment for me was to convert the PMF into the tsum and take it from there via the 2 possible cases for the if-then-else expression.

I also had problems at the start to define the BitVec as a Fintype to use the PMF.uniformOfFintype. The BitVec contains the isomorphism to the Fin (2^n), however from what I uderstand the Lean4 does not infer this automatically, hence the explicit instance is required here.

The other main difficulty was designing the Interface, Library and Adversary abstraction. It turned out that its hard to find a balance between designing a DSL (domain-specific language) and re-using the Mathblib4 structures to be usable for all proofs in the book. After researching the VCVio [2] implementation, I realized that the Library must be similar to the OracleComp monadic structure. This turned out to consume much more time then I've originally expected.

Future Work

The next step is to wrap the Claim 1.4.1 into the library abstraction in order to obtain to prove Claim 2.2.2.

To complete this task a more time is required to understand deeper the structure of OracleComp used in the VCVio and the related GameEquiv. It seems that the structure used in VCVio are very similar to the library-based approach presented in the Joy of Cryptography, however with some minor differences.

References

• [1] The Joy of Cryptography - Mike Rosulek, https://joyofcryptography.com/
• [2] Formally Verified Cryptography Proofs in Lean 4, https://github.com/Verified-zkEVM/VCV-io
• [3] Computationally-Sound Symbolic Cryptography in Lean - Stefan Dziembowski and Grzegorz Fabiański and Daniele Micciancio and Rafał Stefański, https://eprint.iacr.org/2025/1700
• [4] Basic probability in Mathlib, https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/