Abstract
Cryptography plays a key role in the security of modern communication and computer infrastructures; therefore, it is of paramount importance to design cryptographic systems that yield strong security guarantees. To achieve this goal, cryptographic systems are supported by security proofs that establish an upper bound for the probability that a resource-constrained adversary is able to break the cryptographic system. In most cases, security proofs are reductionist, i.e. they construct from an (arbitrary but computationally bounded) adversary that would break the security of the cryptographic construction with some reasonable probability another computationally bounded adversary that would break a hardness assumption with reasonable probability. This approach, known as provable security, is in principle able to deliver rigorous and detailed mathematical proofs. However, new cryptographic designs (and consequently their security analyses) are increasingly complex, and there is a growing emphasis on shifting from algorithmic descriptions to implementation-level descriptions that account for implementation details, recommendations from standards when they exist, and possibly side-channels. As a consequence, cryptographic proofs are becoming increasingly error-prone and difficult to check. One promising solution to address these concerns is to develop machine-checked frameworks that support the construction and automated verification of cryptographic systems. Although many such frameworks exist for the symbolic model of cryptography, comparatively little work has been done to develop machine-checked frameworks to reason directly in the computational model commonly used by cryptographers
An up-to-date and living version of this document and the EasyCrypt formalization and proofs it refers to can be found at https://www.easycrypt.info/Tutorial
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In: ACM Communications and Computer Security (CCS), pp. 1217–1230. ACM (2013)
Almeida, J.B., Barbosa, M., Barthe, G., Davy, G., Dupressoir, F., Grégoire, B., Strub, P.-Y.: Verified implementations for secure and verifiable computation. Cryptology ePrint Archive, Report 2014/456 (2014), http://eprint.iacr.org/
Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Lakhnech, Y., Schmidt, B., Béguelin, S.Z.: Fully automated analysis of padding-based encryption in the computational model. In: ACM Communications and Computer Security (CCS), pp. 1247–1260. ACM (2013)
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., Zanella-Béguelin, S.: Formal certification of code-based cryptographic proofs. In: ACM Principles of Programming Languages (POPL), pp. 90–101. ACM (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., Strub, PY. (2014). EasyCrypt: A Tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds) Foundations of Security Analysis and Design VII. FOSAD FOSAD 2013 2012. Lecture Notes in Computer Science, vol 8604. Springer, Cham. https://doi.org/10.1007/978-3-319-10082-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-10082-1_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10081-4
Online ISBN: 978-3-319-10082-1
eBook Packages: Computer ScienceComputer Science (R0)