diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 5b6ea796..18e14598 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -1,9 +1,7 @@ name: Lean Action CI on: - push: pull_request: - workflow_dispatch: jobs: build: 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.lean b/docs/site/CryptLib.lean index dc91598f..5c4d454a 100644 --- a/docs/site/CryptLib.lean +++ b/docs/site/CryptLib.lean @@ -1,6 +1 @@ import CryptLib.Front -import CryptLib.Overview -import CryptLib.Primitives -import CryptLib.GettingStarted -import CryptLib.Blog -import CryptLib.Blog.Hello diff --git a/docs/site/CryptLib/Blog.lean b/docs/site/CryptLib/Blog.lean deleted file mode 100644 index ee403f3d..00000000 --- a/docs/site/CryptLib/Blog.lean +++ /dev/null @@ -1,6 +0,0 @@ -import VersoBlog -open Verso Genre Blog - -#doc (Page) "Blog" => - -News, notes and technical reports from the Cryptlib project. diff --git a/docs/site/CryptLib/Blog/Hello.lean b/docs/site/CryptLib/Blog/Hello.lean deleted file mode 100644 index a87d1639..00000000 --- a/docs/site/CryptLib/Blog/Hello.lean +++ /dev/null @@ -1,15 +0,0 @@ -import VersoBlog -open Verso Genre Blog - -#doc (Post) "Cryptlib has a website" => -%%% -authors := ["The Cryptlib authors"] -date := {year := 2026, month := 10, day := 16} -%%% - -Cryptlib now has a home on the web. Besides this blog, the site hosts the -[API reference](api/), generated by doc-gen4 straight from the Lean sources for every module, -definition and lemma in the library. - -Future posts will cover how individual primitives are specified and proved, and how we check them -against reference implementations. diff --git a/docs/site/CryptLib/Front.lean b/docs/site/CryptLib/Front.lean index 3451ca9b..c9ea8002 100644 --- a/docs/site/CryptLib/Front.lean +++ b/docs/site/CryptLib/Front.lean @@ -3,46 +3,108 @@ open Verso Genre Blog #doc (Page) "Cryptlib" => +```leanInit demo +``` + +```lean demo -show +inductive KEMError where + | badCiphertext + | unsafePublicKey +``` + # 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 [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 software that a user can run on their computer, perhaps high assurance security software +or perhaps protocol simulators. +* Cryptlib can be used to prove security properties of cryptographic primitives and protocols, where we only need lean's type checking and aren't using any build artifacts. + +So in that sense the "specification rides along with the code". + +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. It's +still a useful contract; all instances must define the trait's +methods. In Lean you do this with a structure type which has fields +with function definitions. All instances of the structure type must +define an implementation of the type's specified function +fields. Cryptlib uses a structure 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₁⟩ +``` + +:::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' +``` + +:::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/CryptLib/GettingStarted.lean b/docs/site/CryptLib/GettingStarted.lean deleted file mode 100644 index 7df47761..00000000 --- a/docs/site/CryptLib/GettingStarted.lean +++ /dev/null @@ -1,42 +0,0 @@ -import VersoBlog -open Verso Genre Blog - -#doc (Page) "Getting started" => - -# Build - -Cryptlib builds with Lake, using the toolchain pinned in `lean-toolchain`: - -``` -git clone https://github.com/katzenpost/cryptlib -cd Cryptlib -lake exe cache get # fetch prebuilt Mathlib -lake build -``` - -# Use it as a dependency - -``` -[[require]] -name = "Cryptlib" -git = "https://github.com/katzenpost/cryptlib" -rev = "main" -``` - -# Test - -``` -make test # build everything and run every suite -make help # list every target, including one per suite -``` - -The suites read their known-answer vectors from `testdata/` by relative path, so run them from the -repository root. - -# Benchmark - -``` -make bench # every NIKE, KEM and Sphinx benchmark -make bench-kem # one suite -make bench BENCH_ARGS='--match "kem MLKEM768 decap"' -``` diff --git a/docs/site/CryptLib/Overview.lean b/docs/site/CryptLib/Overview.lean deleted file mode 100644 index 7336f031..00000000 --- a/docs/site/CryptLib/Overview.lean +++ /dev/null @@ -1,40 +0,0 @@ -import VersoBlog -open Verso Genre Blog - -#doc (Page) "Overview" => - -# Proof obligations as structure fields - -In Cryptlib, every kind of primitive (NIKE, KEM, signature scheme and so on) is a Lean -structure. The structure holds the primitive's types and operations, and also propositions about -those operations. To give an instance, you have to supply proofs of those propositions, so every -instance satisfies them by construction. - -For example, the NIKE structure has a `commutes` field stating that deriving a shared secret from -either side gives the same result, g^x^y = g^y^x. An X25519 instance that compiles is an X25519 -whose key agreement provably agrees. - -# Two X25519 implementations - -The repository contains two implementations of X25519: - -* A constant-time Montgomery ladder following RFC 7748, ported from Rust by hand. Proving - commutativity for the ladder directly is hard. -* An implementation on top of Mathlib's Weierstrass-curve API. Mathlib already proves the group - laws, so `commutes` follows almost immediately. - -# Test vectors - -Proofs cover the properties the types state. Byte-level agreement with other implementations is -checked with known-answer vectors: - -* NIST ACVP vectors for ML-KEM-768. -* RFC vectors for Ed25519, Argon2, HKDF and AES-GCM-SIV. -* Vectors generated by the Go libraries [hpqc](https://github.com/katzenpost/hpqc) and - [Katzenpost](https://github.com/katzenpost/katzenpost). - -These vectors are copied into `testdata/`, and `make verify-vectors` checks them against their -upstream sources. - -Some of the code is written by LLM agents. Vectors are the gate that every such contribution has to -pass. diff --git a/docs/site/CryptLib/Primitives.lean b/docs/site/CryptLib/Primitives.lean deleted file mode 100644 index 9d9fa0f2..00000000 --- a/docs/site/CryptLib/Primitives.lean +++ /dev/null @@ -1,63 +0,0 @@ -import VersoBlog -open Verso Genre Blog - -#doc (Page) "Primitives" => - -# NIKE: non-interactive key exchange - -* X25519, constant-time Montgomery ladder (RFC 7748) -* X25519 over Mathlib's Weierstrass-curve API - -# KEM: key encapsulation - -* X25519 turned into a KEM with hashed ElGamal (the NIKE-to-KEM adapter), using either the - `blake2b-xof` or the `sha256-v1` PRF -* ML-KEM-768 (FIPS 203), built from [VCVio](https://github.com/dtumad/VCV-io)'s pure-Lean NTT, CBD - and encoding, checked against NIST ACVP vectors -* Hedged ML-KEM-768, which hashes the encapsulation message before use -* A KEM combiner (Giacon–Heuer–Poettering split-PRF, keyed BLAKE2b-256) over any number of - ingredient KEMs, instantiated as X25519 + ML-KEM-768 and cross-checked against hpqc - -# Signatures - -* Ed25519 (RFC 8032), plain and blinded - -# AEAD - -* AES-256-GCM-SIV (RFC 8452) - -# Hash functions and XOFs - -* SHA-256, SHA-512, SHA-512/256 -* BLAKE2b, keyed and unkeyed, any digest length -* BLAKE2Xb - -# MAC - -* HMAC-SHA256 (RFC 2104) - -# Stream ciphers - -* AES-256-CTR -* ChaCha20 - -# Wide-block cipher - -* AEZ v5, restricted to the parameters Sphinx uses - -# KDF - -* HKDF-BLAKE2b-512, HKDF-SHA256 (RFC 5869) -* Argon2d, Argon2i, Argon2id (RFC 9106) - -# Data structures - -* Binary Merkle hash tree, polymorphic over the hash function - -# Protocol components - -* *Sphinx:* the mix network packet format, in both NIKE and KEM variants. It works with any number - of hops, any KEM or NIKE and any payload size, and is binary compatible with Katzenpost, including - with the X25519 + ML-KEM-768 hybrid as the per-hop KEM. -* *BACAP:* Blinded Cryptographic Capabilities, which works like a private distributed hash table - and is used to build messaging systems. diff --git a/docs/site/Main.lean b/docs/site/Main.lean index 472e3865..b9019333 100644 --- a/docs/site/Main.lean +++ b/docs/site/Main.lean @@ -6,18 +6,7 @@ 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 - | some html => {{ }} return {{ @@ -26,15 +15,13 @@ def primary (version : String) : Template := do {{s!"{← param (α := String) "title"} · Cryptlib"}} {{← builtinHeader}} -
- {{logo}}"Cryptlib" + "Cryptlib"
{{← param "content"}} - {{posts}}