Threshold Dilithium: FROST-Inspired Post-Quantum Signatures

FROST (Flexible Round-Optimized Schnorr Threshold signatures) demonstrates how to build threshold signatures from Schnorr's linear structure. Dilithium, the lattice-based signature scheme standardized as ML-DSA, shares this linear structure. This post describes how to adapt the FROST approach to the Dilithium setting.

What FROST Is Really Doing

FROST splits a group secret key into shares using Shamir secret sharing. Each signer holds one share. During signing, each signer contributes a partial signature based on their share and some randomness. An aggregator combines these partials into a single signature indistinguishable from one produced by a single signer.

The key insight is that Schnorr signatures are linear in both the secret key and the nonce. The sum of partial secrets behaves like one secret. The sum of partial nonces behaves like one nonce. FROST exploits this linearity while adding careful bookkeeping to prevent nonce reuse and rogue-key attacks.

Dilithium in Brief

Dilithium is a linear algebra construction over polynomial rings with carefully managed noise. Keys are vectors over a ring. Signing samples a short random vector y, computes a commitment via matrix multiplication, hashes the commitment with the message to produce a challenge, and combines y with the secret and challenge into a response.

The response must satisfy norm bounds. If the response is too large, the signer rejects and resamples. This rejection sampling prevents information leakage about the secret key. The structure resembles Schnorr lifted into a lattice setting with additional constraints on vector lengths.

Adapting FROST to Dilithium

The adaptation follows from asking which parts of the signing equation can be split across participants and recombined. The answer mirrors FROST.

We secret-share the key by splitting the secret key vector into additive shares. Each participant holds one share. The shares sum to the full secret key. We distribute randomness by having each signer sample their own piece of the ephemeral vector. The pieces sum to produce the global randomness used in a standard signature.

Reconstruction happens only at the signature level. No signer sees the full secret key or full randomness. The final signature is indistinguishable from one produced by a single signer holding the complete key.

Protocol Structure

The protocol runs in two rounds following the FROST pattern.

In round one, each signer commits to their randomness and broadcasts the commitment. After collecting all commitments, the group computes a shared challenge by hashing the message and aggregate commitment.

In round two, each signer uses their secret share and randomness share to compute a partial response. The aggregator collects partial responses and sums them into the final response. The resulting signature pairs this response with the aggregate commitment and passes standard Dilithium verification.

What Changes in the Lattice Setting

Several aspects require more care in Dilithium than in Schnorr.

Rejection sampling becomes distributed. In single-signer Dilithium, the signer rejects and restarts if the response norm is too large. In a threshold setting, rejection must happen locally without requiring distributed coordination. Each signer applies a tighter local bound so that any valid combination of partials satisfies the global bound.

The noise structure is higher-dimensional. Randomness is not a simple scalar but a vector in a polynomial ring. Sharing and combining this randomness while preserving security requires careful design. The commitment and response objects are larger than their Schnorr counterparts.

Communication costs increase. Partial signatures and commitments are vectors or polynomials rather than group elements. The protocol must ensure each participant can complete their work locally without excessive bandwidth.

Why This Works

The concept is straightforward. FROST works because Schnorr is linear in the secret and nonce. Dilithium signatures are also linear constructions over a module with managed noise. Thresholdizing Dilithium respects this linearity. The secret key equals the sum of shares. The signing randomness equals the sum of shares. The final response equals the sum of partial responses. Everything happens in the same algebraic space as the single-signer scheme.

The verifier sees an ordinary Dilithium signature. The distributed key and randomness are invisible. Verification uses the standard algorithm with no awareness of the threshold structure.

Practical Considerations

Threshold Dilithium signatures may not be practical for many use cases. Dilithium signatures are substantially larger than ECDSA or Schnorr signatures. A Dilithium2 signature is on the order of 2.5 KB compared to ~64 bytes for ECDSA. Threshold variants do not increase this size, but applications sensitive to signature size should evaluate whether the overhead is acceptable.

The scheme is therefore best suited for contexts where post-quantum security is required and signature size is not the primary constraint.

Ice Nine Protocol Specification Overview

Ice Nine is a threshold signature scheme in the lattice setting. It follows the Schnorr pattern adapted for post-quantum security. The protocol operates in two rounds. Parties hold additive shares of a master secret. They produce partial signatures that aggregate into a single valid signature.

The design supports both $n$-of-$n$ and $t$-of-$n$ threshold configurations. In the $n$-of-$n$ case all parties must participate. In the $t$-of-$n$ case any subset of $t$ or more parties can sign. Lagrange interpolation coefficients adjust the partial shares in the threshold case.

Getting Started

This section provides a practical overview of the protocol flow from key generation through signing.

Protocol Flow

A typical deployment follows these steps.

1. Configuration: Create a ThresholdConfig with party count, threshold, and security parameters.
2. Key Generation: Run DKG to establish shared key material. Each party receives a secret share.
3. Signing Sessions: For each message, run the two-round signing protocol to produce a threshold signature.
4. Verification: Any party can verify signatures using the public key.

Configuration

Start by creating a threshold configuration.

-- Create configuration for 5 parties with Dilithium2 security
let cfg := ThresholdConfig.dilithium2 5

-- The default threshold is 2/3+1 = 4 for 5 parties
-- cfg.threshold = 4
-- cfg.globalBound = 130994
-- cfg.localBound = 32748

See Threshold Configuration for detailed parameter guidance.

Key Generation

Run distributed key generation to establish shared keys.

-- Each party generates their DKG contribution
let (commitMsg, secretState) := dkgCommit S partyId randomness

-- Broadcast commit messages, then reveal
let revealMsg := dkgReveal S secretState

-- After receiving all reveals, compute key shares
let keyShare := dkgFinalize S partyId allCommits allReveals

The DKG protocol uses commit-reveal to prevent rogue-key attacks. Each party receives a KeyShare containing their secret share and the global public key. See Key Generation for DKG modes and VSS.

Signing

Signing proceeds in two rounds with session types enforcing correct usage.

-- Round 1: Commit to nonces
let nonce := FreshNonce.sample S  -- Sample fresh nonce
let ready := initSession S keyShare message session nonce
let (committed, commitMsg) := commit S ready
-- Broadcast commitMsg

-- After receiving all commits, reveal
let (revealed, revealMsg) := reveal S committed challenge bindingFactor aggregateW
-- Broadcast revealMsg

-- Round 2: Produce signature share
let (signed, shareMsg) ← signWithLocalRejection S revealed cfg sampleNonce
-- Broadcast shareMsg

-- Aggregator combines shares
let signature := aggregateValidated S cfg protocolCfg challenge commits shares pkShares factors

The FreshNonce type ensures nonces are used exactly once. The signWithLocalRejection function handles norm bounds locally without distributed retries. See Two-Round Threshold Signing for the complete protocol.

Verification

Verify signatures against the public key.

let valid := verify S signature publicKey message

Verification checks the algebraic relation A(z) = w + c·pk and the norm bound. See Verification for details.

Error Handling

Protocol operations return structured errors for recovery.

match result with
| .ok signature => -- Success
| .error e =>
    -- Check if error identifies a misbehaving party
    match BlameableError.blamedParty e with
    | some party => excludeParty party
    | none => handleOperationalError e

See Extensions for error recovery patterns across protocol phases.

Extension Operations

After initial setup, use extension protocols for operational needs.

Share Refresh updates shares without changing the key. Run periodically for proactive security.

Share Repair recovers a lost share using contributions from other parties.

Rerandomization masks shares and nonces for unlinkability between sessions.

See Extensions for these protocols.

CRDT-Based State Management

The implementation uses a semilattice/CRDT architecture for protocol state. Each protocol phase (commit, reveal, shares, done) carries state that forms a join-semilattice. The join operation (⊔) merges states from different replicas or out-of-order message arrivals.

Protocol progress is modeled as transitions between phases: commit → reveal → shares → done. Each phase carries accumulated data. States within a phase merge via componentwise join. The type-indexed implementation (Protocol/State/PhaseIndexed.lean) makes invalid phase transitions compile-time errors.

Messages are stored in MsgMap structures keyed by sender ID. This makes conflicting messages from the same sender un-expressable in the type system. Each party can contribute at most one message per phase.

The coordination protocols (RefreshCoord, RepairCoord) cleanly separate concerns into three layers:

• CRDT layer (process*): Pure merge semantics that are idempotent, commutative, and always succeed. Use for replication and networking.
• Validation layer (detect*, validate*): Conflict detection without modifying state. Use for auditing and security.
• Combined (process*Validated): Merge and validation in one call, returning (newState, Option error).

Step functions that advance state are monotone with respect to the semilattice order. This ensures that merging divergent traces preserves safety properties. If $a\le b$ then $\mathsf{step}(a)\le \mathsf{step}(b)$.

Protocol state combines with auxiliary CRDT data for refresh masks, repair bundles, and rerandomization masks. The product of semilattices is itself a semilattice.

Why This Works: Linearity as a Common Thread

The core insight of the Ice Nine protocol is that Dilithium, like Schnorr, is fundamentally linear. This linearity enables threshold signing and makes the protocol work.

In single-signer Dilithium, the signature response is computed as $z=y+c\cdot s_1$ where $y$ is a random ephemeral value and $s_1$ is the secret key. This is a direct linear combination in both variables. A threshold variant distributes the secret as $s_1={\sum }_i{s}_{1,i}$ (additive shares) and the randomness as $y={\sum }_i{y}_i$ (signer contributions). Each signer produces $z_i=y_i+c\cdot s_{1,i}$.

When these partials are summed, we get $z={\sum }_i{z}_i={\sum }_i(y_i+c\cdot s_{1,i})={\sum }_i{y}_i+c\cdot {\sum }_i{s}_{1,i}=y+c\cdot s_1$. The aggregated response is identical to what a single signer would produce with the full secret and full randomness.

This is the core mechanism of FROST applied to the lattice setting. The threshold scheme is not a different scheme; it is the base scheme distributed and recombined through linearity. The final signature is indistinguishable from a single-signer signature under the group key.

Linearity also enables the norm bound guarantee. By the triangle inequality, if each partial satisfies $\Vert z_i{\Vert }_{\infty }\le B_{\text{local}}$, then the sum automatically satisfies $\Vert z{\Vert }_{\infty }\le T\cdot B_{\text{local}}$ where $T$ is the number of aggregated partials. By choosing $B_{\text{local}}=\lfloor B_{\text{global}}/T\rfloor$, the global bound is guaranteed for any combination of valid partials. This is a mathematical certainty, not probabilistic.

The linearity property is what makes the entire protocol work: threshold signing that produces standard signatures, BFT-compatible design with per-signer validation, and deterministic norm bound guarantees via the triangle inequality.

Session Types

The implementation uses session types to enforce disciplined handling of secret material, making certain classes of errors impossible to express.

The signing protocol (Protocol/Sign/Session.lean) uses linear session types where each state transition consumes the previous state. Nonces are wrapped in FreshNonce structures that can only be consumed once. Nonce reuse is a compile-time error, not a runtime check.

Signature extraction requires a ThresholdCtx that pairs the active signer set with a proof that $|S|\ge t$. This prevents signatures from being produced without sufficient participation.

Specification Components

Algebraic Setting. Secrets live in a module $\mathcal{S}$ over a scalar ring. Public keys live in a module $\mathcal{P}$. A linear map $A:\mathcal{S}\to \mathcal{P}$ connects them. Commitments bind public values. A hash function produces challenges.

Key Generation. Two modes exist. A trusted dealer can sample the master secret and distribute shares. Alternatively parties can run a distributed key generation protocol. Both modes produce additive shares $s_i$ with ${\sum }_i{s}_i=s$. The DKG protocol uses the commit-reveal pattern with CRDT-mergeable state. Following FROST, each party provides a proof of knowledge (PoK) during DKG to prevent rogue-key attacks. For malicious security, Verifiable Secret Sharing (VSS) allows parties to verify shares against polynomial commitments.

Signing. Signing proceeds in two rounds with phase-indexed state. In round one each party commits to a nonce. After all commits arrive parties reveal their nonces and compute a shared challenge. In round two each party produces a partial signature. An aggregator combines the partials into the final signature. State at each phase is mergeable.

Verification. A verifier checks the aggregated signature against the public key. The check uses the linear map $A$ and the hash function. The signature is valid if the recomputed challenge matches and the norm bound is satisfied.

Extensions. The protocol supports several extensions. Complaints identify misbehaving parties. Share refresh updates shares using zero-sum mask functions that merge via join; two refresh modes are available: a coordinator-based protocol (Protocol/Shares/RefreshCoord.lean) and a fully distributed DKG-based protocol (Protocol/Shares/RefreshDKG.lean) where parties contribute zero-polynomials without a trusted coordinator. Share repair combines helper deltas via append-based bundles; a coordination protocol (Protocol/Shares/RepairCoord.lean) handles Lagrange coefficient computation and contribution verification. Rerandomization applies zero-sum masks to shares and nonces with merge-preserving structure.

Security. The protocol assumes binding commitments and models the hash as a random oracle. Under these assumptions it achieves threshold unforgeability. Formal proofs reside in the Lean verification modules. Totality theorems ensure that validation functions always return either success or a structured error.

Module Organization

The implementation is organized into focused modules within subdirectories:

Protocol/Core/ - Foundation types and utilities:

• Core/Core.lean - Scheme record, key shares, DKG messages, linear security wrappers
• Core/CRDT.lean - CRDT primitives: Join typeclass, MsgMap sender-keyed collection
• Core/Security.lean - Security markers (Zeroizable, ConstantTimeEq), SecretBox, NonceBox
• Core/Patterns.lean - Reusable patterns: constraint aliases, commit-reveal framework, utilities
• Core/Error.lean - BlameableError typeclass, error utilities
• Core/Lagrange.lean - Unified Lagrange coefficient API
• Core/Serialize.lean - Serialization API for network transport
• Core/ThresholdConfig.lean - Threshold configuration and local rejection bounds
• Core/NormBounded.lean - Norm bound predicates and verification
• Core/Abort.lean - Session-level abort coordination for liveness failures

Protocol/Sign/ - Signing protocol:

• Sign/Types.lean - Session tracking, signing messages, error types
• Sign/Core.lean - Challenge computation, n-of-n aggregation
• Sign/Threshold.lean - Coefficient strategies, threshold context
• Sign/Session.lean - Session-typed API preventing nonce reuse
• Sign/ThresholdMerge.lean - Threshold-aware state merge operations
• Sign/LocalRejection.lean - Local rejection sampling for norm bounds
• Sign/ValidatedAggregation.lean - Validated signature aggregation
• Sign/NonceLifecycle.lean - Nonce lifecycle tracking and safety

Protocol/DKG/ - Distributed key generation:

• DKG/Core.lean - Basic DKG protocol
• DKG/Threshold.lean - Threshold DKG with exclusion
• DKG/Feldman.lean - Polynomial commitments, share verification
• DKG/VSSDKG.lean - VSS transcript, complaint mechanism
• DKG/Dealer.lean - Trusted dealer mode

Protocol/Shares/ - Share management:

• Shares/Refresh.lean - Share refresh with zero-sum masks
• Shares/RefreshCoord.lean - Coordinator-based refresh protocol
• Shares/RefreshDKG.lean - DKG-based distributed refresh (no coordinator)
• Shares/RefreshState.lean - Refresh state CRDT
• Shares/Repair.lean - Share repair protocol
• Shares/RepairCoord.lean - Repair coordination with commit-reveal
• Shares/Rerandomize.lean - Signature rerandomization

Protocol/State/ - Phase state and CRDT operations:

• State/Phase.lean - Phase state with MsgMap CRDT
• State/PhaseIndexed.lean - Type-indexed phase transitions
• State/PhaseHandlers.lean - Phase transition handlers
• State/PhaseSig.lean - Phase signatures
• State/PhaseMerge.lean - Composite state merging

Top-level modules:

• Crypto.lean - Cryptographic primitives (hash, commitment)
• Instances.lean - Concrete scheme instantiations (Int, ZMod)
• Norms.lean - Norm bounds for lattice parameters
• Samples.lean - Sample transcript generation for testing

Proofs/ - Formal verification (separate from protocol):

Proofs/Core/ - Foundation for proofs:

• Proofs/Core/Assumptions.lean - Cryptographic assumptions, axiom index, Dilithium parameters
• Proofs/Core/ListLemmas.lean - Reusable lemmas for list operations and sums
• Proofs/Core/HighBits.lean - HighBits specification for Dilithium error absorption
• Proofs/Core/NormProperties.lean - Norm bound properties and lemmas
• Proofs/Core/MsgMapLemmas.lean - MsgMap CRDT lemmas

Proofs/Probability/ - Probabilistic analysis:

• Proofs/Probability/Dist.lean - Distribution properties and analysis
• Proofs/Probability/Indistinguishability.lean - Computational indistinguishability
• Proofs/Probability/Rejection.lean - Rejection sampling analysis
• Proofs/Probability/Commitment.lean - Commitment scheme probability properties

Proofs/Correctness/ - Happy-path proofs:

• Proofs/Correctness/Correctness.lean - Verification theorems
• Proofs/Correctness/DKG.lean - DKG correctness proofs
• Proofs/Correctness/Sign.lean - Signing correctness proofs
• Proofs/Correctness/Lagrange.lean - Lagrange interpolation correctness
• Proofs/Correctness/ThresholdConfig.lean - Threshold configuration correctness

Proofs/Soundness/ - Security proofs:

• Proofs/Soundness/Soundness.lean - Special soundness, nonce reuse attack, SIS reduction
• Proofs/Soundness/VSS.lean - VSS security properties
• Proofs/Soundness/Robustness.lean - Protocol robustness properties
• Proofs/Soundness/LocalRejection.lean - Local rejection sampling soundness

Proofs/Extensions/ - Extension protocol proofs:

• Proofs/Extensions/Phase.lean - Phase handler monotonicity (CRDT safety)
• Proofs/Extensions/Coordination.lean - Refresh/repair coordination security
• Proofs/Extensions/RefreshCoord.lean - Refresh coordination proofs
• Proofs/Extensions/Repair.lean - Share repair correctness
• Proofs/Extensions/RefreshRepair.lean - Refresh invariants, rerandomization

Lattice Cryptography

The security of Ice Nine reduces to standard lattice hardness assumptions:

Short Integer Solution (SIS). Given matrix $A\in {\mathbb{Z}}_q^{n\times m}$, finding short $z$ with $Az=0$ is hard. Signature unforgeability reduces to SIS: a forger that produces valid signatures can be used to solve SIS instances.

Module Learning With Errors (MLWE). Distinguishing $(A,As+e)$ from $(A,u)$ where $s,e$ are small is hard. Key secrecy reduces to MLWE: recovering the secret key from the public key requires solving MLWE.

Rejection Sampling. The signing protocol uses rejection sampling to ensure signatures are independent of the secret key. If the response norm exceeds the bound ${\gamma }_1-\beta$, the party aborts and retries with a fresh nonce. Expected attempts: ~4 for Dilithium parameters.

Parameter Validation. The implementation includes lightweight parameter validation to catch obviously insecure configurations. The standard parameter sets follow NIST FIPS 204 (ML-DSA/Dilithium).

Linear Types for Security-Critical Values

The implementation uses linear-style type discipline to prevent misuse of single-use values. While Lean doesn't have true linear types, private constructors and module-scoped access functions make violations visible and intentional.

Linear wrappers:

Pattern: Each wrapper has:

1. Private constructor (private mk) - prevents arbitrary creation
2. Private value field - prevents direct access outside module
3. Public creation function - controlled entry point
4. consume function - extracts value and produces consumption proof

structure LinearMask (S : Scheme) where
  private mk ::
  private partyId : S.PartyId
  private maskValue : S.Secret
  private publicImage : S.Public

def LinearMask.consume (m : LinearMask S) : S.Secret × MaskConsumed S

The consumption proof (MaskConsumed, DeltaConsumed, OpeningConsumed) can be required by downstream functions to ensure the value was properly consumed.

Nonce Safety

Critical property: Nonce reuse completely breaks Schnorr-style signatures. If the same nonce $y$ is used with two different challenges $c_1,c_2$:

• $z_1=y+c_1\cdot sk$
• $z_2=y+c_2\cdot sk$
• Then $sk=(z_1-z_2)/(c_1-c_2)$

The session-typed signing protocol makes nonce reuse a compile-time error. Each FreshNonce can only be consumed once, and the type system enforces that signing sessions progress linearly through states without backtracking.

Implementation Security

The implementation includes comprehensive security documentation in Protocol/Core/Security.lean:

Randomness Requirements: All secret values (shares, nonces, commitment openings) must be sampled from a CSPRNG. Nonce reuse is catastrophic. The session-typed API makes it a compile-time error.

Side-Channel Considerations: The specification flags timing-vulnerable functions (Lagrange computation, norm checks). Production implementations must use constant-time primitives. The ConstantTimeEq typeclass (in Security.lean) marks types requiring constant-time equality comparison.

Memory Zeroization: Sensitive values must be securely erased after use. Platform-specific APIs are documented for C, POSIX, Windows, and Rust. The Zeroizable typeclass (in Security.lean) marks types requiring secure erasure.

Secret Wrappers: The SecretBox and NonceBox types (in Security.lean) wrap sensitive values with private constructors, discouraging accidental duplication or exposure. Use SecretBox.wrap and NonceBox.fresh to create instances.

Docs Index

1. Algebraic Setting: Algebraic primitives, module structure, lattice instantiations, and semilattice definitions
2. Key Generation: Dealer and distributed key generation with CRDT state, VSS, party exclusion
3. Signing Protocol: Two-round signing protocol with session types, rejection sampling
4. Verification: Signature verification and threshold context
5. Extensions: Complaints, refresh/repair coordination, rerandomization, type-indexed phases
6. Protocol Integration: External context binding, evidence piggybacking, fast-path signing, self-validating shares
7. Threshold Configuration: ThresholdConfig parameters and tuning

Algebraic Setting

The protocol is parameterized by an abstract scheme structure. This structure defines the algebraic objects and operations. Concrete instantiations choose specific rings and modules.

Scheme Record

The Scheme structure bundles the algebraic setting with cryptographic oracles. It keeps types abstract so proofs and implementations can swap in concrete rings and primitives.

structure Scheme where
  PartyId   : Type
  Message   : Type
  Secret    : Type
  Public    : Type
  Challenge : Type
  Scalar    : Type

  [scalarSemiring : Semiring Scalar]
  [secretAdd      : AddCommGroup Secret]
  [publicAdd      : AddCommGroup Public]
  [secretModule   : Module Scalar Secret]
  [publicModule   : Module Scalar Public]
  [challengeSMulSecret : SMul Challenge Secret]
  [challengeSMulPublic : SMul Challenge Public]

  A : Secret →ₗ[Scalar] Public

  Commitment : Type
  Opening    : Type
  commit     : Public → Opening → Commitment
  commitBinding : ∀ {x₁ x₂ o₁ o₂}, commit x₁ o₁ = commit x₂ o₂ → x₁ = x₂

  -- Domain-separated hash functions (FROST pattern)
  hashCollisionResistant : Prop
  hashToScalar : ByteArray → ByteArray → Scalar  -- H(domain, data)
  hashDkg : PartyId → Public → Public → Scalar   -- H_dkg for PoK
  hash : Message → Public → List PartyId → List Commitment → Public → Challenge

  -- Optional identifier derivation
  deriveIdentifier : ByteArray → Option PartyId := fun _ => none

  normOK : Secret → Prop
  [normOKDecidable : DecidablePred normOK]

Modules and Scalars

Let $R$ denote a commutative semiring with unity. This serves as the scalar ring. Common choices include ${\mathbb{Z}}_q$ for a prime $q$.

The secret space $\mathcal{S}$ is an additive commutative group. It carries an $R$-module structure. Secrets are elements of $\mathcal{S}$.

The public space $\mathcal{P}$ is also an additive commutative group with an $R$-module structure. Public keys are elements of $\mathcal{P}$.

In lattice instantiations both spaces may be polynomial rings or vectors over ${\mathbb{Z}}_q$.

The Linear Map A

The core algebraic structure is a linear map $A:\mathcal{S}\to \mathcal{P}$. This map is $R$-linear. It satisfies

$$A(s_1+s_2)=A(s_1)+A(s_2)$$

and

$$A(r\cdot s)=r\cdot A(s)$$

for all secrets $s_1,s_2,s\in \mathcal{S}$ and scalars $r\in R$.

The map $A$ connects private shares to their public counterparts. If $s_i$ is a secret share then ${\mathsf{pk}}_i=A(s_i)$ is the corresponding public share.

Linearity ensures that aggregation in $\mathcal{S}$ corresponds to aggregation in $\mathcal{P}$. The sum of public shares equals the image of the sum of secret shares. This property underlies the threshold aggregation.

Linearity in Lattice Signatures

Dilithium and other lattice-based signature schemes inherit a fundamental linearity property from their algebraic structure. This linearity is precisely what enables threshold signing.

Why Dilithium is Linear

In Dilithium signing, the response is computed as $z=y+c\cdot s_1$ where $y$ is random and $s_1$ is the secret key. This sum respects linearity in both variables. Unlike schemes where the signature is output as a function of intermediate hash values, Dilithium's response is a direct linear combination.

The same linearity holds in threshold settings. If $s_1={\sum }_i{s}_{1,i}$ (secret shares) and each signer produces $z_i=y_i+c\cdot s_{1,i}$, then the sum $z={\sum }_i{z}_i={\sum }_i{y}_i+c\cdot {\sum }_i{s}_{1,i}=y+c\cdot s_1$ produces the same response as a single signer with full secret.

This is the core insight of FROST applied to the lattice setting. The threshold scheme is not a different scheme; it is the base scheme distributed and recombined through linearity.

Norm Bounds via Triangle Inequality

In single-signer Dilithium, the response must satisfy a global norm bound. In threshold signing, each signer produces a partial $z_i$, and these are summed to produce the global response $z={\sum }_i{z}_i$.

By the triangle inequality, $\Vert z{\Vert }_{\infty }=\Vert {\sum }_i{z}_i{\Vert }_{\infty }\le {\sum }_i\Vert z_i{\Vert }_{\infty }$.

If we ensure that each partial satisfies a local bound $\Vert z_i{\Vert }_{\infty }\le B_{\text{local}}$, and we aggregate at most $T$ partials, then the global response is guaranteed to satisfy

$$\Vert z{\Vert }_{\infty }\le T\cdot B_{\text{local}}.$$

By setting $B_{\text{local}}=\lfloor B_{\text{global}}/T\rfloor$, we obtain a hard guarantee that any combination of $T$ or fewer valid partials automatically satisfies the global Dilithium bound. This is a mathematical certainty, not a probabilistic property.

Each signer enforces the local bound via internal rejection sampling. The aggregator enforces it by checking each partial before inclusion. Once the aggregator has collected $T$ valid partials (all satisfying $\Vert z_i{\Vert }_{\infty }\le B_{\text{local}}$), it is mathematically guaranteed that their sum satisfies the global bound. No further norm checking is needed; no distributed coordination or restart is required.

Design Choice: No Explicit Error Term

In Dilithium, the public key includes an error term: $t=A{s}_1+s_2$ where $s_2$ is small. This makes $t$ indistinguishable from random under MLWE. During verification, Dilithium uses a HighBits() function to absorb the error term $c\cdot s_2$.

We deliberately keep the abstract map $A:\mathcal{S}\to \mathcal{P}$ without an explicit error term for these reasons:

1. Abstraction boundary. The error term is a key generation detail. Once the public key $t$ is computed, signing and verification only need the linear relationship $A(z)=A(y)+c\cdot A(s_1)$.

2. HighBits is an implementation detail. The truncation that absorbs $c\cdot s_2$ can be encoded in the concrete instantiation:

   • The hash function can hash HighBits(w) rather than full $w$
   • The normOK predicate can include the HighBits consistency check

3. Clean protocol logic. The signing and verification math stays clean: $$z=y+c\cdot s$$ $$A(z)-c\cdot \mathsf{pk}=A(y)=w$$ The error handling lives in the concrete instantiation, not the abstract protocol.

4. Instantiation flexibility. Different lattice schemes handle errors differently (Dilithium vs Falcon vs others). The abstract Scheme lets each instantiation encode its approach appropriately.

For a Dilithium instantiation, the Scheme record would be configured as:

def dilithiumScheme (params : DilithiumParams) : Scheme :=
  { Secret := PolyVec params.l      -- s₁ ∈ R_q^l
  , Public := PolyVec params.k      -- t = As₁ + s₂ (precomputed at keygen)
  , A := dilithiumKeyMap            -- maps response z to Az
  , normOK := fun z =>
      dilithiumNormCheck z params ∧
      highBitsConsistent z params   -- both quality checks
  , hash := fun m pk ... w =>
      hashHighBits (highBits w params.gamma2) m  -- hash truncated w
  , ... }

The error term $s_2$ is baked into the public key during key generation. The normOK predicate enforces both the coefficient bound $\Vert z{\Vert }_{\infty }<{\gamma }_1-\beta$ and the HighBits consistency check. The hash function operates on truncated values as Dilithium requires.

HighBits Specification

The HighBits function is formally specified in Proofs/Core/HighBits.lean:

structure HighBitsSpec (P : Type*) [AddCommGroup P] where
  highBits : P → P
  gamma2 : Nat
  isSmall : P → Prop
  idempotent : ∀ x, highBits (highBits x) = highBits x
  absorbs_small : ∀ (w e : P), isSmall e →
    highBits (w + e) = highBits w ∨ highBits (w - e) = highBits w

The key property is absorption: small perturbations don't change HighBits. During verification:

• Signer computes: $w_1=\text{HighBits}(Ay)$
• Verifier computes: $w_1^{\prime }=\text{HighBits}(Az-c\cdot t)$

Since $t=A{s}_1+s_2$ and $z=y+c\cdot s_1$: $$Az-c\cdot t=Ay-c\cdot s_2$$

The absorption property ensures $\text{HighBits}(Ay)=\text{HighBits}(Ay-c\cdot s_2)$ when $\Vert c\cdot s_2{\Vert }_{\infty }<{\gamma }_2$.

Challenges

The challenge space is a separate type. In typical instantiations challenges are scalars from $R$ or a related ring. Challenges act on secrets and publics via scalar multiplication.

For a challenge $c$ and secret $s$ the product $c\cdot s$ is a secret. For a challenge $c$ and public $p$ the product $c\cdot p$ is a public. This action must be compatible with the module structure.

Commitments

A commitment scheme binds a public value to a commitment string. Let $\mathsf{Com}:\mathcal{P}\times \mathcal{O}\to \mathcal{C}$ denote the commitment function. Here $\mathcal{O}$ is the opening space and $\mathcal{C}$ is the commitment space.

The binding property requires that

$$\mathsf{Com}(x_1,o_1)=\mathsf{Com}(x_2,o_2)⟹x_1=x_2$$

for all $x_1,x_2\in \mathcal{P}$ and $o_1,o_2\in \mathcal{O}$.

This property ensures that a commitment uniquely determines the committed value. Adversaries cannot produce two different openings for the same commitment.

Hash Functions

Following FROST, we use domain-separated hash functions for different protocol operations. This prevents cross-protocol attacks where a hash collision in one context could be exploited in another.

Domain Separation

Each hash function uses a unique domain prefix:

Challenge Hash (H2)

The primary hash function maps protocol inputs to challenges:

$$H_2:\mathcal{M}\times \mathcal{P}\times \mathsf{List}(\mathsf{PartyId})\times \mathsf{List}(\mathcal{C})\times \mathcal{P}\to \mathcal{C}h$$

The inputs are the message $m$, the global public key $\mathsf{pk}$, the participant set $S$, the list of commitments, and the aggregated nonce $w$.

DKG Hash (HDKG)

Used for proof of knowledge in DKG:

$$H_{\text{dkg}}:\mathsf{PartyId}\times \mathcal{P}\times \mathcal{P}\to R$$

Maps (party ID, public key, commitment) to a scalar challenge.

Identifier Derivation (HID)

The deriveIdentifier function maps arbitrary byte strings to party identifiers:

$$H_{\text{id}}:\mathsf{ByteArray}\to \mathsf{Option}(\mathsf{PartyId})$$

Uses domain prefix ice-nine-v1-id. Returns none if the derived value is zero (invalid identifier).

-- In Scheme record
deriveIdentifier : ByteArray → Option PartyId := fun _ => none

-- Convenience function
def Scheme.deriveId (S : Scheme) (data : ByteArray) : Option S.PartyId :=
  S.deriveIdentifier data

This enables deterministic identifier derivation from human-readable strings or external identifiers.

Random Oracle Model

In security proofs the hash is modeled as a random oracle. This means it behaves as a uniformly random function. The random oracle model enables simulation-based security arguments.

Norm Predicate

A norm predicate $\mathsf{normOK}:\mathcal{S}\to \mathsf{Prop}$ gates acceptance. Signatures with large response vectors are rejected.

The predicate captures a bound on the norm of the response. For lattice signatures this prevents leakage through the response distribution. Rejection sampling or abort strategies ensure the bound holds.

In the abstract model the predicate is a parameter. Concrete instantiations define it based on the lattice parameters.

Dilithium-Style Norm Bounds

For Dilithium-style signatures, the norm check uses:

• ${\ell }_{\infty }$ norm: $\Vert z{\Vert }_{\infty }={\max }_i|z_i|$
• Rejection bound: $\Vert z{\Vert }_{\infty }<{\gamma }_1-\beta$ where $\beta =\tau \cdot \eta$

structure DilithiumParams where
  n      : Nat := 256    -- ring dimension
  q      : Nat := 8380417 -- modulus
  tau    : Nat           -- challenge weight (number of ±1)
  eta    : Nat           -- secret coefficient bound
  gamma1 : Nat           -- nonce coefficient range
  gamma2 : Nat           -- low-bits range

def dilithiumNormOK (p : DilithiumParams) (z : List Int) : Prop :=
  vecInfNorm z < p.gamma1 - p.tau * p.eta

Standard parameter sets (defined and validated in Proofs/Core/Assumptions.lean):

structure DilithiumSigningParams where
  tau : Nat           -- challenge weight
  eta : Nat           -- secret coefficient bound
  gamma1 : Nat        -- nonce coefficient range
  gamma2 : Nat        -- low-bits truncation range

def DilithiumSigningParams.beta (p : DilithiumSigningParams) : Nat :=
  p.tau * p.eta

-- Critical security constraints (proven for each parameter set):
-- γ₁ > β ensures rejection sampling has room
-- γ₂ > β ensures HighBits absorbs error
theorem dilithiumL2_gamma1_ok : dilithiumL2.gamma1 > dilithiumL2.beta
theorem dilithiumL2_gamma2_ok : dilithiumL2.gamma2 > dilithiumL2.beta

Security Parameter Guidance

When selecting parameters for threshold deployment, consider how threshold configuration affects security margins.

Threshold and Local Bounds. The local rejection bound is B_local = B_global / T where T is the number of signers. More signers means each signer must produce smaller partials. This affects rejection rates but not core security assumptions.

Security Level Selection. Choose the security level based on your threat model, not performance concerns.

The 128-bit level provides security comparable to AES-128. The 192-bit and 256-bit levels provide additional margins against potential improvements in lattice algorithms.

Threshold and Fault Tolerance. The default 2/3+1 threshold balances security and liveness.

Lower thresholds improve liveness but reduce the cost of compromise. An adversary needs fewer corrupted parties to forge signatures.

Signer Count Limits. The local bound B_local decreases as T increases. Very large signer counts reduce B_local to the point where rejection rates become impractical.

For deployments with more than 20 signers, consider using Dilithium3 or Dilithium5 for larger global bounds.

Parameter Validation. Always validate parameter configurations using ThresholdConfig.validate. The validation checks:

• Threshold does not exceed party count
• maxSigners is at least threshold
• Local bound is positive after division
• Global bound is sufficient for the configuration

Configurations from untrusted sources should be validated before use even if they were created through ThresholdConfig.create.

Concrete Scheme Instantiations

The implementation provides a lattice-friendly scheme in Instances.lean:

Lattice Scheme

Integer vectors with hash-based commitments and Dilithium-style norm checking.

structure LatticeParams where
  n : Nat := 256          -- dimension
  q : Nat := 8380417      -- modulus
  bound : Nat := 1 <<< 19 -- ℓ∞ bound (approx Dilithium γ1)

def latticeScheme (p : LatticeParams := {}) : Scheme :=
  { PartyId   := Nat
  , Message   := ByteArray
  , Secret    := Fin p.n → Int
  , Public    := Fin p.n → Int
  , Challenge := Int
  , Scalar    := Int
  , A := LinearMap.id
  , Commitment := LatticeCommitment (Fin p.n → Int) (Fin p.n → Int)
  , Opening := Fin p.n → Int
  , commit := latticeCommit  -- hash-based: H(encode(w, nonce))
  , normOK := fun v => intVecInfLeq p.bound v
  , ... }

This models the SIS/LWE structure:

• Secret key: $s\in {\mathbb{Z}}^n$ (integer vector with bounded coefficients)
• Public key: $t=A\cdot s$ (identity map for simplicity)
• Norm bound: $\Vert z{\Vert }_{\infty }\le \text{bound}$ for signature validity
• Commitments: Hash-based with axiomatized binding

The hash-based commitment uses hashBytes(encodePair(w, nonce)) where encodePair serializes the value and opening. Binding is axiomatized via HashBinding assumption.

Semilattice Structure

Protocol state at each phase forms a join-semilattice. A semilattice is an algebraic structure with a binary join operation $\bigsqcup$ that is commutative, associative, and idempotent.

$$a\bigsqcup b=b\bigsqcup a$$ $$a\bigsqcup (b\bigsqcup c)=(a\bigsqcup b)\bigsqcup c$$ $$a\bigsqcup a=a$$

The join induces a partial order: $a\le b$ iff $a\bigsqcup b=b$.

Message Map Semilattice

Protocol messages are stored in MsgMap structures, which are hash maps keyed by sender ID. This design makes conflicting messages from the same sender un-expressable at the type level.

structure MsgMap (S : Scheme) (M : Type*) [BEq S.PartyId] [Hashable S.PartyId] where
  map : Std.HashMap S.PartyId M

instance : Join (MsgMap S M) := ⟨MsgMap.merge⟩
instance : LE (MsgMap S M) := ⟨fun a b => a.map.toList.all (fun (k, _) => b.map.contains k)⟩

The merge operation takes the union of keys, keeping the first value on conflict. This provides:

• Conflict-freedom by construction: At most one message per sender
• Commutativity: Merge order doesn't affect the set of senders
• Idempotence: Merging a map with itself is identity
• Strict mode: tryInsert returns conflict indicators for misbehavior detection

This provides the foundation for merging commit maps, reveal maps, and share maps while preventing Byzantine parties from injecting multiple conflicting messages.

Product Semilattice

If $\alpha$ and $\beta$ are semilattices, their product $\alpha \times \beta$ is a semilattice under componentwise join.

instance prodJoin (α β) [Join α] [Join β] : Join (α × β) :=
  ⟨fun a b => (a.1 ⊔ b.1, a.2 ⊔ b.2)⟩

This allows combining protocol state with auxiliary data (refresh masks, repair bundles, rerandomization masks).

CRDT Semantics

Semilattice merge ensures conflict-free replicated data type (CRDT) semantics. Replicas can merge states in any order and converge to the same result. This is essential for handling:

• Out-of-order message delivery
• Network partitions and rejoins
• Concurrent protocol executions

Instance Constraint Patterns

The protocol modules use consistent instance requirements:

For HashMap-based structures (MsgMap, NonceRegistry):

• [BEq S.PartyId] - Boolean equality
• [Hashable S.PartyId] - Hash function for HashMap

For decidable equality (if-then-else, match guards):

• [DecidableEq S.PartyId] - Prop-valued equality with decision procedure

For field arithmetic (Lagrange coefficients):

• [Field S.Scalar] - Division required for λ_i = Π x_j / (x_j - x_i)
• [DecidableEq S.Scalar] - For checking degeneracy

Lagrange Interpolation

The Protocol/Core/Lagrange.lean module provides a unified API for computing Lagrange interpolation coefficients used across threshold protocols.

Core Function

def coeffAtZero [Field F] [DecidableEq F]
    (partyScalar : F)
    (allScalars : List F)
    : F :=
  let others := allScalars.filter (· ≠ partyScalar)
  others.foldl (fun acc xj => acc * (xj / (xj - partyScalar))) 1

This computes ${\lambda }_i={\prod }_{j\ne i}\frac{x_j}{x_j-x_i}$ for evaluating at 0.

Scheme-Aware API

def schemeCoeffAtZero (S : Scheme)
    [Field S.Scalar] [DecidableEq S.Scalar] [DecidableEq S.PartyId]
    (pidToScalar : S.PartyId → S.Scalar)
    (allParties : List S.PartyId)
    (party : S.PartyId)
    : S.Scalar

def buildPartyCoeffs (S : Scheme)
    [Field S.Scalar] [DecidableEq S.Scalar] [DecidableEq S.PartyId]
    (pidToScalar : S.PartyId → S.Scalar)
    (parties : List S.PartyId)
    : List (PartyCoeff S)

These functions integrate with the Scheme type for protocol use, including batch computation and precomputed coefficient storage.

Secret Wrappers

Secrets and nonces are wrapped in opaque structures to discourage accidental duplication or exposure.

/-- Wrapper for secrets with private constructor.
    Forces explicit acknowledgment when accessing secret material. -/
structure SecretBox (α : Type*) where
  private mk ::
  val : α

/-- Wrap a secret value. -/
def SecretBox.wrap (secret : α) : SecretBox α := ⟨secret⟩

/-- Wrapper for nonces to highlight their ephemeral nature.
    Nonce reuse is catastrophic: treat these as single-use. -/
structure NonceBox (α : Type*) where
  private mk ::
  val : α

/-- Create from a freshly sampled nonce. -/
def NonceBox.fresh (nonce : α) : NonceBox α := ⟨nonce⟩

The private constructors prevent arbitrary creation of wrapped values. Use SecretBox.wrap and NonceBox.fresh to create instances. This lightweight discipline signals intent. Code that accesses the val field must explicitly acknowledge it is handling secret material.

Both types have Zeroizable and ConstantTimeEq marker instances to indicate security requirements for production implementations.

Key Share Integration:

structure KeyShare (S : Scheme) where
  pid  : S.PartyId        -- party identifier
  sk_i : SecretBox S.Secret  -- wrapped secret share
  pk_i : S.Public         -- public share = A(sk_i)
  pk   : S.Public         -- global public key

/-- Create KeyShare from unwrapped secret (use during DKG). -/
def KeyShare.create (S : Scheme) (pid : S.PartyId) (sk : S.Secret) (pk_i pk : S.Public)
    : KeyShare S :=
  { pid := pid, sk_i := ⟨sk⟩, pk_i := pk_i, pk := pk }

/-- Access secret for cryptographic operations. -/
def KeyShare.secret (share : KeyShare S) : S.Secret :=
  share.sk_i.val

All protocol code that needs the secret share calls share.secret rather than pattern-matching on the SecretBox. This creates a clear audit trail for secret access.

Single-Signer Schnorr Relation

The threshold protocol generalizes the single-signer Schnorr pattern. The single-signer version proceeds as follows.

Key generation. Sample a short secret $s\in \mathcal{S}$. Compute the public key $\mathsf{pk}=A(s)$.

Signing. Given message $m$:

1. Sample a short ephemeral secret $y\in \mathcal{S}$.
2. Compute the nonce $w=A(y)$.
3. Compute the challenge $c=H(m,\mathsf{pk},w)$.
4. Compute the response $z=y+c\cdot s$.
5. Output signature $(z,c)$.

Verification. Given signature $(z,c)$ and message $m$:

1. Compute $w^{\prime }=A(z)-c\cdot \mathsf{pk}$.
2. Check $\mathsf{normOK}(z)$.
3. Compute $c^{\prime }=H(m,\mathsf{pk},w^{\prime })$.
4. Accept if $c^{\prime }=c$.

The threshold protocol distributes $s$ among parties. Each party holds a share $s_i$ with ${\sum }_i{s}_i=s$. The signing procedure produces partial responses $z_i$ that aggregate to $z={\sum }_i{z}_i$.

Key Generation

Key generation produces the master secret and distributes shares among parties. Two modes are supported. A trusted dealer can sample and distribute shares directly. Alternatively parties can run a distributed key generation protocol without trusting any single entity.

Both modes produce additive shares. Each party $P_i$ holds a secret share $s_i\in \mathcal{S}$. The shares sum to the master secret $s={\sum }_i{s}_i$. The corresponding public key is $\mathsf{pk}=A(s)$.

Key Share Structure

After key generation each party holds a KeyShare containing its local view.

structure KeyShare (S : Scheme) where
  pid  : S.PartyId          -- party identifier
  sk_i : SecretBox S.Secret -- secret share (wrapped for safety)
  pk_i : S.Public           -- public share = A(sk_i)
  pk   : S.Public           -- global public key

The secret share is wrapped in a SecretBox with a private constructor. This prevents accidental duplication or exposure of the secret material. Access the secret via KeyShare.secret:

/-- Create KeyShare from unwrapped secret (use during DKG). -/
def KeyShare.create (S : Scheme) (pid : S.PartyId) (sk : S.Secret) (pk_i pk : S.Public)
    : KeyShare S :=
  { pid := pid, sk_i := SecretBox.wrap sk, pk_i := pk_i, pk := pk }

/-- Get the unwrapped secret share for computation.
    **Security**: Only use when the secret is needed for cryptographic operations. -/
def KeyShare.secret (share : KeyShare S) : S.Secret :=
  share.sk_i.val

The key share is the persistent credential a signer carries into the signing protocol.

Trusted Dealer Mode

In trusted dealer mode a single entity generates and distributes all shares. This mode is simpler but requires trust in the dealer.

Dealer Output Structure

The dealer produces a DealerShare for each party and a DealerTranscript bundling the complete key material.

structure DealerShare (S : Scheme) :=
  (pid      : S.PartyId)
  (sk_i     : S.Secret)
  (pk_i     : S.Public)
  (opening  : S.Opening)
  (commitPk : S.Commitment)

structure DealerTranscript (S : Scheme) :=
  (shares : List (DealerShare S))
  (pk     : S.Public)

Dealer Procedure

The dealer proceeds as follows.

1. Sample a short master secret $s\in \mathcal{S}$.
2. For each party $P_i$ sample a short share $s_i\in \mathcal{S}$.
3. Adjust the final share so that ${\sum }_i{s}_i=s$.
4. Compute each public share ${\mathsf{pk}}_i=A(s_i)$.
5. Compute the global public key $\mathsf{pk}=A(s)$.
6. Commit to each public share as ${\mathsf{Com}}_i=\mathsf{Com}({\mathsf{pk}}_i,r_i)$ for random openings $r_i$.
7. Publish the global public key and all commitments.
8. Send each party $P_i$ its secret share $s_i$ over a secure channel.

The pure implementation dealerKeygen takes pre-sampled secrets and openings to keep IO/randomness out of the core logic.

Dealer Correctness

The linearity of $A$ ensures consistency. Since ${\sum }_i{s}_i=s$ the sum of public shares equals the global public key.

$$\sum _i{\mathsf{pk}}_i=\sum _{i}A(s_i)=A\left(\sum _i{s}_i\right)=A(s)=\mathsf{pk}$$

Parties can verify this relation after receiving their shares. They compute $A(s_i)$ and check that the published commitment opens correctly.

Trust Assumption

The dealer learns the master secret $s$. This mode is appropriate when a trusted party exists or when the protocol operates in a setting where the dealer is later destroyed. For stronger security guarantees use distributed key generation.

Distributed Key Generation

Distributed key generation removes the need for a trusted dealer. Parties jointly generate shares such that no single party learns the master secret. The protocol runs in two rounds with CRDT-mergeable state at each phase.

Message Types

The DKG protocol uses commit and reveal messages. Following FROST, commit messages include a proof of knowledge to prevent rogue-key attacks.

/-- Proof of knowledge for DKG: proves knowledge of secret corresponding to public key. -/
structure ProofOfKnowledge (S : Scheme) where
  commitment : S.Public   -- R = A(k) for random nonce k
  response   : S.Secret   -- μ = k + c·sk where c = H_dkg(pid, pk, R)

structure DkgCommitMsg (S : Scheme) where
  sender   : S.PartyId
  commitPk : S.Commitment
  pok      : ProofOfKnowledge S  -- proof of knowledge (prevents rogue-key attacks)

structure DkgRevealMsg (S : Scheme) where
  sender  : S.PartyId
  pk_i    : S.Public
  opening : S.Opening

Proof of Knowledge

The proof of knowledge (PoK) prevents rogue-key attacks where an adversary chooses their public key as a function of honest parties' keys. Each party proves knowledge of the secret corresponding to their public share.

Generation (during Round 1):

1. Sample random nonce $k$
2. Compute commitment $R=A(k)$
3. Compute challenge $c=H_{\text{dkg}}(\text{pid},{\text{pk}}_i,R)$
4. Compute response $\mu =k+c\cdot s_i$

Verification (during aggregation): Check that $A(\mu )=R+c\cdot {\text{pk}}_i$

This works because $A(\mu )=A(k+c\cdot s_i)=A(k)+c\cdot A(s_i)=R+c\cdot {\text{pk}}_i$.

def verifyProofOfKnowledge (S : Scheme) [DecidableEq S.Public]
    (pid : S.PartyId) (pk : S.Public) (pok : ProofOfKnowledge S) : Bool :=
  let c := S.hashDkg pid pk pok.commitment
  S.A pok.response = pok.commitment + c • pk

Party State

Each party $P_i$ maintains local state during the protocol.

structure DkgLocalState (S : Scheme) :=
  (pid    : S.PartyId)
  (sk_i   : S.Secret)
  (pk_i   : S.Public)
  (openPk : S.Opening)

The local state contains:

• A secret share $s_i\in \mathcal{S}$ sampled locally.
• An opening value $r_i\in \mathcal{O}$ for the commitment.
• The commitment ${\mathsf{Com}}_i=\mathsf{Com}({\mathsf{pk}}_i,r_i)$ where ${\mathsf{pk}}_i=A(s_i)$.

Round 1: Commit

In round one each party commits to its public share.

1. Party $P_i$ samples a short secret share $s_i\in \mathcal{S}$.
2. Compute the public share ${\mathsf{pk}}_i=A(s_i)$.
3. Sample a random opening $r_i\in \mathcal{O}$.
4. Compute the commitment ${\mathsf{Com}}_i=\mathsf{Com}({\mathsf{pk}}_i,r_i)$.
5. Broadcast the commitment ${\mathsf{Com}}_i$ to all parties.

Parties wait until they receive commitments from all other participants. The commitment hides the public share until the reveal phase.

Round 2: Reveal

In round two each party reveals its public share and opening.

1. Party $P_i$ broadcasts the pair $({\mathsf{pk}}_i,r_i)$.
2. Each party verifies all received openings.
3. For each received pair $({\mathsf{pk}}_j,r_j)$ check that ${\mathsf{Com}}_j=\mathsf{Com}({\mathsf{pk}}_j,r_j)$.
4. If any verification fails the party aborts or files a complaint.

The binding property of the commitment ensures that a dishonest party cannot change its public share after seeing others.

Aggregation

After successful verification all parties compute the global public key.

$$\mathsf{pk}=\sum _i{\mathsf{pk}}_i$$

Each party stores the set of all public shares $\{{\mathsf{pk}}_i\}$ and the global key $\mathsf{pk}$. Secret shares remain private. Only party $P_i$ knows $s_i$.

Error Handling

Several error conditions may arise during DKG. The implementation provides structured error types.

inductive DkgError (PartyId : Type) where
  | lengthMismatch : DkgError PartyId
  | duplicatePids  : DkgError PartyId
  | commitMismatch : PartyId → DkgError PartyId
  | invalidProofOfKnowledge : PartyId → DkgError PartyId

Missing commitment. If a party does not receive a commitment from $P_j$ within a timeout it marks $P_j$ as absent. The protocol can proceed with the remaining parties if enough are present. Detected via lengthMismatch.

Invalid opening. If $\mathsf{Com}({\mathsf{pk}}_j,r_j)\ne {\mathsf{Com}}_j$ then party $P_j$ is marked as malicious. Detected via commitMismatch.

Invalid proof of knowledge. If $A(\mu )\ne R+c\cdot {\mathsf{pk}}_j$ for party $P_j$'s PoK, this indicates either a malicious party attempting a rogue-key attack or corruption of the PoK data. Detected via invalidProofOfKnowledge.

Duplicate participants. If the same party identifier appears twice, detected via duplicatePids.

Inconsistent views. If parties disagree about which commitments were received they must run a consensus or abort. The protocol assumes a broadcast channel or equivalent.

Checked Aggregation

The dkgAggregateChecked function validates the transcript before computing the global public key. It accepts lists extracted from the CRDT state (via CommitState.commitList, etc.):

def dkgAggregateChecked
  (S : Scheme) [DecidableEq S.PartyId]
  (commits : List (DkgCommitMsg S))
  (reveals : List (DkgRevealMsg S))
  : Except (DkgError S.PartyId) S.Public

Note: The internal CRDT state uses MsgMap (hash maps keyed by sender) which guarantees at most one message per party. The aggregation functions receive lists extracted from these maps, so duplicates are already eliminated.

It returns either the public key or a structured error identifying the failure mode. The totality theorem ensures this function always returns a result:

lemma dkgAggregateChecked_total : (result).isOk ∨ (result).isError

Validity Predicate

A transcript is valid when commits and reveals align by party identifier and each opening matches its commitment.

def dkgValid
  (S : Scheme)
  (commits : List (DkgCommitMsg S))
  (reveals : List (DkgRevealMsg S)) : Prop :=
  List.Forall₂
    (fun c r => c.sender = r.sender ∧ S.commit r.pk_i r.opening = c.commitPk)
    commits reveals

If dkgAggregateChecked succeeds, then dkgValid holds.

Threshold Considerations

In a $t$-of-$n$ threshold setting any $t$ parties can sign. The key generation phase produces additive shares. Threshold functionality arises during signing through Lagrange interpolation.

Lagrange Coefficients

Let $S\subseteq \{1,\dots ,n\}$ be a signing subset with $|S|\ge t$. The Lagrange coefficient for party $i\in S$ is

$${\lambda }_i^S=\prod _{j\in S,j\ne i}\frac{j}{j-i}$$

These coefficients satisfy ${\sum }_{i\in S}{\lambda }_i^S\cdot s_i=s$ when the shares are derived from a degree $t-1$ polynomial evaluated at points $1,\dots ,n$.

Additive vs Polynomial Shares

The base protocol uses additive shares where ${\sum }_i{s}_i=s$. For $n$-of-$n$ signing this is sufficient. For $t$-of-$n$ signing the shares must encode polynomial structure.

One approach is to run a verifiable secret sharing protocol during DKG. Each party $P_i$ shares its contribution $s_i$ as a polynomial. After aggregation each party holds a share of the sum of polynomials. The implementation provides Feldman VSS in Protocol/DKG/Feldman.lean and Protocol/DKG/VSSDKG.lean.

An alternative approach uses additive shares with Lagrange adjustment at signing time. The Lagrange coefficients are computed over the active signer set $S$.

Verifiable Secret Sharing (VSS)

Feldman VSS provides malicious security by allowing recipients to verify their shares against polynomial commitments. This detects cheating dealers before shares are used.

Polynomial Commitment

A dealer commits to polynomial $f(x)=a_0+a_{1}x+\cdots +a_{t-1}{x}^{t-1}$ by publishing $C_i=A(a_i)$ for each coefficient.

structure PolyCommitment (S : Scheme) where
  commitments : List S.Public  -- [A(a₀), A(a₁), ..., A(a_{t-1})]
  threshold : Nat
  consistent : commitments.length = threshold

Share Verification

Party $j$ verifies share $s_j=f(j)$ by checking:

$$A(s_j)=\sum _{i=0}^{t-1}{j}^i\cdot C_i$$

This works because $A$ is linear: $$A(f(j))=A\left(\sum _i{a}_i\cdot j^i\right)=\sum _i{j}^i\cdot A(a_i)=\sum _i{j}^i\cdot C_i$$

def verifyShare (S : Scheme) [Module S.Scalar S.Public]
    (comm : PolyCommitment S) (share : VSSShare S) : Prop :=
  S.A share.value = expectedPublicValue S comm share.evalPoint

VSS Transcript

A complete VSS dealing is captured in a transcript structure with proof obligations:

def evalPointsDistinct {S : Scheme} [DecidableEq S.Scalar]
    (shares : List (VSSShare S)) : Prop :=
  (shares.map (·.evalPoint)).Nodup

structure VSSTranscript (S : Scheme) [DecidableEq S.Scalar] where
  commitment : PolyCommitment S
  shares : List (VSSShare S)
  evalPointsNodup : evalPointsDistinct shares  -- required for Lagrange interpolation

The evalPointsNodup proof ensures all shares have distinct evaluation points, which is essential for Lagrange interpolation to work correctly. The tryCreateVSSTranscript function provides runtime-checked construction:

def tryCreateVSSTranscript (S : Scheme) [DecidableEq S.Scalar]
    (p : Polynomial S.Secret)
    (parties : List (S.PartyId × S.Scalar))
    : Option (VSSTranscript S) :=
  if h : (parties.map Prod.snd).Nodup then
    some (createVSSTranscript S p parties h)
  else
    none

Complaint Mechanism

If verification fails, a party files a complaint with evidence:

structure VSSComplaint (S : Scheme) where
  complainant : S.PartyId
  accused : S.PartyId
  badShare : VSSShare S
  commitment : PolyCommitment S

Complaints are publicly verifiable. Anyone can check that the share does not verify against the commitment.

VSS-DKG Integration

In VSS-DKG, each party acts as a dealer for their own contribution:

1. Party $P_i$ samples polynomial $f_i(x)$ with $f_i(0)=s{k}_i$
2. Party $P_i$ broadcasts commitment to $f_i$
3. Party $P_i$ sends share $f_i(j)$ privately to each party $P_j$
4. Each party verifies received shares against commitments
5. Invalid shares generate complaints. Valid complaints identify faulty dealers.
6. Aggregate: $s{k}_j={\sum }_i{f}_i(j)$ and $pk={\sum }_{i}A(f_i(0))$

def vssFinalize (S : Scheme)
    (st : VSSLocalState S)
    (allCommitments : List (VSSCommitMsg S))
    : Option (KeyShare S)

Security Properties

Correctness. Honest shares verify: if $s_j=f(j)$ and $C_i=A(a_i)$, verification succeeds.

Soundness. Invalid shares are detected. A complaint is valid iff the share fails verification.

Binding. Commitment determines the polynomial (up to kernel of $A$). Dealer cannot equivocate.

Hiding. Fewer than $t$ shares reveal nothing about the secret (information-theoretic).

Public Key Verification

Any external verifier can check the consistency of published data.

1. Verify that each commitment ${\mathsf{Com}}_i$ opens to ${\mathsf{pk}}_i$.
2. Verify that $\mathsf{pk}={\sum }_i{\mathsf{pk}}_i$.

These checks do not require knowledge of secret shares. They ensure that the published public key corresponds to the committed shares.

DKG with Complaints

The threshold DKG variant collects complaints when verification fails rather than immediately aborting.

inductive Complaint (PartyId : Type) where
  | openingMismatch (accused : PartyId)
  | missingReveal (accused : PartyId)

The dkgAggregateWithComplaints function returns either the public key or a list of complaints.

def dkgAggregateWithComplaints
  (S : Scheme) [DecidableEq S.PartyId]
  (commits : List (DkgCommitMsg S))
  (reveals : List (DkgRevealMsg S))
  : Except (List (Complaint S.PartyId)) S.Public

This enables exclusion of misbehaving parties while continuing with the honest subset.

Party Exclusion

After collecting complaints, the protocol computes which parties should be excluded.

def Complaint.accused : Complaint PartyId → PartyId
  | .openingMismatch p => p
  | .missingReveal p => p

def accusedParties (complaints : List (Complaint PartyId)) : List PartyId :=
  (complaints.map Complaint.accused).dedup

def excludeFaulty (allParties : List PartyId) (complaints : List (Complaint PartyId)) : List PartyId :=
  let faulty := accusedParties complaints
  allParties.filter (fun p => p ∉ faulty)

Quorum Check

For threshold security, enough valid parties must remain:

inductive ExclusionResult (PartyId : Type)
  | quorumMet (validParties : List PartyId)   -- can continue
  | quorumFailed (validCount : Nat) (needed : Nat)  -- must abort

def hasThresholdQuorum (allParties complaints : List _) (threshold : Nat) : Bool :=
  (excludeFaulty allParties complaints).length ≥ threshold

If $|valid|\ge t$, the protocol can continue. Otherwise it must abort.

Reconstruction from Subset

When some parties are excluded, the remaining valid parties can reconstruct the public key using Lagrange interpolation.

def dkgLagrangeCoeff [Field F] (pidToScalar : PartyId → F) (validPids : List PartyId) (i : PartyId) : F :=
  let xi := pidToScalar i
  let others := validPids.filter (· ≠ i)
  (others.map (fun j => let xj := pidToScalar j; xj / (xj - xi))).prod

def reconstructPkFromSubset
    (S : Scheme) [Field S.Scalar]
    (pidToScalar : S.PartyId → S.Scalar)
    (validReveals : List (DkgRevealMsg S)) : S.Public :=
  let validPids := validReveals.map (·.sender)
  let weightedPks := validReveals.map fun r =>
    let λ_i := dkgLagrangeCoeff pidToScalar validPids r.sender
    λ_i • r.pk_i
  weightedPks.sum

Full DKG with Exclusion

The dkgWithExclusion function combines complaint handling with reconstruction:

def dkgWithExclusion
    (S : Scheme) [Field S.Scalar]
    (pidToScalar : S.PartyId → S.Scalar)
    (allParties : List S.PartyId)
    (commits : List (DkgCommitMsg S))
    (reveals : List (DkgRevealMsg S))
    (threshold : Nat)
    : Except (List (Complaint S.PartyId) × Nat) (S.Public × List S.PartyId) :=
  let complaints := dkgCheckComplaints S commits reveals
  if complaints.isEmpty then
    -- No complaints: simple aggregation
    Except.ok ((reveals.map (·.pk_i)).sum, allParties)
  else
    -- Try reconstruction from valid subset
    let validParties := excludeFaulty allParties complaints
    if validParties.length ≥ threshold then
      let validReveals := filterValidReveals reveals validParties
      let pk := reconstructPkFromSubset S pidToScalar validReveals
      Except.ok (pk, validParties)
    else
      Except.error (complaints, validParties.length)

Threshold Parameters

structure DKGParams where
  n : Nat                    -- total parties
  t : Nat                    -- threshold
  threshold_valid : t ≤ n    -- proof that t ≤ n

def DKGParams.maxFaulty (p : DKGParams) : Nat := p.n - p.t

def DKGParams.canContinue (p : DKGParams) (faultyCount : Nat) : Bool :=
  faultyCount ≤ p.maxFaulty

Finalizing Key Shares

After DKG completes successfully, each party converts its local state into a persistent key share using KeyShare.create:

def finalizeKeyShare
  (S : Scheme)
  (st : DkgLocalState S)
  (pk : S.Public)
  : KeyShare S :=
  KeyShare.create S st.pid st.sk_i st.pk_i pk

The KeyShare.create function wraps the secret in a SecretBox, ensuring the protective wrapper is applied at the point of creation.

Security Properties

Secrecy. No coalition of fewer than $t$ parties learns the master secret $s$.

Correctness. Honest execution produces shares that satisfy $A({\sum }_i{s}_i)=\mathsf{pk}$.

Robustness. If all parties are honest the protocol terminates successfully. If a party misbehaves it is detected through commitment verification.

Totality. The checked aggregation functions always return either success or a structured error.

Two-Round Threshold Signing

The signing protocol produces a threshold signature from partial contributions. It runs in two rounds with phase-indexed CRDT state. The first round commits to ephemeral nonces. The second round produces partial signatures. An aggregator combines the partials into a final signature.

Module Structure

The signing implementation is split across focused modules for maintainability:

• Protocol/Sign/Types.lean - Core types: SessionTracker, NonceRegistry, message types (SignCommitMsg, SignRevealWMsg, SignShareMsg), error types (SignError), and output types (Signature, SignatureDone)

• Protocol/Sign/LocalRejection.lean - Local rejection sampling for norm bounds (eliminates global retry coordination)

• Protocol/Core/Abort.lean - Session-level abort coordination for liveness failures and security violations

• Protocol/Sign/Core.lean - Core functions: lagrangeCoeffAtZero, lagrangeCoeffs, computeChallenge, aggregateSignature, aggregateSignatureLagrange, ValidSignTranscript, validateSigning

• Protocol/Sign/Threshold.lean - Threshold support: CoeffStrategy, strategyOK, SignMode, ThresholdCtx, context constructors (mkAllCtx, mkThresholdCtx, mkThresholdCtxComputed), and context-based aggregation

• Protocol/Sign/Sign.lean - Re-exports from all submodules for backward compatibility

• Protocol/Sign/Session.lean - Session-typed API that makes nonce reuse a compile-time error

Phase-Indexed State

The signing protocol uses phase-indexed state that forms a join-semilattice at each phase.

inductive Phase
  | commit
  | reveal
  | shares
  | done

Each phase carries accumulated data that can be merged with the join operation (⊔).

Inputs

Each signing session requires the following inputs.

• Message. The message $m\in \mathcal{M}$ to be signed.
• Signer set. The active signing subset $S\subseteq \{1,\dots ,n\}$.
• Secret shares. Each party $P_i\in S$ holds its secret share $s_i$.
• Public key. All parties know the global public key $\mathsf{pk}$.
• Public shares. All parties know the public shares $\{{\mathsf{pk}}_j\}$ from key generation.

Message Types

The protocol uses three message types across its phases.

structure SignCommitMsg (S : Scheme) where
  sender     : S.PartyId
  session    : Nat
  commitW    : S.Commitment  -- hash commitment to hiding nonce
  hidingVal  : S.Public      -- public hiding commitment W_hiding = A(hiding nonce)
  bindingVal : S.Public      -- public binding commitment W_binding = A(binding nonce)
  context    : ExternalContext := {}  -- for external protocol binding

structure SignRevealWMsg (S : Scheme) where
  sender  : S.PartyId
  session : Nat
  opening : S.Opening  -- opening for commitment verification
  context : ExternalContext := {}

structure SignShareMsg (S : Scheme) where
  sender  : S.PartyId
  session : Nat
  z_i     : S.Secret
  context : ExternalContext := {}  -- for external protocol binding

All message types include an optional context field for binding to external protocols. See Protocol Integration for details.

Dual Nonce Structure (FROST Pattern)

Following FROST, we use two nonces per signer instead of one:

• Hiding nonce: Protects against adaptive adversaries
• Binding nonce: Commits to the signing context (message + all commitments)

This provides stronger security against adaptive chosen-message attacks.

structure SigningNonces (S : Scheme) where
  hidingVal  : S.Secret   -- protects signer from adaptive adversaries
  bindingVal : S.Secret   -- commits to signing context

structure SigningCommitments (S : Scheme) where
  hidingVal  : S.Public   -- W_hiding = A(hiding nonce)
  bindingVal : S.Public   -- W_binding = A(binding nonce)

Domain-Separated Hash Functions (FROST H4, H5)

Following FROST, the signing protocol uses domain-separated hash functions:

• H4 (Message pre-hashing): hashMessage pre-hashes large messages before signing, using domain prefix ice-nine-v1-msg. This enables efficient signing of arbitrarily large messages.

• H5 (Commitment list hashing): hashCommitmentList produces canonical encodings of commitment lists, using domain prefix ice-nine-v1-com. This ensures all parties compute identical binding factors.

def hashMessage (S : Scheme) (msg : S.Message) : ByteArray :=
  HashDomain.message ++ serializeMessage msg

def hashCommitmentList (S : Scheme) (commits : List (SignCommitMsg S)) : ByteArray :=
  HashDomain.commitmentList ++ encodeCommitmentList S commits

Binding Factor Derivation

The binding factor ${\rho }_i$ binds each signer's nonce to the full signing context:

$${\rho }_i=H_1(\text{msg},\mathsf{pk},\text{encoded\_commitments},i)$$

where $H_1$ uses domain prefix ice-nine-v1-rho.

The effective nonce is then:

$$y_{\text{eff}}=y_{\text{hiding}}+\rho \cdot y_{\text{binding}}$$ $$w_{\text{eff}}=W_{\text{hiding}}+\rho \cdot W_{\text{binding}}$$

This prevents an adversary from adaptively choosing the message after seeing nonce commitments.

Party State

Each party $P_i$ maintains local state during signing.

structure SignLocalState (S : Scheme) where
  share   : KeyShare S             -- party's long-term credential from DKG
  msg     : S.Message              -- message being signed
  session : Nat                    -- unique session identifier
  nonces  : SigningNonces S        -- dual ephemeral nonces (NEVER reuse!)
  commits : SigningCommitments S   -- public nonce commitments
  openW   : S.Opening              -- commitment randomness for hiding commitment

The local state contains:

• The ephemeral nonces $(y_{\text{hiding}},y_{\text{binding}})\in {\mathcal{S}}^2$ sampled for this session.
• The public commitments $W_{\text{hiding}}=A(y_{\text{hiding}})$ and $W_{\text{binding}}=A(y_{\text{binding}})$.
• The commitment opening $\rho \in \mathcal{O}$.
• The session identifier for binding.

Round 1: Nonce Commitment

In round one each party commits to an ephemeral nonce. This commitment prevents adaptive attacks where an adversary chooses its nonce after seeing others.

Procedure (session-typed API)

The implementation no longer exposes raw signRound1/2. Use the linear, session-typed API in Protocol/Sign/Session.lean:

open IceNine.Protocol.SignSession

-- caller supplies fresh randomness
let ready := initSession S keyShare msg session hidingNonce bindingNonce opening
match commit S ready with
| .error err => -- session reuse or commitment reuse detected locally
| .ok { committed, msg := commitMsg, tracker, nonceReg } =>
  -- after collecting commits and computing challenge/binding factors:
  let (revealed, revealMsg, tracker', nonceReg') :=
    reveal S committed challenge bindingFactor aggregateW tracker nonceReg
  match sign S revealed tracker' nonceReg' with
  | .inl (signed, tracker'', nonceReg'') => finalize S signed
  | .inr _      => -- retry with NEW FreshNonce via retryWithFreshNonce

Round‑1 message contents are identical: each SignCommitMsg carries the hash commitment plus both public nonce values.

Each party $P_i\in S$ still samples fresh $(y_{\text{hiding}},y_{\text{binding}})$, computes $W_{\text{hiding}}=A(y_{\text{hiding}})$, $W_{\text{binding}}=A(y_{\text{binding}})$, samples an opening ${\rho }_i$, and broadcasts the commitment to $W_{\text{hiding}}$ together with both public nonces. The implementation also:

• marks the session as used in a per-party SessionTracker
• records commitW in a per-party NonceRegistry and rejects if the same commitment was used in a different session for that party.

Commit Phase State

The commit phase accumulates commit messages in a semilattice structure.

structure CommitState (S : Scheme) :=
  (commits : List (DkgCommitMsg S))

instance (S : Scheme) : Join (CommitState S) :=
  ⟨fun a b => { commits := a.commits ⊔ b.commits }⟩

Waiting for Commits

Each party waits until it receives commitments from all other parties in $S$. If a commitment does not arrive within a timeout the party may abort or exclude the missing party.

Nonce Reveal and Challenge Computation

After all commitments are received parties reveal their nonces and compute the shared challenge.

Reveal Phase

Each party $P_i$ broadcasts only the opening ${\rho }_i$ for its hiding commitment. The public nonces (hidingVal, bindingVal) were already sent in Round 1 inside SignCommitMsg. Trackers (SessionTracker, NonceRegistry) are threaded through. No additional updates occur in this phase.

Verification

Each party verifies all received openings. For each $P_j\in S$ check that

$$\mathsf{Com}(w_j,{\rho }_j)={\mathsf{Com}}_j^{(w)}$$

If any opening is invalid the party aborts the session. It may also file a complaint identifying the misbehaving party.

Nonce Aggregation

After successful verification compute the aggregated nonce.

$$w=\sum _{i\in S}{w}_i$$

Challenge Derivation

Compute the challenge using the hash function.

$$c=H(m,\mathsf{pk},S,\{{\mathsf{Com}}_i^{(w)}{\}}_{i\in S},w)$$

The challenge depends on the message, public key, signer set, all commitments, and the aggregated nonce. Including the commitments in the hash input binds the challenge to the commit phase.

Round 2: Partial Signatures

In round two each party produces its partial signature.

n-of-n Case

In the $n$-of-$n$ setting all parties must participate. The session transition sign in SignSession computes each partial signature as

$$z_i=y_i+c\cdot s_i$$

This is the standard Schnorr response. The ephemeral secret masks the product of challenge and secret share. The function returns none if the norm check fails.

t-of-n Case

In the $t$-of-$n$ setting a subset of parties signs. Each party must adjust its contribution using Lagrange coefficients.

structure LagrangeCoeff (S : Scheme) :=
  (pid    : S.PartyId)
  (lambda : S.Scalar)

Let ${\lambda }_i^S$ denote the Lagrange coefficient for party $i$ over the signing set $S$. Party $P_i$ computes

$$z_i=y_i+c\cdot {\lambda }_i^S\cdot s_i$$

The Lagrange coefficient ensures that the sum of adjusted shares equals the master secret.

Lagrange Coefficient Computation

def lagrangeCoeffAtZero
  (S : Scheme) [Field S.Scalar] [DecidableEq S.PartyId]
  (pidToScalar : S.PartyId → S.Scalar)
  (Sset : List S.PartyId) (i : S.PartyId) : S.Scalar

The Lagrange coefficient for party $i$ over set $S$ is

$${\lambda }_i^S=\prod _{j\in S,j\ne i}\frac{j}{j-i}$$

This computation uses party identifiers as evaluation points. All arithmetic is in the scalar ring $R$. Returns 0 if duplicate identifiers would cause division by zero.

Norm Check

Before broadcasting the partial signature each party may check the norm.

$$\mathsf{normOK}(z_i)$$

If the norm exceeds the bound the party aborts this session. It can retry with a fresh nonce. This check prevents leakage through the response distribution.

Broadcasting Partials

Each party $P_i$ broadcasts its partial signature $z_i$ to all parties in $S$.

Aggregation

An aggregator collects all partial signatures and produces the final signature.

Shares Phase State

The shares phase accumulates partial signatures along with threshold context. Messages are stored in MsgMap structures keyed by sender ID, making conflicting messages from the same sender un-expressable.

structure ShareState (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId] :=
  (commits : CommitMap S)   -- at most one commit per party
  (reveals : RevealMap S)   -- at most one reveal per party
  (shares  : ShareMap S)    -- at most one share per party
  (active  : Finset S.PartyId)

structure ShareWithCtx (S : Scheme) :=
  (state : ShareState S)
  (ctx   : ThresholdCtx S)

The MsgMap structure provides conflict detection: tryAddShare returns a conflict indicator if a party attempts to submit multiple shares, enabling detection of Byzantine behavior.

The threshold context ensures aggregation only proceeds when sufficient parties contribute.

inductive SignMode | all | threshold

inductive CoeffStrategy (S : Scheme)
  | ones                                      -- n-of-n: z = Σ z_i
  | lagrange (coeffs : List (LagrangeCoeff S)) -- t-of-n: z = Σ λ_i·z_i

structure ThresholdCtx (S : Scheme) :=
  (active     : Finset S.PartyId)    -- participating signers
  (t          : Nat)                 -- threshold (t = |active| for n-of-n)
  (mode       : SignMode)            -- n-of-n vs t-of-n
  (strategy   : CoeffStrategy S)     -- aggregation method
  (card_ge    : t ≤ active.card)     -- proof: have enough signers
  (strategy_ok : strategyOK S active.toList strategy) -- coeffs align

The CoeffStrategy type selects the aggregation path:

• ones: simple sum z = Σ z_i (n-of-n, no field operations)
• lagrange coeffs: weighted sum z = Σ λ_i·z_i (t-of-n, requires field)

Context Constructors

Smart constructors build ThresholdCtx with proofs:

-- n-of-n: threshold = |active|, strategy = ones
def mkAllCtx (S : Scheme) [DecidableEq S.PartyId]
  (active : Finset S.PartyId) : ThresholdCtx S

-- t-of-n with pre-supplied coefficients
def mkThresholdCtx
  (S : Scheme) [DecidableEq S.PartyId]
  (active : Finset S.PartyId)
  (t : Nat)
  (coeffs : List (LagrangeCoeff S))
  (hcard : t ≤ active.card)
  (halign : coeffs.map (·.pid) = active.toList)
  (hlen : coeffs.length = active.toList.length)
  : ThresholdCtx S

-- t-of-n with computed Lagrange coefficients (requires Field)
def mkThresholdCtxComputed
  (S : Scheme) [Field S.Scalar] [DecidableEq S.PartyId]
  (active : Finset S.PartyId)
  (t : Nat)
  (pidToScalar : S.PartyId → S.Scalar)
  (hcard : t ≤ active.card) : ThresholdCtx S

Collecting Partials

The aggregator receives $z_i$ from each $P_i\in S$. If any partial is missing the aggregator may wait or abort.

Signature Structure

structure Signature (S : Scheme) :=
  (z       : S.Secret)
  (c       : S.Challenge)
  (Sset    : List S.PartyId)
  (commits : List S.Commitment)
  (context : ExternalContext := {})  -- merged from contributing shares

The signature's context is merged from all contributing shares, enabling external protocols to verify consensus binding.

Signature Computation

For n-of-n aggregation:

def aggregateSignature
  (S    : Scheme)
  (c    : S.Challenge)
  (Sset : List S.PartyId)
  (commits : List S.Commitment)
  (shares : List (SignShareMsg S))
  : Signature S

Compute the aggregated response.

$$z=\sum _{i\in S}{z}_i$$

For t-of-n aggregation with Lagrange weighting:

def aggregateSignatureLagrange
  (S    : Scheme)
  (c    : S.Challenge)
  (Sset : List S.PartyId)
  (commits : List S.Commitment)
  (coeffs : List (LagrangeCoeff S))
  (shares : List (SignShareMsg S))
  : Signature S

Strategy-Based Aggregation

The aggregateWithStrategy function selects the aggregation path based on the coefficient strategy:

def aggregateWithStrategy
  (S    : Scheme) [DecidableEq S.PartyId]
  (c    : S.Challenge)
  (active : List S.PartyId)
  (commits : List S.Commitment)
  (shares : List (SignShareMsg S))
  (strategy : CoeffStrategy S)
  : Option (Signature S)

This function validates that all shares come from the declared active set, then dispatches to aggregateSignature (for .ones) or aggregateSignatureLagrange (for .lagrange coeffs).

Context-Based Aggregation

For full validation using the threshold context:

def aggregateSignatureWithCtx
  (S    : Scheme) [DecidableEq S.PartyId]
  (c    : S.Challenge)
  (ctx  : ThresholdCtx S)
  (commits : List S.Commitment)
  (shares : List (SignShareMsg S))
  : Option (Signature S)

This function checks sharesFromActive (membership validation) before delegating to aggregateWithStrategy using the context's strategy.

Final Signature

The signature consists of the following components.

$$\sigma =(z,c,S,\{{\mathsf{Com}}_i^{(w)}{\}}_{i\in S})$$

The signature includes the aggregated response, the challenge, the signer set, and all nonce commitments.

Correctness

The aggregated response satisfies the verification equation. Consider the $n$-of-$n$ case.

$$z=\sum _{i\in S}{z}_i=\sum _{i\in S}(y_i+c\cdot s_i)=\sum _{i\in S}{y}_i+c\cdot \sum _{i\in S}{s}_i=y+c\cdot s$$

where $y={\sum }_i{y}_i$ and $s={\sum }_i{s}_i$.

Applying the linear map $A$ gives

$$A(z)=A(y)+c\cdot A(s)=w+c\cdot \mathsf{pk}$$

Rearranging yields

$$A(z)-c\cdot \mathsf{pk}=w$$

The verifier recomputes $w$ from this equation and checks the challenge.

t-of-n Correctness

In the $t$-of-$n$ case the Lagrange coefficients ensure

$$\sum _{i\in S}{\lambda }_i^S\cdot s_i=s$$

The rest of the argument follows as above.

Session Binding

The challenge binds to the specific session through several mechanisms.

1. The message $m$ is included in the hash input.
2. The public key $\mathsf{pk}$ is included.
3. The signer set $S$ is included.
4. All nonce commitments are included.
5. The aggregated nonce $w$ is included.

This binding prevents cross-session attacks where an adversary reuses partial signatures from different sessions.

Transcript Validation

The validateSigning function checks the entire signing transcript before aggregation. Its current signature also requires precomputed binding factors (derived from the commit list):

def validateSigning
  (S     : Scheme) [DecidableEq S.PartyId]
  (pk    : S.Public)
  (m     : S.Message)
  (Sset  : List S.PartyId)
  (commits : List (SignCommitMsg S))
  (reveals : List (SignRevealWMsg S))
  (bindingFactors : BindingFactors S)
  (shares  : List (SignShareMsg S))
  : Except (SignError S.PartyId) (Signature S)

Callers must compute bindingFactors (e.g., via computeBindingFactors) and supply them. Otherwise validation will not type-check.

Error Types

inductive SignError (PartyId : Type) where
  | lengthMismatch : SignError PartyId
  | participantMismatch : PartyId → SignError PartyId
  | duplicateParticipants : PartyId → SignError PartyId
  | commitMismatch : PartyId → SignError PartyId
  | sessionMismatch : Nat → Nat → SignError PartyId

Note: Legacy error variants (normCheckFailed, maxRetriesExceeded, sessionAborted) have been removed. With local rejection sampling, norm bounds are handled locally. Session-level aborts use AbortReason from Protocol/Core/Abort.lean.

Valid Transcript Predicate

structure ValidSignTranscript (S : Scheme)
  (Sset : List S.PartyId)
  (commits : List (SignCommitMsg S))
  (reveals : List (SignRevealWMsg S))
  (shares  : List (SignShareMsg S)) : Prop where
  len_comm_reveal : commits.length = reveals.length
  len_reveal_share : reveals.length = shares.length
  pids_nodup : (commits.map (·.sender)).Nodup
  pids_eq : commits.map (·.sender) = Sset
  commit_open_ok : List.Forall₂ (fun c r => c.sender = r.sender ∧ S.commit c.hiding r.opening = c.commitW) commits reveals
  sessions_ok : let sess := (commits.head?.map (·.session)).getD 0; ∀ sh ∈ shares, sh.session = sess

Monotonic Step Functions

State transitions are monotone with respect to the semilattice order.

def stepCommit (S : Scheme) (msg : DkgCommitMsg S) (st : CommitState S) : CommitState S :=
  { commits := st.commits ⊔ [msg] }

lemma stepCommit_monotone (S : Scheme) (msg : DkgCommitMsg S) :
  ∀ a b, a ≤ b → stepCommit S msg a ≤ stepCommit S msg b

Similar monotonicity holds for stepReveal and stepShare.

Abort Conditions

The signing protocol may abort under several conditions.

Missing commitment. A party in $S$ does not broadcast its commitment.

Invalid opening. A received opening does not match its commitment.

Missing partial. A party does not broadcast its partial signature.

Norm violation. A partial signature fails the norm check.

Inconsistent challenge. Parties compute different challenges due to inconsistent views.

Session mismatch. Messages have inconsistent session identifiers.

When aborting parties should discard all session state. They should not reuse the ephemeral nonce $y_i$ in any future session.

Session Tracking and Nonce Safety

CRITICAL: Nonce reuse completely breaks Schnorr-style signatures.

If the same nonce $y$ is used with two different challenges $c_1,c_2$:

• $z_1=y+c_1\cdot sk$
• $z_2=y+c_2\cdot sk$

The secret key can be recovered: $sk=(z_1-z_2)/(c_1-c_2)$

This attack is formalized in Proofs/Soundness/Soundness.lean as the nonce_reuse_key_recovery theorem. See Verification: Special Soundness for the formal proof.

Session Tracker

Each party tracks used session IDs:

structure SessionTracker (S : Scheme) where
  usedSessions : Finset Nat    -- sessions that have been used
  partyId : S.PartyId

def SessionTracker.isFresh (tracker : SessionTracker S) (session : Nat) : Bool :=
  session ∉ tracker.usedSessions

def SessionTracker.markUsed (tracker : SessionTracker S) (session : Nat) : SessionTracker S :=
  { tracker with usedSessions := tracker.usedSessions.insert session }

Session Validation

inductive SessionCheckResult
  | ok                           -- session is fresh
  | alreadyUsed (session : Nat)  -- DANGER: would reuse nonce
  | invalidId

def checkSession (tracker : SessionTracker S) (session : Nat) : SessionCheckResult :=
  if tracker.isFresh session then .ok
  else .alreadyUsed session

Nonce Registry

For network-wide detection, the NonceRegistry uses HashMap-based indices for O(1) lookup:

structure NonceRegistry (S : Scheme)
    [BEq S.PartyId] [Hashable S.PartyId]
    [BEq S.Commitment] [Hashable S.Commitment] where
  bySession : Std.HashMap (S.PartyId × Nat) S.Commitment      -- primary index
  byCommitment : Std.HashMap (S.PartyId × S.Commitment) (List Nat)  -- reverse index

def NonceRegistry.hasCommitment (reg : NonceRegistry S)
    (pid : S.PartyId) (session : Nat) (commit : S.Commitment) : Bool :=
  match reg.bySession.get? (pid, session) with
  | some c => c == commit
  | none => false

def NonceRegistry.detectReuse (reg : NonceRegistry S)
    (pid : S.PartyId) (commit : S.Commitment) : Option (Nat × Nat) :=
  match reg.byCommitment.get? (pid, commit) with
  | some (s1 :: s2 :: _) => if s1 ≠ s2 then some (s1, s2) else none
  | _ => none

The dual index structure provides:

• O(1) lookup by (partyId, session) for commitment retrieval
• O(1) reuse detection by (partyId, commitment) for security monitoring

Local Rejection Sampling

In lattice signatures, the response $z$ must have bounded norm to prevent leakage. Ice Nine uses local rejection sampling where each signer independently ensures their partial signature satisfies norm bounds before broadcasting.

Key Invariant

If each of $T$ signers produces $z_i$ with $\Vert z_i{\Vert }_{\infty }\le B_{\text{local}}$, then the aggregate $z=\sum z_i$ satisfies $\Vert z{\Vert }_{\infty }\le T\cdot B_{\text{local}}\le B_{\text{global}}$.

This eliminates global rejection as a distributed control-flow path.

Local Sign Result

inductive LocalSignResult (S : Scheme)
  | success (z_i : S.Secret) (hidingNonce bindingNonce : S.Secret) (attempts : Nat)
  | failure (err : LocalRejectionError S.PartyId)

Rejection Loop

Each signer runs local rejection sampling independently:

def localRejectionLoop (S : Scheme) (cfg : ThresholdConfig)
    (partyId : S.PartyId) (sk_i : S.Secret) (challenge : S.Challenge)
    (bindingFactor : S.Scalar) (sampleNonce : IO (S.Secret × S.Secret))
    : IO (LocalSignResult S)

The loop:

1. Samples fresh nonce pair $(y_{\text{hiding}},y_{\text{binding}})$
2. Computes $z_i=y_{\text{hiding}}+\rho \cdot y_{\text{binding}}+c\cdot s{k}_i$
3. Checks if $\Vert z_i{\Vert }_{\infty }\le B_{\text{local}}$
4. Returns success or retries with new nonces (up to maxLocalAttempts)

Parallelization

Local rejection is trivially parallelizable:

• Across signers: Each signer's loop is independent
• Within signer: Batch multiple nonce candidates (localRejectionLoopParallel)
• Within batch: SIMD/vectorized norm checking

Reference: Lyubashevsky, "Fiat-Shamir with Aborts", ASIACRYPT 2009.

Session Abort Coordination

While local rejection handles norm bounds, session-level aborts are needed for:

• Liveness failures: Parties offline, session times out
• Security violations: Trust assumption violated (more than $n-t$ faulty parties)
• Explicit cancellation: Group decides to abandon signing

Abort Reasons

inductive AbortReason (PartyId : Type*) where
  -- Liveness failures (require f+1 votes)
  | timeout (respondents : Nat) (required : Nat)
  | insufficientParticipants (actual : Nat) (required : Nat)
  | partyUnresponsive (parties : List PartyId)

  -- Security violations (immediate abort, no voting)
  | trustViolation (faultyCount : Nat) (maxTolerable : Nat)
  | globalNormExceeded (aggregateNorm : Nat) (bound : Nat)
  | tooManyComplaints (complaints : Nat) (maxTolerable : Nat)

  -- Explicit request (requires f+1 votes)
  | requestedBy (requester : PartyId)

Abort State (CRDT)

structure AbortState (S : Scheme) where
  session : Nat
  votes : Finset S.PartyId
  reasons : List (AbortReason S.PartyId)
  immediateTriggered : Bool := false

instance (S : Scheme) : Join (AbortState S) :=
  ⟨fun a b => {
    session := a.session
    votes := a.votes ∪ b.votes
    reasons := (a.reasons ++ b.reasons).dedup
    immediateTriggered := a.immediateTriggered || b.immediateTriggered
  }⟩

Abort Threshold

Abort consensus uses ThresholdConfig.abortThreshold which is $f+1$ where $f=n-t$ (max faulty parties). This ensures at least one honest party agreed to abort, preventing malicious minorities from forcing spurious aborts.

def ThresholdConfig.abortThreshold (cfg : ThresholdConfig) : Nat :=
  cfg.maxFaulty + 1

def AbortState.shouldAbort (state : AbortState S) (cfg : ThresholdConfig) : Bool :=
  state.hasImmediateReason || state.isConfirmedByVotes cfg

Security violations trigger immediate abort without voting.

Session-Typed Signing

The Protocol/Sign/Session.lean module provides a session-typed API that makes nonce reuse a compile-time error rather than a runtime check. Each signing session progresses through states that consume the previous state, ensuring nonces are used exactly once.

Session State Machine

ReadyToCommit ──► Committed ──► Revealed ──► SignedWithStats ──► Done
                      │              │
                      └──────► Aborted ◄──────┘

Each transition consumes its input state. There is no way to "go back" or reuse a consumed state. The ReadyToCommit state contains a FreshNonce that gets consumed during the commit transition. Sessions may transition to Aborted from Committed or Revealed when abort consensus is reached.

Linear Nonce (Dual Nonce Version)

Following FROST, we use two nonces per signer:

structure FreshNonce (S : Scheme) where
  private mk ::
  private hidingNonce : S.Secret    -- secret hiding nonce
  private bindingNonce : S.Secret   -- secret binding nonce
  private publicHiding : S.Public   -- W_hiding = A(hiding)
  private publicBinding : S.Public  -- W_binding = A(binding)
  private opening : S.Opening       -- commitment opening

def FreshNonce.sample (S : Scheme) (h b : S.Secret) (opening : S.Opening) : FreshNonce S

The private constructor prevents arbitrary creation. The only way to create a FreshNonce is via sample with fresh randomness for both hiding and binding nonces.

Session States

Each state carries the data accumulated up to that point (dual nonce version):

structure ReadyToCommit (S : Scheme) where
  keyShare : KeyShare S
  nonce : FreshNonce S      -- dual nonces, will be consumed on commit
  message : S.Message
  session : Nat

structure Committed (S : Scheme) where
  keyShare : KeyShare S
  private hidingNonce : S.Secret   -- moved from FreshNonce
  private bindingNonce : S.Secret  -- moved from FreshNonce
  publicHiding : S.Public
  publicBinding : S.Public
  opening : S.Opening
  message : S.Message
  session : Nat
  commitment : S.Commitment
  nonceConsumed : NonceConsumed S  -- proof token

structure Revealed (S : Scheme) where
  keyShare : KeyShare S
  private hidingNonce : S.Secret
  private bindingNonce : S.Secret
  publicHiding : S.Public
  publicBinding : S.Public
  message : S.Message
  session : Nat
  challenge : S.Challenge
  bindingFactor : S.Scalar     -- ρ for this signer
  aggregateNonce : S.Public    -- w = Σ (W_hiding_i + ρ_i·W_binding_i)

structure SignedWithStats (S : Scheme) extends Signed S where
  localAttempts : Nat      -- number of local rejection attempts
  hidingNonce : S.Secret   -- the nonce used
  bindingNonce : S.Secret

structure Done (S : Scheme) where
  shareMsg : SignShareMsg S

structure Aborted (S : Scheme) where
  session : Nat
  reason : AbortReason S.PartyId
  voteCount : Nat

Session Transitions

Each transition function consumes its input and produces the next state:

-- Consumes ReadyToCommit, produces Committed
-- The FreshNonce inside is consumed; cannot be accessed again
def commit (S : Scheme) (ready : ReadyToCommit S)
    : Except (SignError S.PartyId) (CommitResult S)

-- Consumes Committed, produces Revealed
-- Receives challenge, binding factor, and aggregate nonce from coordinator
def reveal (S : Scheme) (committed : Committed S)
    (challenge : S.Challenge) (bindingFactor : S.Scalar) (aggregateW : S.Public)
    : Revealed S × SignRevealWMsg S × SessionTracker S × NonceRegistry S

-- Consumes Revealed, produces SignedWithStats using local rejection sampling
-- Never fails norm check because rejection happens internally
def signWithLocalRejection (S : Scheme) (revealed : Revealed S)
    (cfg : ThresholdConfig) (sampleNonce : IO (S.Secret × S.Secret))
    : IO (Except (LocalRejectionError S.PartyId) (SignedWithStats S))

-- Consumes Signed, produces Done
def finalize (S : Scheme) (signed : Signed S) : Done S

-- Abort transitions (consume current state, produce Aborted)
def abortFromCommitted (S : Scheme) (committed : Committed S)
    (reason : AbortReason S.PartyId) (voteCount : Nat) : Aborted S

def abortFromRevealed (S : Scheme) (revealed : Revealed S)
    (reason : AbortReason S.PartyId) (voteCount : Nat) : Aborted S

Local Rejection Sampling

Ice Nine implements restart-free threshold Dilithium signing with local rejection sampling. Each signer applies rejection sampling locally before sending their partial signature. The bounds are chosen so that any valid combination of partials automatically satisfies global bounds.

The key invariant is that if each of T signers produces z_i with ‖z_i‖∞ ≤ B_local, then the aggregate z = Σz_i satisfies ‖z‖∞ ≤ T · B_local ≤ B_global. This eliminates global rejection as a distributed control-flow path. Given sufficient honest parties at or above threshold, signing does not trigger a distributed restart due to rejection sampling.

With local rejection sampling, norm bounds are handled locally by each signer. Each signer runs rejection sampling independently until producing a valid partial. No global retry coordination is needed. The signWithLocalRejection function never returns a norm failure.

Design Rationale

Local rejection sampling is designed for BFT consensus integration. In a typical BFT setting with n = 3f+1 validators and threshold t = 2f+1, at most f validators can be Byzantine. The signing protocol must produce signatures despite malicious behavior, without allowing a small coalition to stall progress.

The naive approach to threshold Dilithium would check the global bound after aggregation. If the aggregate z exceeds the bound, all parties must restart with fresh randomness. This creates a liveness vulnerability: a single malicious party could repeatedly cause the ceremony to fail by sending out-of-bounds partials.

Local rejection eliminates this vulnerability through a mathematical guarantee. By the triangle inequality:

$$\Vert z{\Vert }_{\infty }={\Vert \sum _{i\in S}{z}_i\Vert }_{\infty }\le \sum _{i\in S}\Vert z_i{\Vert }_{\infty }$$

If each partial satisfies ‖z_i‖∞ ≤ B_local and we aggregate at most T partials, then ‖z‖∞ ≤ T · B_local. Setting B_local = B_global / T guarantees that any combination of valid partials produces a valid aggregate. Global overflow becomes mathematically impossible, not just unlikely.

The aggregator enforces per-share bounds and discards invalid partials. With at least 2f+1 honest validators, there always exist t valid partials to aggregate. Malicious parties can only cause their own shares to be rejected. They cannot force a distributed restart.

Trade-offs

Local rejection changes the scheme parameters compared to single-signer Dilithium.

More local sampling. Tighter per-signer bounds (B_local < B_global) increase the expected number of rejection sampling iterations per signer. This is additional CPU cost but does not affect the distributed protocol. The extra work is invisible to other parties.

Narrower distribution. The effective distribution on z is more constrained than standard Dilithium. This means the scheme is "Dilithium-like with stricter bounds" rather than a bit-for-bit clone of ML-DSA. Security arguments must account for the modified bounds.

Exceptional global rejection. If global rejection ever occurs despite local bounds, it indicates either a negligible probability event or Byzantine behavior (shares that passed local validation but were crafted to overflow when combined). This is treated as a security anomaly, not normal control flow.

Local Rejection vs Global Abort

Session aborts are for global failures that cannot be resolved locally:

• Timeout waiting for other parties
• Security violations (trust assumption breached)
• Explicit cancellation by consensus

Type-Level Guarantees

The session type system provides these guarantees:

1. Nonce uniqueness: Each FreshNonce can only be consumed once. The commit function consumes the ReadyToCommit state, and the nonce value moves into Committed. There's no path back.

2. Linear flow: States can only progress forward. Each transition consumes its input. Sessions may also transition to Aborted.

3. Local rejection: With signWithLocalRejection, norm bounds are satisfied during signing via local rejection sampling. No global retry loop is needed.

4. Compile-time enforcement: These are not runtime checks. The type system prevents writing code that would reuse a nonce.

5. Abort safety: Aborted sessions cannot continue. Once a session transitions to Aborted, any consumed nonces are invalidated.

Example: Nonce Reuse is Uncompilable

-- This CANNOT compile because `ready` is consumed by first `commit`
def badNonceReuse (S : Scheme) (ready : ReadyToCommit S) :=
  let (committed1, _) := commit S ready  -- consumes ready
  let (committed2, _) := commit S ready  -- ERROR: ready already consumed
  (committed1, committed2)

Fast-Path Signing

For latency-sensitive applications, Ice Nine supports single-round signing when nonces are precomputed and pre-shared. This mode skips the commit-reveal round by preparing nonces during idle time.

Precomputed Nonces

structure PrecomputedNonce (S : Scheme) where
  commitment : S.Commitment
  nonce : FreshNonce S
  publicHiding : S.Public
  publicBinding : S.Public
  generatedAt : Nat
  maxAge : Nat := 3600  -- 1 hour default expiry

structure NoncePool (S : Scheme) where
  available : List (PrecomputedNonce S)
  consumedCount : Nat := 0

Fast Signing Function

def signFast (S : Scheme)
    (keyShare : KeyShare S)
    (precomputed : PrecomputedNonce S)
    (challenge : S.Challenge)
    (bindingFactor : S.Scalar)
    (session : Nat)
    (context : ExternalContext := {})
    : Option (SignShareMsg S)

This function produces a signature share immediately using a precomputed nonce. It SHOULD return none if the norm check fails, requiring a fresh nonce. The current Lean code stubs out the norm check and always returns some. Production code must call S.normOK here and propagate failure.

Security Assumptions

Fast-path signing trusts that:

1. Nonce commitments were honestly generated
2. Nonces are not being reused (enforced by FreshNonce type)
3. Precomputed nonces have not expired
4. The coordinator will aggregate honestly

Use standard two-round signing when these assumptions don't hold.

See Protocol Integration for detailed usage patterns with external consensus protocols.

Security Considerations

Nonce reuse. Using the same nonce $y_i$ in two sessions leaks the secret share $s_i$. Session types make nonce reuse a compile-time error.

Commitment binding. The commitment prevents a party from choosing its nonce adaptively. This protects against rogue key attacks.

Challenge entropy. The hash function must produce challenges with sufficient entropy. In the random oracle model this is guaranteed.

Norm bounds. The norm check prevents statistical leakage of the secret through the response distribution. Local rejection sampling ensures each partial signature is independent of the secret. No global retry coordination is needed.

Abort coordination. Session-level aborts (for liveness failures or security violations) use CRDT state with an $f+1$ threshold, ensuring at least one honest party agreed to abort.

Totality. The validation function always returns either a valid signature or a structured error.

Nonce Lifecycle

The Protocol/Sign/NonceLifecycle.lean module provides unified effect abstractions for nonce management. It consolidates session tracking, nonce registry, and pool management into a single composable interface with explicit error handling.

Nonce Safety Invariants

The module enforces four safety invariants.

Session uniqueness ensures each session ID is used at most once per party. Reusing a session ID could lead to nonce reuse.

Commitment uniqueness ensures each nonce commitment appears in at most one session. If the same commitment appears twice, a nonce was reused.

Consumption tracking ensures nonces are consumed exactly once. The FreshNonce type enforces this at compile time. The runtime registry provides defense-in-depth.

Expiry enforcement ensures precomputed nonces expire and cannot be used past their maximum age. This prevents stale nonces from being used after key rotation.

NonceState Structure

The NonceState structure consolidates all nonce-related tracking.

structure NonceState (S : Scheme) where
  partyId : S.PartyId
  usedSessions : Finset Nat
  commitBySession : Std.HashMap (S.PartyId × Nat) S.Commitment
  sessionsByCommit : Std.HashMap (S.PartyId × S.Commitment) (List Nat)
  poolAvailable : List (PrecomputedNonce S)
  poolConsumed : Nat

The usedSessions field tracks all sessions where commit has occurred. The commitBySession map provides forward lookup from session to commitment. The sessionsByCommit map provides reverse lookup for reuse detection.

NonceError Type

Nonce operations return typed errors for precise error handling.

inductive NonceError (PartyId : Type*)
  | sessionAlreadyUsed (session : Nat) (party : Option PartyId)
  | commitmentReuse (session1 session2 : Nat) (party : PartyId)
  | nonceExpired (generatedAt currentTime maxAge : Nat)
  | poolEmpty
  | poolExhausted (consumed : Nat)
  | invalidSession (reason : String)
  | nonceNotFound (session : Nat)

The commitmentReuse error is a security violation. The BlameableError instance identifies the party responsible. Other errors are operational without blame attribution.

Pure Operations

The NonceOp namespace provides pure operations on NonceState.

-- Check session freshness
def checkFresh (session : Nat) (st : NonceState S) : NonceResult S Unit

-- Mark session as used
def markUsed (session : Nat) (st : NonceState S) : NonceResult S Unit

-- Record a commitment
def recordCommitment (session : Nat) (commit : S.Commitment) (st : NonceState S)
    : NonceResult S Unit

-- Check for reuse and throw if detected
def assertNoReuse (commit : S.Commitment) (st : NonceState S) : NonceResult S Unit

-- Full commit operation: check fresh, mark used, record, check reuse
def commitSession (session : Nat) (commit : S.Commitment) (st : NonceState S)
    : NonceResult S Unit

The commitSession operation combines all checks into a single atomic operation. It ensures session freshness, marks the session as used, records the commitment, and checks for reuse.

Monadic Interface

The NonceM monad provides composition for chaining operations.

abbrev NonceM (S : Scheme) :=
  StateT (NonceState S) (Except (NonceError S.PartyId))

-- Run and get final state
def NonceM.run (m : NonceM S α) (st : NonceState S)
    : Except (NonceError S.PartyId) (α × NonceState S)

The monadic interface threads state automatically and short-circuits on errors.

Session Type Integration

The module bridges runtime tracking with compile-time session types.

-- Create ReadyToCommit using NonceState for tracking
def initSessionWithState (S : Scheme) (keyShare : KeyShare S) (message : S.Message)
    (session : Nat) (nonce : FreshNonce S) (st : NonceState S) : ReadyToCommit S

-- Commit transition that updates NonceState
def commitWithState (S : Scheme) (ready : ReadyToCommit S) (st : NonceState S)
    : Except (NonceError S.PartyId) (Committed S × SignCommitMsg S × NonceState S)

The commitWithState function consumes the FreshNonce inside ReadyToCommit. Session types prevent reuse at compile time. The NonceState provides runtime detection as defense-in-depth.

Validated Aggregation

The Protocol/Sign/ValidatedAggregation.lean module provides per-share validation during signature aggregation. This enables local rejection sampling by validating each partial signature before aggregation and collecting blame for invalid shares.

Validation Process

Validated aggregation performs three checks on each share.

Norm bound check verifies ‖z_i‖∞ ≤ B_local where B_local is the local rejection bound from ThresholdConfig. Shares exceeding the bound are rejected.

Algebraic check verifies A(z_i) = w_eff + c·pk_i where w_eff is the effective nonce commitment incorporating the binding factor. This detects malformed shares.

Commitment presence verifies the share has a corresponding commitment from round 1. Missing commitments indicate protocol violations.

ShareValidationError

Validation errors identify the responsible party.

inductive ShareValidationError (PartyId : Type*)
  | normExceeded (party : PartyId) (actual : Nat) (bound : Nat)
  | algebraicInvalid (party : PartyId) (reason : String)
  | missingCommitment (party : PartyId)
  | missingBindingFactor (party : PartyId)

All error variants implement BlameableError for blame attribution.

AggregationResult

The aggregation result contains the signature (if successful), blame information, and statistics.

structure AggregationResult (S : Scheme) where
  signature : Option (Signature S)
  includedParties : List S.PartyId
  blame : BlameResult S.PartyId
  success : Bool
  totalReceived : Nat
  validCount : Nat

The blame field contains collected errors according to ProtocolConfig. The includedParties list identifies which shares were aggregated.

aggregateValidated Function

The primary aggregation function validates shares and aggregates valid ones.

def aggregateValidated (S : Scheme) (cfg : ThresholdConfig)
    (protocolCfg : ProtocolConfig) (challenge : S.Challenge)
    (commitments : List (SignCommitMsg S)) (shares : List (SignShareMsg S))
    (pkShares : S.PartyId → S.Public) (bindingFactors : BindingFactors S)
    : AggregationResult S

The function validates all shares, partitions them into valid and invalid, collects blame according to protocolCfg, and aggregates the first threshold valid shares.

Guarantee

If at least threshold parties produce valid shares, the aggregate signature is guaranteed to satisfy the global norm bound. This follows from the local bound relationship: T · B_local ≤ B_global.

Byzantine Robustness

The aggregator validates each partial independently and discards invalid ones. Validation checks three conditions.

Structural validity ensures the partial has correct dimensions and format. Norm bound checking verifies ‖z_i‖∞ ≤ B_local where B_local is the local rejection bound. Algebraic validity checks that A(z_i) = w_eff + c·pk_i where w_eff incorporates the binding factor.

Parties that send out-of-bound or algebraically invalid partials have their shares rejected. The aggregator does not attempt to include them in the signature. This allows misbehaving parties to be identified and excluded.

Given n = 3f+1 validators with at most f Byzantine, there always exist at least t = 2f+1 honest validators. These honest validators will produce valid partials. The aggregator collects valid partials until reaching the threshold, then produces a valid signature.

A malicious party can slow the signing ceremony by sending invalid partials, but cannot prevent a valid signature from being produced. The combination of per-share validation and honest majority ensures liveness despite Byzantine participants.

Verification

Verification checks that a signature is valid for a given message and public key. The procedure uses the linear map $A$ and the hash function. It does not require knowledge of any secret shares.

Inputs

The verifier receives the following inputs.

• Signature. The Signature structure containing:

  structure Signature (S : Scheme) where
    z       : S.Secret
    c       : S.Challenge
    Sset    : List S.PartyId
    commits : List S.Commitment
    context : ExternalContext := {}
  

• Message. The message $m\in \mathcal{M}$ that was signed.
• Public key. The global public key $\mathsf{pk}$.

Verification Procedure

The verify function checks signature validity.

def verify
  (S   : Scheme)
  (pk  : S.Public)
  (m   : S.Message)
  (sig : Signature S)
  : Prop :=
  let w' : S.Public := S.A sig.z - (sig.c • pk)
  S.normOK sig.z ∧
    let c' := S.hash m pk sig.Sset sig.commits w'
    c' = sig.c

The verifier executes the following steps.

Step 1: Nonce Recovery

Compute the recovered nonce from the signature components.

$$w^{\prime }=A(z)-c\cdot \mathsf{pk}$$

This computation uses the linear map $A$ applied to the response $z$. It subtracts the challenge times the public key.

Step 2: Norm Check

Verify that the response satisfies the norm bound.

$$\mathsf{normOK}(z)$$

If the response has excessive norm the signature is invalid. This check rejects signatures that could leak information through the response distribution.

Step 3: Challenge Recomputation

Compute the expected challenge using the hash function.

$$c^{\prime }=H(m,\mathsf{pk},S,\{{\mathsf{Com}}_i^{(w)}{\}}_{i\in S},w^{\prime })$$

The hash input matches the signing protocol. It includes the message, public key, signer set, all nonce commitments, and the recovered nonce.

Step 4: Challenge Comparison

Compare the recomputed challenge to the signature's challenge.

$$c^{\prime }\stackrel{?}{=}c$$

If the challenges match the signature is valid. Otherwise the signature is invalid.

Verification Correctness

We show that valid signatures pass verification. Consider a signature produced by honest parties.

The aggregated response is

$$z=\sum _{i\in S}{z}_i=\sum _{i\in S}(y_i+c\cdot s_i)$$

In the $n$-of-$n$ case this simplifies to

$$z=y+c\cdot s$$

where $y={\sum }_i{y}_i$ and $s={\sum }_i{s}_i$.

Applying $A$ and using linearity gives

$$A(z)=A(y+c\cdot s)=A(y)+c\cdot A(s)=w+c\cdot \mathsf{pk}$$

Subtracting $c\cdot \mathsf{pk}$ yields

$$A(z)-c\cdot \mathsf{pk}=w$$

The recovered nonce equals the original aggregated nonce. Since the hash inputs are identical the recomputed challenge matches the original. The signature passes verification.

t-of-n Correctness

In the $t$-of-$n$ case the Lagrange coefficients ensure

$$\sum _{i\in S}{\lambda }_i^S\cdot s_i=s$$

The aggregated response is

$$z=\sum _{i\in S}(y_i+c\cdot {\lambda }_i^S\cdot s_i)=y+c\cdot s$$

The rest of the argument follows identically.

Algebraic Identity

The core algebraic identity underlying verification is

$$A(z)-c\cdot \mathsf{pk}=\sum _{i\in S}A(y_i)=w$$

This identity holds because of the following chain of equalities.

$$A(z)=A\left(\sum _{i\in S}{z}_i\right)=\sum _{i\in S}A(z_i)$$

For each partial response

$$A(z_i)=A(y_i+c\cdot s_i)=A(y_i)+c\cdot A(s_i)=w_i+c\cdot {\mathsf{pk}}_i$$

Summing over the signer set

$$A(z)=\sum _{i\in S}(w_i+c\cdot {\mathsf{pk}}_i)=w+c\cdot \sum _{i\in S}{\mathsf{pk}}_i$$

In the $n$-of-$n$ case the public shares sum to the global key

$$\sum _{i\in S}{\mathsf{pk}}_i=\mathsf{pk}$$

Therefore

$$A(z)=w+c\cdot \mathsf{pk}$$

and the verification equation follows.

Commitment Verification

The nonce commitments serve two purposes during verification.

Session Binding

The commitments are included in the hash input. This binds the challenge to the specific signing session. An adversary cannot reuse partial signatures from different sessions because the commitments would differ.

Audit Trail

The commitments provide an audit trail. A verifier can check that the signing session followed the protocol. Without access to the openings the verifier cannot check the commitments directly. However the commitments still bind the signers to their original nonces.

Error Cases

Several conditions cause verification to fail.

Invalid response. The response $z$ does not satisfy $\mathsf{normOK}(z)$.

Challenge mismatch. The recomputed challenge $c^{\prime }$ differs from the signature's challenge $c$.

Malformed signature. The signature does not contain all required components.

Batch Verification

When verifying multiple signatures with the same public key some computations can be shared.

Shared Public Key Computation

If multiple signatures use the same $\mathsf{pk}$ the verifier can cache $\mathsf{pk}$ rather than recomputing it.

Parallel Hash Evaluation

The hash computations for different signatures are independent. They can run in parallel.

Aggregated Equation Check

For a batch of $k$ signatures with random weights ${\alpha }_1,\dots ,{\alpha }_k$ the verifier can check

$$\sum _{j=1}^k{\alpha }_j\cdot (A(z_j)-c_j\cdot \mathsf{pk})=\sum _{j=1}^k{\alpha }_j\cdot w_j$$

This aggregated check is faster than checking each equation separately. A failure requires checking signatures individually to identify the invalid ones.

Phase-Restricted Signature Extraction

Signatures can only be extracted from the done phase. Earlier phases cannot produce signatures by construction.

def extractSignature (S : Scheme) : State S .done → Signature S
  | ⟨sig⟩ => sig

For threshold-aware extraction with context:

structure DoneWithCtx (S : Scheme) :=
  (ctx : ThresholdCtx S)
  (sig : Signature S)

def extractSignatureWithCtx (S : Scheme) : DoneWithCtx S → Signature S
  | ⟨_, sig⟩ => sig

This phase-based discipline ensures signatures are only produced after complete protocol execution.

Correctness Theorems

The Lean implementation provides formal correctness proofs in Proofs/Correctness/Correctness.lean.

Generic Happy-Path Correctness

theorem verify_happy_generic
    (S : Scheme) [DecidableEq S.PartyId]
    (pk : S.Public)
    (m : S.Message)
    (Sset : List S.PartyId)
    (commits : List (SignCommitMsg S))
    (reveals : List (SignRevealWMsg S))
    (shares  : List (SignShareMsg S))
    (hvalid : ValidSignTranscript S Sset commits reveals shares) :
  let w := reveals.foldl (fun acc r => acc + r.w_i) (0 : S.Public)
  let c := S.hash m pk Sset (commits.map (·.commitW)) w
  verify S pk m (aggregateSignature S c Sset (commits.map (·.commitW)) shares)

Lattice Scheme Correctness

theorem verify_happy_lattice
    (pk : latticeScheme.Public)
    (m : latticeScheme.Message)
    (Sset : List latticeScheme.PartyId)
    (commits : List (SignCommitMsg latticeScheme))
    (reveals : List (SignRevealWMsg latticeScheme))
    (shares  : List (SignShareMsg latticeScheme))
    (hvalid : ValidSignTranscript latticeScheme Sset commits reveals shares) :
  let w := reveals.foldl (fun acc r => acc + r.w_i) (0 : latticeScheme.Public)
  let c := latticeScheme.hash m pk Sset (commits.map (·.commitW)) w
  verify latticeScheme pk m (aggregateSignature latticeScheme c Sset (commits.map (·.commitW)) shares)

Core Linearity Lemma

These lemmas are in Proofs/Core/ListLemmas.lean:

lemma sum_zipWith_add_smul
    {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
    (c : R) (ys sks : List M) (hlen : ys.length = sks.length) :
    (zipWith (fun y s => y + c • s) ys sks).sum = ys.sum + c • sks.sum

Soundness

Verification is sound under the security assumptions. If the hash function behaves as a random oracle an adversary cannot produce a valid signature without knowing the secret shares.

The binding property of commitments prevents an adversary from adaptively choosing nonces. The norm check prevents signatures with excessive response norms.

Special Soundness

The core security property is special soundness: two valid signatures with the same nonce but different challenges reveal the secret key.

Given two valid signature equations with the same nonce $w$ but different challenges:

• $A(z_1)=w+c_1\cdot \mathsf{pk}$
• $A(z_2)=w+c_2\cdot \mathsf{pk}$

We can derive: $A(z_1-z_2)=(c_1-c_2)\cdot \mathsf{pk}$

If $c_1\ne c_2$ and we're in a field, this reveals $\mathsf{sk}$ such that $\mathsf{pk}=A(\mathsf{sk})$:

$$\mathsf{sk}=(c_1-c_2{)}^{-1}\cdot (z_1-z_2)$$

This property explains:

1. Why nonce reuse is catastrophic - the secret key can be algebraically recovered
2. The basis for the Fiat-Shamir security proof - a simulator can rewind a forger to extract two transcripts
3. The core of the SIS reduction - extracted differences are short vectors in ker(A)

theorem special_soundness_algebraic
    {M : Type*} [AddCommGroup M]
    {R : Type*} [Ring R] [Module R M]
    (A : M →ₗ[R] M) (z₁ z₂ w pk : M) (c₁ c₂ : R)
    (hv1 : A z₁ = w + c₁ • pk)
    (hv2 : A z₂ = w + c₂ • pk) :
    A (z₁ - z₂) = (c₁ - c₂) • pk

theorem nonce_reuse_key_recovery
    {F : Type*} [Field F]
    {M : Type*} [AddCommGroup M] [Module F M]
    (z₁ z₂ sk : M) (c₁ c₂ : F)
    (hne : c₁ ≠ c₂)
    (heq : z₁ - z₂ = (c₁ - c₂) • sk) :
    sk = (c₁ - c₂)⁻¹ • (z₁ - z₂)

Unforgeability Reduction to SIS

Signature unforgeability reduces to the Short Integer Solution problem via special soundness.

Reduction outline:

1. Challenger generates SIS instance: matrix $A$, wants short $z$ with $Az=0$
2. Embed $A$ as the public key: $\mathsf{pk}=A$ (viewing pk as derived from A)
3. Simulate signing oracle using random oracle programming
4. When forger outputs $(m^{\ast },{\sigma }^{\ast })$, rewind to get second signature with same $w$
5. Use special soundness to extract difference $z_1-z_2$
6. This difference is a short vector in ker(A) → SIS solution

Tightness: The reduction loses a factor of $Q_h$ (hash queries) from rewinding.

structure EUFCMAtoSIS (S : Scheme) (p : SISParams) where
  forgerAdvantage : Real
  signingQueries : Nat
  hashQueries : Nat
  sisAdvantage : Real
  reduction_bound : sisAdvantage ≥ forgerAdvantage / hashQueries

Threshold Response Independence

For threshold signatures, response independence holds for the aggregated response. If each party's response $z_i$ is independent of their share $s_i$ (by local rejection sampling), then the aggregate $z=\sum z_i$ is independent of the master secret $s=\sum s_i$.

Composition argument:

1. Each $z_i=y_i+c\cdot s_i$ where $y_i$ is the party's nonce
2. Local rejection sampling ensures $z_i$ is statistically independent of $s_i$
3. By linearity: $z=\sum z_i=\sum y_i+c\cdot \sum s_i=y+c\cdot s$
4. Since each $z_i$ reveals nothing about $s_i$, and parties don't see each other's $s_i$, the aggregate reveals nothing about $s$

This standard composition follows from Lyubashevsky's "Fiat-Shamir with Aborts" applied to each party individually.

Reference: Lyubashevsky, "Fiat-Shamir with Aborts", ASIACRYPT 2009.

Axiom Index

All axioms used throughout the codebase are documented in Proofs/Core/Assumptions.lean. They fall into three categories:

1. Mathlib-equivalent: Properties provable with Mathlib but requiring significant integration work (e.g., coeffs_sum_to_one for Lagrange interpolation)

2. Cryptographic assumptions: Properties requiring computational hardness assumptions (e.g., vss_hiding, SISHard, MLWEHard)

3. Implementation details: Properties about data structures requiring extensive formalization (e.g., MsgMap.merge_idem)

Each axiom includes a justification and literature reference. See Proofs/Core/Assumptions.lean for the complete index.

Security Assumptions Structure

structure Assumptions (S : Scheme) where
  hashRO            : Prop                    -- hash modeled as QROM (Fiat-Shamir)
  commitCR          : Prop                    -- commitment collision resistant (implies binding)
  hashBinding       : HashBinding             -- binding for hash-based commitment
  commitHiding      : HidingAssumption S      -- commitment hiding (requires ROM; NOT formally proven)
  normLeakageBound  : Prop                    -- norm bounds prevent leakage
  corruptionBound   : Nat                     -- max corrupted parties < threshold
  sisParams         : Option SISParams        -- SIS parameters for unforgeability
  mlweParams        : Option MLWEParams       -- MLWE parameters for key secrecy

def thresholdUFcma (S : Scheme) (A : Assumptions S) : Prop :=
  A.hashRO ∧ A.commitCR ∧ A.normLeakageBound

Collision Resistance and Hiding

Hash-based commitments derive their properties from the underlying hash function:

-- Collision resistance: finding x₁ ≠ x₂ with H(x₁) = H(x₂) is hard
structure CollisionResistant (H : α → β) : Prop where
  no_collisions : True  -- axiomatized

-- Hiding: commitments reveal nothing about the value (requires ROM)
structure HidingAssumption (S : Scheme) : Prop where
  hiding : True  -- axiomatized; NOT provable without probabilistic reasoning

Important: Hiding is NOT formally proven in Lean. It requires probabilistic reasoning that Lean cannot express. Protocols needing hiding must explicitly include this assumption.

Lattice Hardness Assumptions

Security reduces to standard lattice problems:

Short Integer Solution (SIS)

Given $A\in {\mathbb{Z}}_q^{n\times m}$, find short $z$ with $Az=0\mathrm{mod}q$.

structure SISParams where
  n : Nat              -- lattice dimension (rows of A)
  m : Nat              -- columns of A
  q : Nat              -- modulus
  beta : Nat           -- solution norm bound
  m_large : m > n * Nat.log2 q := by decide  -- security requirement

structure SISInstance (p : SISParams) where
  A : Fin p.n → Fin p.m → ZMod p.q   -- public matrix

structure SISSolution (p : SISParams) (inst : SISInstance p) where
  z : Fin p.m → Int
  z_short : ∀ i, Int.natAbs (z i) ≤ p.beta
  z_nonzero : ∃ i, z i ≠ 0
  Az_zero : ∀ i : Fin p.n,
    (Finset.univ.sum fun j => inst.A i j * (z j : ZMod p.q)) = 0

def SISHard (p : SISParams) : Prop := True  -- axiomatized

Reduction: A forger that produces valid signatures can be used to solve SIS.

Module Learning With Errors (MLWE)

Distinguish $(A,As+e)$ from $(A,u)$ where $s,e$ are small.

structure MLWEParams where
  n : Nat    -- ring dimension (degree of R_q = Z_q[X]/(X^n + 1))
  k : Nat    -- module rank (number of ring elements in secret)
  q : Nat    -- modulus
  eta : Nat  -- error distribution parameter

structure MLWEInstance (p : MLWEParams) where
  A : Fin p.k → Fin p.k → (Fin p.n → ZMod p.q)  -- public matrix
  b : Fin p.k → (Fin p.n → ZMod p.q)            -- public vector b = As + e

structure MLWESecret (p : MLWEParams) where
  s : Fin p.k → (Fin p.n → Int)                 -- secret vector
  e : Fin p.k → (Fin p.n → Int)                 -- error vector
  s_short : ∀ i j, Int.natAbs (s i j) ≤ p.eta
  e_short : ∀ i j, Int.natAbs (e i j) ≤ p.eta

def MLWEHard (p : MLWEParams) : Prop := True  -- axiomatized

Reduction: Recovering the secret key from the public key requires solving MLWE.

Full Lattice Assumptions

structure LatticeAssumptions (S : Scheme) extends Assumptions S where
  sisInst   : SISParams           -- SIS instance derived from scheme
  mlweInst  : MLWEParams          -- MLWE instance derived from scheme
  sis_hard  : SISHard sisInst     -- SIS is hard for these parameters
  mlwe_hard : MLWEHard mlweInst   -- MLWE is hard for these parameters

def keySecrecy (S : Scheme) (A : LatticeAssumptions S) : Prop :=
  A.mlwe_hard

def livenessOrAbort (S : Scheme) (A : Assumptions S) : Prop := True

Parameter Validation

Lightweight checks catch obviously insecure parameters. These are necessary conditions, not sufficient for security - real analysis requires the lattice estimator.

def minSecureDimension : Nat := 256

def SISParams.isSecure (p : SISParams) : Prop :=
  p.n ≥ minSecureDimension ∧
  p.m ≥ 2 * p.n ∧
  p.beta < p.q / 2

def MLWEParams.isSecure (p : MLWEParams) : Prop :=
  p.n ≥ minSecureDimension ∧
  p.k ≥ 1 ∧
  p.eta ≤ 4

def isPowerOf2 (n : Nat) : Bool :=
  n > 0 && (n &&& (n - 1)) = 0

The implementation uses standard NIST FIPS 204 (ML-DSA/Dilithium) parameter sets which provide 128, 192, and 256 bits of security.

Batch Verification Implementation

This section provides implementation guidance for batch verification in Rust.

Mathematical Foundation

For $k$ signatures with random weights ${\alpha }_1,\dots ,{\alpha }_k$, batch verification checks:

$$\sum _{j=1}^k{\alpha }_j\cdot (A(z_j)-c_j\cdot {\mathsf{pk}}_j)=\sum _{j=1}^k{\alpha }_j\cdot w_j$$

This can be rewritten as a single multiscalar multiplication:

$$\sum _{j=1}^k{\alpha }_j\cdot A(z_j)-\sum _{j=1}^k{\alpha }_j{c}_j\cdot {\mathsf{pk}}_j=\sum _{j=1}^k{\alpha }_j\cdot w_j$$

When using the same public key for all signatures:

$$A\left(\sum _{j=1}^k{\alpha }_j{z}_j\right)-\left(\sum _{j=1}^k{\alpha }_j{c}_j\right)\cdot \mathsf{pk}=\sum _{j=1}^k{\alpha }_j\cdot w_j$$

Security Requirements

Random weights prevent an adversary from constructing signatures that cancel each other out. With 128-bit random weights, the probability of a forgery passing batch verification is negligible ($2^{-128}$).

• Weights MUST be cryptographically random (CSPRNG)
• Weights MUST be at least 128 bits for security
• Weights MUST be generated fresh for each batch verification

Rust Data Structures

#![allow(unused)]
fn main() {
/// Entry for batch verification
pub struct BatchEntry<S: Scheme> {
    pub message: S::Message,
    pub signature: Signature<S>,
    pub public_key: S::Public,
}

/// Batch verification context
pub struct BatchContext<S: Scheme> {
    entries: Vec<BatchEntry<S>>,
}

/// Batch verification result
pub enum BatchResult {
    /// All signatures verified
    AllValid,
    /// Batch failed - need individual verification
    BatchFailed,
    /// Individual failures identified
    Failures(Vec<usize>),
}
}

Batch Verification Algorithm

#![allow(unused)]
fn main() {
impl<S: Scheme> BatchContext<S> {
    pub fn verify(&self, rng: &mut impl CryptoRng) -> BatchResult {
        if self.entries.len() < 2 {
            // For single entry, verify individually
            return self.verify_individual();
        }

        // Generate random 128-bit weights
        let weights: Vec<S::Scalar> = self.entries
            .iter()
            .map(|_| S::Scalar::random_128bit(rng))
            .collect();

        // Compute LHS: Σ αⱼ·A(zⱼ) - Σ αⱼcⱼ·pkⱼ
        let mut lhs = S::Public::zero();
        for (entry, weight) in self.entries.iter().zip(&weights) {
            let az = S::A(&entry.signature.z);
            let c_pk = entry.signature.c * entry.public_key;
            lhs += weight * (az - c_pk);
        }

        // Compute RHS: Σ αⱼ·wⱼ
        let mut rhs = S::Public::zero();
        for (entry, weight) in self.entries.iter().zip(&weights) {
            let w = recover_nonce(&entry.signature, &entry.public_key);
            rhs += weight * w;
        }

        // Check equation
        if lhs == rhs {
            BatchResult::AllValid
        } else {
            // Fall back to individual verification
            self.identify_failures()
        }
    }

    fn identify_failures(&self) -> BatchResult {
        let failures: Vec<usize> = self.entries
            .iter()
            .enumerate()
            .filter(|(_, e)| !verify_single(e))
            .map(|(i, _)| i)
            .collect();

        if failures.is_empty() {
            // Rare case: batch failed but all individual pass
            // Could indicate implementation bug
            BatchResult::AllValid
        } else {
            BatchResult::Failures(failures)
        }
    }
}
}

Performance Optimizations

Single Multiscalar Multiplication

For best performance, use a single multiscalar multiplication (MSM) operation:

#![allow(unused)]
fn main() {
// Instead of computing each term separately:
// for each j: lhs += weight[j] * (A(z[j]) - c[j] * pk[j])

// Collect all scalars and points:
let scalars: Vec<Scalar> = /* ... */;
let points: Vec<Point> = /* ... */;

// Single MSM operation
let result = multiscalar_mul(&scalars, &points);
}

Libraries like curve25519-dalek or arkworks provide efficient MSM implementations.

Same Public Key Optimization

When all signatures use the same public key:

#![allow(unused)]
fn main() {
// Combine challenge terms
let combined_challenge: Scalar = weights
    .iter()
    .zip(&challenges)
    .map(|(w, c)| w * c)
    .sum();

// Single public key multiplication
let pk_term = combined_challenge * public_key;
}

Performance Expectations

Estimates based on typical lattice signature verification. Actual performance depends on implementation.

Error Handling Strategies

When batch verification fails:

1. Binary search (optional): Split batch in half, verify each half. Repeat to narrow down failures. Complexity: O(log n) batch verifications.

2. Full fallback: Verify all signatures individually. Complexity: O(n) individual verifications.

Choose based on expected failure rate:

• Low failure rate: Binary search is faster
• High failure rate: Full fallback is simpler

Benchmarking

#![allow(unused)]
fn main() {
#[bench]
fn bench_batch_verification(b: &mut Bencher) {
    let entries = generate_valid_entries(100);
    let mut rng = OsRng;

    b.iter(|| {
        let ctx = BatchContext::new(entries.clone());
        ctx.verify(&mut rng)
    });
}
}

References

• Bellare, Garay, Rabin. "Fast Batch Verification for Modular Exponentiation and Digital Signatures" (EUROCRYPT 1998)
• FROST RFC Section 5.3: Batch Verification
• dalek-cryptography/bulletproofs: Efficient MSM implementations

Extensions

The core protocol supports several extensions. These extensions address operational requirements beyond basic signing. They enable share management and enhanced privacy. All extension state structures form semilattices that merge via join.

Error Handling

The Protocol/Core/Error.lean module provides unified error handling patterns across the protocol.

BlameableError Typeclass

Errors that can identify a misbehaving party implement the BlameableError typeclass:

class BlameableError (E : Type*) (PartyId : Type*) where
  blamedParty : E → Option PartyId

instance : BlameableError (DkgError PartyId) PartyId where
  blamedParty
    | .lengthMismatch => none
    | .duplicatePids => none
    | .commitMismatch p => some p

instance : BlameableError (Complaint PartyId) PartyId where
  blamedParty c := some c.accused

instance : BlameableError (VSS.VSSError PartyId) PartyId where
  blamedParty
    | .shareVerificationFailed accused _ => some accused
    | .missingCommitment p => some p
    | .missingShare from _ => some from
    | .thresholdMismatch _ _ => none
    | .duplicateDealer p => some p

Cheater Detection Modes

Following FROST, we provide configurable cheater detection:

inductive CheaterDetectionMode
  | disabled      -- No blame tracking (best performance)
  | firstCheater  -- Stop after finding one cheater (good balance)
  | allCheaters   -- Exhaustively identify all cheaters (complete but slower)

structure ProtocolConfig where
  cheaterDetection : CheaterDetectionMode := .firstCheater
  maxErrors : Nat := 0  -- 0 = unlimited

def ProtocolConfig.default : ProtocolConfig
def ProtocolConfig.highSecurity : ProtocolConfig   -- allCheaters mode
def ProtocolConfig.performance : ProtocolConfig    -- disabled mode

Error Aggregation

Utilities for collecting and analyzing errors across protocol execution:

/-- Count how many errors blame a specific party -/
def countBlame (errors : List E) (party : PartyId) : Nat

/-- Get all unique blamed parties from a list of errors -/
def allBlamedParties (errors : List E) : List PartyId

/-- Collect blame respecting detection mode -/
def collectBlame (config : ProtocolConfig) (errors : List E) : BlameResult PartyId

Error Categories

Session Abort Coordination

The Protocol/Core/Abort.lean module provides abort coordination for session-level failures that cannot be handled locally. Unlike local rejection sampling which handles norm bounds within a single signer, aborts require distributed consensus to abandon a session.

When Aborts Are Needed

Session aborts handle failures that affect the entire signing session.

Liveness failures occur when parties are offline or unresponsive. These require f+1 votes to confirm the abort. Examples include session timeout with insufficient responses and specific parties detected as unresponsive.

Security violations trigger immediate abort without voting. These indicate the protocol cannot safely continue. Examples include trust violations where more than n-t parties are faulty, aggregate signatures exceeding bounds despite local rejection, and DKG/VSS with too many complaints.

Explicit cancellation occurs when a party requests abort. This also requires f+1 votes to confirm.

Abort Reasons

The AbortReason type categorizes why a session needs to abort.

inductive AbortReason (PartyId : Type*) where
  -- Liveness failures (require f+1 votes)
  | timeout (respondents : Nat) (required : Nat)
  | insufficientParticipants (actual : Nat) (required : Nat)
  | partyUnresponsive (parties : List PartyId)

  -- Security violations (immediate abort)
  | trustViolation (faultyCount : Nat) (maxTolerable : Nat)
  | globalNormExceeded (aggregateNorm : Nat) (bound : Nat)
  | tooManyComplaints (complaints : Nat) (maxTolerable : Nat)

  -- Explicit request (requires f+1 votes)
  | requestedBy (requester : PartyId)

The isImmediate method returns true for security violations that bypass voting. The isSecurityViolation method distinguishes security issues from liveness issues.

Abort State (CRDT)

Abort state forms a CRDT for distributed coordination.

structure AbortState (S : Scheme) where
  session : Nat
  votes : Finset S.PartyId
  reasons : List (AbortReason S.PartyId)
  immediateTriggered : Bool := false

The CRDT merge unions the vote sets, concatenates reasons with deduplication, and ORs the immediate flag. This allows replicas to merge abort proposals from different parties in any order.

Abort Threshold

The abort threshold is f+1 where f = n - t is the maximum faulty parties. This ensures at least one honest party agreed to abort.

def AbortState.shouldAbort (state : AbortState S) (cfg : ThresholdConfig) : Bool :=
  state.hasImmediateReason || state.isConfirmedByVotes cfg

A session aborts when either an immediate reason was triggered or f+1 parties voted. The +1 prevents a coalition of f malicious parties from forcing spurious aborts.

Abort Messages

Parties propose aborts by broadcasting AbortMsg messages.

structure AbortMsg (S : Scheme) where
  sender : S.PartyId
  session : Nat
  reason : AbortReason S.PartyId
  evidence : List S.PartyId := []

Convenience constructors create messages for common scenarios. The AbortMsg.timeout constructor creates timeout messages. The AbortMsg.unresponsive constructor identifies specific unresponsive parties. The AbortMsg.trustViolation constructor reports security violations.

Processing Abort Messages

The AbortState.processMsg method updates state when receiving an abort message.

def AbortState.processMsg (state : AbortState S) (msg : AbortMsg S) : AbortState S :=
  if msg.session = state.session then
    Join.join state (AbortState.fromMsg msg)
  else
    state  -- Ignore messages for different sessions

Messages for different sessions are ignored. Messages for the current session are merged into the CRDT state.

Relationship to Local Rejection

Local rejection and session aborts serve different purposes.

Local rejection handles per-party issues within a signing attempt. Each party independently retries until finding a valid response. Session aborts handle failures that require distributed coordination to resolve.

Security Markers

The Protocol/Core/Security.lean module provides typeclass markers for implementation security requirements. These markers document FFI implementation obligations.

Zeroizable Typeclass

Marks types containing secret material that must be securely erased from memory after use.

class Zeroizable (α : Type*) where
  needsZeroization : Bool := true

instance : Zeroizable (SecretBox α)
instance : Zeroizable (LinearMask S)
instance : Zeroizable (LinearDelta S)
instance : Zeroizable (LinearOpening S)

Implementation guidance:

ConstantTimeEq Typeclass

Marks types requiring constant-time equality comparison to prevent timing side-channels.

class ConstantTimeEq (α : Type*) where
  requiresConstantTime : Bool := true

instance : ConstantTimeEq (SecretBox α)
instance : ConstantTimeEq (LinearMask S)
instance : ConstantTimeEq (LinearDelta S)

Implementation guidance:

• Use subtle::ConstantTimeEq in Rust
• Use CRYPTO_memcmp() from OpenSSL
• Never use early-exit comparison loops
• Avoid branching on secret-dependent values

Linear Security Wrappers

The protocol uses linear-style type discipline to prevent misuse of single-use sensitive values. Private constructors and module-scoped access make violations visible.

LinearMask

Refresh masks that must be applied exactly once to preserve the zero-sum invariant.

structure LinearMask (S : Scheme) where
  private mk ::
  private partyId : S.PartyId
  private maskValue : S.Secret
  private publicImage : S.Public

def LinearMask.create (S : Scheme) (pid : S.PartyId) (mask : S.Secret) : LinearMask S
def LinearMask.consume (m : LinearMask S) : S.Secret × MaskConsumed S

Security: If a mask is applied twice or not at all, the sum of masks will not be zero and the global secret changes.

LinearDelta

Repair contributions that must be aggregated exactly once.

structure LinearDelta (S : Scheme) where
  private mk ::
  private senderId : S.PartyId
  private targetId : S.PartyId
  private deltaValue : S.Secret

def LinearDelta.create (S : Scheme) (sender target : S.PartyId) (delta : S.Secret) : LinearDelta S
def LinearDelta.consume (d : LinearDelta S) : S.Secret × DeltaConsumed S

Security: Using a delta twice adds its value twice to the reconstruction sum, corrupting the repaired share.

LinearOpening

Commitment randomness that should be used exactly once to prevent equivocation.

structure LinearOpening (S : Scheme) where
  private mk ::
  private openingValue : S.Opening
  private used : Bool := false

def LinearOpening.fresh (S : Scheme) (opening : S.Opening) : LinearOpening S
def LinearOpening.consume (o : LinearOpening S) : S.Opening × OpeningConsumed S

Security: Reusing an opening with different values could allow opening the same commitment to different values.

Consumption Proofs

Each linear type produces a consumption proof when consumed:

structure MaskConsumed (S : Scheme) where
  private mk ::
  forParty : S.PartyId

structure DeltaConsumed (S : Scheme) where
  private mk ::
  fromHelper : S.PartyId

structure OpeningConsumed (S : Scheme) where
  private mk ::
  consumed : Unit := ()

Downstream functions can require these proofs to ensure proper consumption occurred.

Reusable Protocol Patterns

The Protocol/Core/Patterns.lean module provides reusable abstractions for common protocol patterns. Scheme-specific versions are re-exported from Protocol/Core/Core.lean.

Constraint Aliases

Standard constraint combinations are aliased for cleaner signatures. Generic versions in Patterns.lean work with any type, while Core.lean provides Scheme-specific aliases:

-- Generic (Patterns.lean):
abbrev HashConstraints (PartyId : Type*) := BEq PartyId × Hashable PartyId
abbrev StateConstraints (PartyId : Type*) := HashConstraints PartyId × DecidableEq PartyId
abbrev FieldConstraints (Scalar : Type*) := Field Scalar × DecidableEq Scalar

-- Scheme-specific (Core.lean):
abbrev PartyIdHash (S : Scheme) := BEq S.PartyId × Hashable S.PartyId
abbrev PartyIdState (S : Scheme) := PartyIdHash S × DecidableEq S.PartyId
abbrev ScalarField (S : Scheme) := Field S.Scalar × DecidableEq S.Scalar

Usage:

-- Before (verbose):
def foo (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId] [DecidableEq S.PartyId] ...

-- After (concise):
def foo (S : Scheme) [PartyIdState S] ...

Generic Share Verification

The pattern A(secret) = expectedPublic is centralized:

def verifySecretPublic (S : Scheme) (secret : S.Secret) (expectedPublic : S.Public) : Prop :=
  S.A secret = expectedPublic

def verifySecretPublicBool (S : Scheme) [DecidableEq S.Public]
    (secret : S.Secret) (expectedPublic : S.Public) : Bool :=
  S.A secret = expectedPublic

def verifyCommitmentOpening (S : Scheme) [DecidableEq S.Commitment]
    (value : S.Public) (opening : S.Opening) (expectedCommit : S.Commitment) : Bool :=
  S.commit value opening = expectedCommit

Used consistently across:

• VSS share verification
• Repair share reconstruction
• Refresh share updates
• DKG public key verification

Commit-Reveal Framework

Generic types for commit-reveal protocol phases (in Patterns.lean):

/-- Generic validation error -/
inductive CommitRevealError (PhaseType PartyId : Type*)
  | wrongPhase (current : PhaseType)
  | senderNotAuthorized (sender : PartyId)
  | duplicateMessage (sender : PartyId)
  | commitmentMismatch (sender : PartyId)
  | missingCommit (sender : PartyId)
  | verificationFailed (sender : PartyId) (reason : String)

/-- Typeclass for messages with sender -/
class HasSender (M : Type*) (PartyId : Type*) where
  sender : M → PartyId

def getSender [HasSender M PartyId] (m : M) : PartyId := HasSender.sender m

Scheme-specific verification (in Core.lean):

/-- Typeclass for verifiable commit-reveal pairs -/
class CommitVerifiable (CommitMsg RevealMsg : Type*) (S : Scheme) where
  verifyOpening : S → CommitMsg → RevealMsg → Bool

Utility Functions

These utilities are in Patterns.lean:

/-- Check party authorization -/
def isAuthorized (authorizedParties : List PartyId) (party : PartyId) : Bool

/-- Extract unique values by key (replaces map+dedup pattern) -/
def extractUnique (key : α → β) (items : List α) : List β

External Protocol Integration

The Protocol/Core/Core.lean and Protocol/Sign/Types.lean modules provide integration points for external consensus and coordination protocols.

External Context

All signing messages can carry optional context for binding to external protocol instances:

structure ExternalContext where
  consensusId : Option ByteArray := none    -- external session identifier
  resultId : Option ByteArray := none       -- what is being signed (e.g., H(op, prestate))
  prestateHash : Option ByteArray := none   -- state validation
  evidenceDelta : Option ByteArray := none  -- CRDT evidence for propagation

Evidence Carrier Typeclass

The EvidenceCarrier typeclass enables piggybacking CRDT evidence deltas on signing messages:

class EvidenceCarrier (M : Type*) where
  attachEvidence : M → ByteArray → M
  extractEvidence : M → Option ByteArray
  hasEvidence : M → Bool := fun m => (extractEvidence m).isSome

Instances are provided for all signing message types (SignCommitMsg, SignRevealWMsg, SignShareMsg) and Signature.

Self-Validating Shares

For gossip-based fallback protocols, ValidatableShare bundles a share with enough context for independent validation:

structure ValidatableShare (S : Scheme) where
  share : SignShareMsg S
  nonceCommit : S.Commitment
  publicHiding : S.Public
  publicBinding : S.Public
  pkShare : S.Public

Recipients can validate the share without full session state using ValidatableShare.isWellFormed.

Context-Aware Aggregation

When aggregating shares from multiple parties, context consistency can be validated:

def aggregateWithContextValidation (S : Scheme) (c : S.Challenge)
    (Sset : List S.PartyId) (commits : List S.Commitment)
    (shares : List (SignShareMsg S))
    : Except String (Signature S)

This catches Byzantine behavior where a party signs different operations.

See Protocol Integration for detailed usage patterns.

Serialization

The Protocol/Core/Serialize.lean module provides type-safe serialization for network transport.

Serialization Headers

Messages include headers for version and scheme identification:

inductive SchemeId
  | mlDsa44 | mlDsa65 | mlDsa87 | custom (id : ByteArray)

structure SerializationHeader where
  version : UInt8       -- protocol version (currently 1)
  schemeId : SchemeId   -- parameter set identifier

class SerializableWithHeader (α : Type*) extends Serializable α where
  header : SerializationHeader
  toBytesWithHeader : α → ByteArray
  fromBytesWithHeader : ByteArray → Option α

This enables:

• Version negotiation: Detect incompatible protocol versions
• Parameter validation: Verify scheme compatibility before deserializing
• Safe upgrades: Add new schemes without breaking existing deployments

Serializable Typeclass

class Serializable (α : Type*) where
  toBytes : α → ByteArray
  fromBytes : ByteArray → Option α

Implementations are provided for primitives (Nat, Int, ByteArray), compound types (Option, List), and all protocol messages.

Wire Format

The wire format uses little-endian encoding with explicit length prefixes:

Message Wrapping

Messages are wrapped with type tags for network transport:

inductive MessageTag
  | dkgCommit | dkgReveal
  | signCommit | signReveal | signShare
  | signature
  | abort

structure WrappedMessage where
  tag : MessageTag
  payload : ByteArray

def WrappedMessage.toBytes (msg : WrappedMessage) : ByteArray :=
  -- tag (1 byte) + length (4 bytes) + payload

Security Note: Deserialization is a potential attack surface. All fromBytes implementations validate input lengths and return none on malformed input.

Complaints

The complaint mechanism identifies misbehaving parties. It activates when protocol invariants are violated.

Complaint Types

Two complaint variants cover the main failure modes.

inductive Complaint (PartyId : Type) where
  | openingMismatch (accused : PartyId)
  | missingReveal (accused : PartyId)

Complaint Triggers

A party files a complaint under the following conditions.

Invalid commitment opening. Party $P_j$ reveals a pair $({\mathsf{pk}}_j,r_j)$ that does not match its commitment ${\mathsf{Com}}_j$. Generates openingMismatch.

Missing message. Party $P_j$ fails to send a required message within the timeout. Generates missingReveal.

Inconsistent session. The participant set $S$ differs from the expected set.

Invalid partial signature. Party $P_j$ produces a partial signature $z_j$ that fails verification.

Aggregation with Complaints

DKG aggregation returns either the public key or a list of complaints identifying misbehaving parties.

def dkgAggregateWithComplaints
  (S : Scheme) [DecidableEq S.PartyId]
  (commits : List (DkgCommitMsg S))
  (reveals : List (DkgRevealMsg S))
  : Except (List (Complaint S.PartyId)) S.Public

Complaint Resolution

When a party files a complaint the protocol may proceed in different ways.

Abort. All parties discard the current session. They may retry with a new session excluding the accused party.

Exclude. The accused party is removed from the participant set. The remaining parties continue if the threshold is still met.

Penalize. In applications with economic stakes the accused party may lose a deposit or face other penalties.

Complaint Verification

A complaint is verifiable when it includes evidence. For a commitment opening failure the evidence is the commitment, the revealed pair, and a proof that they do not match. Other parties can independently verify the complaint.

Handling Byzantine Signers

In threshold signing, Byzantine signers may attempt to disrupt the protocol by sending invalid partial signatures. The protocol handles such behavior through per-share validation, allowing honest parties to detect and exclude misbehavior without halting progress.

Per-Share Validation

The aggregator treats each partial signature as an independent object. For each partial ${\sigma }_i$ from signer $i$, the aggregator performs three validation checks.

Structural validity checks that the partial is well-formed and consistent with commitments. The partial must have correct dimension, correct modulus, and match the commitment structure.

Norm bound checking verifies $\Vert z_i{\Vert }_{\infty }\le B_{\text{local}}$. This ensures each partial satisfies the local bound that, when combined with other valid partials, produces a globally valid signature.

Algebraic validity verifies the partial against the signer's public share ${\mathsf{pk}}_i$. This is analogous to FROST's per-share verification relation. The partial must satisfy a relation like $A(z_i)=w_{\text{eff}}+c\cdot {\mathsf{pk}}_i$ where $w_{\text{eff}}$ is derived from the commitment.

Invalid Share Handling

If any check fails, the aggregator discards that partial share. The aggregator does not attempt to include that share in the aggregate. Instead, it records evidence of misbehavior. This evidence can support later exclusion decisions or penalties in consensus protocols.

The aggregator then waits for valid shares from other signers, continuing until it has collected $t$ valid partials (where $t\ge 2f+1$ under the BFT assumption).

Byzantine Resilience Guarantee

Because there are at least $2f+1$ honest validators, there exist at least $t$ honest signers whose partials will be valid. The aggregator can always collect $t$ valid partials and complete the signature despite up to $f$ malicious validators.

This ensures that no single participant, nor any coalition of size $\le f$, can prevent the threshold signature from being formed. Malicious signers cannot force global rejection or restart. They can only delay the process by not participating or by sending invalid shares that are simply rejected.

Misbehavior Detection

Per-share validation enables attribution. Each invalid partial can be tied to a specific signer via its ID. This makes misbehavior identifiable and attributable even though the final signature itself remains a standard Dilithium signature under the group key.

The protocol transcript contains all per-signer checks, allowing external auditors to verify which parties sent invalid shares. This supports automated exclusion policies or manual review in consensus systems.

Share Refresh

Share refresh updates the shares without changing the public key. This procedure provides proactive security. Even if an adversary compromises old shares the refreshed shares are independent.

Mask Function Structure

Masks are represented as functions from party identifier to secret.

structure MaskFn (S : Scheme) :=
  (mask : S.PartyId → S.Secret)

instance (S : Scheme) : Join (MaskFn S) :=
  ⟨fun a b => { mask := fun pid => a.mask pid + b.mask pid }⟩

The join merges masks by pointwise addition.

Zero-Sum Mask Invariant

The zero-sum property is captured in a dependent structure.

structure ZeroSumMaskFn (S : Scheme) (active : Finset S.PartyId) :=
  (fn : MaskFn S)
  (sum_zero : (active.toList.map (fun pid => fn.mask pid)).sum = 0)

instance (S : Scheme) (active : Finset S.PartyId) : Join (ZeroSumMaskFn S active)

Merging zero-sum masks preserves zero-sum on the same active set.

Refresh Overview

Each party $P_i$ holds a share $s_i$. After refresh each party holds a new share $s_i^{\prime }=s_i+{\delta }_i$. The masks ${\delta }_i$ sum to zero.

$$\sum _i{\delta }_i=0$$

This ensures the master secret is unchanged.

$$\sum _i{s}_i^{\prime }=\sum _i(s_i+{\delta }_i)=\sum _i{s}_i+\sum _i{\delta }_i=s+0=s$$

Refresh Function

Applies a mask to each share and recomputes the corresponding public share.

def refreshShares
  (S : Scheme)
  (m : MaskFn S)
  (shares : List (KeyShare S)) : List (KeyShare S) :=
  shares.map (fun ks =>
    let sk' := ks.secret + m.mask ks.pid
    let pk' := S.A sk'
    KeyShare.create S ks.pid sk' pk' ks.pk)

Mask Generation

The masks must sum to zero. One approach is as follows.

1. Each party $P_i$ samples a random mask contribution ${\mu }_i\in \mathcal{S}$.
2. Parties run a protocol to compute a common offset $\mu ={\sum }_i{\mu }_i$.
3. Each party sets ${\delta }_i={\mu }_i-\mu /n$ in a way that ensures ${\sum }_i{\delta }_i=0$.

An alternative uses pairwise contributions. Party $P_i$ sends ${\delta }_{ij}$ to party $P_j$ and receives ${\delta }_{ji}$ from $P_j$. The net contribution is ${\delta }_i={\sum }_{j\ne i}({\delta }_{ij}-{\delta }_{ji})$. These contributions cancel pairwise.

Public Share Update

After refresh each party computes its new public share.

$${\mathsf{pk}}_i^{\prime }=A(s_i^{\prime })=A(s_i+{\delta }_i)=A(s_i)+A({\delta }_i)={\mathsf{pk}}_i+A({\delta }_i)$$

The global public key remains unchanged because

$$\sum _i{\mathsf{pk}}_i^{\prime }=\sum _i{\mathsf{pk}}_i+\sum _{i}A({\delta }_i)=\mathsf{pk}+A\left(\sum _i{\delta }_i\right)=\mathsf{pk}+A(0)=\mathsf{pk}$$

Refresh Protocol

A full refresh protocol runs as follows.

1. Each party generates its mask contribution.
2. Parties exchange commitments to their contributions.
3. Parties reveal their contributions.
4. Each party verifies all commitments.
5. Each party computes its new share.
6. Parties publish new commitments to their public shares.
7. External verifiers can check the consistency of the new public shares.

Refresh Coordination Protocol

The Protocol/Shares/RefreshCoord.lean module provides a distributed protocol for generating zero-sum masks without a trusted coordinator.

Phases:

1. Commit: Each party commits to their random mask
2. Reveal: Parties reveal masks after all commits received
3. Adjust: Coordinator computes adjustment to achieve zero-sum
4. Apply: All parties apply masks to their shares

CRDT Design: Uses MsgMap for commits and reveals to ensure at most one message per party. This makes conflicting messages un-expressable at the type level.

abbrev MaskCommitMap (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId] :=
  MsgMap S (MaskCommitMsg S)

abbrev MaskRevealMap (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId] :=
  MsgMap S (MaskRevealMsg S)

structure RefreshRoundState (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId] where
  phase : RefreshPhase
  parties : List S.PartyId
  roundNum : Nat
  coordStrategy : CoordinatorStrategy S.PartyId
  maskCommits : MaskCommitMap S    -- at most one per party
  maskReveals : MaskRevealMap S    -- at most one per party
  adjustment : Option (AdjustmentMsg S)

Commitment Design: The protocol commits to A(mask) (the public image) rather than the mask itself. This enables:

• Public verifiability without revealing the secret mask
• Consistency with DKG (which commits to public shares)
• Simple zero-sum verification via A(Σ m_i)

Architecture: Separated CRDT and Validation

The protocol separates concerns into two layers:

1. CRDT Layer - Pure merge semantics for replication/networking
2. Validation Layer - Conflict detection for auditing/security

-- CRDT merge: idempotent, always succeeds, silently ignores duplicates
def processCommit (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId]
    (st : RefreshRoundState S) (msg : MaskCommitMsg S)
    : RefreshRoundState S

def processReveal (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId]
    (st : RefreshRoundState S) (msg : MaskRevealMsg S)
    : RefreshRoundState S

-- Validation: detect conflicts without modifying state
def detectCommitConflict (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId]
    (st : RefreshRoundState S) (msg : MaskCommitMsg S)
    : Option (MaskCommitMsg S)

def validateCommit (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId]
    (st : RefreshRoundState S) (msg : MaskCommitMsg S)
    : Option (CommitValidationError S)

-- Combined: merge + validation in one call
def processCommitValidated (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId]
    (st : RefreshRoundState S) (msg : MaskCommitMsg S)
    : RefreshRoundState S × Option (CommitValidationError S)

Design Rationale:

• CRDT functions can be used directly for networking without error handling in merge path
• Validation is explicit and composable. Call it when you need it.
• Follows "make illegal states unrepresentable" at CRDT level, "detect suspicious patterns" separately

Coordinator Selection:

inductive CoordinatorStrategy (PartyId : Type*)
  | fixed (pid : PartyId)      -- always same coordinator
  | roundRobin (round : Nat)   -- rotate based on round number
  | random (seed : Nat)        -- pseudo-random selection

Zero-Sum Verification: The coordinator computes adjustment $m_n=-{\sum }_{i\ne n}{m}_i$ ensuring ${\sum }_i{m}_i=0$:

def computeAdjustment (S : Scheme) [BEq S.PartyId] [Hashable S.PartyId]
    [DecidableEq S.PartyId] [Inhabited S.PartyId]
    (st : RefreshRoundState S) : Option S.Secret :=
  if st.phase = .adjust then
    let coord := st.coordinator
    let otherMasks := st.maskReveals.toList.filter (fun r => r.sender ≠ coord)
    let sumOthers := (otherMasks.map (·.mask)).sum
    some (-sumOthers)
  else none

DKG-Based Refresh Protocol

The Protocol/Shares/RefreshDKG.lean module provides a fully distributed refresh protocol without a trusted coordinator. Each party contributes a zero-polynomial (polynomial with constant term 0), ensuring the master secret remains unchanged while all shares are updated.

Three-Round Protocol:

1. Round 1 (Commit): Each party samples a random polynomial $f_i(x)$ with $f_i(0)=0$ and broadcasts a commitment to its polynomial coefficients.

2. Round 2 (Share): Each party evaluates its polynomial at all other parties' identifiers and sends the shares privately.

3. Round 3 (Verify & Apply): Each party verifies received shares against commitments and computes its refresh delta as the sum of all received shares.