A Cryptographically Verified Implementation of crypto_box

No ratings

Presented at LondonCryptoDay 2017 by

Markulf Kohlweiss

The crypto_box construction is a simple Diffie-Hellman based KEM-DEM construction introduced and implemented by Bernstein et al. in their crypto library NaCl. The construction was popularised by libsodium, a fork of NaCl, and is designed to be used modularly in a broad range of applications such as DNSCurve and Mega. The simplicity of crypto_box and its modular nature make it a great example to showcase code-based cryptographic verification techniques in F*, the program verification tool used by miTLS.