Paper 2025/1569 Original: eprint.iacr.org/2025/1569 ↗

How Hard Can It Be to Formalize a Proof? Lessons from Formalizing CryptoBox Three Times in EasyCrypt

Abstract

Provable security is a cornerstone of modern cryptography, aiming to provide formal and precise security guarantees. However, for various reasons, security proofs are not always properly verified, possibly leading to unwarranted security claims and, in the worst case, deployment of insecure constructions. To further enhance trust and assurance, machine-checked cryptography makes these proofs more formal and rigorous. Unfortunately, the complexity of writing machine-verifiable proofs remains prohibitively high in many interesting use-cases. In this paper, we investigate the sources of this complexity, specifically examining how the style of security definitions influences the difficulty of constructing machine-verifiable proofs in the context of game-playing security. Concretely, we present a new security proof for the generic construction of a PKAE scheme from a NIKE and AE scheme, written in a code-based, game-playing style à la Bellare and Rogaway, and compare it to the same proof written in the style of state-separating proofs, a methodology for developing modular game-playing security proofs. Additionally, we explore a third “blended” style designed to avoid anticipated difficulties with the formalization. Our findings suggest that the choice of definition style impacts proof complexity—including, we argue, in detailed pen-and-paper proofs—with trade-offs depending on the proof writer’s goals.