International Association
for Cryptologic Research

The SandboxAQ Cybersecurity Group are looking for a Staff Software Engineer to join our R&D team. You will be a key player on a team of diverse experts, developing new features and tackling a wide array of challenges across our technology stack. Your responsibilities will involve a variety of complex technical domains, including systems-level programming, large-scale data analysis, and security automation. We are looking for a versatile engineer with deep cryptographic expertise and the ability to solve complex, systems-level problems across a variety of programming languages.

Key Responsibilities:

• Collaborate with R&D and Product stakeholders to prototype new capabilities and explore future features.
• Apply strong systems engineering skills to design and build proof-of-concept solutions for complex security challenges.
• Design and implement systems for managing and analyzing large-scale, security-related data.
• Write high-quality, reusable code for R&D projects across a variety of languages, such as Rust, Go, or Python.
• Conduct technical investigations and present findings that will help shape the company's strategic direction.
• Own greenfield projects from the initial design phase through to a working prototype.

Essential Skills & Experience:

• 5+ years of industry experience building, deploying, and maintaining complex software projects and data pipelines.
• Demonstrated mastery across multiple languages, with required expertise in a systems language (e.g., Rust, C++, Zig) and fluency in higher-level languages (e.g., Python, Golang, Kotlin).
• Deep engineering knowledge of symmetric and asymmetric cryptography, cryptographic protocols, and their real-world application.
• Proven ability to apply academic foundations to real-world engineering challenges.
• Strong analytical thinking and communication skills, with an ability to thrive in a collaborative, fast-paced environment.

Highly desired skills and experience include a PhD/MSc in Cryptography, Computer Science, or Mathematics. More information available on the jobs page.

Closing date for applications:

Contact: James Howe

More information: https://www.sandboxaq.com/careers-list?ashby_jid=357a6ee1-3fe1-44f3-838a-f81df8b4e044

Simula UiB (https://simula-uib.com) is a research institute in Cryptography and Information Theory located in Bergen, Norway. The Department of Cryptography is currently looking for two motivated candidates for postdoctoral researcher positions in Fully Homomorphic Encryption (FHE).

The successful candidates will work on two different projects named PREMAL and SECSHARE, respectively, in Håvard Raddum’s team. We are looking for candidates with a PhD degree in Cryptography, Computer Science, Mathematics, or a closely related field to work on the two projects. The focus of the two projects and the profile for their ideal candidates are described on the linked website where you apply (link below and in the headline).

The positions are both for a three-year period. Simula UiB currently has 11 early-career researchers working on a range of research problems in cryptography and information theory.

Simula UiB offers:

Excellent opportunities for conducting high-quality research as part of a highly competent and motivated team of researchers.

An informal, inclusive and international working environment.

Support for travel and opportunities to build international networks.

Modern office facilities, located at Marineholmen in the city centre of Bergen.

A competitive salary; starting salary from NOK 595 000.

Numerous employee benefits, including access to a company cabin, sponsored social events, an equipment budget, and a comprehensive travel/health insurance policy.

Relocation assistance, including complimentary Norwegian language courses.

Healthy wellness and work-life balance arrangements.

Deadline: 15 March 2026

Read more and apply at: https://www.simula.no/careers/job-openings/postdoctoral-fellows-in-fully-homomorphic-encryption-at-simula-uib

Closing date for applications:

Contact: Håvard Raddum

More information: https://www.simula.no/careers/job-openings/postdoctoral-fellows-in-fully-homomorphic-encryption-at-simula-uib

Homomorphic Encryption (HE) provides strong data privacy for cloud services but at the cost of prohibitive computational overhead. While GPUs have emerged as a practical platform for accelerating HE, there remains an order-of-magnitude energy-efficiency gap compared to specialized (but expensive) HE ASICs. This paper explores an alternate direction: leveraging existing AI accelerators, like Google's TPUs with coarse-grained compute and memory architectures, to offer a path toward ASIC-level energy efficiency for HE. However, this architectural paradigm creates a fundamental mismatch with SoTA HE algorithms designed for GPUs. These algorithms rely heavily on: (1) high-precision (32-bit) integer arithmetic to now run on a TPU's low-throughput vector unit, leaving its high-throughput low-precision (8-bit) matrix engine (MXU) idle, and (2) fine-grained data permutations that are inefficient on the TPU's coarse-grained memory subsystem. Consequently, porting GPU-optimized HE libraries to TPUs results in severe resource under-utilization and performance degradation. To tackle above challenges, we introduce CROSS, a compiler framework that systematically transforms HE workloads to align with the TPU's architecture. CROSS makes two key contributions: (1) Basis-Aligned Transformation (BAT), a novel technique that converts high-precision modular arithmetic into dense, low-precision (INT8) matrix multiplications, unlocking and improving the utilization of TPU's MXU for HE, and (2) Memory-Aligned Transformation (MAT), which eliminates costly runtime data reordering by embedding reordering into compute kernels through offline parameter transformation. CROSS (TPU v6e) achieves higher throughput per watt on NTT and HE operators than WarpDrive, FIDESlib, FAB, HEAP, and Cheddar, establishing AI ASIC as the SotA efficient platform for HE operators. Code: https://github.com/EfficientPPML/CROSS

Nearly all existing SNARK systems are optimized for arithmetic over finite fields. Using them to prove statements involving ring arithmetic, which underlies lattice-based cryptography and fully homomorphic encryption (FHE), incurs substantial overhead. Consequently, practical deployments of FHE often rely on the \textit{honest-but-curious} assumptions, leaving a gap in the verifiability of the FHE computation. Several recent works have explored zero-knowledge proofs tailored to lattice-based schemes, yet still suffer from high prover costs and limited scalability.

In this work, we introduce Dinocchio, the first distributed SNARK for rings with constant proof size and constant verification time. For a setting with $m$ sub-provers, Dinocchio achieves an approximately $m$-fold speedup in prover time compared to Rinocchio (JoC'23), while preserving the constant verification time independent of $m$.

We demonstrate the practicality of Dinocchio through matrix multiplication, which is a crucial building block to large-scale lattice-based applications. With matrices of size $2^{12} \times 2^{12}$, the corresponding arithmetic circuit contains $\sim2^{32}$ constraints, which is beyond the reach of all existing works. Our microbenchmarks show that Dinocchio can generate a succinct proof in around $9.23$ hours with $128$ sub-provers, more than $108\times$ faster than the prior work, and the verifier completes the verification in under $16$ seconds.

Anonymous communication is essential for secure and private interactions over public networks. Existing solutions that provide provable anonymity rely on the so-called simple I/O setting, where every participant sends and receives the same number of messages, masking their true communication pattern. The only known way to enforce this setting is through dialing protocols. Such protocols establish pairwise conversations, but each recipient inevitably learns who attempted to contact them, violating sender anonymity, the guaranty that even the recipient cannot determine who attempted to contact them.

In this work, we introduce the notion of enhanced dialing protocols, a broad class of protocols that enforce the simple I/O setting. We also initiate the first formal study of such protocols with respect to sender anonymity. We introduce a framework that captures three key properties: security, correctness, and fairness. Within this framework, we present Fusion, a protocol that achieves perfect correctness and fairness while incurring only unavoidable leakage, and Fusion+, a differentially private variant that reduces this leakage at the cost of some correctness. Through theoretical analysis, we quantify the fundamental trade-off between privacy and correctness in Fusion+.

The Fujisaki-Okamoto transform is a popular solution to design post- quantum public key encryption schemes, or key encapsulation mechanisms. In order to ensure security against chosen-ciphertext attacks, it checks the validity of ciphertexts by re-encrypting decrypted messages. This operation in turn leads to severe side- channel weaknesses, because the re-encrypted messages can be made key-dependent. Hence, distinguishing them thanks to leakage is sufficient to extract (long-term) secret key information. As a result, recent works suggested to ensure the validity of ciphertexts by other means than re-encryption. For now, the main candidate for this purpose, integrated in the Polka encryption scheme (PKC 2023) and analyzed more generically by Hövelmanns et al. (EUROCRYPT 2025), is to use continuous norm checks through the decryption process. In this paper, we evaluate the extent to which replacing the FO-transform by such norm checks helps resistance against leakage. Negatively, we exhibit new attack vectors that were not anticipated in previous (heuristic) analyzes. Positively, we observe that the removal of the FO-transform nevertheless reduces the attack surface and we identify possible tracks to further minimize it. Overall, our results therefore shed light on the challenge of designing post-quantum public-key encryption schemes, or key encapsulation mechanisms, that can be efficiently protected against side-channel attacks. We hope they can inform theory about leakage sources that could be better taken over by design, to develop new schemes allowing a scarcer use of implementation-level countermeasures.

In this work, we present Hachi, a concretely efficient multilinear polynomial commitment scheme that offers succinct proof sizes of $\mathrm{poly}(\ell,\lambda)$ and achieves a “square-root” verifier time complexity of $\tilde{O}(\sqrt{2^\ell \lambda})$ for $\ell$-variate polynomials under the Module-SIS assumption. Compared to the current state-of-the-art scheme, Greyhound (CRYPTO~2024), Hachi provides an asymptotic improvement of $\tilde{O}(\lambda)$ in verification time, which translates into a practical 12.5-fold speedup, while maintaining compact proofs of approximately $55$ KB.

To improve the verification time, we adopt the sumcheck protocol. Note that the standard sumcheck has efficiency bottlenecks for lattice-based constructions, since lattice operations are usually performed over power-of-two cyclotomic rings $\mathbf{R}_{q} := \mathbb{Z}_q[X]/(X^d + 1)$. To address this challenge, we provide a novel approach that integrates Greyhound with the ring-switching idea proposed by Huang, Mao and Zhang (ePrint 2025). Surprisingly, under this approach, the verifier does not need to perform any multiplication over $\mathbf{R}_{q}$, enabling a much faster verification time. This technique could be of independent interest for building lattice-based SNARKs, particularly for achieving faster verification.

As a separate contribution, we introduce a generic reduction that converts polynomial evaluation proofs over extension fields $\mathbb{F}_{q^k}$ (under suitable parameter regimes) into equivalent statements over cyclotomic rings $\mathbf{R}_{q}$. This reduction is compatible with existing lattice-based polynomial commitment schemes and can be integrated as a modular enhancement to broaden applicability to statements over extension fields.

The Module Learning With Errors ($\mathsf{MLWE}$) problem is the fundamental hardness assumption underlying the key encapsulation and signature schemes ML-KEM and ML-DSA, which have been selected by NIST for post-quantum cryptography standardization. Understanding its quantum hardness is crucial for assessing the security of these standardized schemes.

Inspired by the equivalence between $\mathsf{LWE}$ and Extrapolated Dihedral Cosets Problem ($\mathsf{EDCP}$) in [Brakerski, Kirshanova, Stehlé and Wen, PKC 2018], we show that the $\mathsf{MLWE}$ problem is as hard as a variant of the $\mathsf{EDCP}$, which we refer to as the structured $\mathsf{EDCP}$ ($\mathsf{stEDCP}$). This extension from $\mathsf{EDCP}$ to $\mathsf{stEDCP}$ relies crucially on the algebraic structure of the ring underlying $\mathsf{MLWE}$: the extrapolation depends not only on the noise rate, but also on the ring’s degree. In fact, an $\mathsf{stEDCP}$ state forms a superposition over an exponential (in ring degree) number of possibilities. Our equivalence result holds for $\mathsf{MLWE}$ defined over power-of-two cyclotomic rings with constant module rank, a setting of particular relevance in cryptographic applications. Moreover, we present a reduction from $\mathsf{stEDCP}$ to $\mathsf{EDCP}$. Therefore, to analyze the quantum hardness of $\mathsf{MLWE}$, it may be advantageous to study $\mathsf{stEDCP}$, which might be easier than $\mathsf{EDCP}$.

In this work, we present a practical fault-injection attack against the current Unbalanced Oil and Vinegar signature scheme non-deterministic implementation that enables complete secret key recovery from a single faulty signature, given one prior fault-free signature. By applying fault injection to disrupt the mixing of the vinegar and oil components during signature generation, the secret key can be recovered directly from the faulty signature. We validate the attack experimentally on a real device using an electromagnetic fault injection setup, establishing the required glitch in practice rather than through simulation. Our experimental results indicate that a single execution of the attack achieves a success rate exceeding 90%. Furthermore, we demonstrate the real-world feasibility of the attack by transferring the attack parameters to an architecturally equivalent target, requiring only minor recalibration. To the best of our knowledge, this is the first work to demonstrate an electromagnetic fault-injection attack in the context of multivariate-based signature schemes. Additionally, we discuss possible countermeasures to protect implementations of UOV-based schemes against such physical attacks.

Recent interest in fully homomorphic encryption (FHE) has motivated efforts to develop faster and more efficient homomorphic logic circuits. Currently, Torus FHE (TFHE) provides the fastest gate-level bootstrapping and enables homomorphic evaluation over encrypted bits. Prior works typically utilize standard Computer Aided Design (CAD) tools to synthesize TFHE-amenable gate-level netlists. However, the logic resynthesis and technology mapping stages of these tools are designed for reducing area and power rather than bootstrapped gates, which leads to suboptimal netlists for homomorphic execution. In this work, we introduce BOLT, a TFHE-amenable CAD synthesis framework that explicitly targets reductions in bootstrapping depth. BOLT employs a bootstrapping-aware logic resynthesis stage to rewrite sub-networks in the input netlist into functionally equivalent forms that can be evaluated with a single bootstrapping operation. Following this, our bootstrapping-aware technology mapping stage incorporates a custom simulated annealing-based scheduler to decide whether each transformed sub-network should replace its original counterpart immediately or be deferred to enable better future opportunities. Through extensive evaluation on standard benchmark circuits, BOLT achieves significant improvements in homomorphic evaluation time, delivering $8\times$ speedup over the current state-of-the-art and $31\times$ speedup over prior work on FHEW-like schemes.

At EUROCRYPT 2020, Hosoyamada and Sasaki obtained the first dedicated quantum collision attacks on hash functions reaching more rounds than the classical ones. Indeed, as the speedup of generic quantum collision search is less than quadratic, an attack based on Grover's search may become comparatively more efficient in the quantum setting.

In this paper, we focus on collision attacks on double-block length hash functions, and more precisely the Hirose compression function (HCF). At ToSC 2021, Chauhan et al. found a 10-round free-start collision attack on HCF-AES-256. At ToSC 2024, Lee and Hong corrected its complexity analysis. However, these two works are superseded by another result of Hirose and Kuwakado (IMACC 2021), which shows that for any $2n$-bit HCF hash function, a quantum free-start collision attack of complexity $\mathcal{O}(2^{n/2})$ exists. While both the works of Chauhan et al. and Lee and Hong are above this generic complexity, we find that a classical attack from Chen et al. (IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 2016) translates to a 9-round quantum attack on HCF-AES-256.

Next, we study the security of HCF against quantum collision attacks (not free-start). We use a generic strategy that transforms a partial preimage attack into a quantum collision attack, and give several applications on HCF hash functions: a 6-round attack on AES-256 and a 15-round attack on Romulus (based on Skinny), both exceeding the reach of classical attacks.

Side-channel attacks (SCAs) represent an important threat for the implementation of cryptographic algorithms. These attacks exploit the information leakage found in the physical magnitudes of hardware devices (e.g. current draw, electromagnetic emanation). Threshold Implementations (TIs) aim to mitigate SCAs by implementing a modified version of the algorithm that operates over randomized shares of its input and intermediate values. This strategy relies on the possibility of splitting the algorithm to be protected into sub-functions that satisfy certain properties about their dependence structure on the randomized shares. Non-complete set coverings (NCSCs) are combinatorial objects that can provide this dependence structure and guide the design of TIs. Given the desired order of protection $d$ and the algebraic degree $t$ of the functions to be implemented, for an NCSC to be useful, its cardinality $r$ should be small and similar to the number of input shares $s$.

This work contributes to the study of NCSCs for efficient TIs by finding smaller coverings and proving novel theoretical bounds on their cardinality. We present a new NCSC for the case $t=3,d=2$ that is optimal and NCSCs for the cases $t=3,d=3$ and $t=4,d=2$ whose sizes are close to the lower bounds. We also present new combinatorial properties of these coverings and an algorithm for the search of small NCSCs.

In november 2024, the Ethereum foundation (EF) issued a bounty program with challenges on Poseidon and Poseidon2. The goal of these challenges is to find CICO solutions on different round-reduced instances of Poseidon and Poseidon2, defined on different prime fields. We denote the four main instances Poseidon-256, Poseidon2-64, Poseidon2-31m and Poseidon2-31k. In the challenges, the goal is to solve CICO-1 for Poseidon-256 and Poseidon-64, and CICO-2 for Poseidon-31m and Poseidon-31k.

We found CICO solutions to the first 3 proposed instances of Poseidon2-31m and Poseidon2-31k, along with solutions for the first two Poseidon-256 instances. These solutions have been confirmed to be correct and eligible for bounty by the Ethereum fundation, except for the first instance of Poseidon-256, which was claimed by another team before us. In order to solve the instances of Poseidon2-31m and Poseidon2-31k, we used a new resultant-based approach, whereas our attacks on Poseidon-256 only relies on already-known univariate root finding.

Recent work at NDSS 2024 demonstrated that widely deployed NAT behaviors in Wi-Fi routers - including port preservation, insufficient reverse-path validation, and the absence of TCP window tracking enable off-path TCP hijacking attacks in NATed wireless networks. These attacks exploit design weaknesses in NAT gateway routers to detect whether some internal client behind the NAT maintains an active TCP connection with a target server and, upon detection, to disrupt or manipulate that connection. In this paper, we show that these behaviors have significantly broader privacy implications. We demonstrate that an off-path attacker can not only hijack active TCP connections but also accurately infer the private IP addresses of individual clients behind a NAT that are engaged in TCP commu- nication with a target server. Our attack operates under the same realistic assumptions as prior work, yet leverages previously unex- plored behaviors in NAT state management and TCP control-plane interactions to reconstruct the full client-side connection tuple. We evaluate our attack both in a controlled laboratory testbed and in a real-world Wi-Fi network. For SSH connections, our method reliably identifies the private IP addresses of connected clients and enables forcible termination of their TCP sessions. For HTTPS connections, although the attacker successfully terminates the un- derlying TCP connection, modern browsers rapidly re-establish a new connection using new ephemeral ports; nevertheless, our attack reveals the private IP addresses of the originating clients, ex- posing a persistent privacy leakage. Our findings demonstrate that off-path TCP hijacking attacks in NATed Wi-Fi networks pose a seri- ous and previously unrecognized threat to client privacy, extending well beyond connection disruption to enable deanonymization of internal hosts.

We study the cryptographic properties of sums of commutators of quaternions modulo $q$. We show that for certain parameters, the distribution of the sum of commutators of uniformly random elements with elements sampled from a discrete Gaussian is statistically close to uniform. We also give reductions from worst-case lattice problems such as SIVP to SIS-style problems defined using commutators on structured quaternionic lattices. Together these results indicate one-wayness and collision resistance of the sum-of-commutators function, under worst-case assumptions on lattices. We use this to develop a linearly homomorphic commitment scheme, dubbed `ABBA', which in many cases can be substituted for the widely-used Ajtai commitment scheme. We demonstrate the utility of the properties of commutation by replacing the Ajtai commitments used in Neo (a state-of-the-art folding scheme from lattices) with ABBA commitments, obtaining a 25% commitment size reduction and an almost equally efficient scheme.

Bridges, protocols that enforce a state transition on a destination ledger conditioned on an event on a source ledger, are central to modern DeFi. Conventional designs implicitly assume the source ledger event is publicly observable, an assumption that breaks with Layer-2 payment channels such as the Lightning Network, where state updates occur off-chain between counterparties and are invisible to others. This state of affairs advocates for new bridge designs for this setting.

This paper introduces OptiBridge, a bridge between a payment channel (e.g., Lightning Network) and a smart-contract blockchain (e.g., Ethereum) that preserves safety and liveness without adding trust assumptions and remains fully compatible with existing Lightning and Ethereum stacks. OptiBridge follows an optimistic path in the common case: two honest channel peers materialize the intended state on the destination chain by revealing a pre-agreed secret. To handle faults and adversarial behavior, OptiBridge provides a dispute path orchestrated by a more expressive contract that is deployed {only on demand}. An implementation demonstrates substantial cost savings in the optimistic case: compared to Alba (NDSS’25), the optimistic contract deployment uses $\sim 73\%$ less gas ($1.22$M vs. $4.51$M), and proof submission costs $40{,}107$ vs. $253{,}566$ gas; when disputes arise, the dispute contract deployment costs $2{,}785{,}514$ gas and the core dispute call is cheaper ($196{,}438$ vs.$515{,}860$). Our analysis shows that rational users strictly prefer the optimistic path, whereas the dispute mechanism prevents coin theft and imposes higher fees and delays on the deviator.

The quantum random oracle model (QROM) has become the de-facto model to analyze post-quantum security of practical cryptographic schemes which use hash functions. The quantum random permutation model (QRPM), on the other hand, has not enjoyed a similar level of success for studying permutation-based schemes. A main reason is that it lacks the features offered by the former model to enable security proofs: namely, query-recording and reprogramming.

In this work, we present a new approach to simulate bidirectional-query random permutation oracles using Feistel constructions which unlock the above two features in the QRPM. We then show the potential of our framework by: • Analyzing the post-quantum security of a recent variant of the Fiat-Shamir transformation — called duplex-sponge Fiat-Shamir (Chiesa and Orrù, TCC 2025) — which is deployed in the wild. • Recovering a meaningful quantum query lower bound for the double-sided zero search problem — the hardness of which was conjectured by Unruh, but has resisted many attempts until very recently — via a simpler approach that generalizes the compressed oracle technique (Zhandry, Crypto 2019) to the QRPM.

All in all, our work demonstrates how the "Feistel toolkit" enables us to achieve reprogramming and query-recording for quantum random permutations, thereby effectively bridging the gap between the QROM and the QRPM in terms of analyzing real-world post-quantum cryptographic schemes and relevant quantum query complexity problems.

A blind signature scheme is an interactive protocol that enables a user to obtain a signature on a message without revealing any information about the message–signature pair to the signer. Despite more than 40 years of research, all existing constructions suffer from at least two of the following limitations.

1. The protocol is not round-optimal, requiring more than two messages to be exchanged during the signature phase.

2. There is only game-based security and/or lack of composability with global and observable setup (i.e., there is a need for trusted parameters or to program random oracles).

3. There is a need (unlike regular signatures) of demanding hardness assumptions, especially when targeting post-quantum security.

In this work, we bypass prior results by showing how to blindly sign a message, simultaneously overcoming all of the above three limitations. Specifically, we construct a (Global) Universally Composable (UC), two-round (optimal) blind signature protocol that relies only on one-way functions (optimal), without trusted parameters. The only deviation from the plain model is the need for a global non-programmable random oracle (NPRO). Nicely, our scheme can be instantiated from a variety of assumptions believed to be post-quantum secure (e.g., AES). A central technical component of our scheme is the construction of a novel commitment scheme that enjoys a special (mild) form of composability, which may be of independent interest. Finally, we argue that a concrete instantiation of our scheme has signature sizes and communication complexity suitable for practical applications.

Recently, the notion of dynamic zk-SNARKs was introduced. A dynamic zk-SNARK augments a standard zk-SNARK with an efficient update algorithm. Given a valid source statement-witness pair $(x,w)$ together with a verifying proof $p$, and a valid target statement-witness pair $(x',w')$, the update algorithm outputs a verifying proof $p'$ for $(x',w')$. Crucially, $p'$ is not recomputed from scratch; instead, the update algorithm takes time roughly proportional to the Hamming distance between $(x,w)$ and $(x',w')$, analogous to how dynamic data structures update the result of a computation after a small change.

In this paper, we initiate the study of designated-verifier dynamic zk-SNARKs: dynamic zk-SNARKs in which only a designated verifier, holding secret verification state, can be convinced by a proof. Following recent advances in designated-verifier zk-SNARKs---such as efficient post-quantum designated verifier SNARKs (CCS 2021) and designated verifier SNARKs with very small proofs (CRYPTO 2025)---we construct a designated-verifier dynamic zk-SNARK with $O(\log n)$ update time, constant proof size, and concrete efficiency. Our construction significantly outperforms Dynalog (both asymptotically and concretely), the only publicly verifiable dynamic zk-SNARK with polylogarithmic update time (Wang et al., 2024).

The concrete efficiency of our construction enables, for the first time, an efficient implementation of a dynamic proof of index: Given a digest $d$ of an arbitrary set and a digest $d'$ of its sorted index (e.g., binary search tree), we produce a SNARK proof certifying the consistency of $d$ and $d'$. More importantly, this proof can be updated in sublinear time when the underlying set changes---for example, when an element is modified or inserted, potentially altering the sorted order. We demonstrate applications of designated-verifier dynamic proofs of index to verifiable dynamic database outsourcing, where a client outsources a database and later maintains verifiable indices for efficient query answering, even under arbitrary database updates.

In the formal verification of complexity-theoretic properties of cryptography, researchers have traditionally attempted to capture ``overwhelming truth'' (satisfaction with all but negligible probability) via satisfaction on individual traces of probabilistic execution. However, this approach introduces significant complexity when quantification is present: satisfaction of existential quantification over traces often produces witnesses---such as nonce-guessing oracles---that witnesses that, without further constraints, may not correspond to meaningful global objects like PPT algorithms respecting causal structure. This discrepancy creates significant obstacles when attempting to combine trace properties, such as reachability, with properties that hold globally, such as algorithmic indistinguishability.

We resolve this by shifting from local satisfaction on individual traces to a semantics based on ever-decreasing non-negligible sets. We demonstrate that the logical key to this unification lies in first-order modal logic S4 with non-negligible sets as possible worlds, rather than the propositional S5 fragment with traces as possible worlds suggested in previous investigations by the Squirrel Prover team. By introducing a PPT computational first-order S4 Kripke semantics and adopting Fitting's embedding for trace properties, we provide a unified quantified treatment of overwhelming truth for trace properties and indistinguishability that admits cut-elimination and remains sound and complete---resolving an open question in the literature.

We show that Fitting's embedding naturally accommodates the higher-order quantification used in the Squirrel prover by interpreting function types as sorts in a many-sorted first-order logic; this reduces the need for the specialized $\texttt{const}$ predicate and its associated structural restrictions. Finally, using our findings, we present a hybrid semantics for CryptoVampire that eliminates the need for bounded Skolemization.