A Coq proof of the correctness of X25519 in TweetNaCl.

Peter Schwabe Benoît Viguier Timmy Weerwag Freek Wiedijk

Published in: IACR Cryptol. ePrint Arch. (2021)

Keyphrases

theorem prover
provably correct
formal methods
theorem proving
automated theorem proving
mathematical proofs
proof search
neural network
digital libraries
lower bound
special case
first order logic
inference rules
proof theory
automated theorem provers
geometry theorem proving