G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, pp.90-101, 2009.

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computeraided security proofs for the working cryptographer, Advances in Cryptology (CRYPTO), pp.71-90, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01112075

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub et al., Proving the tls handshake secure (as it is), Advances in Cryptology (CRYPTO), pp.235-255, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102231

N. J. Al-fardan and K. G. Paterson, Lucky thirteen: Breaking the tls and dtls record protocols, IEEE Symposium on Security and Privacy, pp.526-540, 2013.

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

G. Barthe, G. Betarte, J. Campo, C. Luna, and D. Pichardie, Systemlevel non-interference for constant-time cryptography, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.1267-1279, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01101950

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC, IACR Cryptology ePrint Archive, vol.2015, p.1241, 2015.

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

. Openssl, Bignum squaring may produce incorrect results (cve-20143570), 2015.

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green et al., Imperfect forward secrecy: How diffie-hellman fails in practice, ACM Conference on Computer and Communications Security (CCS), pp.5-17, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01184171

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

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

E. Kasper, We ? SSL, Real World Cryptography, 2015.

A. Langlet, W. Chang, and &. Quic-crypto, , 2015.

E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.3, IETF Internet Draft, 2016.

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing tls with verified cryptographic security, IEEE Symposium on Security & Privacy (Oakland), pp.445-462, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863373

T. Jager, J. Schwenk, and J. Somorovsky, Practical invalid curve attacks on tls-ecdh, Computer Security-ESORICS 2015, pp.407-425, 2015.

Y. Chen, C. Hsu, H. Lin, P. Schwabe, M. Tsai et al.,

B. Wang, S. Yang, and . Yang, Verifying curve25519 software, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.299-309, 2014.

D. J. Bernstein, Citations in this document, vol.4, 2007.

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

E. Bartzia and P. Strub, A formal library for elliptic curves in the coq proof assistant, Interactive Theorem Proving, pp.77-92, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102288

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations, ACM Conference on Computer and Communications Security (CCS), pp.1217-1230, 2013.

N. Koblitz, Elliptic curve cryptosystems, Mathematics of Computation, vol.48, issue.177, pp.203-209, 1987.

W. J. Bowman and A. Ahmed, Noninterference for free, ACM International Conference on Functional Programming (ICFP), pp.101-113, 2015.

, SAGE script for montgomery curves addition and doubling

, SAGE script for weierstrass curves addition, vol.27

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

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno et al., Ironclad apps: End-to-end security via automated fullsystem verification, 11th USENIX Symposium on Operating Systems Design and Implementation, pp.165-181, 2014.

L. Beringer, A. Petcher, Q. Y. Katherine, and A. W. Appel, Verified correctness and security of openssl hmac, 24th USENIX Security Symposium (USENIX Security 15, pp.207-221, 2015.

G. Inc, Cryptol

, Type := Mixin { : 2 != 0; : 3 != 0 }. Record ecuType := {A:K; B:K; :4 * A?3 + 27 * B?2 != 0}. Inductive point := EC Inf | EC In of K & K. Notation

, Definition oncurve (p : point) := if p is (x, y) then y?2 == x?3 + A * x + B else true

, Definition add (p1 p2 : point) := let p1 := if oncurve p1 then p1 else EC Inf in let p2 := if oncurve p2 then p2 else EC Inf in match p1, Type := EC p of oncurve p. Definition neg (p : point) := if p is (x, y) then (x, ?y) else EC Inf

, Lemma addO (p q : point): oncurve (add p q)

, Definition addec (p1 p2 : ec) : ec := EC p1 p2 (addO p1 p2)

. , n:nat) (p:point K) = p * + n