Abstract
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].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Almeida, J.B., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Béguelin, S.Z.: Full proof cryptography: Verifiable compilation of efficient zero-knowledge protocols. In: 19th ACM Conference on Computer and Communications Security, CCS 2012. ACM (2012)
Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-Aided Security Proofs for the Working Cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)
Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90–101. ACM, New York (2009)
Barthe, G., Pointcheval, D., Béguelin, S.Z.: Verified security of redundancy-free encryption from Rabin and RSA. In: 19th ACM Conference on Computer and Communications Security, CCS 2012. ACM (to appear, 2012)
Bellare, M., Rogaway, P.: Optimal Asymmetric Encryption. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 92–111. Springer, Heidelberg (1995)
Bellare, M., Rogaway, P.: The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006)
Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270–299 (1984)
Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005)
Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Grégoire, B., Kunz, C., Lakhnech, Y., Zanella Béguelin, S. (2012). Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-35308-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35307-9
Online ISBN: 978-3-642-35308-6
eBook Packages: Computer ScienceComputer Science (R0)