25 Jul - Markulf Kolweiss - Proving Fast and Slow: A Proof of Cryptobox using Algebraic Rules instead of Boilerplate

Cryptographic protocols often compose multiple primitives. The proof of security of the protocol contains reductions that are to the most part conceptually easy but complicated because they have to simulate the full behaviour of the protocol. These long reductions often stretch tens of pages and can obscure the interesting aspects of the proof. Consequently the proofs are hard to get right and difficult to read and verify. In this paper, we present a new way of factoring game-hop based security proofs and of clarifying reductions. Our proof techniques do not require simulators, but are compatible with the simulation paradigm. We hope that the reader will find our key technique obvious in hindsight: We exploit associativity of algorithm composition, and we split each reduction into 3 small, simple steps: (1) Functional equivalence, (2) Associativity and (3) a trivial reduction. We call the third step a “composition lemma”. In order to ease the functional equivalence step, we provide well-founded algebraic rules.  The goal of our algebraic rules is to free the writer from writing “boilerplate” proofs and to make proofs clear, crisp and accessible. Using our techniques, it becomes more difficult to accidentally hide “hacks” within the proof, and we hope to empower writers with guidance to think through the proof thoroughly. Moreover, we hope that our algebraic rules and our “composition lemma” ease readability and verifiability of proofs, for readers and writers alike. As an application of our new techniques, we provide arguably the first formal security analysis of crypto box the most complex component of the NaCl cryptographic library. This result is of independent interest.