J. Bacelar-almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC, Fast Software Encryption -23rd International Conference, FSE 2016, pp.163-184, 2016.
DOI : 10.1007/3-540-46035-7_35

K. David-adrian, Z. Bhargavan, P. Durumeric, M. Gaudry, J. A. Green et al., Imperfect forward secrecy: How diffie-hellman fails in practice, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pp.5-17, 2015.

[. Avigad, K. Donnelly, D. Gray, and P. Raff, A formally verified proof of the prime number theorem, ACM Transactions on Computational Logic, vol.9, issue.1, 2007.
DOI : 10.1145/1297658.1297660

M. Leonard and . Adleman, A subexponential algorithm for the discrete logarithm problem with applications to cryptography (abstract)

J. Avigad and J. Harrison, Formally verified mathematics, Communications of the ACM, vol.57, issue.4, pp.66-75, 2014.
DOI : 10.1145/2591012

A. Andrew and W. Appel, Verification of a cryptographic primitive: Sha- 256, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.37, issue.2, p.7, 2015.

A. W. Appel, Verification of a Cryptographic Primitive, ACM Transactions on Programming Languages and Systems, vol.37, issue.2, p.7, 2015.
DOI : 10.1145/2345156.1993532

M. Avalle, A. Pironti, and R. Sisto, Formal verification of security protocol implementations: a survey, Formal Aspects of Computing, vol.155, issue.1, pp.1-25, 2012.
DOI : 10.1016/j.entcs.2005.11.052
URL : https://hal.archives-ouvertes.fr/hal-00863392

G. Gilles-barthe, J. Betarte, C. Campo, D. Luna, and . Pichardie, System-level non-interference for constant-time cryptography, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.1267-1279, 2014.

[. Béguelin, G. Barthe, B. Grégoire, and F. Olmedo, Formally certifying the security of digital signature schemes, 30th IEEE Symposium on Security and Privacy, pp.17-20, 2009.

]. B. Bbpv11a, M. Brumley, D. Barbosa, F. Page, and . Vercauteren, Practical realisation and elimination of an ecc-related software bug attack, Cryptology ePrint Archive Report, vol.633, 2011.

[. Brumley, M. Barbosa, D. Page, and F. Vercauteren, Practical Realisation and Elimination of an ECC-Related Software Bug Attack, IACR Cryptology ePrint Archive, vol.48, issue.177, p.633, 2011.
DOI : 10.1007/11761679_2

B. Billy, M. Brumley, D. Barbosa, F. Page, and . Vercauteren, Practical realisation and elimination of an ecc-related software bug attack, Topics in Cryptology?CT-RSA 2012, pp.171-186, 2012.

S. Bernard, Y. Bertot, L. Rideau, and P. Strub, Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pp.76-87, 2016.
DOI : 10.1023/A:1026518331905

Y. Bertot and P. Castéran, Coq'Art: examples and exercises, 2004.

W. Joppe, C. Bos, H. Costello, K. E. Hisil, and . Lauter, High-performance scalar multiplication using 8-dimensional GLV/GLS decomposition, Cryptographic Hardware and Embedded Systems -CHES 2013 -15th International Workshop Proceedings, pp.331-348, 2013.

M. Backes, G. Doychev, and B. Köpf, Preventing sidechannel leaks in web traffic: A formal approach, 20th Annual Network and Distributed System Security Symposium, NDSS 2013, 2013.

]. D. Ber and . Bernstein, qhasm: tools to help write high-speed software

. Ber06, J. Daniel, and . Bernstein, Curve25519: new diffie-hellman speed records, Public Key Cryptography-PKC 2006, pp.207-228, 2006.

Y. Bertot, Introduction to dependent types in coq, 2008.

D. Boneh and M. K. Franklin, Identity based encryption from the weil pairing, IACR Cryptology ePrint Archive, p.90, 2001.
DOI : 10.1137/s0097539701398521
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.3708

C. Bfk-+-14-]-karthikeyan-bhargavan, M. Fournet, A. Kohlweiss, P. Pironti, S. Strub et al., Proving the tls handshake secure (as it is), Advances in Cryptology (CRYPTO), pp.235-255, 2014.

[. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology (CRYPTO), pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

[. Barthe, B. Grégoire, R. Janvier, and S. Z. Béguelin, Formal certification of code-based cryptographic proofs, IACR Cryptology ePrint Archive, p.314, 2007.

[. Barthe, B. Grégoire, Y. Lakhnech, and S. Z. Béguelin, Beyond provable security verifiable IND-CCA security of OAEP Topics in Cryptology -CT-RSA 2011 -The Cryptographers' Track at the RSA Conference, Proceedings, volume 6558 of Lecture Notes in Computer Science, pp.180-196, 2011.

[. Barthe, B. Grégoire, and S. Z. Béguelin, Formal certification of code-based cryptographic proofs, pp.90-101, 2009.
DOI : 10.1145/1480881.1480894
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.330.771

. Sidi-ould and . Biha, Finite groups representation theory with coq, Intelligent Computer Mathematics, 16th Symposium 8th International Conference, MKM 2009, Held as Part of CICM 2009 Proceedings, volume 5625 of Lecture Notes in Computer Science, pp.438-452, 2009.

. Sidi-ould and . Biha, Composants mathématiques pour la théorie des groupes. (Mathematical components for groups theory), 2010.

E. Brier and M. Joye, Fast Point Multiplication on Elliptic Curves through Isogenies, AAECC, pp.43-50, 2003.
DOI : 10.1007/3-540-44828-4_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.6968

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648

[. Beringer, A. Petcher, K. Q. Ye, and A. W. Appel, Verified correctness and security of openssl hmac, 24th USENIX Security Symposium (USENIX Security 15), pp.207-221, 2015.

A. Brauer, On addition chains, Bulletin of the American Mathematical Society, vol.45, issue.10, pp.736-739
DOI : 10.1090/S0002-9904-1939-07068-7

L. Buttyan, Formal methods in the design of cryptographic protocols (state of the art), 1999.

J. W. and S. Cassels, LMSST: 24 Lectures on Elliptic Curves, 1991.
DOI : 10.1017/CBO9781139172530

V. David, G. V. Chudnovsky, and . Chudnovsky, Sequences of numbers generated by addition in formal groups and new primality and factorization tests, Advances in Applied Mathematics, vol.7, pp.385-434, 1986.

T. Coquand and G. P. Huet, Constructions: A higher order proof system for mechanizing mathematics, European Conference on Computer Algebra, pp.151-184, 1985.
DOI : 10.1007/3-540-15983-5_13
URL : https://hal.archives-ouvertes.fr/inria-00076155

Y. Chen, C. Hsu, H. Lin, P. Schwabe, M. Tsai et al., Verifying Curve25519 Software, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pp.299-309, 2014.
DOI : 10.1145/363235.363259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.564.7481

H. Cohen, A. Miyaji, and T. Ono, Efficient Elliptic Curve Exponentiation Using Mixed Coordinates, Advances in Cryptology -ASIACRYPT '98, International Conference on the Theory and Applications of Cryptology and Information Security Proceedings, volume 1514 of Lecture Notes in Computer Science, pp.51-65, 1998.
DOI : 10.1007/3-540-49649-1_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2566

S. Checkoway, R. Niederhagen, A. Everspaugh, M. Green, T. Lange et al., On the practical exploitability of dual EC in TLS implementations, Proceedings of the 23rd USENIX Security Symposium, pp.319-335, 2014.

C. Cohen, Formalized algebraic numbers: construction and firstorder theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

C. Cohen, Pragmatic Quotient Types in Coq, ITP, pp.213-228, 2013.
DOI : 10.1007/978-3-642-39634-2_17

T. Coquand and C. Paulin, Inductively defined types, Conference on Computer Logic, pp.50-66, 1988.
DOI : 10.1007/3-540-52335-9_47

W. Diffie and M. E. Hellman, New directions in cryptography, IEEE Transactions on Information Theory, vol.22, issue.6, pp.644-654, 1976.
DOI : 10.1109/TIT.1976.1055638
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.9720

J. Duan, J. Hurd, G. Li, S. Owens, K. Slind et al., Functional Correctness Proofs of Encryption Algorithms, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, pp.519-533, 2005.
DOI : 10.1007/11591191_36
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.4929

C. Doche, T. Icart, and D. R. Kohel, Efficient Scalar Multiplication by Isogeny Decompositions, IACR Cryptology ePrint Archive, p.420, 2005.
DOI : 10.1007/11745853_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.2150

C. Doche, T. Icart, and D. R. Kohel, Efficient Scalar Multiplication by Isogeny Decompositions, Public Key Cryptography, pp.191-206, 2006.
DOI : 10.1007/11745853_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.2150

S. Vassil, L. Dimitrov, P. Imbert, and . Kumar-mishra, Efficient and secure elliptic curve point multiplication using doublebase chains, Advances in Cryptology - ASIACRYPT 2005, 11th International Conference on the Theory and Application of Cryptology and Information Security Proceedings, volume 3788 of Lecture Notes in Computer Science, pp.59-78, 2005.

S. Vassil, G. A. Dimitrov, W. C. Jullien, and . Miller, An algorithm for modular exponentiation, Inf. Process. Lett, vol.66, issue.3, pp.155-159, 1998.

M. Dénès, A. Mörtberg, and V. Siles, A Refinement-Based Approach to Computational Algebra in Coq, Interactive Theorem Proving -Third International Conference, ITP 2012 Proceedings, pp.83-98, 2012.
DOI : 10.1007/978-3-642-32347-8_7

A. Faz-hernández, P. Longa, and A. H. Sánchez, Efficient and secure algorithms for GLV-based scalar multiplication and their implementation on GLV???GLS curves (extended version), Journal of Cryptographic Engineering, vol.49, issue.9
DOI : 10.1007/3-540-45861-1_31

[. Frege, Grundgesetze der Arithmetik: Begriffsschriftlich abgeleitet, 1893.

S. Friedl, An elementary proof of the group law for elliptic curves. The Group Law on Elliptic Curves, 1998.

W. Fulton, Algebraic curves -an introduction to algebraic geometry (reprint vrom 1969) Advanced book classics, 1989.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A machinechecked proof of the odd order theorem, Interactive Theorem Proving -4th International Conference Proceedings, volume 7998 of Lecture Notes in Computer Science, pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

D. Steven and . Galbraith, Mathematics of Public Key Cryptography, 2012.

[. Garillot, Generic Proof Tools and Finite Group Theory. (Outils génériques de preuve et théorie des groupes finis), 2011.
URL : https://hal.archives-ouvertes.fr/pastel-00649586

S. D. Galbraith, X. Lin, and M. Scott, Endomorphisms for Faster Elliptic Curve Cryptography on a Large Class of Curves, 28th Annual International Conference on the Theory and Applications of Cryptographic Techniques Proceedings, pp.518-535, 2009.
DOI : 10.1007/3-540-48892-8_15

R. P. Gallant, R. J. Lambert, and S. A. Vanstone, Faster Point Multiplication on Elliptic Curves with Efficient Endomorphisms
DOI : 10.1007/3-540-44647-8_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.2004

S. Goldwasser and S. Micali, Probabilistic encryption, Journal of Computer and System Sciences, vol.28, issue.2, pp.270-299, 1984.
DOI : 10.1016/0022-0000(84)90070-9
URL : http://doi.org/10.1016/0022-0000(84)90070-9

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in coq, J. Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Theorem Proving in Higher Order Logics, 20th International Conference Proceedings, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

[. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, Computer Mathematics, 8th Asian Symposium, ASCM 2007, p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28

[. Gonthier, Point-free, set-free concrete linear algebra The Netherlands, Interactive Theorem Proving -Second International Conference Proceedings, volume 6898 of Lecture Notes in Computer Science, pp.103-118, 2011.
DOI : 10.1007/978-3-642-22863-6_10

M. Daniel and . Gordon, A survey of fast exponentiation methods, J. Algorithms, vol.27, issue.1, pp.129-146, 1998.

L. Daniel-genkin and . Pachmanov, Itamar Pipman, Eran Tromer, and Yuval Yarom. Ecdsa key extraction from mobile devices via nonintrusive physical side channels, 2016.

P. Guillot, Courbes Elliptiques, une présentation élémentaire pour la cryptographie, 2010.

J. Hurd, M. Gordon, and A. Fox, Formalized elliptic curve cryptography, High Confidence Software and Systems, 2006.

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno et al., Ironclad apps: Endto-end security via automated full-system verification, 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14), pp.165-181, 2014.

[. Hisel, Addition law on elliptic curves, 2014.

[. Icart, How to Hash into Elliptic Curves, 29th Annual International Cryptology Conference Proceedings, pp.303-316, 2009.
DOI : 10.1007/978-3-642-03356-8_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.215.5920

N. Koblitz, Elliptic curve cryptosystems, Mathematics of Computation, vol.48, issue.177, pp.203-209, 1987.
DOI : 10.1090/S0025-5718-1987-0866109-5

J. López and R. Dahab, Fast Multiplication on Elliptic Curves Over GF(2m) without precomputation, Cryptographic Hardware and Embedded Systems, First International Workshop, CHES'99 Proceedings, volume 1717 of Lecture Notes in Computer Science, pp.316-327, 1999.
DOI : 10.1007/3-540-48059-5_27

A. Langley and M. Hamburg, Elliptic curves for security, IETF RFC, vol.7748, 2016.
DOI : 10.17487/RFC7748

P. Longa, High-Speed Elliptic Curve and Pairing-Based Cryptography, 2011.

P. Longa and F. Sica, Four-Dimensional Gallant???Lambert???Vanstone Scalar Multiplication, Journal of Cryptology, vol.77, issue.262, pp.248-283, 2014.
DOI : 10.1007/s13389-011-0017-8
URL : http://arxiv.org/abs/1106.5149

C. A. Meadows, Formal methods for cryptographic protocol analysis: emerging issues and trends, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.44-54, 2003.
DOI : 10.1109/JSAC.2002.806125
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.7842

S. Victor and . Miller, Use of elliptic curves in cryptography, CRYPTO, pp.417-426, 1985.

S. Victor and . Miller, Short programs for functions on curves, 1986.

L. Peter and . Montgomery, Speeding the Pollard and elliptic curve methods of factorization, Mathematics of Computation, vol.48, pp.243-264, 1987.

A. Menezes, T. Okamoto, and S. A. Vanstone, Reducing elliptic curve logarithms to logarithms in a finite field, IEEE Transactions on Information Theory, vol.39, issue.5, pp.1639-1646, 1993.
DOI : 10.1109/18.259647

S. Micali and L. Reyzin, Physically Observable Cryptography, IACR Cryptology ePrint Archive, p.120, 2003.
DOI : 10.1007/978-3-540-24638-1_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.6299

I. Niven, The Transcendence of &#960, The American Mathematical Monthly, vol.46, issue.8, pp.469-471, 1939.
DOI : 10.2307/2302515

. Ope15 and . Openssl, Bignum squaring may produce incorrect results (cve-2014- 3570), 2015.

K. Okeya and K. Sakurai, Efficient Elliptic Curve Cryptosystems from a Scalar Multiplication Algorithm with Recovery of the y-Coordinate on a Montgomery-Form Elliptic Curve, Cryptographic Hardware and Embedded Systems -CHES 2001, Third International Workshop Proceedings , volume 2162 of Lecture Notes in Computer Science, pp.126-141, 2001.
DOI : 10.1007/3-540-44709-1_12

J. M. Pollard, Monte Carlo methods for index computation mod p, Mathematics of Computation, vol.32, pp.918-924, 1978.
DOI : 10.2307/2006496

F. Pfenning and C. Paulin-mohring, Inductively defined types in the Calculus of Constructions, Mathematical Foundations of Programming Semantics 5th International Conference Proceedings, volume 442 of Lecture Notes in Computer Science, pp.209-228, 1989.
DOI : 10.1007/BFb0040259

E. Prouff and M. Rivain, Masking against Side-Channel Attacks: A Formal Security Proof, Advances in Cryptology -EUROCRYPT 2013, 32nd Annual International Conference on the Theory and Applications of Cryptographic Techniques, pp.142-159, 2013.
DOI : 10.1007/978-3-642-38348-9_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.460.3576

G. W. Reitwiesner, Binary arithmetic Advances in Computers, pp.231-308, 1960.

R. Schoof, Nonsingular plane cubic curves over finite fields, Journal of Combinatorial Theory, Series A, vol.46, issue.2, pp.183-211, 1987.
DOI : 10.1016/0097-3165(87)90003-3
URL : http://doi.org/10.1016/0097-3165(87)90003-3

F. Sica, M. Ciet, and J. Quisquater, Analysis of the Gallant-Lambert-Vanstone Method Based on Efficient Endomorphisms: Elliptic and Hyperelliptic Curves, Selected Areas in Cryptography, 9th Annual International Workshop, SAC 2002, pp.21-36, 2002.
DOI : 10.1007/3-540-36492-7_3

E. Whitman, S. , and D. L. Dill, Automatic formal verification of block cipher implementations, In FMCAD, pp.1-7, 2008.

A. Shamir, Identity-Based Cryptosystems and Signature Schemes, CRYPTO, pp.47-53, 1984.
DOI : 10.1007/3-540-39568-7_5
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-39568-7_5.pdf

C. Swamy, C. Hriicu, A. Keller, A. Rastogi, S. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.256-270, 2016.
DOI : 10.1145/2837614.2837655
URL : https://hal.archives-ouvertes.fr/hal-01265793

J. H. Silverman, The arithmetic of elliptic curves, Graduate Texts in Mathematics, vol.106, 2009.

[. Smith, The $$\mathbb {Q}$$ Q -curve Construction for Endomorphism-Accelerated Elliptic Curves, Journal of Cryptology, vol.29, issue.4, pp.806-832, 2016.
DOI : 10.1006/jnth.1999.2463

[. Standaert, G. Tal, M. Malkin, and . Yung, A formal practice-oriented model for the analysis of side-channel attacks

[. Stern, Why Provable Security Matters?, Advances in Cryptology -EUROCRYPT 2003, International Conference on the Theory and Applications of Cryptographic Techniques Proceedings, volume 2656 of Lecture Notes in Computer Science, pp.449-461, 2003.
DOI : 10.1007/3-540-39200-9_28

G. Ernst and . Straus, Addition chains of vectors (problem 5125

V. Andrew and . Sutherland, Elliptic curves as abelian groups, 2015.

]. B. Svdw11, E. Spitters, and . Van-der-weegen, Type classes for mathematics in type theory. Arxiv preprint arXiv, pp.1102-1323, 2011.

N. Smart, F. Vercauteren, and A. Muzereau, The equivalence between the dhp and dlp for elliptic curves used in practical applications, LMS Journal of Computation and Mathematics, vol.7, pp.50-72, 2004.

]. A. Tar55 and . Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, pp.285-309, 1955.

L. Théry and G. Hanrot, Primality Proving with Elliptic Curves, TPHOLs, pp.319-333, 2007.
DOI : 10.1007/978-3-540-74591-4_24

L. Théry, Proving the group law for elliptic curves formally, 2007.

F. Wiedijk and . Introduction, The Seventeen Provers of the World, Lecture Notes in Computer Science, vol.3600, pp.1-9, 2006.
DOI : 10.1007/11542384

J. Karim-zinzindohoue, E. Bartzia, and K. Bhargavan, A Verified Extensible Library of Elliptic Curves, 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp.296-309, 2016.
DOI : 10.1109/CSF.2016.28