Super cool, I've always wanted to implement the Signal Protocol in Nim. > In my humble opinion, the core cryptographic library for nim should have at > least one cryptographic primitive in each category:
* PRP - N/A * PRNG: <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/csprngs/sysrand.nim> * AEAD: Almost, Chacha20 and Poly1305 are implemented (albeit my Poly1305 impl is very slow as I was experimenting pure (mod 2¹³⁰-5) operations instead of usual impl * <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/ciphers/chacha20.nim> * <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/mac/mac_poly1305.nim> * Stream Cipher: Chacha20 * PRF - N/A * KDF: <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/kdf/kdf_hkdf.nim> * HKDF: <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/kdf/kdf_hkdf.nim> * HMAC: <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/mac/mac_hmac.nim> * NIKE - N/A * KEM - N/A * Signature Scheme: <https://github.com/mratsim/constantine/blob/v0.1.0/constantine/signatures/bls_signatures.nim>. Adding EdDSA or ECDSA shouldn't be that hard. Re formal verification, this is something I'm quite interested in, but ideally instead of implementing spec in say Lean I write the spec and generate code from like what is done by: * fiat-crypto: <https://github.com/mit-plv/fiat-crypto> * CryptOpt (formally verifiex x86 assembly: <https://github.com/0xADE1A1DE/CryptOpt> * hacl-star / Evercrypt for QUIC / TLS v1.3: * <https://project-everest.github.io/> * <https://hacl-star.github.io/> See for example signal-star, formally verified signal protocol: * <https://www.computer.org/csdl/proceedings-article/sp/2019/666000b256/1dlwheTvbEI> * <https://github.com/Inria-Prosecco/libsignal-protocol-wasm-fstar>
