, ChaCha20 and Poly1305 for IETF Protocols, IETF RFC, vol.7539, 2015.

, Elliptic Curves for Security, IETF RFC, vol.7748, 2016.

J. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire et al., Jasmin: High-assurance and high-speed cryptography, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS, pp.1807-1823, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01649140

A. W. Appel, Verified software toolchain, NASA Formal Methods-4th International Symposium, NFM 2012, p.2, 2012.
DOI : 10.1007/978-3-642-19718-5_1
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-19718-5_1.pdf

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., Easycrypt: A tutorial, Foundations of Security Analysis and Design VII-FOSAD 2012/2013 Tutorial Lectures, vol.8604, pp.146-166, 2013.
DOI : 10.1007/978-3-319-10082-1_6
URL : https://hal.archives-ouvertes.fr/hal-01114366

,

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, pp.146-166, 2014.
DOI : 10.1007/978-3-319-10082-1_6
URL : https://hal.archives-ouvertes.fr/hal-01114366

D. J. Bernstein, Cache-timing attacks on aes, 2005.

B. Blanchet, A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, pp.193-207, 2007.
DOI : 10.1109/tdsc.2007.1005

H. Böck, A. Zauner, S. Devlin, J. Somorovsky, and P. Jovanovic, Nonce-disrespecting adversaries: Practical forgery attacks on GCM in TLS, 10th USENIX Workshop on Offensive Technologies (WOOT 16). USENIX Association, 2016.

B. Bond, C. Hawblitzel, M. Kapritsos, K. R. Leino, J. R. Lorch et al., Vale: Verifying high-performance cryptographic assembly code, Proceedings of the USENIX Security Symposium, 2017.

, Federal Information Processing Standards Publication, 2012.

N. T. Courtois, P. Emirdag, and F. Valsorda, Private key recovery combination attacks: On extreme fragility of popular bitcoin key management, wallet and cold storage solutions in presence of poor rng events, Cryptology ePrint Archive, vol.848, 2014.

. Bhargavan,

M. Dworkin, Recommendation for Block Cipher Modes of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special Publication, pp.800-838, 2007.
DOI : 10.6028/nist.sp.800-38gr1-draft
URL : https://doi.org/10.6028/nist.sp.800-38gr1-draft

M. J. Dworkin, E. B. Barker, J. R. Nechvatal, J. Foti, L. E. Bassham et al., Advanced Encryption Standard (AES). NIST FIPS-197, 2001.

A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala, Simple high-level code for cryptographic arithmetic-with proofs, without compromises, S&P'19: Proceedings of the IEEE Symposium on Security & Privacy, 2019.

A. N. Institute, Public Key Cryptography for the Financial Services Industry: The Elliptic Curve Digital Signature Algorithm. ANSI X9, pp.62-1998

S. Josefsson and I. Liusvaara, Edwards-Curve Digital Signature Algorithm (EdDSA), RFC, vol.8032, 2017.
DOI : 10.17487/rfc8032
URL : https://www.rfc-editor.org/rfc/pdfrfc/rfc8032.txt.pdf

E. Käsper and P. Schwabe, Faster and timing-attack resistant aes-gcm, Cryptographic Hardware and Embedded Systems-CHES 2009, pp.1-17, 2009.

A. Langley, M. Hamburg, and S. Turner, Elliptic Curves for Security, RFC, vol.7748, 2016.
DOI : 10.17487/rfc7748
URL : https://www.rfc-editor.org/rfc/pdfrfc/rfc7748.txt.pdf

N. Mouha, M. S. Raunak, D. R. Kuhn, and R. Kacker, Finding bugs in cryptographic hash function implementations. Cryptology ePrint Archive, 2017.
DOI : 10.1109/tr.2018.2847247

A. Petcher and G. Morrisett, The foundational cryptography framework, Principles of Security and Trust, pp.53-72, 2015.
DOI : 10.1007/978-3-662-46666-7_4
URL : http://arxiv.org/pdf/1410.3735.pdf

A. Petcher and G. Morrisett, The foundational cryptography framework, Principles of Security and Trust-4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, pp.53-72, 2015.

N. Swamy, C. Hrit¸cuhrit¸cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.256-270
URL : https://hal.archives-ouvertes.fr/hal-01265793

A. Tomb, Automated verification of real-world cryptographic implementations, IEEE Security and Privacy, vol.14, issue.6, pp.26-33, 2016.

J. K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, HACL*: A verified modern cryptographic library, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp.1789-1806, 2017.