Crate golden_dkg 

golden-dkg

Pure-crypto library implementing the Golden non-interactive Distributed Key Generation protocol from Bünz, Choi, Komlo (IACR 2025/1924).

Golden achieves public verifiability in a single broadcast round using an exponent Verifiable Random Function (eVRF) built on Diffie-Hellman key exchange. Security relies only on discrete-log/DDH assumptions over BLS12-381. The output is Shamir secret shares of a field element sk distributed to all participants, together with a public key PK = g^sk.

Protocols

Protocol	Module	Description
DKG	dkg	One-round distributed key generation (Section 5, Figure 4)
Refresh	refresh	Proactive share rotation – same group, rotate shares (Section 5.2)
Reshare	reshare	Membership change – transfer secret to a new group

Quick Start

use golden_dkg::{dkg, types::*};
use std::collections::HashMap;
use ark_bls12_381::G1Affine;
use ark_ff::UniformRand;

let mut rng = rand::rngs::OsRng;

// 1. Each participant generates an identity keypair + proof of knowledge
let alice = Participant::new(1, &mut rng);
let bob = Participant::new(2, &mut rng);

// 2. Build peer map (in real code, exchange PKs over an authenticated channel)
let mut peers = HashMap::new();
peers.insert(alice.id, alice.pk);
peers.insert(bob.id, bob.pk);

// 3. Configure the session
let config = DkgConfig {
    n: 2,
    t: 2,
    beta: Scalar::rand(&mut rng),
    session_id: SessionId::random(&mut rng),
};

// 4. Round 0: each participant creates a dealing
let alice_dealing = dkg::create_dealing(&alice, &config, &peers, &mut rng)?;
let bob_dealing = dkg::create_dealing(&bob, &config, &peers, &mut rng)?;

// 5. Broadcast dealing.message to all participants (network layer)

// 6. Verify received dealings (publicly verifiable -- anyone can check)
dkg::verify_dealing(&bob_dealing.message, &peers, &config)?;
dkg::verify_dealing(&alice_dealing.message, &peers, &config)?;

// 7. Complete: decrypt shares and produce DKG output
let mut alice_received = HashMap::new();
alice_received.insert(bob.id, bob_dealing.message.clone());
let alice_output = dkg::complete(&alice, &alice_dealing, &alice_received, &peers, &config)?;

// alice_output.public_key  -- the shared group public key PK = g^sk
// alice_output.secret_share -- Alice's secret key share sk_i
// alice_output.public_key_shares -- per-participant public key shares PK_j = g^{sk_j}

Feature Flags

Feature	Description
borsh	Enable Borsh serialization for all message types

Security Properties

• Public verifiability: all participants (and external observers) can verify all dealings non-interactively without any secret information
• No trusted setup: transparent proof system via ark-spartan NIZK
• DL/DDH only: security relies on discrete-log and decisional Diffie-Hellman assumptions (no pairings, no random oracle model for the core protocol)
• Replay protection: types::SessionId nonces prevent replaying old messages
• Rogue-key protection: Schnorr proof of knowledge (schnorr_pok) on PKI registration prevents adversarial key choices
• Secret zeroization: secret keys are zeroed from memory on drop via types::SecretScalar

Formal Verification

This crate has multi-layer formal verification covering the paper math, the Rust implementation, and the bridge between them. See formal_verification/README.md for the full verification chain diagram and detailed status (formal_verification/README.md in the repository root).

Approach

The verification uses three tools in a “sandwich” architecture:

Top layer – Lean 4 + Mathlib (paper math): 38 machine-checked theorems prove the algebraic properties stated in the paper: Shamir reconstruction, Feldman VSS completeness, eVRF DH symmetry, refresh/reshare correctness, eVRF circuit completeness, security game hops, and the LHL bound. These are pure math proofs that hold in any field/group satisfying the standard algebraic axioms.

Bottom layer – hax + F* (Rust implementation): The hax tool extracts the Rust source code into 18 F* modules. F* lax-checks all modules, verifying that the extracted code is well-typed against the arkworks type models. Non-crypto code (serialization, memory zeroization) is excluded via #[hax_lib::exclude].

Bridge layer – F* specification files: 6 F* spec files state the correctness properties (mirroring the Lean theorems) and prove the extracted Rust code satisfies them. Key proofs include: eVRF pad symmetry (DH commutativity through the full derive_pad function), encrypt/decrypt roundtrip, Lagrange interpolation correctness for concrete cases (n=2,3), VSS ciphertext check (EC distributivity), and refresh/reshare algebraic invariants.

Additionally, 20 Kani bounded model checking harnesses prove panic-freedom and structural invariants across all modules.

Remaining Items

Two items are intentionally left unproved:

• reshare_dealer_binding (F*, assume val): States that if g^a == g^b then a == b. This is the Discrete Logarithm hardness assumption – a standard cryptographic assumption that cannot be proved, only assumed.

• golden_uc_security (Lean, sorry): The full UC composition theorem bounding the distinguishing advantage as |prob_real - prob_ideal| <= n * adv_evrf. This requires 8-12 weeks of research-level formalization using probabilistic frameworks (VCV-io or SSProve). The statement is complete; the proof infrastructure is in place.

Running the Verification Pipeline

After any code change, run the full verification suite:

# Full verification (cargo test + Lean + hax re-extraction + F* lax-check)
make verify

# Quick check (cargo test + Lean only, ~2 min)
make verify-quick

# Force full re-run (clears cached stamps)
make -C formal_verification clean && make verify

Prerequisites: Lean 4 via elan, F* v2025.10.06, hax v0.3.6 with opam switch hax-engine. See formal_verification/README.md for installation details.

Paper Reference

Benedikt Bünz, Kevin Choi, Chelsea Komlo. “Golden: Lightweight Non-Interactive Distributed Key Generation.” IACR ePrint 2025/1924. https://eprint.iacr.org/2025/1924

Modules

consensus

Simplex BFT consensus – pure state machine core. Enabled by the consensus feature (on by default). Simplex BFT consensus – pure state machine core.

dkg

High-level DKG API: one-round distributed key generation.

error

Error types for the Golden DKG protocol.

refresh

Proactive share rotation (key refresh) per Section 5.2 of the Golden paper.

reshare

Membership-change resharing: transfer a shared secret to a new group.

schnorr_pok

Schnorr Proof of Knowledge for PKI registration.

shamir

Shamir Secret Sharing per Section 3.3 of the Golden paper.

threshold

Threshold BLS signatures, vetKeys IBE, and drand-compatible beacon. Enabled by the threshold feature (on by default). Threshold BLS signatures, vetKeys IBE, and drand-compatible beacon.

types

Core data types for the Golden DKG protocol.

zk_evrf

Zero-knowledge eVRF proof system per Section 4 of the Golden paper.