Cryptology ePrint Archive
Not a member yet
24907 research outputs found
Sort by
Universally Composable Password-Hardened Encryption
Get PDFPassword-Hardened Encryption (PHE) protects against offline brute-force attacks by involving an external ratelimiter that enforces rate-limited decryption without learning passwords or keys. Threshold Password-Hardened Encryption (TPHE), introduced by Brost et al. (CCS’20), distributes this trust among multiple ratelimiters. Despite its promise, the security foundations of TPHE remain unclear. We make three contributions:
(1) We uncover a flaw in the proof of Brost et al.’s TPHE scheme, which invalidates its claimed security and leaves the guarantees of existing constructions uncertain;
(2) We provide the first universal composability (UC) formalization of PHE and TPHE, unifying previous fragmented models and supporting key rotation, an essential feature for long-term security and related primitives such as updatable encryption;
(3) We present the first provably secure TPHE scheme, which is both round-optimal and UC-secure, thus composable in real-world settings; and we implement and evaluate our protocol, demonstrating practical efficiency that outperforms prior work in realistic WAN scenarios
Haystack ciphers: White-box countermeasures as Symmetric encryption
Get PDFIn the area of white-box cryptography implementations, many existing protections are susceptible to attacks derived from physical cryptanalysis, which can be applied with minimal human effort and no prior design knowledge. The absence of a clear and comprehensive security model hinders the development of effective countermeasures against these attacks.
We introduce the Haystack ciphers, a formal model for the security of white-box countermeasures against such attacks. In this model, the countermeasures are represented simply as symmetric-key encryption schemes. We show that their chosen-plaintext (IND-CPA) security is closely related to the resistance of the countermeasures against computational trace-based attacks. Similarly, their chosen-ciphertext (IND-CCA) security is closely associated with the resistance against fault injection attacks in the white-box model.
Secure Haystack ciphers constitute the next formal milestone for advancing white-box designs and countermeasures, the minimal requirement that is not currently clearly achieved but is plausibly feasible with available tools.
We review the white-box literature with respect to our model and bridge the gap between white-box and fault attacks, which are very powerful but were only partially considered in the white-box literature so far. We study known fault protections from the physical cryptography literature and present new fault attacks in the white-box setting, which raises the need and shapes the requirements for future secure countermeasures against fault attacks
Generic Anonymity Wrapper for Messaging Protocols
Get PDFModern messengers use advanced end-to-end encryption protocols to protect message content even if user secrets are ever temporarily exposed. Yet, encryption alone does not prevent user tracking, as protocols often attach metadata, such as sequence numbers, public keys, or even plain user identifiers. This metadata reveals the social network as well as communication patterns between users. Existing protocols that hide metadata in Signal (i.e., Sealed Sender), for MLS-like constructions (Hashimoto et al., CCS 2022), or in mesh networks (Bienstock et al., CCS 2023) are relatively inefficient or specially tailored for only particular settings. Moreover, all existing practical solutions reveal crucial metadata upon exposures of user secrets.
In this work, we introduce a formal definition of Anonymity Wrappers (AW) that generically hide metadata of underlying two-party and group messaging protocols. Our definition captures forward and post-compromise anonymity as well as authenticity in the presence of temporary state exposures. Inspired by prior wrapper designs, the idea of our provably secure AW construction is to use shared keys of the underlying wrapped (group) messaging protocols to derive and continuously update symmetric keys for hiding metadata. Beyond hiding metadata on the wire, we also avoid and hide structural metadata in users\u27 local states for stronger anonymity upon their exposure.
We implement our construction, evaluate its performance, and provide a detailed comparison with Signal\u27s current approach based on Sealed Sender: Our construction reduces the wire size of small 1:1 messages from 441 bytes to 114 bytes. For a group of 100 members, it reduces the wire size of outgoing group messages from 7240 bytes to 155 bytes. We see similar improvements in computation time for encryption and decryption, but these improvements come with substantial storage costs for receivers. For this reason, we develop extensions with a Bloom filter for compressing the receiver storage. Based on this, Signal considers deploying our solution
IND-CPA-D and KR-D Security With Reduced Noise from the HintLWE Problem
Get PDFApproximate Homomorphic Encryption (AHE), introduced by Cheon et al. [CKKS17] offers a powerful solution for encrypting real-valued data by relaxing the correctness requirement and allowing small decryption errors. Existing constructions from (Ring) Learning with Errors achieve standard IND-CPA security, but this does not fully capture scenarios where an adversary observes decrypted outputs. Li and Micciancio [LiMic21] showed that when decryptions are passively leaked, these schemes become vulnerable to practical key recovery attacks even against honest-but-curious attackers. They formalise security when decryptions are shared with new notions of IND-CPA-D and KR-D security.
We propose new techniques to achieve provable IND-CPA-D and KR-D security for AHE, while adding substantially less additional decryption noise than the prior provable results. Our approach hinges on refined game-hopping tools in the bit-security framework, which allow bounding security loss with a lower noise overhead. We also give a noise-adding strategy independent of the number of oracle queries, removing a costly dependence inherent in the previous solution.
Beyond generic noise-flooding, we show that leveraging the recently introduced HintLWE problem [KLSS23] can yield particularly large security gains for AHE ciphertexts that are the result of rescaling , a common operation in CKKS. Our analysis uses the fact that rescale-induced noise amounts to a linear ``hint on the secret to enable a tighter reduction to LWE (via HintLWE). In many practical parameter regimes where the rescaling noise dominates, our results imply an additional precision loss of as little as two bits is sufficient to restore a high level of security against passive key-recovery attacks for standard parameters.
Overall, our results enable a provably secure and efficient real-world deployment of Approximate Homomorphic Encryption in scenarios with realistic security requirements
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt
Get PDFWe propose a hybrid formal verification approach that combines high-level deductive reasoning and circuit-based reasoning and apply it to highly optimized cryptographic assembly code. Our approach permits scaling up formal verifi- cation in two complementary directions: 1) it reduces the proof effort required for low-level functions where the computation logics are obfuscated by the intricate use of architecture-specific instructions and 2) it permits amortizing the effort of proving one implementation by using equivalence checking to propagate the guarantees to other implementations of the same computation using different optimizations or targeting different architectures. We demonstrate our approach via an extension to the EasyCrypt proof assistant and by revisiting formally verified implementations of ML-KEM in Jasmin. As a result, we obtain the first formally verified implementation of ML-KEM that offers performance comparable to the fastest non-verified implementation in x86-64 architectures
Meet-in-the-Middle Attacks on Full ChiLow-32
Get PDFThis work presents the first full-round attacks on ChiLow-32 and ChiLow-40, two tweakable low-latency block ciphers presented at EUROCRYPT\u2725.
We first describe a straightforward Meet-in-the-Middle attack on full ChiLow-32 with multiple known plaintext-ciphertext pairs.To improve this attack, we carefully evaluate the dependencies in ChiLow, to remove equivalent keys and reduce the number of key guesses. With a novel method to propagate differences through multiple ChiChi functions and to map out the state-dependencies, we optimize the attack on ChiLow-32.This results in an attack with time complexity using known plaintext-ciphertext pairs, and an attack with time complexity using chosen ciphertexts.
To attack ChiLow-40, we introduce a method that uses multiple sets of chosen plaintexts for different tweaks to reduce the amount of key material that has to be guessed in the Meet-in-the-Middle step. The final time complexity of this attack is with chosen plaintexts. All of our attacks are within ChiLow\u27s security model, and are currently the best and only known key recovery attacks on full-round ChiLow-32 and ChiLow-40
Round-Efficient Composable Two-Party Quantum Computation
Get PDFWe study secure computation in the plain model against fully concurrent quantum adversaries. While classical simulation-based notions --- such as Super-Polynomial Simulation (SPS) security --- have enabled meaningful forms of concurrent security, very little is known about their quantum counterparts, particularly under standard polynomial-time hardness assumptions.
Our main result is the first post-quantum two-party computation protocol that achieves concurrent SPS security, based solely on the minimal assumption of semi-honest post-quantum oblivious transfer (PQ-OT). Moreover, our protocol has constant round complexity when the underlying PQ-OT protocol is constant-round. This can be viewed as a post-quantum analog of the classical result by Garg et al. [Eurocrypt\u2712], but with a crucial difference: our security proof completely avoids rewinding, making it suitable for quantum settings where rewinding is notoriously challenging due to the no-cloning principle.
By leveraging a compiler of Bartusek et al. [Crypto\u2721], we further extend our result to the fully quantum setting, yielding the first constant-round concurrent SPS two-party computation for quantum functionalities in the plain model.
Additionally, we construct a two-round, public-coin, concurrent SPS post-quantum zero-knowledge protocol for languages in , under the quantum polynomial-time hardness of LWE. This result is notable even in the classical setting
PriSrv+: Privacy and Usability-Enhanced Wireless Service Discovery with Fast and Expressive Matchmaking Encryption
Get PDFService discovery is a fundamental process in wireless networks, enabling devices to find and communicate with services dynamically, and is critical for the seamless operation of modern systems like 5G and IoT. This paper introduces PriSrv+, an advanced privacy and usability-enhanced service discovery protocol for modern wireless networks and resource-constrained environments. PriSrv+ builds upon PriSrv (NDSS\u2724), by addressing critical limitations in expressiveness, privacy, scalability, and efficiency, while maintaining compatibility with widely-used wireless protocols such as mDNS, BLE, and Wi-Fi.
A key innovation in PriSrv+ is the development of Fast and Expressive Matchmaking Encryption (FEME), the first matchmaking encryption scheme capable of supporting expressive access control policies with an unbounded attribute universe, allowing any arbitrary string to be used as an attribute. FEME significantly enhances the flexibility of service discovery while ensuring robust message and attribute privacy. Compared to PriSrv, PriSrv+ optimizes cryptographic operations, achieving 7.62 faster for encryption and 6.23 faster for decryption, and dramatically reduces ciphertext sizes by 87.33. In addition, PriSrv+ reduces communication costs by 87.33 for service broadcast and 86.64 for anonymous mutual authentication compared with PriSrv. Formal security proofs confirm the security of FEME and PriSrv+. Extensive evaluations on multiple platforms demonstrate that PriSrv+ achieves superior performance, scalability, and efficiency compared to existing state-of-the-art protocols
TACITA: Threshold Aggregation without Client Interaction
Get PDFSecure aggregation enables a central server to compute the sum of client inputs without learning any individual input, even in the presence of dropouts or partial participation. This primitive is fundamental to privacy-preserving applications such as federated learning, where clients collaboratively train models without revealing raw data.
We present a new secure aggregation protocol, TACITA, in the single-server setting that satisfies four critical properties simultaneously: (1) one-shot communication from clients with no per-instance setup, (2) input-soundness, i.e. the server cannot manipulate the ciphertexts, (3) constant-size communication per client, independent of the number of participants per-instance, and (4) robustness to client dropouts
Previous works on secure aggregation - Willow and OPA (CRYPTO\u2725) that achieve one-shot communication do not provide input soundness, and allow the server to manipulate the aggregation. They consequently do not achieve full privacy and only achieve Differential Privacy guarantees at best. We achieve full privacy at the cost of assuming a PKI. Specifically, TACITA relies on a novel cryptographic primitive we introduce and realize: succinct multi-key linearly homomorphic threshold signatures (MKLHTS), which enables verifiable aggregation of client-signed inputs with constant-size signatures.
To encrypt client inputs, we adapt the Silent Threshold Encryption (STE) scheme of Garg et al. (CRYPTO 2024) to support ciphertext-specific decryption and additive homomorphism.
We formally prove security in the Universal Composability framework and demonstrate practicality through an open-source proof-of-concept implementation, showing our protocol achieves scalability without sacrificing efficiency or requiring new trust assumptions
How Hard Can It Be to Formalize a Proof? Lessons from Formalizing CryptoBox Three Times in EasyCrypt
Get PDFProvable security is a cornerstone of modern cryptography, aiming to provide formal and precise security guarantees. However, for various reasons, security proofs are not always properly verified, possibly leading to unwarranted security claims and, in the worst case, deployment of insecure constructions. To further enhance trust and assurance, machine-checked cryptography makes these proofs more formal and rigorous. Unfortunately, the complexity of writing machine-verifiable proofs remains prohibitively high in many interesting use-cases. In this paper, we investigate the sources of this complexity, specifically examining how the style of security definitions influences the difficulty of constructing machine-verifiable proofs in the context of game-playing security.
Concretely, we present a new security proof for the generic construction of a PKAE scheme from a NIKE and AE scheme, written in a code-based, game-playing style à la Bellare and Rogaway, and compare it to the same proof written in the style of state-separating proofs, a methodology for developing modular game-playing security proofs. Additionally, we explore a third “blended” style designed to avoid anticipated difficulties with the formalization. Our findings suggest that the choice of definition style impacts proof complexity—including, we argue, in detailed pen-and-paper proofs—with trade-offs depending on the proof writer’s goals