lean cryptography library API for NIKE

Stream: Program verification

[David Stainton 🦡]

Hey I want to help fix the Lean cryptography situation. There's a lot of old bitrot code that looks brilliant and I wish we could use it. I just now made an X25519 FFI for Lean. And I wrote three type classes for the NIKE:

class Key (key : Type) where
  encode : key → ByteArray
  decode : ByteArray → Option key

class PrivateKey (privkey : Type) extends Key privkey

class PublicKey (pubkey : Type) extends Key pubkey

class NIKE (scheme : Type) where
  PublicKeyType : Type
  PrivateKeyType : Type

  generatePrivateKey : IO PrivateKeyType
  generateKeyPair : IO (PublicKeyType × PrivateKeyType)
  derivePublicKey : PrivateKeyType → PublicKeyType
  groupAction : PrivateKeyType → PublicKeyType → PublicKeyType
  encodePrivateKey : PrivateKeyType → ByteArray
  decodePrivateKey : ByteArray → Option PrivateKeyType
  encodePublicKey : PublicKeyType → ByteArray
  decodePublicKey : ByteArray → Option PublicKeyType

These are the bare minimum which any cryptographic construction that uses a NIKE would need.
And I wrote instances of these for the X25519 FFI API:

https://github.com/katzenpost/crypt_walker/blob/main/Lean/CryptWalker/nike/x25519.lean

I'm new to Lean but not new to maintaining cryptography libraries. The simple idea here is to be able to write cryptographic constructions that use the NIKE scheme and the public and private keys in a generic way so that it's polymorphic over the specific NIKE scheme.

lol what i did here is definitely not good enough. eventually I want to implement X25519 in pure Lean. But having faster FFI options for pure Lean cryptographic primitives is actually what I want. Multi-use cryptography library for proving protocol properties and for writing implementations in Lean that are fast.

[David Stainton 🦡]

i'd also eventually like to be able to write a spec for the opaque ffi call to curve25519... could a pure implementation of that function also serve as a spec for the FFI opaque function?

[David Stainton 🦡]

I'm the maintainer of this post quantum cryptography library for golang https://github.com/katzenpost/hpqc
and so I will make this lean library in a similar design which allows for lots of flexible composition.

What composition is there to be had in a cryptography library? lots! Firstly, a NIKE to KEM "adapter" is really just a hashed ElGamal construction. Also I want to make a generic "hybrid NIKE" that combines any two NIKEs together into one. likewise for KEMs, a security preserving KEM combiner using the Split PRF design from the KEM Combiners paper might actually produce the KEMs you are looking for.... where Xwing is a well studied hybrid KEM but not easily modified.

With all of that in place, we can combine any number of NIKEs and KEMs together in hybrid constructions, mixing classic and post quantum primitives together.

[David Stainton 🦡]

I actually kind of hate using ProVerif to produce symbolic proof of cryptographic protocol correctness. Instead with about the same amount of effort, eventually, it will be possible to simply use Lean to write a prototype of cryptographic protocols. if running and testing isn't enough assurance of correctness then write theorems and prove them... which seems to be very easy for you all to prove things with Lean. So maybe in the future it will be easy for me too.

Perhaps I need to learn a lot more Lean to do this right. Feedback welcome.

[David Stainton 🦡]

proving this seems hard

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Field.Basic
import Mathlib.Data.ZMod.Basic

namespace CryptWalker.nike.x25519

def p : ℕ := 2^255 - 19

theorem p_is_prime : Nat.Prime p := by sorry
instance fact_p_is_prime : Fact (Nat.Prime p) := ⟨p_is_prime⟩
instance : Field (ZMod p) := ZMod.instField p

end CryptWalker.nike.x25519

[Alix Trieu]

If you want to prove that 2^255 - 19 is prime, I would suggest to look at how this was proved in coq using CoqPrime, and in action here: https://github.com/mit-plv/fiat-crypto/blob/master/src/Spec/Curve25519.v#L16-L34

[Bolton Bailey]

Also, you can see some discussion of Pratt certificates here

[Bolton Bailey]

Cool to hear someone talk about cryptography in lean, I guess I am guilty of making old bitrotting lean cryptography code as much as anyone. I wonder what you visualize as being in scope for this library: Code-based cryptography? Linear PCP SNARKs? Category-theoretical presentations of the UC framework? Will it include proofs of security? In what model? Game based? Simulation Based? Plain? ROM?

[David Stainton 🦡]

I'd like to write a cryptography library that is useful for prototyping (or implementing) cryptographic protocols that i use in the katzenpost mixnet development. Things like KEM double ratchet, Sphinx cryptographic packet format, PAKE protoocols, etc.

Currently Katzenpost has no use for zero knowledge proof systems and I personally have no experience with such things. The kinds of cryptographic primitives that I want to exist in a Lean library include:

NIKE
KEM
PRF
HMAC
KDF
PRP
stream cipher/PRG
AEAD
signature schemes like ed25519 and Sphincs+

[David Stainton 🦡]

also there ought to be a Noise protocol framework library for Lean. Currently also Katzenpost is the only project in the world that uses the PQ Noise Protocol framework which is essentially algebraic transformations from the Noise patterns to PQ Noise patterns where ECDH is replaced by KEM encap/decap usage.

[David Stainton 🦡]

I am not a proof engineer. I cannot prove things but maybe I will learn. I am concerned with writing working Lean code but less concerned with proving say... that 2^255-19 is prime. But I can help keep track of such goals and maybe we can give that task to a student.

[Eric Wieser]

Alix Trieu said:

If you want to prove that 2^255 - 19 is prime, I would suggest to look at how this was proved in coq using CoqPrime, and in action here: https://github.com/mit-plv/fiat-crypto/blob/master/src/Spec/Curve25519.v#L16-L34

This thread is pretty amusing

[David Stainton 🦡]

Are the Lean core devs planning on making the ByteArray .... polymorphic over the size in bytes.... like in Rust?

[David Stainton 🦡]

I just realized that my type class above for the NIKE needs to have two more functions to return the private and public key sizes in bytes

[David Stainton 🦡]

Currently with the way ByteArray is, I don't specify the size of byte blobs in the function signature, so the safe sane thing to do is to check the size of such blobs where appropriate.

[David Stainton 🦡]

Or... there's probably several nice ways to carry along that size information.

[David Stainton 🦡]

OMG finally! i got my pure Lean X25519 to work!

[David Stainton 🦡]

that was so hard!... or easy now that i have hindsight ;-)

[David Stainton 🦡]

Is there a benchmarking library for lean?

[David Stainton 🦡]

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Field.Basic
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.ByteArray

import CryptWalker.util.newnat
import CryptWalker.util.newhex

namespace CryptWalker.nike.x25519pure

def p : ℕ := 2^255 - 19
def basepoint : ZMod p := 9
theorem p_is_prime : Nat.Prime p := by sorry
instance fact_p_is_prime : Fact (Nat.Prime p) := ⟨p_is_prime⟩
instance : Field (ZMod p) := ZMod.instField p

def clampScalarBytes (scalarBytes : ByteArray) : ByteArray :=
  let clamped1 := scalarBytes.set! 0 (scalarBytes.get! 0 &&& 0xf8)
  let clamped2 := clamped1.set! 31 ((clamped1.get! 31 &&& 0x7f) ||| 0x40)
  clamped2

def zmodToByteArray (x : ZMod p) : ByteArray :=
  let bytes := ByteArray.mk $ Array.mk $ (ByteArray.toList $ natToBytes x.val).reverse
  bytes ++ ByteArray.mk (Array.mk (List.replicate (32 - bytes.size) 0))

def byteArrayToZmod (ba : ByteArray) : ZMod p :=
  let n := (ByteArray.mk $ Array.mk ba.toList.reverse).foldl (fun acc b => acc * 256 + b.toNat) 0
  n

def clampScalar (scalar : ZMod p) : ZMod p :=
  let b := zmodToByteArray scalar
  let newB := clampScalarBytes b
  byteArrayToZmod newB

structure LadderState :=
  (x1 : ZMod p)
  (x2 : ZMod p)
  (z2 : ZMod p)
  (x3 : ZMod p)
  (z3 : ZMod p)

def montgomery_step (s : LadderState) : LadderState :=
  let tmp0 := s.x3 - s.z3
  let tmp1 := s.x2 - s.z2
  let x2 := s.x2 + s.z2
  let z2 := s.x3 + s.z3
  let z3 := (tmp0 * x2)
  let z2 := z2 * tmp1
  let tmp0 := tmp1^2
  let tmp1 := x2^2
  let x3 := z3 + z2
  let z2 := z3 - z2
  let x2 := tmp1 * tmp0
  let tmp1 := tmp1 - tmp0
  let z2 := z2^2
  let z3 := tmp1 * 121666
  let x3 := x3^2
  let tmp0 := tmp0 + z3
  let z3 := s.x1 * z2
  let z2 := tmp1 * tmp0
  { s with x2 := x2, z2 := z2, x3 := x3, z3 := z3 }

def montgomery_ladder (scalar : ZMod p) (point : ZMod p) : LadderState :=
  let e : ByteArray := zmodToByteArray scalar
  let initState : LadderState := {
    x1 := point,
    x2 := 1,
    z2 := 0,
    x3 := point,
    z3 := 1
  }
  let finalState := (List.range 255).reverse.foldl (fun (state, swap) pos =>
    let byteIndex := pos / 8
    let bitIndex := pos % 8
    let b : UInt8 := Nat.toUInt8 ((e.get! byteIndex).toNat >>> bitIndex) &&& 1
    let newSwap := swap ^^^ b
    let (x2, x3) := if newSwap == 1 then (state.x3, state.x2) else (state.x2, state.x3)
    let (z2, z3) := if newSwap == 1 then (state.z3, state.z2) else (state.z2, state.z3)
    let newState := montgomery_step { state with x2 := x2, x3 := x3, z2 := z2, z3 := z3 }
    (newState, b)
  ) (initState, 0)

  let finalSwap := finalState.snd
  let finalState := finalState.fst
  let (x2, x3) := if finalSwap == 1 then (finalState.x3, finalState.x2) else (finalState.x2, finalState.x3)
  let (z2, z3) := if finalSwap == 1 then (finalState.z3, finalState.z2) else (finalState.z2, finalState.z3)
  { finalState with x2 := x2, x3 := x3, z2 := z2, z3 := z3 }

def scalarmult (scalarBytes : ByteArray) (point : ZMod p) : ZMod p :=
  let clampedScalar := byteArrayToZmod $ clampScalarBytes scalarBytes
  let finalState := montgomery_ladder clampedScalar point
  finalState.x2 * finalState.z2⁻¹

def curve25519 (scalarBytes : ByteArray) (point : ByteArray) : ByteArray :=
  zmodToByteArray $ scalarmult scalarBytes $ byteArrayToZmod point

end CryptWalker.nike.x25519pure

[David Stainton 🦡]

my manual benchmarking shows this x25519 to be about 80,000 ns per group operation. whereas in golang with an optimized implementation of x25519 i get about 40,000 ns per group op.

I see that timeit will be in a future release of the standard lean library so then i'll be able to use it for benchmarking. until then, my manual benchmarking process sucks so i probably won't do it that much.

[Eric Wieser]

Are you compiling to a binary or timing in the editor?

[David Stainton 🦡]

compile to binary. program runs group action 10,000 times. run program on commandline with "time" command to measure time. use calculator to divide elapsed time by 10,000. duh manual benchmark for real huuugaaa boogaa caveman like myself.

[David Stainton 🦡]

the fact that Lean doesn't have a benchmark library is extremely frustrating.

[David Stainton 🦡]

the fact that everyone so far cannot even admit this shortcoming is also frustrating.

[David Stainton 🦡]

dudes... general purpose programming languages all have benchmark libraries. Lean doesn't only because it's new... and not for a another reason other than that.

[David Stainton 🦡]

perhaps there are some technical reasons wrapped up in this situation. like... if you compile a C object file then maybe benchmarking that is more accurate. sure but way less convenient to use C tooling.

[David Stainton 🦡]

benchmarking from a text editor is a hilarious suggestion that must've been meant as a joke

[David Stainton 🦡]

um oh also i'm rocking Lean stable so i don't get to use timeit until that function is landed in stable... so it would not even be possible for me to benchmark from my text editor.

[Eric Wieser]

David Stainton said:

benchmarking from a text editor is a hilarious suggestion that must've been meant as a joke

I'm referring to set_option trace.profiler true in, which profiles rather than benchmarks. Since much of lean is used in-editor, the performance of the interpreter in the editor is something that the community cares about a lot.

[Eric Wieser]

David Stainton said:

um oh also i'm rocking Lean stable so i don't get to use timeit until that function is landed in stable... so it would not even be possible for me to benchmark from my text editor.

I don't know what you mean by "stable", but timeit is in 4.10.0 which is the latest stable release

[David Stainton 🦡]

okay i think i might have a local tooling problem that i need to fix. it prevents me from using timeint although i'm using 4.10.0

[David Stainton 🦡]

whenever i build my lean project with lake it downloads the latest lean leanprover/lean4:v4.11.0-rc2

[David Stainton 🦡]

recently got more ECDH curves working: X448 and X41417