Paper 2026/143

A Unified Treatment of Reachability and Indistinguishability Properties: First-Order Logic with Overwhelming Truth

Mitsuhiro Okada, Keio University

Abstract

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.

BibTeX

@misc{cryptoeprint:2026/143,
author = {Gergei Bana and Mitsuhiro Okada},
title = {A Unified Treatment of Reachability and Indistinguishability Properties: First-Order Logic with Overwhelming Truth},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/143},
year = {2026},
url = {https://eprint.iacr.org/2026/143}
}