search

hacl-star / hacl-star

HACL*, a formally verified cryptographic library written in F*
Apache License 2.0
1.63k stars 170 forks source link

Support for NaCL's (libsodium's) hchacha20-based box #225

Open copy opened 4 years ago

copy commented 4 years ago

This came up while implementing an OCaml dnscrypt client:

Currently, HACL exposes NaCL's crypto_box_* functions, which are based on hsalsa20. However, DNSCrypt also requires a box construction based on hchacha20. It doesn't seem to be part of the original NaCL, but the libsodium implementation is here.

I'm not sure if this in scope for the project, but it would certainly be nice to build my library on top of some verified cryptography :-)

msprotz commented 2 years ago

Is this still relevant? We're currently short on resources so there would have to be a significant integration and/or benefit for us to take the time to implement this.

This would actually be a great first project for a student or someone wanting to play with the verification side of things.

copy commented 1 year ago

It is still relevant in the sense that dnscrypt is actively used, uses hchacha20 under the hood and there is no verified implementation. On the other hand, it's a fairly niche construction, that doesn't seem to be used much outside of dnscrypt.

I'll agree, that it's a good first issue.

msprotz commented 1 year ago

Is the OCaml DNScrypt client used by any big projects out there? Trying to think about how to motivate this...

copy commented 1 year ago

I doubt it, it's used in some private projects, but I guess I should "properly" publish it. I meant to say that it's also useful for other dnscrypt implementations.