International Association
for Cryptologic Research

We observe that the existing norms within cryptography do not expect protocol analysts to document the sociotechnical properties that a deployed system should have. To help close this potential gap, we develop a framework that allows bringing sociotechnical dimensions into analyses of cryptographic systems, and in particular facilitates "in-context" analysis of proposed cryptographic deployments on top of widely-accepted cryptographic modeling techniques. To explore the utility of our framework, we use Apple's 2021 CSAM scanning proposal as a case study. We show how our framework naturally surfaces many of the criticisms of Apple's proposal and helps us identify a previously undocumented property of the proposal.

FAEST is a family of post-quantum signature schemes based on VOLE-in-the-Head, and is one of the nine candidates advanced to the third round of the NIST Additional Digital Signature process. FAEST relies only on symmetric cryptographic primitives, including block ciphers and hash functions, and does not require structured number-theoretic assumptions.

We propose two families of signature schemes, SM4th and uBlockith, targeting 128-bit and 256-bit classical security, respectively. SM4th and uBlockith follow the FAEST framework but instantiate it with Chinese-designed block ciphers, including SM4, uBlock, and Ballet. We further design constraint systems tailored to these block ciphers and provide instruction-set-aware optimized implementations.

Our evaluation on two Intel platforms and a Hygon platform shows that the end-to-end performance of the proposed schemes is strongly platform dependent. On an Intel platform with native SM4 support, the SM4th variants achieve performance comparable to the corresponding FAEST-128 variants, with a gap of less than $1\times$. On the Hygon platform with native CIS-SM4 support, the SM4th variants are within approximately $3\times$ of FAEST-128. The SM4th-EM-s (short) variant has a combined public-key and signature size of $3\,850$ bytes, compared with $3\,938$ bytes for FAEST-EM-128s. The uBlockith variants remain approximately $3$--$4\times$ slower than FAEST-256. These results demonstrate the feasibility and costs of instantiating VOLE-based signatures with the selected Chinese block ciphers.

Standard Tseitin encodings of the SHA-256 nonlinear functions Ch and Maj can hide conditioned differential projections from Boolean Constraint Propagation (BCP). We materialize them as short, semantically redundant CNF clauses. A cofactor theorem characterizes all controlled differential linear forms; its implemented unit-vector specialization returns exactly all minimum-control projections, yielding four Ch and twelve Maj clauses per bit. The clauses preserve models, introduce no variables, and strictly strengthen BCP on an explicit gate fragment. We claim neither propagation completeness nor a general affine compiler.

We evaluate mechanism separately from performance and distinguish the production bundle from the proposed layer. Frozen studies show a fixed-formula bundle benefit, but the matched clause isolation fails its effect gate and an unrestricted control is inconclusive. We therefore show neither a solver-independent speedup nor a new cryptanalytic attack. The restricted weight-15 C15 census passes the CaDiCaL rule but not the Kissat rule. In the stratified C16 extension, the frozen decisions are too censored for CaDiCaL and too censored for Kissat; these solver-stratified labels are not pooled. A pinned three-solver replay validates larger-bundle execution but cannot attribute performance to the clauses. A variable-preserving probe exposes all 32 tested implications only after augmentation.

Public blockchains expose all state and computation by default, which is incompatible with financial applications that require confidentiality. Solana achieves high throughput and sub-second confirmation, making it an attractive settlement layer, yet it offers no general mechanism for computing over encrypted state: fully homomorphic encryption (FHE) remains orders of magnitude too slow for interactive use, secure multi-party computation (MPC) incurs heavy communication, and Solana’s native confidential-transfer extension hides only token amounts and sup- ports no programmable logic. We present Encifher, a confidentiality coprocessor for Solana that brings general, programmable computation over encrypted state to a high-throughput chain. Encifher adopts the ciphertext-handle and symbolic-execution interface of confidential-computing coprocessors (e.g., Zama’s fhEVM), but resolves it inside a Trusted Execution Environment (TEE) rather than with a fully homomorphic evaluator: on-chain Solana programs manipulate only 128-bit handles to ciphertexts, while an off-chain coprocessor running inside a hardware enclave fetches the corresponding ciphertexts from a public data availability layer, decrypts and computes on plaintext within the enclave, re-encrypts, and commits attested, Merkle-anchored results back on chain. A key observation is that Solana’s account model and parallel (Sealevel) scheduler turn the transaction’s declared read/write set into the dependency graph of the confidential computation, yielding parallel, correctly-ordered execution of encrypted operations without a bespoke scheduler. To avoid the single-point-of-failure of an enclave holding a master decryption key, Encifher distributes trust across a threshold-decryption committee and verifies enclave attestation on chain. Encifher is deployed in production, powering confidential payments, swaps, and a cross-chain bridge. In production, a confidential swap settles in a single Solana transaction costing 157,000 compute units; the AES-256-GCM symmetric-encryption layer runs at over a million operations per second and threshold decryption completes in single-digit to tens of milliseconds (near-plaintext speed, against the many-orders-of-magnitude overhead of FHE), and Encifher has served over 5,000 users and 50,000 confidential operations. We are explicit about the cost of this design point: Encifher reduces the trust base to TEE integrity, honest threshold key management, and the cloud attestation root, rather than to cryptographic hardness alone.

Sender untraceability hides the account spent by a cryptocurrency transfer among a set of candidates, its masking set. What a transfer does to that set separates two designs: classical schemes retain the whole set and append a nullifier marking the spent account, so the ledger grows with every transfer; constant-state schemes instead consume and replace the entire set. We ask how this choice affects synchronization.

We formalize the two designs as the linear and constant untraceable asset transfer objects (LUAT and CUAT) and locate them in the consensus hierarchy. In LUAT, transfers from distinct accounts commute. Its consensus number is 2, compared with 1 for standard asset transfer, independently of the masking-set size and of the untraceability notion, and LUAT is starvation-free. Partitioning the accounts into fixed masking sets lets exhausted sets be garbage-collected without increasing that number.

In CUAT, a transfer consumes and replaces every account of its masking set, so two transfers whose sets intersect cannot both take effect. We formalize this with the conflict graph on masking sets, whose edges join sets sharing an account. Under weak untraceability, which protects a transaction in isolation, the consensus number is unbounded already for one-round protocols. Under strong untraceability, which protects against an observer of the complete history, untraceability holds on a history exactly when any two accounts sharing a masking set occur in the same number of the masking sets in it. This uniform incidence bounds the conflict graph, and matching constructions attain it, so the consensus number is determined exactly and grows quadratically in the masking-set size. Finally, CUAT is not starvation-free. The two objects therefore pay for the same privacy differently: LUAT in storage, CUAT in synchronization and fairness.

Recent advances in fully homomorphic encryption (FHE) have enabled privacy-preserving machine learning directly over encrypted data. As a representative recurrent architecture, the long short-term memory (LSTM) network is widely used for modeling sequential dependencies, yet existing FHE-based LSTM inference schemes still suffer from high latency and limited scalability. In this paper, we present an efficient privacy-preserving LSTM inference protocol on encrypted sequential data based on FHE. We insert a lightweight normalization module before nonlinear activations to bound the hidden states, thereby enabling accurate low-degree polynomial approximations of the Sigmoid, Tanh, and inverse square-root functions via a hybrid Remez and least-squares strategy. We implement the proposed protocol using the Lattigo library, incorporating ciphertext packing optimization, rotation minimization, and SIMD-based parallelization. Experiments show that on standard text classification benchmarks, our encrypted LSTM achieves competitive accuracy compared with plaintext models and consistently outperforms the state-of-the-art FHE-based method, achieving up to a 4.7x speedup.

Free Hosting Platforms (FHPs) let users publish websites with minimal cost and configuration, but the same provider-managed infrastructure can also be used to host phishing websites. We study how this setting affects Certificate Transparency (CT)-based phishing detection by analyzing X.509, CT, and URL features across FHP phishing, FHP benign, non-FHP phishing, and popular benign websites. Reflecting the shared and wildcard certificate practices common in this setting, we analyze the certificate-level and domain-level data separately.

Our measurement study shows that many apparent phishing indicators instead reflect hosting-provider characteristics: in our domain-level correlation analysis, hosting-platform status is more strongly associated with the extracted X.509, CT, and URL features than phishing status is, with the strongest FHP-associated feature (subdomain levels, $\eta=0.54$) exceeding the strongest phishing-associated feature (certificate validity period, $\eta=0.31$).

We further evaluate two representative CT-based phishing detection frameworks on FHP-only data and discover that provider-managed infrastructure creates challenges for applying them directly. These findings show the need for future work on CT-based phishing detection methods that account for this deployment setting, especially as AI tools lower the effort required to create convincing phishing websites at scale.

Zero knowledge is formalized via a simulator — i.e., an efficient computation which simulates the view of a (malicious) verifier. The foundational results in constant-round zero knowledge [GMW86,FS90,GK96] all use expected polynomial-time (EPT) simulators, and there is evidence that strict poly-time simulators do not exist for these protocols [BL02]. In the post-quantum setting, we must upgrade the simulator to at least quantum polynomial time (QPT) in order to properly simulate quantum verifiers. Chia et al. [CCLY22] proved a surprising negative result which precludes non-trivial ZK for constant-round protocols with both (strict) QPT and a natural notion of expected quantum polynomial-time (EQPT) black-box simulation. In light of this, Lombardi, Spooner, and Ma [LMS22] introduced a novel EQPT notion, coherent-runtime EQPT or EQPT$_c$, and showed that the [GMW86,FS90,GK96] protocols all allow for EQPT$_c$ simulation.

In this work, we identify a fundamental issue with the definition of EQPT$_c$ simulation, and propose a resolution. In particular, we demonstrate that EQPT$_c$ computation is not necessarily efficient and can, in fact, decide any classical decision problem. This is possible through a freedom of choice in selecting a unitary dilation for an efficient quantum channel. We propose an revised definition which carefully restricts this choice, and prove that the definition preserves the zero knowledge of the [GMW86,FS90,GK96] protocols. Additionally, by upgrading the [GK96] framework to the fully quantum setting, we demonstrate for the first time a constant-round (malicious verifier) zero knowledge proof system for QMA (with EQPT$_c$ simulation).

Password-based authentication remains widespread, and large-scale sets of leaked hashes enable practical offline brute-force attacks. Multi-target attacks, which check candidates against large sets of hashes simultaneously, are particularly effective. Understanding the capabilities of low-cost platforms for such attacks is important to assess real-world password security risks.

Therefore, we present BF², a modular and scalable FPGA–CPU framework that accelerates multi-target password recovery. BF² combines a password-candidate generator, a fully-pipelined NT hash core, a Bloom filter stage to filter non-matching candidates, and a multi-threaded host-side component that performs exact membership check using a perfect hash function. We implement BF² on the low-cost, \$199 NiteFury II board. With 16 parallel pipelines running at a 100 MHz clock frequency, our FPGA implementation generates $1.6\times10^9$ hashes/s. In our experiments, BF² demonstrates up to $7.5\times$ higher throughput than John the Ripper, and reduces power consumption by as much as $90\%$ compared to Hashcat on an RTX 5000.

For cryptosystems whose security relies on the hardness of decoding in the sublinear regime, the best known attacks are based on Information Set Decoding (ISD). In this regime, which is particularly relevant to HQC and Pseudorandom Correlation Generators (PCG), the cost of Gaussian elimination is no longer negligible and significantly affects the overall attack complexity.

In this work, we revisit the Reduce-and-Prange technique of Kim and Lee, which reduces the cost of Gaussian elimination by reusing partial pivots. We refine its complexity analysis using branching-process techniques, thereby obtaining a more accurate assessment of its performance. We then extend partial pivot reuse to Stern's algorithm and introduce MAGE-Stern, a multilevel amortized Gaussian elimination variant of Stern's algorithm.

Under a consistent logic-gate cost model, MAGE-Stern improves upon the best previously known attack against HQC by approximately 3 bits in time complexity, while reducing the memory complexity by about 12 bits. In particular, we estimate the security of the standardized HQC Category I parameter set at approximately 140 bits, about 3 bits below its NIST security target. We further combine multilevel amortized Gaussian elimination with the projective decoding framework of Carrier, Hatey, and Tillich, and investigate its application to regular decoding. Applied to the reference Pseudorandom Correlation Generator (PCG) parameter sets of Boyle, Couteau, Gilboa, and Ishai, the resulting algorithms improve upon the best previously known attacks by up to 6 bits across a broad range of practical parameters.

Private set union~(PSU) allows two parties to compute the union of their private sets without revealing their intersection. In many real-world applications, parties' datasets undergo frequent updates as elements are added or removed over time. Existing PSU protocols, however, must recompute the entire union from scratch whenever either party's set changes. This becomes highly inefficient when updates are small or frequent relative to the original set sizes. In this paper, we introduce the first updatable PSU~(uPSU) protocol for the standard two-party setting, which supports efficient incremental updates. We present a systematic classification of all possible update scenarios, which shows that only a small subset of updated elements actually modify the union, and establish the leakage baseline for uPSU. Based on these classification and leakage baseline, we provide a generic construction for uPSU that uses existing PSI and a tagged variant of PSU as building blocks. We prove security against semi-honest adversaries in the simulation-based model, and guarantee that incremental updates reveal no more information than a fresh execution of a standard PSU protocol on the updated sets. We instantiate and implement our generic construction using Kim et al.'s PSU protocol~(ACM SAC 2026) and Raghuraman and Rindal's PSI protocol~(ACM CCS 2022), demonstrating significant performance improvements over full recomputation of the union, even though its cost still depends on the original set size rather than purely on the update size. For set size $n = 2^{20}$ and update size $t = 2^{12}$, our protocol achieves a 14.1--45.4$\times$ speedup with a 4.8--59.1$\times$ communication reduction over full recomputation using baseline PSU protocols.

In the information-theoretic model, parties communicate over sender-authenticated point-to-point channels, but use no digital signatures or other transferable cryptographic certificates; the adversary is otherwise computationally unbounded. We present \name, an information-theoretic Byzantine agreement protocol for partial synchrony with a good-case latency of two rounds that achieves the optimal resilience bound of $n = 5f - 1$ in this setting. When the actual network delay after GST is at most $\delta \le \Delta$, our protocol achieves a \emph{robust} good-case latency of $2\delta$. The protocol proceeds in views and guarantees a worst-case view latency of at most $2\Delta + 2\delta$. Moreover, each party requires only $O(1)$ words of persistent storage, and each view incurs $O(n^2)$ messages of $O(1)$ words each.

Outsourcing computations to cloud providers raises significant data privacy concerns, making Privacy-Preserving Computation via Fully Homomorphic Encryption (FHE) increasingly vital. However, adapting data sorting routines to the FHE domain introduces severe performance bottlenecks. This survey systematizes the state-of-the-art in FHE-based sorting algorithms. A novel complexity metric, FHE-Effort, is introduced to accurately evaluate homomorphic circuit efficiency. Eighteen algorithms are benchmarked across three major FHE schemes using a unified codebase. The analysis concludes that TFHE is currently the most efficient scheme for sorting applications, and sorting networks like Odd-Even Merge and Bitonic Sort offer the optimal algorithmic architectures.

Efficient polynomial multiplication and matrix-vector operations are fundamental to computational algebra and modern cryptography. In lattice-based post-quantum cryptography (PQC), schemes utilizing Number Theoretic Transform (NTT)-unfriendly rings require highly optimized subquadratic multiplication algorithms. In this paper, we establish a rigorous mathematical framework for generalized $k$-way split polynomial multiplication and Toeplitz Matrix-Vector Product (TMVP) algorithms over arbitrary fields. First, we construct generalized $k$-way Schoolbook and Karatsuba multiplication algorithms, deriving exact closed-form recurrence relations and arithmetic complexities for any integer $k$. Second, we introduce a novel $k$-way TMVP algorithm utilizing optimal evaluation points and matrix row-reversal techniques. We mathematically prove that this generalized formulation strictly achieves the theoretical interpolation lower bound, requiring exactly $2k-1$ subproblems and yielding a subquadratic asymptotic complexity of $O(n^{\log_k(2k-1)})$. Furthermore, we determine the optimal consecutive application sequence of $k$-way Karatsuba and Schoolbook algorithms for any input size $n$, proving that the peak efficiency is driven entirely by the prime factorization of $n$. Finally, we establish exact algebraic crossover thresholds, demonstrating that our generalized TMVP formulas and optimal algorithmic sequences significantly outperform state-of-the-art unequal $k$-way splits and classical combinations in the literature, providing minimum arithmetic operation counts for $k \in \{5, 6, 8, 12\}$ and inputs of power-of-two and power-of-three dimensions.

Over the last decades, symbolic (Dolev-Yao) methods for the analysis of security protocols have proven to be effective to analyze and establish strong guarantees for widely deployed protocols and systems, such as TLS 1.3, E-voting protocols, EMV, and MLS. On the one hand, analysis methods like Tamarin and ProVerif provide automation and support for user-defined equational theories. On the other hand, methods like DY* offer more flexible and modular reasoning, but hardcode threat models and do not support custom equational theories.

We present DyLean, a framework for the symbolic analysis of cryptographic protocols in the Lean theorem prover. Our framework comprises both a flexible general-purpose symbolic semantics, as well as a concrete proof methodology.

DyLean allows defining protocols and expected security properties; its semantics and equational theories can be customized by the user. Furthermore, the semantics are agnostic of the specific proof methodology: our goal is to provide a generic framework that can be used by the community as a foundation to develop various proof methodologies.

Moreover, we provide a concrete proof methodology inspired by DY*, based on trace invariants. Thus, DyLean inherits from the qualities of DY*: it is able to analyze protocols involving unbounded loops or datastructures, and is able to compose security proofs in a variety of scenarios. Our proof methodology improves on DY* by allowing for user-defined equational theories and threat models. We exercise DyLean on several focused case studies, which include protocols using merkle trees, ratcheting protocols, post-quantum protocols, and protocols analyzed under different equational theories, which demonstrates that DyLean can effectively analyze protocols with each of these features.

Proof-of-useful-work (PoUW) certifies computational hardness, not utility: a certified computation need not be anyone's demanded job. We separate three properties of a work receipt — work soundness ($\mathsf{W}$), job binding ($\mathsf{B}$), and demand exogeneity ($\mathsf{E}$) — and locate the gap at $\mathsf{E}$. Two results are unconditional. First, payments between coalition-controlled requesters and workers are recoverable transfers that contribute no Sybil-resistant cost, so no security lower bound may count them (Lemma 1). Second, under free pseudonyms and endogenous observation a coalition can simulate the receipts of economically independent requesters, so endogenous receipts cannot certify $\mathsf{E}$ (Theorem 1); we lower-bound the cost of evading a stated class of provenance estimators. Building on these, a robustness bound: because a permissionless mechanism must remain live on the zero-demand path, its leader-election floor cannot depend on the demand component of service receipts (Theorem 2), and any admissible receipt boost is quantitatively capped. Fork-independent salvage value of useful outputs can leave security neutral, negative, or positive depending on salvage asymmetry and demand, which we characterize in a stylized free-entry model. Constructively, an irrecoverable tax on every settled payment makes the burn — not proof of independence — the security resource. Deployed evidence comprises one reported audit (Pearl cuPOW) and a reward-program farming analogue; the election-side failure is, at present, a model prediction. Useful-computation receipts are appropriate instruments for payment, collateral, and loss allocation — and a bounded, priced election boost — but not the leader-election floor.

Hamming Quasi-Cyclic (HQC) is a code-based key encapsulation mechanism selected by NIST for standardization, making its resistance to implementation attacks critically important. We present a side-channel attack that exploits load/store leakage in the manipulation of HQC's sparse secret vectors. Analysing Cortex-M4 assembly generated from the reference implementation, we identify a leakage surface in which the low and high 32-bit halves of each 64-bit word leak with different strengths, due to compiler-generated register spilling. We exploit this leakage to construct a simple zero-word distinguisher classifying machine words of the secret vector as zero or nonzero from electromagnetic measurements. The recovered zero positions are then translated into decoding hints, reducing HQC key recovery to a shortened syndrome-decoding problem. We analyse the resulting decoding complexity for all HQC parameter sets: at 32-bit granularity an expected $88.7\%$ of the machine words of~$y$ are zero for HQC-1, cutting the decoding to ${\approx}\,2^{46}$ bit operations. Experiments on a Cortex-M4 validate the predicted low/high-half asymmetry---approximately $500$ traces for the stronger low-half channel and $5{,}000$ for the weaker high-half channel---and recover the zero words of an HQC-1 key at 32-bit granularity. Finally, we discuss practical countermeasures that eliminate the sparsity exploited by the attack.

We formalize the notion of polynomial commitment schemes (PCSs) in the proof assistant Isabelle/HOL and formally verify the security proofs of two variants of the widely popular Kate, Zaverucha, and Goldberg (KZG) construction. Moreover, we formalize the Algebraic Group Model (AGM) by Fuchsbauer, Kiltz, and Loss using a novel constraint-programming-inspired approach. We formalize a reusable abstract definition of polynomial commitment schemes and define games for correctness, binding, hiding, and knowledge soundness/extractability. Based on this, we verify all applicable security proofs for two concrete PCS constructions: the standard (DL-)KZG and a batched KZG, using our AGM formalization in the knowledge-soundness proofs. Our proofs follow Shoup’s sequence-of-games approach, with machine-checked transitions, and are carried out in the CryptHOL framework for formal verification of cryptography in Isabelle. To our knowledge, this work is the first formalization of polynomial commitment schemes, the first formalization of the AGM, and the first formal verification of the security proofs for any concrete polynomial commitment scheme. This work lays the foundation for the formal verification of advanced cryptographic constructions, such as pairing-based zero-knowledge proofs (ZKPs) and succinct arguments.

We study large-scale, field-agnostic, hash-based polynomial commitment schemes (PCSs) with the goal of minimizing prover time while preserving polylogarithmic proof size and verifier time. This setting is motivated by advanced applications of zero-knowledge succinct non-interactive arguments of knowledge (zkSNARKs) such as zero-knowledge machine learning (zkML), where committed polynomials may encode billions of parameters and large prime fields are desirable for avoiding wraparound in fixed-point arithmetic.

We introduce SwitchFold, a generic construction of a hash-based multilinear PCS from any sequence of linear codes with geometrically increasing block lengths. The polylogarithmic proof size and verifier time do not rely on any specific algebraic structure of the codes, while the linear prover time follows solely from the linear encoding time. At its core, SwitchFold recursively applies the code-switching technique (Ron-Zewi and Rothblum, JACM ’24), reducing each multilinear extension (MLE) claim under one code to a simpler MLE claim under a shorter code. The generator-matrix MLE claims produced by code switching are accumulated across repeated PCS openings using an accumulation scheme (Bünz et al., TCC ’20), and are then proved through a final recursion. We instantiate SwitchFold with the Brakedown code sequence (Golovnev et al., CRYPTO ’23), whose recursive code structure aligns naturally with our framework; we call the resulting scheme BrakeFold. In contrast to prior code-switching PCSs such as Blaze (Brehm et al., EUROCRYPT ’25) and BrakingBase (Nair et al., ASIACRYPT ’25), SwitchFold does not require an auxiliary foldable code. At the scale of one billion coefficients and 100-bit security, the marginal cost of each additional PCS opening in BrakeFold yields 3.5× smaller proof size and 20.6× faster verification than Brakedown, with only a 1.3× increase in prover time. Its succinctness matches that of BaseFold (Zeilberger et al., CRYPTO ’24), while reducing prover time by 17.0×.

As the usage of Artificial Intelligence (AI) for sensitive purposes increases, there is a growing need for privacy-aware explainable AI (XAI) tools. In this paper, we present a privacy-preserving counterfactual explanation algorithm. Our starting point is a decision-support model that is able to operate on vertically partitioned datasets, meaning that each party holds a different subset of datapoint attributes. The goal of a counterfactual algorithm is to find, given an observation, a datapoint from the (virtual) dataset that is closest to the observation but has a different label. Our algorithm fully preserves the privacy of the n datapoints belonging to the different parties by combining the strengths of homomorphic encryption and secret sharing. Through a number of experiments, we demonstrate the added value of combining multiple datasets in a realistic scenario and show that the privacy-preserving solution does not affect the accuracy. We fully implement our solution and demonstrate that it scales as to thousands of datapoints.