Paper 2023/1322

Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge

Samuel Dittmer, Stealth Software Technologies
Karim Eldefrawy, SRI International
Stéphane Graham-Lengrand, SRI International
Steve Lu, Stealth Software Technologies
Rafail Ostrovsky, University of California, Los Angeles
Vitor Pereira, SRI International

Despite the notable advances in the development of high-assurance, verified implementations of cryptographic protocols, such implementations typically face significant performance overheads, particularly due to the penalties induced by formal verification and automated extraction of executable code. In this paper, we address some core performance challenges facing computer-aided cryptography by presenting a formal treatment for accelerating such verified implementations based on multiple generic optimizations covering parallelism and memory access. We illustrate our techniques for addressing such performance bottlenecks using the Line-Point Zero-Knowledge (LPZK) protocol as a case study. Our starting point is a new verified implementation of LPZK that we formalize and synthesize using EasyCrypt; our first implementation is developed to reduce the proof effort and without considering the performance of the extracted executable code. We then show how such (automatically) extracted code can be optimized in three different ways to obtain a 3000x speedup and thus matching the performance of the manual implementation of LPZK. We obtain such performance gains by first modifying the algorithmic specifications, then by adopting a provably secure parallel execution model, and finally by optimizing the memory access structures. All optimizations are first formally verified inside EasyCrypt, and then executable code is automatically synthesized from each step of the formalization. For each optimization, we analyze performance gains resulting from it and also address challenges facing the computer-aided security proofs thereof, and challenges facing automated synthesis of executable code with such an optimization.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Minor revision. ACM CCS 2023
Zero-KnowledgeFormal VerificationParallelismVerified ImplementationVerified OptimizationsCode Synthesis
Contact author(s)
samdittmer @ stealthsoftwareinc com
karim eldefrawy @ sri com
stephane graham-lengrand @ csl sri com
steve @ stealthsoftwareinc com
rafail @ cs ucla edu
vitor pereira @ sri com
2023-09-15: last of 2 revisions
2023-09-05: received
See all versions
Short URL
Creative Commons Attribution


      author = {Samuel Dittmer and Karim Eldefrawy and Stéphane Graham-Lengrand and Steve Lu and Rafail Ostrovsky and Vitor Pereira},
      title = {Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge},
      howpublished = {Cryptology ePrint Archive, Paper 2023/1322},
      year = {2023},
      doi = {10.1145/3576915.3616583},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.