### A Coq proof of the correctness of X25519 in TweetNaCl

Peter Schwabe, Benoît Viguier, Timmy Weerwag, and Freek Wiedijk

##### Abstract

We formally prove that the C implementation of the X25519 key-exchange protocol in the TweetNaCl library is correct. We prove both that it correctly implements the protocol from Bernstein's 2006 paper, as standardized in RFC 7748, as well as the absence of undefined behavior like arithmetic overflows and array out-of-bounds errors. We also formally prove, based on the work of Bartzia and Strub, that X25519 is mathematically correct, i.e., that it correctly computes scalar multiplication on the elliptic curve Curve25519. The proofs are all computer-verified using the Coq theorem prover. To establish the link between C and Coq we use the Verified Software Toolchain (VST).

Note: Proofs files are available at the following address: https://doi.org/10.5281/zenodo.4439686

Available format(s)
Category
Public-key cryptography
Publication info
Published elsewhere. 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Keywords
X25519Formal VerificationCoqFormal Methodsmodular cryptographic proofs
Contact author(s)
cs ru nl @ viguier nl
peter @ cryptojedi org
History
Short URL
https://ia.cr/2021/428

CC BY

BibTeX

@misc{cryptoeprint:2021/428,
author = {Peter Schwabe and Benoît Viguier and Timmy Weerwag and Freek Wiedijk},
title = {A Coq proof of the correctness of X25519 in TweetNaCl},
howpublished = {Cryptology ePrint Archive, Paper 2021/428},
year = {2021},
note = {\url{https://eprint.iacr.org/2021/428}},
url = {https://eprint.iacr.org/2021/428}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.