[continued from previous message]

We show how fixed-unitary quantum encryption schemes can be attacked in a black-box setting. We use an efficient technique to invert a unitary transformation on a quantum computer to retrieve an encrypted secret quantum state $\ket{\psi}$. This attack
has a success rate of 100% and can be executed in constant time. We name a vulnerable scheme and suggest how to improve it to invalidate this attack. The proposed attack highlights the importance of carefully designing quantum encryption schemes to
ensure their security against quantum adversaries, even in a black-box setting.



## 2024/512

* Title: Single Trace is All It Takes: Efficient Side-channel Attack on Dilithium
* Authors: Zehua Qiao, Yuejun Liu, Yongbin Zhou, Yuhan Zhao, Shuyi Chen
* [Permalink](https://eprint.iacr.org/2024/512)
* [Download](https://eprint.iacr.org/2024/512.pdf)

### Abstract

As the National Institute of Standards and Technology (NIST) concludes its post-quantum cryptography (PQC) competition, the winning algorithm, Dilithium, enters the deployment phase in 2024. This phase underscores the importance of conducting thorough
practical security evaluations. Our study offers an in-depth side-channel analysis of Dilithium, showcasing the ability to recover the complete private key, ${s}_1$, within ten minutes using just two signatures and achieving a 60 success rate with a
single signature. We focus on analyzing the polynomial addition in Dilithium, $z=y+{cs}_1$, by breaking down the attack into two main phases: the recovery of $y$ and ${cs}_1$ through side-channel attacks, followed by the resolution of a system of error-
prone equations related to ${cs}_1$. Employing Linear Regression-based profiled attacks enables the successful recovery of the full $y$ value with a 40% success rate without the necessity for initial filtering. The extraction of ${cs}_1$ is further
improved using a CNN model, which boasts an average success rate of 75%. A significant innovation of our research is the development of a constrained optimization-based residual analysis technique. This method efficiently recovers ${s}_1$ from a large
set of error-containing equations concerning ${cs}_1$, proving effective even when only 10% of the equations are accurate. We conduct a practical attack on the Dilithium2 implementation on an STM32F4 platform, demonstrating that typically two signatures
are sufficient for complete private key recovery, with a single signature sufficing in optimal conditions. Using a general-purpose PC, the full private key can be reconstructed in ten minutes.



## 2024/513

* Title: Quantum Implementation and Analysis of SHA-2 and SHA-3
* Authors: Kyungbae Jang, Sejin Lim, Yujin Oh, Anubhab Baksi, Sumanta Chakraborty, Hwajeong Seo
* [Permalink](https://eprint.iacr.org/2024/513)
* [Download](https://eprint.iacr.org/2024/513.pdf)

### Abstract

Quantum computers have the potential to solve hard problems that are nearly impossible to solve by classical computers, this has sparked a surge of research to apply quantum technology and algorithm against the cryptographic systems to evaluate for its
quantum resistance. In the process of selecting post-quantum standards, NIST categorizes security levels based on the complexity that quantum computers would require to crack AES encryption (levels 1, 3, and 5) and SHA-2 or SHA-3 (levels 2 and 4).

In assessing the security strength of cryptographic algorithms against quantum threats, accurate predictions of quantum resources are crucial. Following the work of Jaques et al. in Eurocrypt 2020, NIST estimated security levels 1, 3, and 5,
corresponding to quantum circuit size for finding the key for AES-128, AES-192, and AES-256, respectively. This work has been recently followed-up by Huang et al. (Asiacrypt'22) and Liu et al. (Asiacrypt'23). However, for levels 2 and 4, which relate to
the collision finding for the SHA-2 and SHA-3 hash functions, quantum attack complexities are probably not well-studied.

In this paper, we present novel techniques for optimizing the quantum circuit implementations for SHA-2 and SHA-3 algorithms in all the categories specified by NIST. After that, we evaluate the quantum circuits of target cryptographic hash functions for
quantum collision search. Finally, we define the optimal quantum attack complexity for levels 2 and 4, and comment on the security strength of the extended level. We present new concepts to optimize the quantum circuits at the component level and the
architecture level.



## 2024/514

* Title: Zero-Knowledge Proof Vulnerability Analysis and Security Auditing
* Authors: Xueyan Tang, Lingzhi Shi, Xun Wang, Kyle Charbonnet, Shixiang Tang, Shixiao Sun
* [Permalink](https://eprint.iacr.org/2024/514)
* [Download](https://eprint.iacr.org/2024/514.pdf)

### Abstract

Zero-Knowledge Proof (ZKP) technology marks a revolutionary advancement in the field of cryptography, enabling the verification of certain information ownership without revealing any specific details. This technology, with its paradoxical yet powerful
characteristics, provides a solid foundation for a wide range of applications, especially in enhancing the privacy and security of blockchain technology and other cryptographic systems. As ZKP technology increasingly becomes a part of the blockchain
infrastructure, its importance for security and integrity becomes more pronounced. However, the complexity of ZKP implementation and the rapid iteration of the technology introduce various vulnerabilities, challenging the privacy and security it aims to
offer.

This study bases on the integrity, soundness, and zero-knowledge properties of ZKP to meticulously classify existing vulnerabilities and deeply explores multiple categories of vulnerabilities, including integrity issues, soundness problems, information
leakage, and non-standardized cryptographic implementations. Furthermore, we propose a set of defense strategies that include a rigorous security audit process and a robust distributed network security ecosystem. This audit strategy employs a divide-and-
conquer approach, segmenting the project into different levels, from the application layer to the platform-nature infrastructure layer, using threat modeling, linear code checking, and internal cross-review, among other means, aimed at comprehensively
identifying vulnerabilities in ZKP circuits, revealing design flaws in ZKP applications, and accurately identifying inaccuracies in the integration process of ZKP primitives.



## 2024/515

* Title: Inject Less, Recover More: Unlocking the Potential of Document Recovery in Injection Attacks Against SSE
* Authors: Manning Zhang, Zeshun Shi, Huanhuan Chen, Kaitai Liang
* [Permalink](https://eprint.iacr.org/2024/515)
* [Download](https://eprint.iacr.org/2024/515.pdf)

### Abstract

Searchable symmetric encryption has been vulnerable to inference attacks that rely on uniqueness in leakage patterns. However, many keywords in datasets lack distinctive leakage patterns, limiting the effectiveness of such attacks. The file injection
attacks, initially proposed by Cash et al. (CCS 2015), have shown impressive performance with 100% accuracy and no prior knowledge requirement. Nevertheless, this attack fails to recover queries with underlying keywords not present in the injected files.
To address these limitations, our research introduces a novel attack strategy called LEAP-Hierarchical Fusion Attack (LHFA) that combines the strengths of both file injection attacks and inference attacks. Before initiating keyword injection, we
introduce a new approach for inert/active keyword selection. In the phase of selecting injected keywords, we focus on keywords without unique leakage patterns and recover them, leveraging their presence for document recovery. Our goal is to achieve an
amplified effect in query recovery. We demonstrate a minimum query recovery rate of 1.3 queries per injected keyword with a 10% data leakage of a real-life dataset, and initiate further research to overcome challenges associated with non-distinctive
keywords.



## 2024/516

* Title: Similar Data is Powerful: Enhancing Inference Attacks on SSE with Volume Leakages
* Authors: Björn Ho, Huanhuan Chen, Zeshun Shi, Kaitai Liang
* [Permalink](https://eprint.iacr.org/2024/516)
* [Download](https://eprint.iacr.org/2024/516.pdf)

### Abstract

Searchable symmetric encryption (SSE) schemes provide users with the ability to perform keyword searches on encrypted databases without the need for decryption. While this functionality is advantageous, it introduces the potential for inadvertent
information disclosure, thereby exposing SSE systems to various types of attacks. In this work, we introduce a new inference attack aimed at enhancing the query recovery accuracy of RefScore (presented at USENIX 2021). The proposed approach capitalizes
on both similar data knowledge and an additional volume leakage as auxiliary information, facilitating the extraction of keyword matches from leaked data. Empirical evaluations conducted on multiple real-world datasets demonstrate a notable enhancement
in query recovery accuracy, up to 19.5%. We also analyze the performance of the proposed attack in the presence of diverse countermeasures.



## 2024/517

* Title: Fast pairings via biextensions and cubical arithmetic
* Authors: Damien Robert
* [Permalink](https://eprint.iacr.org/2024/517)
* [Download](https://eprint.iacr.org/2024/517.pdf)

### Abstract

Biextensions associated to line bundles on abelian varieties allows to reinterpret the usual Weil, Tate, Ate, optimal Ate, \ldots, pairings as monodromy pairings. We introduce a cubical arithmetic, derived from the canonical cubical torsor structure of
these line bundles, to obtain an efficient arithmetic of these biextensions.

This unifies and extends Miller's standard algorithm to compute pairings along with other algorithms like elliptic nets and theta functions, and allows to adapt these algorithms to pairings on any model of abelian varieties with a polarisation $\Phi_D$,
as long as we have an explicit theorem of the square for $D$.

In particular, we give explicit formulas for the arithmetic of the biextension (and cubical torsor structure) associated to the divisor $D=2(0_E)$ on an elliptic curve. We derive very efficient pairing formulas on elliptic curves and Kummer lines.
Notably for generic pairings on Montgomery curves, our cubical biextension ladder algorithm to compute pairings costs only $15M$ by bits, which as far as I know is faster than any pairing doubling formula in the literature.



## 2024/518

* Title: Software-Defined Cryptography: A Design Feature of Cryptographic Agility
* Authors: Jihoon Cho, Changhoon Lee, Eunkyung Kim, Jieun Lee, Beumjin Cho
* [Permalink](https://eprint.iacr.org/2024/518)
* [Download](https://eprint.iacr.org/2024/518.pdf)

### Abstract

Cryptographic agility, or crypto-agility, is a design feature that enables agile updates to new cryptographic algorithms and standards without the need to modify or replace the surrounding infrastructure. This paper examines the prerequisites for crypto-
agility and proposes its desired design feature. More specifically, we investigate the design characteristics of widely deployed cybersecurity paradigms, i.e., zero trust, and apply its design feature to crypto-agility, achieving greater visibility and
automation in cryptographic management.



## 2024/519

* Title: On implementation of Stickel's key exchange protocol over max-min and max-$T$ semirings
* Authors: Sulaiman Alhussaini, Serge˘ı Sergeev
* [Permalink](https://eprint.iacr.org/2024/519)
* [Download](https://eprint.iacr.org/2024/519.pdf)

### Abstract

Given that the tropical Stickel protocol and its variants are all vulnerable to the generalized Kotov-Ushakov attack, we suggest employing the max-min semiring and, more generally, max-$T$ semiring where the multiplication is based on a $T-$norm, as a
framework to implement the Stickel protocol. While the Stickel protocol over max-min semiring or max-$T$ semiring remains susceptible to a form of Kotov-Ushakov attack, we demonstrate that it exhibits significantly increased resistance against this
attack when compared to the tropical (max-plus) implementation.



## 2024/520

* Title: A note on securing insertion-only Cuckoo filters
* Authors: Fernando Virdia, Mia Filić
* [Permalink](https://eprint.iacr.org/2024/520)
* [Download](https://eprint.iacr.org/2024/520.pdf)

### Abstract

We describe a small tweak to Cuckoo filters that allows securing them under insertions using the techniques from Filić et al. (ACM CCS 2022), without the need for an outer PRF call.



## 2024/521

* Title: LIT-SiGamal: An efficient isogeny-based PKE based on a LIT diagram
* Authors: Tomoki Moriya
* [Permalink](https://eprint.iacr.org/2024/521)
* [Download](https://eprint.iacr.org/2024/521.pdf)

### Abstract

In this paper, we propose a novel isogeny-based public key encryption (PKE) scheme named LIT-SiGamal. This is based on a LIT diagram and SiGamal. SiGamal is an isogeny-based PKE scheme that uses a commutative diagram with an auxiliary point. LIT-SiGamal
uses a LIT diagram which is a commutative diagram consisting of large-degree horizontal isogenies and relatively small-degree vertical isogenies, while the original SiGamal uses a CSIDH diagram.

A strength of LIT-SiGamal is efficient encryption and decryption. QFESTA is an isogeny-based PKE scheme proposed by Nakagawa and Onuki, which is a relatively efficient scheme in isogeny-based PKE schemes. In our experimentation with our proof-of-concept
implementation, the computational time of the encryption of LIT-SiGamal is as efficient as that of QFESTA, and that of the decryption of LIT-SiGamal is about $5$x faster than that of QFESTA.



## 2024/522

* Title: Cryptanalysis of Secure and Lightweight Conditional Privacy-Preserving Authentication for Securing Traffic Emergency Messages in VANETs
* Authors: Mahender Kumar
* [Permalink](https://eprint.iacr.org/2024/522)
* [Download](https://eprint.iacr.org/2024/522.pdf)

### Abstract

In their paper, Wei et al. proposed a lightweight protocol for conditional privacy-preserving authentication in VANET. The protocol aims to achieve ultra-low transmission delay and efficient system secret key (SSK) updating. Their protocol uses a
signature scheme with message recovery to authenticate messages. This scheme provides security against adaptively chosen message attacks. However, our analysis reveals a critical vulnerability in the scheme. It is susceptible to replay attacks, meaning a
malicious vehicle can replay a message multiple times at different timestamps. This action undermines the overall effectiveness of conditional privacy. We suggest possible solutions to address these vulnerabilities and enhance the security of VANET
communication.



## 2024/523

* Title: Unbindable Kemmy Schmidt: ML-KEM is neither MAL-BIND-K-CT nor MAL-BIND-K-PK
* Authors: Sophie Schmieg
* [Permalink](https://eprint.iacr.org/2024/523)
* [Download](https://eprint.iacr.org/2024/523.pdf)

### Abstract

In "Keeping up with the KEMs" Cremers et al. introduced various binding models for KEMs. The authors show that ML-KEM is LEAK-BIND-K-CT and LEAK-BIND-K-PK, i.e. binding the ciphertext and the public key in the case of an adversary having access, but not
being able to manipulate the key material. They further conjecture that ML-KEM also has MAL-BIND-K-PK, but not MAL-BIND-K-CT, the binding of public key or ciphertext to the shared secret in the case of an attacker with the ability to manipulate the key
material.
This short paper demonstrates that ML-KEM does neither have MALBIND-K-CT nor MAL-BIND-K-PK, due to the attacker being able to produce mal-formed private keys, giving concrete examples for both. We also suggest mitigations, and sketch a proof for binding
both ciphertext and public key when the attacker is not able to manipulate the private key as liberally.



## 2024/524

* Title: A Time-Space Tradeoff for the Sumcheck Prover
* Authors: Alessandro Chiesa, Elisabetta Fedele, Giacomo Fenzi, Andrew Zitek-Estrada
* [Permalink](https://eprint.iacr.org/2024/524)
* [Download](https://eprint.iacr.org/2024/524.pdf)

### Abstract

The sumcheck protocol is an interactive protocol for verifying the sum of a low-degree polynomial over a hypercube. This protocol is widely used in practice, where an efficient implementation of the (honest) prover algorithm is paramount. Prior work
contributes highly-efficient prover algorithms for the notable special case of multilinear polynomials (and related settings): [CTY11] uses logarithmic space but runs in superlinear time; in contrast, [VSBW13] runs in linear time but uses linear space.
In this short note, we present a family of prover algorithms for the multilinear sumcheck protocol that offer new time-space tradeoffs. In particular, we recover the aforementioned algorithms as special cases. Moreover, we provide an efficient
implementation of the new algorithms, and our experiments show that the asymptotics translate into new concrete efficiency tradeoffs.



## 2024/525

* Title: Privacy Preserving Biometric Authentication for Fingerprints and Beyond
* Authors: Marina Blanton, Dennis Murphy
* [Permalink](https://eprint.iacr.org/2024/525)
* [Download](https://eprint.iacr.org/2024/525.pdf)

### Abstract

Biometric authentication eliminates the need for users to remember secrets and serves as a convenient mechanism for user authentication. Traditional implementations of biometric-based authentication store sensitive user biometry on the server and the
server becomes an attractive target of attack and a source of large-scale unintended disclosure of biometric data. To mitigate the problem, we can resort to privacy-preserving computation and store only protected biometrics on the server. While a variety
of secure computation techniques is available, our analysis of privacy-preserving biometric computation and biometric authentication constructions revealed that available solutions fall short of addressing the challenges of privacy-preserving biometric
authentication. Thus, in this work we put forward new constructions to address the challenges.

Our solutions employ a helper server and use strong threat models, where a client is always assumed to be malicious, while the helper server can be semi-honest or malicious. We also determined that standard secure multi-party computation security
definitions are insufficient to properly demonstrate security in the two-phase (enrollment and authentication) entity authentication application. We thus extend the model and formally show security in the multi-phase setting, where information can flow
from one phase to another and the set of participants can change between the phases. We implement our constructions and show that they exhibit practical performance for authentication in real time.



## 2024/526

* Title: Optimizing and Implementing Fischlin's Transform for UC-Secure Zero-Knowledge
* Authors: Yi-Hsiu Chen, Yehuda Lindell
* [Permalink](https://eprint.iacr.org/2024/526)
* [Download](https://eprint.iacr.org/2024/526.pdf)

### Abstract

Fischlin's transform (CRYPTO 2005) is an alternative to the Fiat-Shamir transform that enables straight-line extraction when proving knowledge. In this work we focus on the problem of using the Fischlin transform to construct UC-secure zero-knowledge
from Sigma protocols, since UC security -- that guarantees security under general concurrent composition -- requires straight-line (non-rewinding) simulators. We provide a slightly simplified transform that is much easier to understand, and present
algorithmic and implementation optimizations that significantly improve the running time. It appears that the main obstacles to the use of Fischlin in practice is its computational cost and implementation complexity (with multiple parameters that need to
be chosen). We provide clear guidelines and a simple methodology for choosing parameters, and show that with our optimizations the running-time is far lower than expected. For just one example, on a 2023 MacBook, the cost of proving the knowledge of
discrete log with Fischlin is only 0.41ms (on a single core). We also extend the transform so that it can be applied to batch proofs, and show how this can be much more efficient than individually proving each statement. As a contribution of independent
interest, we present a new algorithm for polynomial evaluation on any series of sequential points that does not require roots of unity. We hope that this paper will both encourage and help practitioners implement the Fischlin transform where relevant.



## 2024/528

* Title: The solving degrees for computing Gröbner bases of affine semi-regular polynomial sequences
* Authors: Momonari Kudo, Kazuhiro Yokoyama
* [Permalink](https://eprint.iacr.org/2024/528)
* [Download](https://eprint.iacr.org/2024/528.pdf)

### Abstract

Determining the complexity of computing Gröbner bases is an important problem both in theory and in practice, and for that the solving degree plays a key role. In this paper, we study the solving degrees of affine semi-regular sequences and their
homogenized sequences. Some of our results are considered to give mathematically rigorous proofs of the correctness of methods for computing Gröbner bases of the ideal generated by an affine semi-regular sequence. This paper is a sequel of the authors’
previous work and gives additional results on the solving degrees and important behaviors of Gröbner basis computation.



## 2024/529

* Title: Fully Homomorphic Training and Inference on Binary Decision Tree and Random Forest
* Authors: Hojune Shin, Jina Choi, Dain Lee, Kyoungok Kim, Younho Lee
* [Permalink](https://eprint.iacr.org/2024/529)
* [Download](https://eprint.iacr.org/2024/529.pdf)

### Abstract

This paper introduces a new method for training decision trees and random forests using CKKS homomorphic encryption (HE) in cloud environments, enhancing data privacy from multiple sources. The innovative Homomorphic Binary Decision Tree (HBDT) method
utilizes a modified Gini Impurity index (MGI) for node splitting in encrypted data scenarios. Notably, the proposed training approach operates in a single cloud security domain without the need for decryption, addressing key challenges in privacy-
preserving machine learning.
We also propose an efficient method for inference utilizing only addition for path evaluation even when both models and inputs are encrypted, achieving O(1) multiplicative depth.
Experiments demonstrate that this method surpasses the previous study by Akavia et al.'s by at least 3.7 times in the speed of inference. The study also expands to privacy-preserving random forests, with GPU acceleration ensuring feasibly efficient
performance in both training and inference.



## 2024/530

* Title: An efficient key generation algorithm for GR-NTRU over dihedral group * Authors: Vikas Kumar, Ali Raya, Aditi Kar Gangopadhyay
* [Permalink](https://eprint.iacr.org/2024/530)
* [Download](https://eprint.iacr.org/2024/530.pdf)

### Abstract

In this article, we focus on deriving an easily implementable and efficient method of constructing units of the group ring of dihedral group. We provide
a necessary and sufficient condition that relates the units in the group ring of dihedral group with the units in the group ring of cyclic group. Using this relation and the methods available for inversion in the group ring of the cyclic
group, we introduce an algorithm to construct units efficiently and check its performance experimentally.



## 2024/531

* Title: Avoiding Trusted Setup in Isogeny-based Commitments
* Authors: Gustave Tchoffo Saah, Tako Boris Fouotsa, Emmanuel Fouotsa, Célestin Nkuimi-Jugnia
* [Permalink](https://eprint.iacr.org/2024/531)
* [Download](https://eprint.iacr.org/2024/531.pdf)

### Abstract

In 2021, Sterner proposed a commitment scheme based on supersingular isogenies. For this scheme to be binding, one relies on a trusted party to generate a starting supersingular elliptic curve of unknown endomorphism ring. In fact, the knowledge of the
endomorphism ring allows one to compute an endomorphism of degree a power of a given small prime. Such an endomorphism can then be split into two to obtain two different messages with the same commitment. This is the reason why one needs a curve of
unknown endomorphism ring, and the only known way to generate such supersingular curves is to rely on a trusted party or on some expensive multiparty computation. We observe that if the degree of the endomorphism in play is well chosen, then the
knowledge of the endomorphism ring is not sufficient to efficiently compute such an endomorphism and in some particular cases, one can even prove that endomorphism of a certain degree do not exist. Leveraging these observations, we adapt Sterner's
commitment scheme in such a way that the endomorphism ring of the starting curve can be known and public. This allows us to obtain isogeny-based commitment schemes which can be instantiated without trusted setup requirements.



## 2024/532

* Title: Analysing Cryptography in the Wild - A Retrospective
* Authors: Martin R. Albrecht, Kenneth G. Paterson
* [Permalink](https://eprint.iacr.org/2024/532)
* [Download](https://eprint.iacr.org/2024/532.pdf)

### Abstract

We reflect on our experiences analysing cryptography deployed “in the wild” and give recommendations to fellow researchers about this process.



## 2024/533

* Title: HyCaMi: High-Level Synthesis for Cache Side-Channel Mitigation
* Authors: Heiko Mantel, Joachim Schmidt, Thomas Schneider, Maximilian Stillger, Tim Weißmantel, Hossein Yalame
* [Permalink](https://eprint.iacr.org/2024/533)
* [Download](https://eprint.iacr.org/2024/533.pdf)

### Abstract

Cache side-channels are a major threat to cryptographic implementations, particularly block ciphers. Traditional manual hardening methods transform block ciphers into Boolean circuits, a practice refined since the late 90s. The only existing automatic
approach based on Boolean circuits achieves security but suffers from performance issues. This paper examines the use of Lookup Tables (LUTs) for automatic hardening of block ciphers against cache side-channel attacks. We present a novel method combining
LUT-based synthesis with quantitative static analysis in our HyCaMi framework. Applied to seven block cipher implementations, HyCaMi shows significant improvement in efficiency, being 9.5$\times$ more efficient than previous methods, while effectively
protecting against cache side-channel attacks. Additionally, for the first time, we explore balancing speed with security by adjusting LUT sizes, providing faster performance with slightly reduced leakage guarantees, suitable for scenarios where absolute
security and speed must be balanced.



## 2024/534

* Title: CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
* Authors: Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
* [Permalink](https://eprint.iacr.org/2024/534)
* [Download](https://eprint.iacr.org/2024/534.pdf)

### Abstract

Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized
cryptographic model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models of cryptography yield rigorous guarantees but support at present only interactive proofs and/or restricted
classes of protocols (e.g., stateless ones). A promising approach is given by the computationally complete symbolic attacker (CCSA) model, formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic
guarantees by symbolic protocol analysis. The BC Logic is supported by a recently developed interactive theorem prover, namely Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert
knowledge both in the cryptographic space as well as on the reasoning side.

In this paper, we introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order formalization of protocol properties with
tailored handling of subterm relations. As such, we overcome the burden of interactive proving in higher-order logic and automatically establish soundness of cryptographic protocols using only first-order reasoning. Our first-order encoding of
cryptographic protocols is challenging for various reasons. On the theoretical side, we restrict full first-order logic with cryptographic axioms to ensure that, by losing the expressivity of the higher-order BC Logic, we do not lose soundness of
cryptographic protocols in our first-order encoding. On the practical side, CryptoVampire integrates dedicated proof techniques using first-order saturation algorithms and heuristics, which all together enable leveraging the state-of-the-art Vampire
first-order automated theorem prover as the underlying proving engine of CryptoVampire. Our experimental results showcase the effectiveness of CryptoVampire as a standalone verifier as well as in terms of automation support for Squirrel.



## 2024/535

* Title: NodeGuard: A Highly Efficient Two-Party Computation Framework for Training Large-Scale Gradient Boosting Decision Tree
* Authors: Tianxiang Dai, Yufan Jiang, Yong Li, Fei Mei
* [Permalink](https://eprint.iacr.org/2024/535)
* [Download](https://eprint.iacr.org/2024/535.pdf)

### Abstract

The Gradient Boosting Decision Tree (GBDT) is a well-known machine learning algorithm, which achieves high performance and outstanding interpretability in real-world scenes such as fraud detection, online marketing and risk management. Meanwhile, two
data owners can jointly train a GBDT model without disclosing their private dataset by executing secure Multi-Party Computation (MPC) protocols. In this work, we propose NodeGuard, a highly efficient two party computation (2PC) framework for large-scale
GBDT training and inference. NodeGuard guarantees that no sensitive intermediate results are leaked in the training and inference. The efficiency advantage of NodeGuard is achieved by applying a novel keyed bucket aggregation protocol, which optimizes
the communication and computation complexity globally in the training. Additionally, we introduce a probabilistic approximate division protocol with an optimization for re-scaling, when the divisor is publicly known. Finally, we compare NodeGuard to
state-of-the-art frameworks, and we show that NodeGuard is extremely efficient. It can improve the privacy preserving GBDT training performance by a factor of 5.0 to 131 in LAN and 2.7 to 457 in WAN.



## 2024/536

* Title: Highly-Effective Backdoors for Hash Functions and Beyond
* Authors: Mihir Bellare, Doreen Riepel, Laura Shea
* [Permalink](https://eprint.iacr.org/2024/536)
* [Download](https://eprint.iacr.org/2024/536.pdf)

### Abstract


[continued in next message]

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)