learning-μCMZ primitives roadmap

A hands-on, from-the-paper reimplementation of the basic cryptographic components underlying μCMZ, in Lean 4. The goal is to build intuition by implementing each primitive rather than reusing any existing model.

The reference is Michele Orrù, Revisiting Keyed-Verification Anonymous Credentials, IACR ePrint 2024/1552, cited as O24. Section numbers below point into O24. This project tracks the paper only. It does not follow the layout or design of any other KVAC codebase.

The current scope is primitives only. We stop at the abstract primitive interfaces of §3. The KVAC framework (§4) and the μCMZ scheme itself (§5) are out of scope for now, but the primitives below are exactly the pieces μCMZ is assembled from.

Where the primitives live in O24

The credential schemes (§5 μCMZ, §6 μBBS) are built on the abstract primitives defined in §3 Preliminaries, which are in turn instantiated with a handful of classical group-based building blocks (Pedersen, ElGamal, Schnorr) described in the technical overview (§2.1) and used concretely in §5.1. Our build order goes bottom-up.

  Layer 0  algebraic setting        §3 (Notation), §3.1
              │   prime-order group Γ=(𝔾,p,G); hash oracles H_p, H_𝔾; assumptions
              ▼
  Layer 1  commitments & encryption  building blocks for §5
              │   Pedersen commitment; additively-homomorphic ElGamal
              ▼
  Layer 2  zero-knowledge proofs     §2.6, §3.3, §9
              │   Schnorr Σ-protocol; linear-relation (representation) proofs;
              │   Fiat–Shamir → NIZK; the ZKP=(S,P,V) interface
              ▼
  Layer 3  algebraic MAC             §3.2 (Def 3.1, Fig 5)
              │   MAC=(S,K,M,V) interface + UF-CMVA game (O24 §3.2); the MAC_GGM
              │   construction is CMZ14, used in O24 only via the µCMZ figures
              ▼
  Layer 4  primitive interfaces      §3.3, §3.4
                  NIZK syntax; anonymous-token syntax AT=(S,K,I,V) + OMUF game
                  ── boundary, KVAC syntax (§4.1) is the *scheme*, not a primitive ──

Primitive inventory (the build list)

#	Primitive	O24	What we implement
0a	Prime-order group Γ = (𝔾, p, G)	§3 Notation	scalar field ℤ_p, group 𝔾 of odd prime order p, generator G, scalar mult x•P, group law; GrGen
0b	Hash oracles H_p, H_𝔾	§3 Notation	H_p : {0,1}* → ℤ_p and H_𝔾 : {0,1}* → 𝔾 (random-oracle interfaces)
0c	Hardness assumptions	§3.1	DL, DDH, gap-DL, q-DL, q-DDHI as game definitions (so the security notions are statable). Optional / illustrative.
1a	Pedersen commitment	used in §5.1	Com(m; r) = m•G + r•H; vector version; hiding + binding (stated)
1b	ElGamal encryption	§2.1, §5.1	encryption over 𝔾 under a user key Y; additively homomorphic in the exponent (the issuance trick)
2a	Schnorr Σ-protocol	§2.6	PoK of discrete log via (commit, challenge, response) messages; completeness, special soundness, HVZK
2b	Linear-relation / representation proofs	§5.1	the workhorse Σ-protocol for "X = Σ aᵢ•Bᵢ" used in presentation
2c	Fiat–Shamir → NIZK	§3.3	non-interactive transform via H_p; yields the ZKP = (S, P, V) interface
3	Algebraic MAC	§3.2 (interface + game); CMZ14 (construction)	MAC = (S, K, M, V) and the UF-CMVA game from O24 §3.2; the concrete MAC_GGM V = (x₀ + Σ xᵢmᵢ)•U is from Chase–Meiklejohn–Zaverucha (CCS'14, doi:10.1145/2660267.2660328), appearing in O24 only through the µCMZ figures (§2.3 Fig 1, §5.1 Fig 9)
4a	NIZK syntax + properties	§3.3	completeness, knowledge-soundness, zero-knowledge, simulation-extractability (as the abstract interface μCMZ assumes)
4b	Anonymous-token syntax	§3.4	AT = (S, K, I, V); one-more-unforgeability (OMUF) game, Fig 6

Key definitions pulled from O24 §3 (for reference while implementing)

• Group setting (§3, Notation). GrGen(1^λ) → Γ = (𝔾, p, G) produces a group 𝔾 of odd prime order p generated by G. There are two random oracles, H_p : {0,1}* → ℤ_p and H_𝔾 : {0,1}* → 𝔾. Written additively (xG, X = xG).
• Algebraic MAC (§3.2, Def 3.1). MAC = (S, K, M, V) has four algorithms.
  • crs ← S(1^λ, n) is the setup, which fixes the attribute count n and the message family 𝕄.
  • (sk, pp) ← K(crs) is key generation.
  • σ ← M(sk, m) computes the MAC over attributes m ∈ 𝕄^n and is randomized.
  • 0/1 := V(sk, m, σ) is deterministic verification.
  • The properties are correctness and UF-CMVA unforgeability (game in Fig 5, with Sign and Verify oracles). Remark 3.2 notes that a MAC can be de-randomized in the ROM by seeding its coins with H(m).
• NIZK / ZK argument (§3.3). ZKP = (S, P, V) for a relation family ℛ, with crs ← S(1^λ), π ← P(crs, x, w), and 0/1 ← V(crs, x, π). The properties are completeness, knowledge-soundness (Adv with extractor Ext), zero-knowledge (Adv with simulator Sim), and simulation-extractability.
• Anonymous token (§3.4). AT = (S, K, I, V), a "blind MAC" with optional private metadata bit; correctness, OMUF (Fig 6), unlinkability.

Design decisions (settled)

Decision	Choice	Rationale
Language	Lean 4 (toolchain v4.28.0)	consistency with the surrounding work; VCVio's pin
Scope	primitives only	§3 interfaces + their group-based building blocks
Source	O24 paper only	no reuse of any other KVAC codebase's design
Dependencies	Mathlib + VCVio	ZMod p field; VCVio's PFunctor.FreeM and OracleComp for the randomized/oracle layer
Randomized algorithms	free monad over a PFunctor	one program, two handlers: PMF semantics for correctness, oracle handler for UF-CMVA
Concrete group 𝔾	Schnorr group	order-p subgroup of (ℤ_q)ˣ; #eval-able; Pedersen binding holds honestly (dlog of H base G is unknown)

The toy example instance uses p = 11, q = 23 = 2p+1 (a safe prime), with generator g = 4 (order 11 in (ℤ₂₃)ˣ). The values are tiny, so outputs are readable. The discrete logarithm is trivially recoverable at this size. Increase p, q to cryptographic sizes to make it hard. The algebra (homomorphisms, binding) is honest at any size.

Layout

learning-muCMZ/
├── README.md             this file
├── lakefile.toml         Mathlib + VCVio dependencies
├── lean-toolchain        leanprover/lean4:v4.28.0
├── MuCMZ.lean            library root (each primitive gets a module under MuCMZ/)
├── notes/                tracked notes
│   ├── notes.md          study notes, the project deliverable
│   └── journal.md        design-decision & rationale log
├── doc/                  reserved for Verso/blueprint docs (later)
├── scripts/              tooling
│   └── check-notes-lean.py   type-checks every ```lean block in notes/
└── resources/            paper PDF (untracked, local only)

The main file is notes/notes.md, the project deliverable. Every ```lean block in it is type-checked at commit time by the scripts/hooks/pre-commit git hook, so the notes never contain broken Lean.

Run python3 scripts/check-notes-lean.py to type-check the blocks by hand. It extracts every ```lean block from notes/*.md, concatenates them under a Mathlib and VCVio preamble, and runs `lake env lean`.

Progress

• 0a Prime-order group (PrimeOrderGroup interface plus Schnorr instance)
• 0b Hash oracles H_p, H_𝔾
• 1a Pedersen commitment
• 1b ElGamal encryption
• 2a Schnorr Σ-protocol
• 2b Linear-relation proofs
• 2c Fiat–Shamir → NIZK
• 3 Algebraic MAC (O24 §3.2) — notes §4: MAC=(S,K,M,V), correctness, UF-CMVA game, and MAC_GGM with correctness proved and unforgeability conditional on the GGM hardness assumption
• 4a NIZK syntax + properties
• 4b Anonymous-token syntax + OMUF