Crypt Walker

A cryptographic library for Lean.

The hope is that this Lean library will allow you to write a cryptographic protocol prototype or model. Then you can write theorems and proofs about your model!

cryptographic primitives

NIKE: Non-Interactive Key Exchange

Classical NIKEs:

• X25519 (constant time Montgomery Ladder)

KEM: Key Encapsulation Method

Classical NIKEs adapted to KEM via hashed ElGamal construction:

• X25519

SIGN: Cryptographic Signature Scheme

• Ed25519 (plain and blinded variants)

AEAD: Authenticated Encryption with Associated Data

• AES-256-GCM-SIV (RFC 8452), the misuse-resistant mode BACAP encrypts pigeonhole boxes with, built on AES-256 and POLYVAL

HASH: Cryptographic Hash Function

• SHA-512
• BLAKE2b-512

KDF: Key Derivation Function

• HKDF-BLAKE2b-512 (RFC 5869 with BLAKE2b-512 as the hash)

PRF: Pseuodo Random Function

• SHA256

DATAstructures

• Binary Merkle Hash Tree polymorphic over the hash function

developer notes

building

lake build

testing

All tests can be run individually. Some tests load known-answer test vectors from CryptWalker/testdata/, which are vendored from hpqc to ensure binary compatibility.

lake exe CryptWalker.Data.test
lake exe CryptWalker.NIKE.test
lake exe CryptWalker.KEM.test
lake exe CryptWalker.Hash.test          # SHA-512 vectors from hpqc
lake exe CryptWalker.Hash.hkdf_test     # HKDF-BLAKE2b raw function vectors
lake exe CryptWalker.Hash.hkdf_structured_test  # HKDF structured instance vectors
lake exe CryptWalker.Cipher.test        # AES-256-GCM-SIV vectors from hpqc
lake exe CryptWalker.Sign.test
lake exe CryptWalker.Sign.blinded_test  # blinded Ed25519 vectors from hpqc

test vector files

These JSON files in CryptWalker/testdata/ are generated by hpqc/testvectors/cmd/generate and vendored here. Each file is binary-compatible with the corresponding hpqc test vectors:

File	Primitive	Source
hkdf_blake2b.json	HKDF-BLAKE2b-512 (RFC 5869)	hpqc/bacap/testdata/hkdf_blake2b.json
aes_gcm_siv.json	AES-256-GCM-SIV (RFC 8452)	hpqc/bacap/testdata/aes_gcm_siv.json
blinded_ed25519.json	Blinded Ed25519 signatures	hpqc/sign/ed25519/testdata/blinded_ed25519.json

benchmarks

lake exe CryptWalker.NIKE.benchmark

Benchmark_X25519_ECDH        1000 iter      1253957 ns/op

licensing

AGPLv3