From bb917b3a60eca3b419aef3344aa0dcb5f1bf2022 Mon Sep 17 00:00:00 2001 From: David Stainton Date: Sat, 17 Oct 2026 21:09:52 +0200 Subject: [PATCH 1/8] Update readme and website front page --- README.md | 18 ------ docs/site/CryptLib/Front.lean | 111 +++++++++++++++++++++------------- 2 files changed, 70 insertions(+), 59 deletions(-) diff --git a/README.md b/README.md index 9a0f3c1d..decd95da 100644 --- a/README.md +++ b/README.md @@ -14,24 +14,6 @@ It's got a struct field called "commutes" we says that the group operation is co This is a proof burden to anyone writing an instance of the NIKE type, say for X25519, you need to prove the "commutes" hypothesis for your specific type instance. -This library so far has two implementations of X25519. One of them, a -montgomery ladder implementation, I ported from rust to lean mostly by -hand. Too difficult to prove the operations commute. The other is -entirely written by an LLM agent specifically to have an easy proof. -It uses an existing lean elliptic curve API that exists in mathlib, -and therefore already has existing group lemmas that says the group -operations commute. Therefore the proof is one or two lines of code. - -This library is also a mix of Lean code written by humans and by LLM agents. -We mitigate LLM slop code by means of test vector based unit tests. -For example when implementing BACAP and Sphinx, we first ensured all the necessary test vectors -were present in the hpqc golang cryptography library, here: https://github.com/katzenpost/hpqc -Then we copied those test vectors into the Cryptlib git repo and used them in our verification -step to ensure every cryptographic primitive was implemented correctly. - -TODO: we should probably include all the KAT test vectors for every cryptographic primitive implemented -in this library. - ## cryptographic primitives diff --git a/docs/site/CryptLib/Front.lean b/docs/site/CryptLib/Front.lean index 3451ca9b..9afb5147 100644 --- a/docs/site/CryptLib/Front.lean +++ b/docs/site/CryptLib/Front.lean @@ -5,44 +5,73 @@ open Verso Genre Blog # Abstract -Cryptlib is an experiment in using dependent types to represent cryptographic primitives. -The usual approach is to write the code first and the theorems about it later. Cryptlib works -the other way round. Each kind of primitive is a dependently typed structure that holds the -primitive's data and operations, plus one or more proposition fields that state what we would want -to prove about it. Writing an instance of the structure means discharging those propositions. -Correctness obligations are part of the interface, not an afterthought. - -The non-interactive key exchange (NIKE) type shows the idea. It has a field called `commutes` -which states that the group operation is commutative: g^x^y = g^y^x. Anyone who provides a NIKE -instance, X25519 for example, has to prove `commutes` for that instance. Cryptlib contains two -X25519 implementations. The first is a constant-time Montgomery ladder ported from Rust by hand, -and proving commutativity for it directly is hard. The second is built on Mathlib's elliptic-curve -API. Mathlib already proves the group laws, so its proof takes a line or two. - -# Overview - -The library covers the building blocks of modern, post-quantum-ready protocols: - -* *Key exchange and key encapsulation:* X25519, ML-KEM-768 (FIPS 203), a hedged ML-KEM-768 - variant, and a security-preserving KEM combiner that builds X25519 + ML-KEM-768 hybrids. -* *Signatures:* Ed25519, plain and blinded. -* *Authenticated encryption:* AES-256-GCM-SIV. -* *Hashing:* SHA-2, BLAKE2b and its XOF. -* *Key derivation:* HKDF and Argon2. -* *Stream ciphers and wide-block ciphers:* AES-CTR, ChaCha20 and AEZ. - -On top of these primitives sit two protocol components. The first is the Sphinx packet format, in -both its NIKE and KEM forms, with any number of hops. The second is BACAP (Blinded Cryptographic -Capabilities), a building block for private messaging systems. - -Interoperability is checked byte for byte. The test suites run known-answer vectors from NIST ACVP -and the relevant RFCs, plus vectors from the Go implementations in -[hpqc](https://github.com/katzenpost/hpqc) and [Katzenpost](https://github.com/katzenpost/katzenpost), -which are copied into the repository. Cryptlib's Sphinx packets are binary compatible with the -Katzenpost mixnet's Sphinx implementation, including when the per-hop KEM is the post-quantum -hybrid. - -Cryptlib is written partly by people and partly by LLM agents. Vector-based tests are how we keep -that code honest: no primitive counts as implemented until it reproduces the reference outputs -exactly. The library is free software under the AGPLv3. Its API reference is generated directly -from the Lean sources. +Cryptlib started off as a Lean model of the Golang (and python, rust) cryptography library [hpqc](https://github.com/katzenpost/hpqc/), +hybrid post quantum cryptography, which is used by the [Katzenpost](https://katzenpost.network/) post quamtum decryption mix network. + +Beyond that we have two main goals: + +* Cryptlib can be used to write real cryptography applications in Lean for high assurance security applications +* Cryptlib can also be used to prove cryptographic security properties of primitives and protocols + +In Cryptlib we create a Lean structure type which provides a generic definition for a cryptographic primitive +such as a NIKE (non-interactive key exchange). In languages like Rust traits are mere empty husks +that defines one or more function signatures. There's no trait or interface type in Lean. Instead +we use a structure type in Lean to define a generic cryptographic primitive such as NIKE where some +of the fields contain functions and some of the fields contain data types etc. This is Lean representing +cryptographic primitives in a generic way like Rust or Golang. To take things a step further, we +use dependent types in Lean! For example our NIKE structure type has a proposition that says +the group operation is commutative: + +```lean demo +structure NIKE where +/-- ... --/ + commutes : ∀ sk₁ sk₂, + groupAction sk₁ ⟨derivePublicKey sk₂, derive_safe sk₂⟩ + = groupAction sk₂ ⟨derivePublicKey sk₁, derive_safe sk₁⟩ +``` +**code block caption**: This code block is found in cryptlib here +https://github.com/katzenpost/cryptlib/blob/main/Cryptlib/Primitives/NIKE/NIKE.lean#L12-L73 + +In cryptlib each category of cryptographic primitive shall have a structure type defining +the primitive generically. The type definition will define functions and data types as well as +propositions about that cryptographic primitive. Another example is our generic definition of +the KEM (key encapsulation mechanism) is here: + +```lean demo +structure KEM where +/-- ... --/ + /-- Pre-encapsulation states that cannot cause a decryption failure. `True` for a perfectly + correct KEM; a lattice KEM restricts it to states whose sampled noise stays within bounds. -/ + Reliable : State → Prop := fun _ => True + /-- Round trip for any private key and its derived public key, from a `Reliable` state. -/ + honestRoundTrip : ∀ sk, ∀ s, Reliable s → ∀ c k s', encap (derivePublicKey sk) s = .ok (c, k) s' → + ∀ t, ∃ t', decap sk c t = .ok k t' +``` +**code block caption**: This code block is found in cryptlib here: +https://github.com/katzenpost/cryptlib/blob/main/Cryptlib/Primitives/KEM/KEM.lean#L13-L65 + +There are some obvious and not so obvious benefits of a cryptography library that uses dependent +types to create these additional proof obligations. The most obvious is that it ensures each instance +of these types at least meets the low bar of quality and satisfies the type proposition fields. +However a less obvious advantage is that we get formalized definitions with fewer transitive proof obligations +overall when we compose these dependent types together. + +As an example, we define a NIKE to KEM adapter which is just a hashed ElGamal construction. In Lean it's possible to +write a theorem that says that my NIKE to KEM adapter produces a lawful KEM if it is given a lawful NIKE. However there +is no need to even write that thereom in the first place if dependent types for the NIKE and KEM definitions are +used because they make it impossible to create a type instance that violates their type's proposition fields. + +Our cryptlib NIKE to KEM adapter definition is here: +https://github.com/katzenpost/cryptlib/blob/main/Cryptlib/Primitives/KEM/Adapter.lean#L119-L161 + +This is an example of our usage of depedent types enforcing a proof implicitly and it can do so transitively +as primitive functions are composed together. In many ways this simplifies the proof obligations of the composed protocol. + + + + + + + + + From a2d96eb72b014fb9621af0eac7011980cc4efaab Mon Sep 17 00:00:00 2001 From: Mycroft Date: Sat, 17 Oct 2026 19:16:02 +0000 Subject: [PATCH 2/8] Drop the lock icon and section links, fix the front page's Lean blocks, add code captions The front page's lean blocks had no leanInit context and excerpted code the site cannot import, so the page failed to build. They are now abridged copies of the NIKE and KEM structures that compile in core Lean, each with a small italic caption linking to the source lines at a fixed commit. --- docs/site/CryptLib/Front.lean | 116 ++++++++++++++++++++-------------- docs/site/Main.lean | 13 +--- docs/site/static/favicon.svg | 1 - docs/site/static/style.css | 10 ++- 4 files changed, 74 insertions(+), 66 deletions(-) delete mode 100644 docs/site/static/favicon.svg diff --git a/docs/site/CryptLib/Front.lean b/docs/site/CryptLib/Front.lean index 9afb5147..94137ce4 100644 --- a/docs/site/CryptLib/Front.lean +++ b/docs/site/CryptLib/Front.lean @@ -3,75 +3,97 @@ open Verso Genre Blog #doc (Page) "Cryptlib" => +```leanInit demo +``` + +```lean demo -show +inductive KEMError where + | badCiphertext + | unsafePublicKey +``` + # Abstract -Cryptlib started off as a Lean model of the Golang (and python, rust) cryptography library [hpqc](https://github.com/katzenpost/hpqc/), -hybrid post quantum cryptography, which is used by the [Katzenpost](https://katzenpost.network/) post quamtum decryption mix network. +Cryptlib started off as a Lean model of [hpqc](https://github.com/katzenpost/hpqc/) (hybrid +post-quantum cryptography), a Go, Python and Rust cryptography library used by the +[Katzenpost](https://katzenpost.network/) post-quantum decryption mix network. Beyond that we have two main goals: -* Cryptlib can be used to write real cryptography applications in Lean for high assurance security applications -* Cryptlib can also be used to prove cryptographic security properties of primitives and protocols +* Cryptlib can be used to write real, high-assurance cryptography applications in Lean. +* Cryptlib can be used to prove security properties of cryptographic primitives and protocols. -In Cryptlib we create a Lean structure type which provides a generic definition for a cryptographic primitive -such as a NIKE (non-interactive key exchange). In languages like Rust traits are mere empty husks -that defines one or more function signatures. There's no trait or interface type in Lean. Instead -we use a structure type in Lean to define a generic cryptographic primitive such as NIKE where some -of the fields contain functions and some of the fields contain data types etc. This is Lean representing -cryptographic primitives in a generic way like Rust or Golang. To take things a step further, we -use dependent types in Lean! For example our NIKE structure type has a proposition that says -the group operation is commutative: +For each kind of cryptographic primitive, such as a NIKE (non-interactive key exchange), Cryptlib +defines a Lean structure type that describes the primitive generically. In a language like Rust a +trait is an empty husk that only declares function signatures. Cryptlib uses a structure instead, +where some fields hold functions and others hold data types. So far this is how Rust or Go would +represent a primitive generically. Lean lets us go a step further with dependent types: a field can +also be a proposition. For example, our NIKE structure has a field stating that the group operation +is commutative: ```lean demo structure NIKE where -/-- ... --/ + PrivateKey : Type + PublicKey : Type + SharedSecret : Type + -- ... + Safe : PublicKey → Prop + derivePublicKey : PrivateKey → PublicKey + groupAction : PrivateKey → {pk : PublicKey // Safe pk} → SharedSecret + -- ... + derive_safe : ∀ sk, Safe (derivePublicKey sk) + -- ... commutes : ∀ sk₁ sk₂, groupAction sk₁ ⟨derivePublicKey sk₂, derive_safe sk₂⟩ = groupAction sk₂ ⟨derivePublicKey sk₁, derive_safe sk₁⟩ ``` -**code block caption**: This code block is found in cryptlib here -https://github.com/katzenpost/cryptlib/blob/main/Cryptlib/Primitives/NIKE/NIKE.lean#L12-L73 -In cryptlib each category of cryptographic primitive shall have a structure type defining -the primitive generically. The type definition will define functions and data types as well as -propositions about that cryptographic primitive. Another example is our generic definition of -the KEM (key encapsulation mechanism) is here: +:::htmlDiv (class := "caption") +Abridged from [`Cryptlib/Primitives/NIKE/NIKE.lean`](https://github.com/katzenpost/cryptlib/blob/2165380e906475ac966b72c272c527c93ef2b15b/Cryptlib/Primitives/NIKE/NIKE.lean#L12-L73) +::: + +Each category of cryptographic primitive in Cryptlib has a structure type like this one, defining +its functions and data types together with propositions about the primitive. Our generic definition +of a KEM (key encapsulation mechanism) is another example: ```lean demo structure KEM where -/-- ... --/ + State : Type + PublicKey : Type + PrivateKey : Type + Ciphertext : Type + Plaintext : Type + -- ... + decap : PrivateKey → Ciphertext → EStateM KEMError State Plaintext + encap : PublicKey → EStateM KEMError State (Ciphertext × Plaintext) + /-- Pre-encapsulation states that cannot cause a decryption failure. `True` for a perfectly correct KEM; a lattice KEM restricts it to states whose sampled noise stays within bounds. -/ Reliable : State → Prop := fun _ => True + -- ... + derivePublicKey : PrivateKey → PublicKey + /-- Round trip for any private key and its derived public key, from a `Reliable` state. -/ honestRoundTrip : ∀ sk, ∀ s, Reliable s → ∀ c k s', encap (derivePublicKey sk) s = .ok (c, k) s' → ∀ t, ∃ t', decap sk c t = .ok k t' ``` -**code block caption**: This code block is found in cryptlib here: -https://github.com/katzenpost/cryptlib/blob/main/Cryptlib/Primitives/KEM/KEM.lean#L13-L65 - -There are some obvious and not so obvious benefits of a cryptography library that uses dependent -types to create these additional proof obligations. The most obvious is that it ensures each instance -of these types at least meets the low bar of quality and satisfies the type proposition fields. -However a less obvious advantage is that we get formalized definitions with fewer transitive proof obligations -overall when we compose these dependent types together. - -As an example, we define a NIKE to KEM adapter which is just a hashed ElGamal construction. In Lean it's possible to -write a theorem that says that my NIKE to KEM adapter produces a lawful KEM if it is given a lawful NIKE. However there -is no need to even write that thereom in the first place if dependent types for the NIKE and KEM definitions are -used because they make it impossible to create a type instance that violates their type's proposition fields. - -Our cryptlib NIKE to KEM adapter definition is here: -https://github.com/katzenpost/cryptlib/blob/main/Cryptlib/Primitives/KEM/Adapter.lean#L119-L161 - -This is an example of our usage of depedent types enforcing a proof implicitly and it can do so transitively -as primitive functions are composed together. In many ways this simplifies the proof obligations of the composed protocol. - - - - - - - - +:::htmlDiv (class := "caption") +Abridged from [`Cryptlib/Primitives/KEM/KEM.lean`](https://github.com/katzenpost/cryptlib/blob/2165380e906475ac966b72c272c527c93ef2b15b/Cryptlib/Primitives/KEM/KEM.lean#L13-L65) +::: + +A cryptography library that uses dependent types to add these proof obligations has some obvious +and some less obvious benefits. The obvious one is that every instance of these types meets at +least a basic bar of quality: it satisfies the type's proposition fields. A less obvious advantage +is that when we compose these types, the resulting definitions carry fewer transitive proof +obligations overall. + +For example, we define a NIKE-to-KEM adapter, which is a hashed ElGamal construction. In Lean we +could write a theorem saying the adapter produces a lawful KEM whenever it is given a lawful NIKE. +But with dependent types for the NIKE and KEM definitions there is no need to write that theorem at +all, because it is impossible to construct an instance that violates its type's proposition fields. +See our [NIKE-to-KEM adapter](https://github.com/katzenpost/cryptlib/blob/2165380e906475ac966b72c272c527c93ef2b15b/Cryptlib/Primitives/KEM/Adapter.lean#L119-L161). + +This is an example of dependent types enforcing a proof implicitly, and they keep doing so +transitively as primitives are composed. In many ways this simplifies the proof obligations of the +composed protocol. diff --git a/docs/site/Main.lean b/docs/site/Main.lean index 472e3865..a630dcec 100644 --- a/docs/site/Main.lean +++ b/docs/site/Main.lean @@ -6,14 +6,6 @@ open Verso.Output Html Template Theme def repo := "https://github.com/katzenpost/cryptlib" -def logo : Html := {{ - -}} - def primary (version : String) : Template := do let posts := match (← param? "posts") with | none => Html.empty @@ -26,15 +18,13 @@ def primary (version : String) : Template := do {{s!"{← param (α := String) "title"} · Cryptlib"}} {{← builtinHeader}} -
- {{logo}}"Cryptlib" + "Cryptlib"
{{← param "content"}} - {{posts}}