Secret Sharing and Secure Distributed Matrix Multiplication🔗

This webpage is a documentation of the Lean formalization of secret sharing scheme and its application to distributed matrix multiplication. This is the content of the paper "A Lean Formalization of Perfect Secret Sharing and Secure Distributed Matrix Multiplication", to be presented in the 28th International Conference on Information and Communications Security Fukui, Japan.

Abstract. As distributed systems increasingly rely on advanced cryptographic primitives for privacy and fault tolerance, verifying the correctness of these protocols becomes paramount. Information-theoretic security proofs often depend on intricate linear algebraic properties and combinatorial structures that are prone to subtle errors in corner cases. In this paper, we present the first formalization of secret sharing schemes with general access structure in Lean 4 theorem prover. Our framework formalizes general monotone access structures and verifies Shamir’s scheme through Lagrange interpolation. The basic framework is then extended to secure distributed matrix multiplication. We introduce a modular hierarchy that decouples the abstract distributed protocol from its underlying cryptographic realization, allowing for reusable and extensible security proofs. Additionally, we explore an AI-assisted formalization methodology, demonstrating how Large Language Models can accelerate the generation of boilerplate algebraic structures. This work bridges the gap between abstract information-theoretic cryptography and verifiable software.

Contributors. Parts of the formalization were developed with assistance from Harmonic Aristotle and Gemini 3.1.

The Lean programs for this project can be found in this repo.