Automated Proofs of Pairing-Based Cryptography

Analyzing cryptographic constructions in the computational model, or simply verifying the correctness of security proofs, are complex and error-prone tasks. Although computer tools have significant potential to increase confidence in security proofs and to reduce the time for building these proofs, existing tools are either limited in scope, or can only be used by formal methods experts, and have a significant overhead. In effect, it has remained a challenge to design usable and intuitive tools for building and verifying cryptographic proofs, especially for more advanced fields such as pairing-based or lattice-based cryptography. This paper introduces a formal logic which captures some key reasoning principles in provable security, and more importantly, operates at a level of abstraction that closely matches cryptographic practice. Automatization of the logic is supported by an effective proof search procedure, which in turn embeds (extended and customized) techniques from automated reasoning, symbolic cryptography and program verification. Although the logic is general, some of the techniques for automating proofs are specific to fixed algebraic settings. Therefore, in order to illustrate the strengths of our logic, we implement a new tool, called Auto G&P, which supports extremely compact, and often fully automated, proofs of cryptographic constructions based on (bilinear or multilinear) Diffie-Hellman assumptions. For instance, we provide a 100-line proof of Waters' Dual System Encryption (CRYPTO'09), and fully automatic proofs of Boneh-Boyen Identity-Based Encryption (CRYPTO'04). Finally, we provide an automated tool that generates independently verifiable EasyCrypt proofs from AutoG&P proofs.