[Resource Topic] 2021/428: A Coq proof of the correctness of X25519 in TweetNaCl

Welcome to the resource topic for 2021/428

A Coq proof of the correctness of X25519 in TweetNaCl

Authors: Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk


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).

ePrint: https://eprint.iacr.org/2021/428

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .