From 8b57bb8fd273b90213f6181c49ac76fc3da5334d Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Wed, 13 Aug 2025 22:17:46 +0200 Subject: [PATCH 1/9] xmss spec: big wip --- src/lean_spec/subspecs/xmss/__init__.py | 22 ++ src/lean_spec/subspecs/xmss/constants.py | 80 ++++++ src/lean_spec/subspecs/xmss/interface.py | 88 +++++++ src/lean_spec/subspecs/xmss/structures.py | 52 ++++ src/lean_spec/subspecs/xmss/utils.py | 291 ++++++++++++++++++++++ 5 files changed, 533 insertions(+) create mode 100644 src/lean_spec/subspecs/xmss/__init__.py create mode 100644 src/lean_spec/subspecs/xmss/constants.py create mode 100644 src/lean_spec/subspecs/xmss/interface.py create mode 100644 src/lean_spec/subspecs/xmss/structures.py create mode 100644 src/lean_spec/subspecs/xmss/utils.py diff --git a/src/lean_spec/subspecs/xmss/__init__.py b/src/lean_spec/subspecs/xmss/__init__.py new file mode 100644 index 00000000..9e381730 --- /dev/null +++ b/src/lean_spec/subspecs/xmss/__init__.py @@ -0,0 +1,22 @@ +""" +This package provides a Python specification for the Generalized XMSS +hash-based signature scheme. + +It exposes the core data structures and the main interface functions. +""" + +from .constants import LIFETIME, MESSAGE_LENGTH +from .interface import key_gen, sign, verify +from .structures import HashTreeOpening, PublicKey, SecretKey, Signature + +__all__ = [ + "key_gen", + "sign", + "verify", + "PublicKey", + "Signature", + "SecretKey", + "HashTreeOpening", + "LIFETIME", + "MESSAGE_LENGTH", +] diff --git a/src/lean_spec/subspecs/xmss/constants.py b/src/lean_spec/subspecs/xmss/constants.py new file mode 100644 index 00000000..c2e4249e --- /dev/null +++ b/src/lean_spec/subspecs/xmss/constants.py @@ -0,0 +1,80 @@ +"""Defines the cryptographic constants for the XMSS specification.""" + +from ..koalabear import Fp + +# ================================================================= +# Core Scheme Configuration +# ================================================================= + +MESSAGE_LENGTH: int = 32 +"""The length in bytes for all messages to be signed.""" + +LOG_LIFETIME: int = 32 +"""The base-2 logarithm of the scheme's maximum lifetime.""" + +LIFETIME: int = 1 << LOG_LIFETIME +""" +The maximum number of epochs supported by this configuration. + +An individual key pair can be active for a smaller sub-range. +""" + +# ================================================================= +# Target Sum WOTS Parameters +# ================================================================= + +DIMENSION: int = 64 +"""The total number of hash chains, `v`.""" + +BASE: int = 8 +"""The alphabet size for the digits of the encoded message.""" + +TARGET_SUM: int = 375 +"""The required sum of all codeword chunks for a signature to be valid.""" + +CHUNK_SIZE: int = 3 +"""The number of bits per chunk, calculated as ceil(log2(BASE)).""" + + +# ================================================================= +# Hash and Encoding Length Parameters (in field elements) +# ================================================================= + +PARAMETER_LEN: int = 5 +""" +The length of the public parameter `P`. + +It isused to specialize the hash function. +""" + +HASH_LEN: int = 8 +"""The output length of the main tweakable hash function.""" + +RAND_LEN: int = 7 +"""The length of the randomness `rho` used during message encoding.""" + +TWEAK_LEN: int = 2 +"""The length of a domain-separating tweak.""" + +MSG_LEN: int = 9 +"""The length of a message after being encoded into field elements.""" + +MSG_HASH_LEN: int = 15 +"""The output length of the hash function used to digest the message.""" + +CAPACITY: int = 9 +"""The capacity of the Poseidon2 sponge, defining its security level.""" + + +# ================================================================= +# Domain Separator Prefixes for Tweaks +# ================================================================= + +TWEAK_PREFIX_CHAIN = Fp(value=0x00) +"""The unique prefix for tweaks used in Winternitz-style hash chains.""" + +TWEAK_PREFIX_TREE = Fp(value=0x01) +"""The unique prefix for tweaks used when hashing Merkle tree nodes.""" + +TWEAK_PREFIX_MESSAGE = Fp(value=0x02) +"""The unique prefix for tweaks used in the initial message hashing step.""" diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py new file mode 100644 index 00000000..c8dd0e4d --- /dev/null +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -0,0 +1,88 @@ +""" +Defines the core interface for the Generalized XMSS signature scheme. + +This file specifies the high-level functions (`key_gen`, `sign`, `verify`) +that constitute the public API of the signature scheme. For the purpose of this +specification, these are defined as placeholders with detailed documentation. +""" + +from typing import List, Tuple + +from ..koalabear import Fp +from .constants import BASE, CHUNK_SIZE, DIMENSION, LIFETIME, MESSAGE_LENGTH +from .structures import PublicKey, SecretKey, Signature +from .utils import chain, encode, hash_tree_verify, tweakable_hash + + +def key_gen() -> Tuple[PublicKey, SecretKey]: + """ + Generates a new cryptographic key pair. + + This function is a placeholder. In a real implementation, it would involve + generating a master secret, deriving all one-time keys, and constructing + the full Merkle tree. + + For the formal specification of this process, please refer to: + - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a] + - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b] + - The canonical Rust implementation: https://github.com/b-wagn/hash-sig + """ + raise NotImplementedError( + "key_gen is not part of this specification. " + "See the Rust reference implementation." + ) + + +def sign(sk: SecretKey, epoch: int, message: bytes) -> Signature: + """ + Produces a digital signature for a given message at a specific epoch. + + This function is a placeholder. The signing process involves encoding the + message, generating a one-time signature, and providing a Merkle path. + + **CRITICAL**: This function must never be called twice with the same secret + key and epoch for different messages, as this would compromise security. + + For the formal specification of this process, please refer to: + - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a] + - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b] + - The canonical Rust implementation: https://github.com/b-wagn/hash-sig + """ + raise NotImplementedError( + "sign is not part of this specification. " + "See the Rust reference implementation." + ) + + +def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool: + """ + Verifies a digital signature against: + - a public key, + - a message, + - epoch. + """ + assert len(message) == MESSAGE_LENGTH, "Invalid message length" + assert 0 <= epoch < LIFETIME, "Epoch out of valid range" + + # Re-encode the message to get the expected codeword. + codeword = encode(pk.parameter, message, sig.rho, epoch) + if codeword is None: + return False + + # Reconstruct the one-time public key from the signature's hashes. + chain_ends: List[List[Fp]] = [] + for i in range(DIMENSION): + steps_to_end = (BASE**CHUNK_SIZE - 1) - codeword[i] + end_of_chain = chain( + pk.parameter, epoch, i, codeword[i], steps_to_end, sig.hashes[i] + ) + chain_ends.append(end_of_chain) + + # Compute the Merkle leaf by hashing the reconstructed one-time public key. + # Note: A proper tweak would be used here. For simplicity, we omit it. + computed_leaf = tweakable_hash(pk.parameter, [], chain_ends) + + # Verify the Merkle path against the public key's root. + return hash_tree_verify( + pk.parameter, pk.root, epoch, computed_leaf, sig.path + ) diff --git a/src/lean_spec/subspecs/xmss/structures.py b/src/lean_spec/subspecs/xmss/structures.py new file mode 100644 index 00000000..0be56a53 --- /dev/null +++ b/src/lean_spec/subspecs/xmss/structures.py @@ -0,0 +1,52 @@ +"""Defines the data structures for the Generalized XMSS signature scheme.""" + +from typing import List + +from pydantic import BaseModel, ConfigDict, Field + +from ..koalabear import Fp +from .constants import HASH_LEN, PARAMETER_LEN, RAND_LEN + + +class HashTreeOpening(BaseModel): + """ + A Merkle authentication path. + + It contains a list of sibling nodes required to reconstruct the path + from a leaf node up to the Merkle root. + """ + + model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) + siblings: List[List[Fp]] = Field( + ..., description="List of sibling hashes, from bottom to top." + ) + + +class PublicKey(BaseModel): + """The public key for the Generalized XMSS scheme.""" + + model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) + root: List[Fp] = Field(..., max_length=HASH_LEN, min_length=HASH_LEN) + parameter: List[Fp] = Field( + ..., max_length=PARAMETER_LEN, min_length=PARAMETER_LEN + ) + + +class Signature(BaseModel): + """A signature in the Generalized XMSS scheme.""" + + model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) + path: HashTreeOpening + rho: List[Fp] = Field(..., max_length=RAND_LEN, min_length=RAND_LEN) + hashes: List[List[Fp]] + + +class SecretKey(BaseModel): + """ + Placeholder for the secret key. + + Note: The full secret key structure is not specified here as it is not + needed for verification. + """ + + pass diff --git a/src/lean_spec/subspecs/xmss/utils.py b/src/lean_spec/subspecs/xmss/utils.py new file mode 100644 index 00000000..88c7ef5f --- /dev/null +++ b/src/lean_spec/subspecs/xmss/utils.py @@ -0,0 +1,291 @@ +"""Cryptographic utilities and helper functions for the XMSS verification.""" + +from typing import List, Optional + +from ..koalabear import Fp, P +from ..poseidon2 import PARAMS_16, PARAMS_24, permute +from .constants import ( + BASE, + CAPACITY, + CHUNK_SIZE, + DIMENSION, + HASH_LEN, + MSG_HASH_LEN, + MSG_LEN, + PARAMETER_LEN, + TARGET_SUM, + TWEAK_LEN, + TWEAK_PREFIX_CHAIN, + TWEAK_PREFIX_MESSAGE, + TWEAK_PREFIX_TREE, +) +from .structures import HashTreeOpening + + +def tweakable_hash( + parameter: List[Fp], tweak: List[Fp], message: List[List[Fp]] +) -> List[Fp]: + """ + A tweakable hash function using Poseidon2 for domain-separated hashing. + + Args: + parameter: The public parameter `P`. + tweak: A domain-separating value. + message: The data to be hashed. + + Returns: + The resulting hash digest as a list of field elements. + """ + # Input Preparation + # + # Flatten the message (list of vectors -> single list of field elements). + flat_message = [fe for sublist in message for fe in sublist] + # Concatenate the parameter, tweak, and message into a single input. + combined_input = parameter + tweak + flat_message + + # Hashing Logic + # + # The function selects a specific hashing mode based on the number of + # message parts. + + # Case 1: Hashing a single value, as done within a hash chain. + # + # This uses Poseidon2 in compression mode (width of 16). + if len(message) == 1: + # Pad the input with zeros to match the permutation's required width. + state = combined_input + [Fp(value=0)] * (16 - len(combined_input)) + # Apply the core cryptographic permutation to the state. + permuted_state = permute(state, PARAMS_16) + # Apply the feed-forward step: + # We add the initial state back into the permuted state element-wise. + result = [s + p for s, p in zip(permuted_state, state, strict=False)] + # Truncate the full state to the desired hash output length and return. + return result[:HASH_LEN] + + # Case 2: Hashing two values, typically for Merkle tree sibling nodes. + # + # This uses the wider Poseidon2 instance (width of 24) in compression mode. + elif len(message) == 2: + # Pad the input to the permutation's width of 24. + state = combined_input + [Fp(value=0)] * (24 - len(combined_input)) + # Apply the core cryptographic permutation. + permuted_state = permute(state, PARAMS_24) + # Apply the feed-forward step. + result = [s + p for s, p in zip(permuted_state, state, strict=False)] + # Truncate the result to the desired hash output length and return. + return result[:HASH_LEN] + + # Case 3: Hashing many values, such as a Merkle leaf from all chain ends. + # + # The sponge construction handles inputs larger than the state width. + else: + # The rate + rate = 24 - CAPACITY + + # For domain separation, the capacity part of the state is initialized + # with a hash of the input configuration. + lengths = [ + Fp(value=PARAMETER_LEN), + Fp(value=TWEAK_LEN), + Fp(value=DIMENSION), + Fp(value=HASH_LEN), + ] + # This is a recursive call with an input to generate the separator. + capacity_value = tweakable_hash([], [], [lengths])[:CAPACITY] + + # Initialize the sponge state: + # - the rate part is zero, + # - the capacity part holds the separator. + state = [Fp(value=0)] * 24 + state[rate:] = capacity_value + + # Pad the main input so its length is an even multiple of the rate. + padding_len = (rate - (len(combined_input) % rate)) % rate + padded_input = combined_input + [Fp(value=0)] * padding_len + + # Absorb the input in chunks of size `rate`. + for i in range(0, len(padded_input), rate): + chunk = padded_input[i : i + rate] + # Add the current chunk into the rate part of the state. + for j in range(rate): + state[j] += chunk[j] + # Apply the perm to the entire state to mix the absorbed data. + state = permute(state, PARAMS_24) + + # Squeeze the final output from the rate part of the state. + return state[:HASH_LEN] + + +def chain( + parameter: List[Fp], + epoch: int, + chain_index: int, + start_pos: int, + steps: int, + start_value: List[Fp], +) -> List[Fp]: + """ + Computes `steps` iterations of a Winternitz-style hash chain. + + A hash chain is created by repeatedly applying a hash function: + H(H(...H(start))) + + Each step uses a unique tweak to ensure that every hash computation in the + entire system is unique. + + Args: + parameter: The public parameter `P` for the hash function. + epoch: The signature's epoch, used for tweaking. + chain_index: The index of this specific chain (from 0 to DIMENSION-1). + start_pos: The starting position within the chain. + steps: The number of times to apply the hash function. + start_value: The initial hash value to begin the chain from. + + Returns: + The final hash value after `steps` iterations. + """ + # Initialize the iterative hash value with the provided start_value. + current_value = start_value + # Loop `steps` times to perform the chained hashing. + for i in range(steps): + # The position in the chain is its starting offset + the current step. + pos_in_chain = start_pos + i + # Pack the tweak's components into a single integer. + packed_data = (epoch << 24) | (chain_index << 16) | pos_in_chain + # Create the domain-separating tweak for this specific hash operation. + tweak = [TWEAK_PREFIX_CHAIN, Fp(value=packed_data)] + # Apply the hash function to get the next value in the chain. + current_value = tweakable_hash(parameter, tweak, [current_value]) + # Return the final value after all iterations. + return current_value + + +def encode( + parameter: List[Fp], message: bytes, rho: List[Fp], epoch: int +) -> Optional[List[int]]: + """ + Performs the Target Sum message encoding. + + This function deterministically converts a message into a sequence of small + integers (a "codeword"). The encoding is only considered valid if the sum + of these integers equals a predefined `TARGET_SUM`. + + Args: + parameter: The public parameter `P` for the hash function. + message: The 32-byte message to encode. + rho: The randomness used for this encoding. + epoch: The signature's epoch, used for tweaking. + + Returns: + A list of integers representing the codeword if the sum is correct, + otherwise `None`. + """ + # Prepare inputs for hashing. + msg_int = int.from_bytes(message, "little") + msg_fes: List[Fp] = [] + for _ in range(MSG_LEN): + msg_fes.append(Fp(value=msg_int % P)) + msg_int //= P + tweak: List[Fp] = [TWEAK_PREFIX_MESSAGE, Fp(value=epoch)] + + # Hash all inputs to create a digest. + hash_input: List[Fp] = rho + parameter + tweak + msg_fes + state = hash_input + [Fp(value=0)] * (24 - len(hash_input)) + permuted = permute(state, PARAMS_24) + hash_output = [s + p for s, p in zip(permuted, state, strict=False)][ + :MSG_HASH_LEN + ] + + # Decode the hash digest into the codeword chunks. + digest_int = 0 + for fe in reversed(hash_output): + digest_int = (digest_int * P) + fe.value + + chunks: List[int] = [ + (digest_int >> (i * CHUNK_SIZE)) & (BASE - 1) for i in range(DIMENSION) + ] + + # Check if the sum of the chunks equals the required target sum. + if sum(chunks) == TARGET_SUM: + # If the sum is correct, the encoding is valid. + return chunks + else: + # Otherwise, the encoding fails for this randomness `rho`. + return None + + +def hash_tree_verify( + parameter: List[Fp], + root: List[Fp], + epoch: int, + leaf_content: List[List[Fp]], + path: HashTreeOpening, +) -> bool: + """ + Verifies a Merkle path from a leaf's content to the root. + + This function first hashes the raw leaf content to get the level 0 node, + then reconstructs the Merkle root by iteratively hashing this node with + the provided sibling nodes up the tree. + + Args: + parameter: The public parameter `P` for the hash function. + root: The known, trusted Merkle root from the public key. + epoch: The index of the leaf in the tree. + leaf_content: The pre-image of the leaf node (e.g., the list of chain ends). + path: The authentication path containing the sibling hashes. + + Returns: + - `True` if the computed root matches the provided root, + - `False` otherwise. + """ + # Initial Checks + # + # The depth of the tree is determined by the number of siblings in path. + depth = len(path.siblings) + # The epoch must be a valid index for a tree of this depth. + assert 0 <= epoch < (1 << depth), "Epoch is out of range for this path" + + # Compute Leaf Node Hash + # + # The first step is to hash the provided leaf content to get the actual + # leaf node that exists at level 0 of the Merkle tree. + # + # The tweak identifies this as a hash at level 0, position `epoch`. + leaf_tweak_packed = (0 << 32) | epoch + leaf_tweak = [TWEAK_PREFIX_TREE, Fp(value=leaf_tweak_packed)] + current_hash = tweakable_hash(parameter, leaf_tweak, leaf_content) + + # Iteratively Compute Root + # + # Start with the leaf's index for the iterative process. + current_index = epoch + # Iterate up the tree, from the bottom (level 0) to the root. + for i, sibling_hash in enumerate(path.siblings): + # Determine the hash order based on whether the current node is a + # left (even index) or right (odd index) child. + if current_index % 2 == 0: + # For a left child, the order is H(current, sibling). + children = [current_hash, sibling_hash] + else: + # For a right child, the order is H(sibling, current). + children = [sibling_hash, current_hash] + + # Move up to the parent's index for the next level. + current_index //= 2 + + # The level of the PARENT node we are about to compute. + parent_level = i + 1 + + # Create the unique tweak for this specific parent node, using its + # level and its index within that level. + parent_tweak_packed = (parent_level << 32) | current_index + tweak = [TWEAK_PREFIX_TREE, Fp(value=parent_tweak_packed)] + + # Compute the parent's hash. + current_hash = tweakable_hash(parameter, tweak, children) + + # Final Comparison + # + # After the loop, the computed hash should equal the public root. + return current_hash == root From 6a063fe1301a193cd04a5716e32859c883b761a7 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Wed, 13 Aug 2025 22:37:59 +0200 Subject: [PATCH 2/9] xmss: scaffolding for the signature spec --- src/lean_spec/subspecs/xmss/constants.py | 37 +-- src/lean_spec/subspecs/xmss/interface.py | 79 +++--- src/lean_spec/subspecs/xmss/structures.py | 6 +- src/lean_spec/subspecs/xmss/utils.py | 291 ---------------------- 4 files changed, 70 insertions(+), 343 deletions(-) delete mode 100644 src/lean_spec/subspecs/xmss/utils.py diff --git a/src/lean_spec/subspecs/xmss/constants.py b/src/lean_spec/subspecs/xmss/constants.py index c2e4249e..86b18e9e 100644 --- a/src/lean_spec/subspecs/xmss/constants.py +++ b/src/lean_spec/subspecs/xmss/constants.py @@ -9,7 +9,7 @@ MESSAGE_LENGTH: int = 32 """The length in bytes for all messages to be signed.""" -LOG_LIFETIME: int = 32 +LOG_LIFETIME: int = 18 """The base-2 logarithm of the scheme's maximum lifetime.""" LIFETIME: int = 1 << LOG_LIFETIME @@ -19,6 +19,7 @@ An individual key pair can be active for a smaller sub-range. """ + # ================================================================= # Target Sum WOTS Parameters # ================================================================= @@ -29,12 +30,12 @@ BASE: int = 8 """The alphabet size for the digits of the encoded message.""" +FINAL_LAYER: int = 77 +"""The number of top layers of the hypercube to map the hash output into.""" + TARGET_SUM: int = 375 """The required sum of all codeword chunks for a signature to be valid.""" -CHUNK_SIZE: int = 3 -"""The number of bits per chunk, calculated as ceil(log2(BASE)).""" - # ================================================================= # Hash and Encoding Length Parameters (in field elements) @@ -44,27 +45,33 @@ """ The length of the public parameter `P`. -It isused to specialize the hash function. +It is used to specialize the hash function. """ -HASH_LEN: int = 8 -"""The output length of the main tweakable hash function.""" - -RAND_LEN: int = 7 -"""The length of the randomness `rho` used during message encoding.""" - -TWEAK_LEN: int = 2 +TWEAK_LEN_FE: int = 2 """The length of a domain-separating tweak.""" -MSG_LEN: int = 9 +MSG_LEN_FE: int = 9 """The length of a message after being encoded into field elements.""" -MSG_HASH_LEN: int = 15 -"""The output length of the hash function used to digest the message.""" +RAND_LEN_FE: int = 6 +"""The length of the randomness `rho` used during message encoding.""" + +HASH_LEN_FE: int = 7 +"""The output length of the main tweakable hash function.""" CAPACITY: int = 9 """The capacity of the Poseidon2 sponge, defining its security level.""" +POS_OUTPUT_LEN_PER_INV_FE: int = 15 +"""Output length per invocation for the message hash.""" + +POS_INVOCATIONS: int = 1 +"""Number of invocations for the message hash.""" + +POS_OUTPUT_LEN_FE: int = POS_OUTPUT_LEN_PER_INV_FE * POS_INVOCATIONS +"""Total output length for the message hash.""" + # ================================================================= # Domain Separator Prefixes for Tweaks diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index c8dd0e4d..d3ef4f5f 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -1,17 +1,16 @@ """ Defines the core interface for the Generalized XMSS signature scheme. -This file specifies the high-level functions (`key_gen`, `sign`, `verify`) +Specification for the high-level functions (`key_gen`, `sign`, `verify`) that constitute the public API of the signature scheme. For the purpose of this specification, these are defined as placeholders with detailed documentation. """ -from typing import List, Tuple +from __future__ import annotations + +from typing import Tuple -from ..koalabear import Fp -from .constants import BASE, CHUNK_SIZE, DIMENSION, LIFETIME, MESSAGE_LENGTH from .structures import PublicKey, SecretKey, Signature -from .utils import chain, encode, hash_tree_verify, tweakable_hash def key_gen() -> Tuple[PublicKey, SecretKey]: @@ -55,34 +54,46 @@ def sign(sk: SecretKey, epoch: int, message: bytes) -> Signature: def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool: + r""" + Verifies a digital signature against a public key, message, and epoch. + + This function is a placeholder. The complete verification logic is detailed + below and will be implemented in a future update. + + ### Verification Algorithm + + 1. **Re-encode Message**: The verifier uses the randomness `rho` from the + signature to re-compute the codeword $x = (x_1, \dots, x_v)$ from the + message `m`. This includes calculating the checksum or checking the target sum. + + 2. **Reconstruct One-Time Public Key**: For each intermediate hash `y_i` + in the signature, the verifier completes the corresponding hash chain. + Since `y_i` was computed with $x_i$ steps, the verifier applies the + hash function an additional $w - 1 - x_i$ times to arrive at the + one-time public key component `otpk_{ep,i}`. + + 3. **Compute Merkle Leaf**: The verifier hashes the reconstructed one-time + public key components to compute the expected Merkle leaf for `epoch`. + + 4. **Verify Merkle Path**: The verifier uses the `path` from the signature + to compute a candidate Merkle root starting from the computed leaf. + Verification succeeds if and only if this candidate root matches the + `root` in the `PublicKey`. + + Args: + pk: The public key to verify against. + epoch: The epoch the signature corresponds to. + message: The message that was supposedly signed. + sig: The signature object to be verified. + + Returns: + `True` if the signature is valid, `False` otherwise. + + For the formal specification of this process, please refer to: + - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a] + - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b] + - The canonical Rust implementation: https://github.com/b-wagn/hash-sig """ - Verifies a digital signature against: - - a public key, - - a message, - - epoch. - """ - assert len(message) == MESSAGE_LENGTH, "Invalid message length" - assert 0 <= epoch < LIFETIME, "Epoch out of valid range" - - # Re-encode the message to get the expected codeword. - codeword = encode(pk.parameter, message, sig.rho, epoch) - if codeword is None: - return False - - # Reconstruct the one-time public key from the signature's hashes. - chain_ends: List[List[Fp]] = [] - for i in range(DIMENSION): - steps_to_end = (BASE**CHUNK_SIZE - 1) - codeword[i] - end_of_chain = chain( - pk.parameter, epoch, i, codeword[i], steps_to_end, sig.hashes[i] - ) - chain_ends.append(end_of_chain) - - # Compute the Merkle leaf by hashing the reconstructed one-time public key. - # Note: A proper tweak would be used here. For simplicity, we omit it. - computed_leaf = tweakable_hash(pk.parameter, [], chain_ends) - - # Verify the Merkle path against the public key's root. - return hash_tree_verify( - pk.parameter, pk.root, epoch, computed_leaf, sig.path + raise NotImplementedError( + "verify will be implemented in a future update to the specification." ) diff --git a/src/lean_spec/subspecs/xmss/structures.py b/src/lean_spec/subspecs/xmss/structures.py index 0be56a53..e0f4a6a7 100644 --- a/src/lean_spec/subspecs/xmss/structures.py +++ b/src/lean_spec/subspecs/xmss/structures.py @@ -5,7 +5,7 @@ from pydantic import BaseModel, ConfigDict, Field from ..koalabear import Fp -from .constants import HASH_LEN, PARAMETER_LEN, RAND_LEN +from .constants import HASH_LEN_FE, PARAMETER_LEN, RAND_LEN_FE class HashTreeOpening(BaseModel): @@ -26,7 +26,7 @@ class PublicKey(BaseModel): """The public key for the Generalized XMSS scheme.""" model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) - root: List[Fp] = Field(..., max_length=HASH_LEN, min_length=HASH_LEN) + root: List[Fp] = Field(..., max_length=HASH_LEN_FE, min_length=HASH_LEN_FE) parameter: List[Fp] = Field( ..., max_length=PARAMETER_LEN, min_length=PARAMETER_LEN ) @@ -37,7 +37,7 @@ class Signature(BaseModel): model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) path: HashTreeOpening - rho: List[Fp] = Field(..., max_length=RAND_LEN, min_length=RAND_LEN) + rho: List[Fp] = Field(..., max_length=RAND_LEN_FE, min_length=RAND_LEN_FE) hashes: List[List[Fp]] diff --git a/src/lean_spec/subspecs/xmss/utils.py b/src/lean_spec/subspecs/xmss/utils.py deleted file mode 100644 index 88c7ef5f..00000000 --- a/src/lean_spec/subspecs/xmss/utils.py +++ /dev/null @@ -1,291 +0,0 @@ -"""Cryptographic utilities and helper functions for the XMSS verification.""" - -from typing import List, Optional - -from ..koalabear import Fp, P -from ..poseidon2 import PARAMS_16, PARAMS_24, permute -from .constants import ( - BASE, - CAPACITY, - CHUNK_SIZE, - DIMENSION, - HASH_LEN, - MSG_HASH_LEN, - MSG_LEN, - PARAMETER_LEN, - TARGET_SUM, - TWEAK_LEN, - TWEAK_PREFIX_CHAIN, - TWEAK_PREFIX_MESSAGE, - TWEAK_PREFIX_TREE, -) -from .structures import HashTreeOpening - - -def tweakable_hash( - parameter: List[Fp], tweak: List[Fp], message: List[List[Fp]] -) -> List[Fp]: - """ - A tweakable hash function using Poseidon2 for domain-separated hashing. - - Args: - parameter: The public parameter `P`. - tweak: A domain-separating value. - message: The data to be hashed. - - Returns: - The resulting hash digest as a list of field elements. - """ - # Input Preparation - # - # Flatten the message (list of vectors -> single list of field elements). - flat_message = [fe for sublist in message for fe in sublist] - # Concatenate the parameter, tweak, and message into a single input. - combined_input = parameter + tweak + flat_message - - # Hashing Logic - # - # The function selects a specific hashing mode based on the number of - # message parts. - - # Case 1: Hashing a single value, as done within a hash chain. - # - # This uses Poseidon2 in compression mode (width of 16). - if len(message) == 1: - # Pad the input with zeros to match the permutation's required width. - state = combined_input + [Fp(value=0)] * (16 - len(combined_input)) - # Apply the core cryptographic permutation to the state. - permuted_state = permute(state, PARAMS_16) - # Apply the feed-forward step: - # We add the initial state back into the permuted state element-wise. - result = [s + p for s, p in zip(permuted_state, state, strict=False)] - # Truncate the full state to the desired hash output length and return. - return result[:HASH_LEN] - - # Case 2: Hashing two values, typically for Merkle tree sibling nodes. - # - # This uses the wider Poseidon2 instance (width of 24) in compression mode. - elif len(message) == 2: - # Pad the input to the permutation's width of 24. - state = combined_input + [Fp(value=0)] * (24 - len(combined_input)) - # Apply the core cryptographic permutation. - permuted_state = permute(state, PARAMS_24) - # Apply the feed-forward step. - result = [s + p for s, p in zip(permuted_state, state, strict=False)] - # Truncate the result to the desired hash output length and return. - return result[:HASH_LEN] - - # Case 3: Hashing many values, such as a Merkle leaf from all chain ends. - # - # The sponge construction handles inputs larger than the state width. - else: - # The rate - rate = 24 - CAPACITY - - # For domain separation, the capacity part of the state is initialized - # with a hash of the input configuration. - lengths = [ - Fp(value=PARAMETER_LEN), - Fp(value=TWEAK_LEN), - Fp(value=DIMENSION), - Fp(value=HASH_LEN), - ] - # This is a recursive call with an input to generate the separator. - capacity_value = tweakable_hash([], [], [lengths])[:CAPACITY] - - # Initialize the sponge state: - # - the rate part is zero, - # - the capacity part holds the separator. - state = [Fp(value=0)] * 24 - state[rate:] = capacity_value - - # Pad the main input so its length is an even multiple of the rate. - padding_len = (rate - (len(combined_input) % rate)) % rate - padded_input = combined_input + [Fp(value=0)] * padding_len - - # Absorb the input in chunks of size `rate`. - for i in range(0, len(padded_input), rate): - chunk = padded_input[i : i + rate] - # Add the current chunk into the rate part of the state. - for j in range(rate): - state[j] += chunk[j] - # Apply the perm to the entire state to mix the absorbed data. - state = permute(state, PARAMS_24) - - # Squeeze the final output from the rate part of the state. - return state[:HASH_LEN] - - -def chain( - parameter: List[Fp], - epoch: int, - chain_index: int, - start_pos: int, - steps: int, - start_value: List[Fp], -) -> List[Fp]: - """ - Computes `steps` iterations of a Winternitz-style hash chain. - - A hash chain is created by repeatedly applying a hash function: - H(H(...H(start))) - - Each step uses a unique tweak to ensure that every hash computation in the - entire system is unique. - - Args: - parameter: The public parameter `P` for the hash function. - epoch: The signature's epoch, used for tweaking. - chain_index: The index of this specific chain (from 0 to DIMENSION-1). - start_pos: The starting position within the chain. - steps: The number of times to apply the hash function. - start_value: The initial hash value to begin the chain from. - - Returns: - The final hash value after `steps` iterations. - """ - # Initialize the iterative hash value with the provided start_value. - current_value = start_value - # Loop `steps` times to perform the chained hashing. - for i in range(steps): - # The position in the chain is its starting offset + the current step. - pos_in_chain = start_pos + i - # Pack the tweak's components into a single integer. - packed_data = (epoch << 24) | (chain_index << 16) | pos_in_chain - # Create the domain-separating tweak for this specific hash operation. - tweak = [TWEAK_PREFIX_CHAIN, Fp(value=packed_data)] - # Apply the hash function to get the next value in the chain. - current_value = tweakable_hash(parameter, tweak, [current_value]) - # Return the final value after all iterations. - return current_value - - -def encode( - parameter: List[Fp], message: bytes, rho: List[Fp], epoch: int -) -> Optional[List[int]]: - """ - Performs the Target Sum message encoding. - - This function deterministically converts a message into a sequence of small - integers (a "codeword"). The encoding is only considered valid if the sum - of these integers equals a predefined `TARGET_SUM`. - - Args: - parameter: The public parameter `P` for the hash function. - message: The 32-byte message to encode. - rho: The randomness used for this encoding. - epoch: The signature's epoch, used for tweaking. - - Returns: - A list of integers representing the codeword if the sum is correct, - otherwise `None`. - """ - # Prepare inputs for hashing. - msg_int = int.from_bytes(message, "little") - msg_fes: List[Fp] = [] - for _ in range(MSG_LEN): - msg_fes.append(Fp(value=msg_int % P)) - msg_int //= P - tweak: List[Fp] = [TWEAK_PREFIX_MESSAGE, Fp(value=epoch)] - - # Hash all inputs to create a digest. - hash_input: List[Fp] = rho + parameter + tweak + msg_fes - state = hash_input + [Fp(value=0)] * (24 - len(hash_input)) - permuted = permute(state, PARAMS_24) - hash_output = [s + p for s, p in zip(permuted, state, strict=False)][ - :MSG_HASH_LEN - ] - - # Decode the hash digest into the codeword chunks. - digest_int = 0 - for fe in reversed(hash_output): - digest_int = (digest_int * P) + fe.value - - chunks: List[int] = [ - (digest_int >> (i * CHUNK_SIZE)) & (BASE - 1) for i in range(DIMENSION) - ] - - # Check if the sum of the chunks equals the required target sum. - if sum(chunks) == TARGET_SUM: - # If the sum is correct, the encoding is valid. - return chunks - else: - # Otherwise, the encoding fails for this randomness `rho`. - return None - - -def hash_tree_verify( - parameter: List[Fp], - root: List[Fp], - epoch: int, - leaf_content: List[List[Fp]], - path: HashTreeOpening, -) -> bool: - """ - Verifies a Merkle path from a leaf's content to the root. - - This function first hashes the raw leaf content to get the level 0 node, - then reconstructs the Merkle root by iteratively hashing this node with - the provided sibling nodes up the tree. - - Args: - parameter: The public parameter `P` for the hash function. - root: The known, trusted Merkle root from the public key. - epoch: The index of the leaf in the tree. - leaf_content: The pre-image of the leaf node (e.g., the list of chain ends). - path: The authentication path containing the sibling hashes. - - Returns: - - `True` if the computed root matches the provided root, - - `False` otherwise. - """ - # Initial Checks - # - # The depth of the tree is determined by the number of siblings in path. - depth = len(path.siblings) - # The epoch must be a valid index for a tree of this depth. - assert 0 <= epoch < (1 << depth), "Epoch is out of range for this path" - - # Compute Leaf Node Hash - # - # The first step is to hash the provided leaf content to get the actual - # leaf node that exists at level 0 of the Merkle tree. - # - # The tweak identifies this as a hash at level 0, position `epoch`. - leaf_tweak_packed = (0 << 32) | epoch - leaf_tweak = [TWEAK_PREFIX_TREE, Fp(value=leaf_tweak_packed)] - current_hash = tweakable_hash(parameter, leaf_tweak, leaf_content) - - # Iteratively Compute Root - # - # Start with the leaf's index for the iterative process. - current_index = epoch - # Iterate up the tree, from the bottom (level 0) to the root. - for i, sibling_hash in enumerate(path.siblings): - # Determine the hash order based on whether the current node is a - # left (even index) or right (odd index) child. - if current_index % 2 == 0: - # For a left child, the order is H(current, sibling). - children = [current_hash, sibling_hash] - else: - # For a right child, the order is H(sibling, current). - children = [sibling_hash, current_hash] - - # Move up to the parent's index for the next level. - current_index //= 2 - - # The level of the PARENT node we are about to compute. - parent_level = i + 1 - - # Create the unique tweak for this specific parent node, using its - # level and its index within that level. - parent_tweak_packed = (parent_level << 32) | current_index - tweak = [TWEAK_PREFIX_TREE, Fp(value=parent_tweak_packed)] - - # Compute the parent's hash. - current_hash = tweakable_hash(parameter, tweak, children) - - # Final Comparison - # - # After the loop, the computed hash should equal the public root. - return current_hash == root From b4152ceb6144841b91c07d7127cde5de3a6f4839 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Wed, 13 Aug 2025 22:47:00 +0200 Subject: [PATCH 3/9] linter --- src/lean_spec/subspecs/xmss/interface.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index d3ef4f5f..d19043f9 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -64,7 +64,8 @@ def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool: 1. **Re-encode Message**: The verifier uses the randomness `rho` from the signature to re-compute the codeword $x = (x_1, \dots, x_v)$ from the - message `m`. This includes calculating the checksum or checking the target sum. + message `m`. + This includes calculating the checksum or checking the target sum. 2. **Reconstruct One-Time Public Key**: For each intermediate hash `y_i` in the signature, the verifier completes the corresponding hash chain. From d47eebd794fedfeb6dd24ec0fdcd24c667055f87 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Wed, 13 Aug 2025 22:59:03 +0200 Subject: [PATCH 4/9] modify constants --- src/lean_spec/subspecs/xmss/constants.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lean_spec/subspecs/xmss/constants.py b/src/lean_spec/subspecs/xmss/constants.py index 86b18e9e..7dc0f65a 100644 --- a/src/lean_spec/subspecs/xmss/constants.py +++ b/src/lean_spec/subspecs/xmss/constants.py @@ -9,7 +9,7 @@ MESSAGE_LENGTH: int = 32 """The length in bytes for all messages to be signed.""" -LOG_LIFETIME: int = 18 +LOG_LIFETIME: int = 32 """The base-2 logarithm of the scheme's maximum lifetime.""" LIFETIME: int = 1 << LOG_LIFETIME @@ -54,10 +54,10 @@ MSG_LEN_FE: int = 9 """The length of a message after being encoded into field elements.""" -RAND_LEN_FE: int = 6 +RAND_LEN_FE: int = 7 """The length of the randomness `rho` used during message encoding.""" -HASH_LEN_FE: int = 7 +HASH_LEN_FE: int = 8 """The output length of the main tweakable hash function.""" CAPACITY: int = 9 From 9a466a24b0ea6e3683332223f1997970dad652ae Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 14 Aug 2025 09:09:11 +0200 Subject: [PATCH 5/9] add eprint links in doc --- src/lean_spec/subspecs/xmss/interface.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index d19043f9..06b4dac8 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -22,8 +22,8 @@ def key_gen() -> Tuple[PublicKey, SecretKey]: the full Merkle tree. For the formal specification of this process, please refer to: - - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a] - - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b] + - "Hash-Based Multi-Signatures for Post-Quantum Ethereum": https://eprint.iacr.org/2025/055 + - "Technical Note: LeanSig for Post-Quantum Ethereum": https://eprint.iacr.org/2025/1332 - The canonical Rust implementation: https://github.com/b-wagn/hash-sig """ raise NotImplementedError( @@ -43,8 +43,8 @@ def sign(sk: SecretKey, epoch: int, message: bytes) -> Signature: key and epoch for different messages, as this would compromise security. For the formal specification of this process, please refer to: - - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a] - - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b] + - "Hash-Based Multi-Signatures for Post-Quantum Ethereum": https://eprint.iacr.org/2025/055 + - "Technical Note: LeanSig for Post-Quantum Ethereum": https://eprint.iacr.org/2025/1332 - The canonical Rust implementation: https://github.com/b-wagn/hash-sig """ raise NotImplementedError( @@ -91,8 +91,8 @@ def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool: `True` if the signature is valid, `False` otherwise. For the formal specification of this process, please refer to: - - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a] - - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b] + - "Hash-Based Multi-Signatures for Post-Quantum Ethereum": https://eprint.iacr.org/2025/055 + - "Technical Note: LeanSig for Post-Quantum Ethereum": https://eprint.iacr.org/2025/1332 - The canonical Rust implementation: https://github.com/b-wagn/hash-sig """ raise NotImplementedError( From 6460f6e2ec999ee2a8e98ee6ae8384e987083ede Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 14 Aug 2025 09:13:23 +0200 Subject: [PATCH 6/9] add key gen args --- src/lean_spec/subspecs/xmss/interface.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index 06b4dac8..15d377cf 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -13,7 +13,9 @@ from .structures import PublicKey, SecretKey, Signature -def key_gen() -> Tuple[PublicKey, SecretKey]: +def key_gen( + activation_epoch: int, num_active_epochs: int +) -> Tuple[PublicKey, SecretKey]: """ Generates a new cryptographic key pair. From 9295e3d7e91a73b4e867baeb7852c2d4d00a4d1b Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 14 Aug 2025 09:17:09 +0200 Subject: [PATCH 7/9] add doc for args --- src/lean_spec/subspecs/xmss/interface.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index 15d377cf..98d7b7b7 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -23,6 +23,11 @@ def key_gen( generating a master secret, deriving all one-time keys, and constructing the full Merkle tree. + Args: + activation_epoch: The starting epoch for which this key is active. + num_active_epochs: The number of consecutive epochs + the key is active for. + For the formal specification of this process, please refer to: - "Hash-Based Multi-Signatures for Post-Quantum Ethereum": https://eprint.iacr.org/2025/055 - "Technical Note: LeanSig for Post-Quantum Ethereum": https://eprint.iacr.org/2025/1332 From dd5fcba0d15eb1284f882c349a4f87566f739fcb Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 14 Aug 2025 09:37:50 +0200 Subject: [PATCH 8/9] fix comments --- src/lean_spec/subspecs/xmss/constants.py | 16 +++++++++++++++- src/lean_spec/subspecs/xmss/interface.py | 6 +++--- src/lean_spec/subspecs/xmss/structures.py | 23 ++++++++++++++++++++--- 3 files changed, 38 insertions(+), 7 deletions(-) diff --git a/src/lean_spec/subspecs/xmss/constants.py b/src/lean_spec/subspecs/xmss/constants.py index 7dc0f65a..e2f14bb0 100644 --- a/src/lean_spec/subspecs/xmss/constants.py +++ b/src/lean_spec/subspecs/xmss/constants.py @@ -1,4 +1,18 @@ -"""Defines the cryptographic constants for the XMSS specification.""" +""" +Defines the cryptographic constants for the XMSS specification. + +This specification corresponds to the "hashing-optimized" Top Level Target Sum +instantiation from the canonical Rust implementation. + +.. note:: + This specification uses the **KoalaBear** prime field, which is consistent + with the formal analysis in the reference papers (e.g., Section 5 of the + "LeanSig" technical note: https://eprint.iacr.org/2025/1332). + + The canonical Rust implementation currently uses the `BabyBear` field for + practical reasons but is expected to align with this + specification in the future. +""" from ..koalabear import Fp diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index 98d7b7b7..5203fd2b 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -74,11 +74,11 @@ def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool: message `m`. This includes calculating the checksum or checking the target sum. - 2. **Reconstruct One-Time Public Key**: For each intermediate hash `y_i` + 2. **Reconstruct One-Time Public Key**: For each intermediate hash $y_i$ in the signature, the verifier completes the corresponding hash chain. - Since `y_i` was computed with $x_i$ steps, the verifier applies the + Since $y_i$ was computed with $x_i$ steps, the verifier applies the hash function an additional $w - 1 - x_i$ times to arrive at the - one-time public key component `otpk_{ep,i}`. + one-time public key component $pk_{ep,i}$. 3. **Compute Merkle Leaf**: The verifier hashes the reconstructed one-time public key components to compute the expected Merkle leaf for `epoch`. diff --git a/src/lean_spec/subspecs/xmss/structures.py b/src/lean_spec/subspecs/xmss/structures.py index e0f4a6a7..3fa18cca 100644 --- a/src/lean_spec/subspecs/xmss/structures.py +++ b/src/lean_spec/subspecs/xmss/structures.py @@ -7,6 +7,21 @@ from ..koalabear import Fp from .constants import HASH_LEN_FE, PARAMETER_LEN, RAND_LEN_FE +HashDigest = List[Fp] +""" +A type alias representing a hash digest. +""" + +Parameter = List[Fp] +""" +A type alias representing the public parameter `P`. +""" + +Randomness = List[Fp] +""" +A type alias representing the randomness `rho`. +""" + class HashTreeOpening(BaseModel): """ @@ -17,7 +32,7 @@ class HashTreeOpening(BaseModel): """ model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) - siblings: List[List[Fp]] = Field( + siblings: List[HashDigest] = Field( ..., description="List of sibling hashes, from bottom to top." ) @@ -27,7 +42,7 @@ class PublicKey(BaseModel): model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) root: List[Fp] = Field(..., max_length=HASH_LEN_FE, min_length=HASH_LEN_FE) - parameter: List[Fp] = Field( + parameter: Parameter = Field( ..., max_length=PARAMETER_LEN, min_length=PARAMETER_LEN ) @@ -37,7 +52,9 @@ class Signature(BaseModel): model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True) path: HashTreeOpening - rho: List[Fp] = Field(..., max_length=RAND_LEN_FE, min_length=RAND_LEN_FE) + rho: Randomness = Field( + ..., max_length=RAND_LEN_FE, min_length=RAND_LEN_FE + ) hashes: List[List[Fp]] From be0d0acd21f4c28b861d841b01572ed7d2dacdcf Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 14 Aug 2025 09:52:01 +0200 Subject: [PATCH 9/9] fix comment --- src/lean_spec/subspecs/xmss/interface.py | 8 +++++--- src/lean_spec/subspecs/xmss/structures.py | 16 +++++++++++----- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/lean_spec/subspecs/xmss/interface.py b/src/lean_spec/subspecs/xmss/interface.py index 5203fd2b..e8e7e492 100644 --- a/src/lean_spec/subspecs/xmss/interface.py +++ b/src/lean_spec/subspecs/xmss/interface.py @@ -17,7 +17,7 @@ def key_gen( activation_epoch: int, num_active_epochs: int ) -> Tuple[PublicKey, SecretKey]: """ - Generates a new cryptographic key pair. + Generates a new cryptographic key pair. This is a **randomized** algorithm. This function is a placeholder. In a real implementation, it would involve generating a master secret, deriving all one-time keys, and constructing @@ -41,7 +41,8 @@ def key_gen( def sign(sk: SecretKey, epoch: int, message: bytes) -> Signature: """ - Produces a digital signature for a given message at a specific epoch. + Produces a digital signature for a given message at a specific epoch. This + is a **randomized** algorithm. This function is a placeholder. The signing process involves encoding the message, generating a one-time signature, and providing a Merkle path. @@ -62,7 +63,8 @@ def sign(sk: SecretKey, epoch: int, message: bytes) -> Signature: def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool: r""" - Verifies a digital signature against a public key, message, and epoch. + Verifies a digital signature against a public key, message, and epoch. This + is a **deterministic** algorithm. This function is a placeholder. The complete verification logic is detailed below and will be implemented in a future update. diff --git a/src/lean_spec/subspecs/xmss/structures.py b/src/lean_spec/subspecs/xmss/structures.py index 3fa18cca..306e9948 100644 --- a/src/lean_spec/subspecs/xmss/structures.py +++ b/src/lean_spec/subspecs/xmss/structures.py @@ -1,23 +1,29 @@ """Defines the data structures for the Generalized XMSS signature scheme.""" -from typing import List +from typing import Annotated, List from pydantic import BaseModel, ConfigDict, Field from ..koalabear import Fp from .constants import HASH_LEN_FE, PARAMETER_LEN, RAND_LEN_FE -HashDigest = List[Fp] +HashDigest = Annotated[ + List[Fp], Field(min_length=HASH_LEN_FE, max_length=HASH_LEN_FE) +] """ A type alias representing a hash digest. """ -Parameter = List[Fp] +Parameter = Annotated[ + List[Fp], Field(min_length=PARAMETER_LEN, max_length=PARAMETER_LEN) +] """ A type alias representing the public parameter `P`. """ -Randomness = List[Fp] +Randomness = Annotated[ + List[Fp], Field(min_length=RAND_LEN_FE, max_length=RAND_LEN_FE) +] """ A type alias representing the randomness `rho`. """ @@ -55,7 +61,7 @@ class Signature(BaseModel): rho: Randomness = Field( ..., max_length=RAND_LEN_FE, min_length=RAND_LEN_FE ) - hashes: List[List[Fp]] + hashes: List[HashDigest] class SecretKey(BaseModel):