Skip to content

Lean cryptography library for prototyping/modeling protocols and proving protocol properties.

License

Notifications You must be signed in to change notification settings

katzenpost/CryptWalker

Repository files navigation

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)
  • work-in-progress: X448
  • work-in-progres: X41417
KEM: Key Encapsulation Method

Classical NIKEs adapted to KEM via hashed ElGamal construction:

  • X25519
SIGN: Cryptographic Signature Scheme
  • work-in-progress: ed25519
PRF: Pseuodo Random Function
  • SHA256
  • work-in-progress: SHA512
DATAstructures
  • Binary Merkle Hash Tree polymorphic over the hash function

developer notes

building

lake build

testing

lake exe CryptWalker.Data.test
lake exe CryptWalker.NIKE.test
lake exe CryptWalker.KEM.test

benchmarks

lake exe CryptWalker.NIKE.benchmark

Benchmark_X25519_ECDH        1000 iter      1253957 ns/op

licensing

AGPLv3

About

Lean cryptography library for prototyping/modeling protocols and proving protocol properties.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages