Advancement could lead to more secure, faster online financial transactions and other high-value information exchanges.
A groundbreaking development in modern cryptography is the concept of zero‐knowledge proofs. These proofs are protocols that allow one party — the prover — to convince another party — the verifier — that a statement is true without revealing any information beyond the validity of the statement itself. These protocols are critical for secure financial transactions and sensitive information exchanges, like those conducted by the Department of Defense.
Traditionally, zero-knowledge protocols have been challenging to implement efficiently in real-world applications because they are highly computationally intensive. Addressing this challenge was one of the main goals of the Defense Advanced Research Projects Agency’s (DARPA) Securing Information for Encrypted Verification and Evaluation (SIEVE) program.
“The SIEVE program was very prolific in the production of zero-knowledge papers and software,” said Vitor Pereira, an advanced computer scientist in SRI’s Computer Science Laboratory. “What sets our work apart is that we developed mathematically verified implementations of these cryptographic protocols while matching the speed of unverified approaches.”
“We developed mathematically verified implementations of these protocols while matching the speed of unverified approaches.” — Vitor Pereira
The bottom-line outcome is that the mathematics of these protocols have been formalized and machine-checked, and the implementations have been extracted from the formalizations, leaving no room for manual coding mistakes. This provides high assurance that the implemented protocols behave as intended, functioning correctly and securely.
Pereira added: “The larger goal of such computer-aided cryptography is to gain control of the complexity of security proofs while assuring that security properties are preserved,” highlighting the two papers describing techniques SRI used to verify their zero-knowledge proofs.
The team’s first paper in the SIEVE program introduced the first machine-checked implementation of the “Multiparty Computation in the Head” (MitH) approach to zero-knowledge. This work created the possibility of producing mathematically verified implementations of generic zero-knowledge protocols.
The second paper addressed some core performance challenges of machine-checked cryptography with a formal way to leverage parallelism and produce implementations with optimized memory access. This resulted in a 3,000-fold improvement in execution speed compared to previous verified implementations, matching the performance of unverified, manually coded approaches.
In addition to the published papers, the team made their work available to the broader community via an open-source library called EVOCrypt.
“We are now refining our techniques and extending the reach of our work to new areas, including potential applications in quantum computing,” Pereira said. “That could prove to be an interesting direction for this research.”
Distribution Statement A: Approved for public release, distribution unlimited.
