CertiCrypt [3] and EasyCrypt [2] are machine-checked frameworks for proving the security of cryptographic constructions. Both frameworks adhere to the gamebased approach [9,6,8] to provable security [7], but revisit its realization from a formal verification pespective. More specifically, CertiCrypt and EasyCrypt use a probabilistic programming language pWHILE for expressing cryptographic constructions, security properties, and computational assumptions, and a probabilistic relational Hoare logic pRHL for justifying reasonings in cryptographic proofs. While both tools coincide in their foundations, they differ in their underlying technologies: CertiCrypt is implemented as a set of libraries in the Coq proof assistant, whereas EasyCrypt uses a verification condition generator for pRHL in combination with off-the-shelf SMT solvers and automated theorem provers. Over the last six years, we have used both tools to verify prominent examples of public-key encryption schemes, modes of operation, signature schemes, hash function designs, zero-knowledge proofs. Recently, we have also used both tools to certify the output of a zero-knowledge compiler [1]. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Barthe, G., Grégoire, B., Kunz, C., Lakhnech, Y., & Zanella Béguelin, S. (2012). Automation in computer-aided cryptography: Proofs, attacks and designs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 7–8). https://doi.org/10.1007/978-3-642-35308-6_3
Mendeley helps you to discover research relevant for your work.