Paper 2026/143

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

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, 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 are defined on non-negligible sets such as computability, or global properties, such as algorithmic indistinguishability. We resolve this by shifting from defining local satisfaction as 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 \emph{non-negligible sets} as possible worlds, rather than the propositional S5 fragment with \emph{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, together with a first-order calculus, $\mathsf{BC}^+$, whose sole modal operator is the overwhelming-truth bracket $[\,\cdot\,]$. The calculus is sound and, on its fragment, derives exactly the theorems of first-order S4 with persistence; computational completeness holds on the fragment; cut elimination holds propositionally, while at first order every cut is confined to an optimal Barcan shape. 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.

Note: Clarified more how this one-tier technique relates to the Squirrel Prover's two tiered technique for local and global rules. Introduced an exact (sound and complete) inference system for the fragment of first-order S4 generated by the modality for overwhelming truth [ ] interpreted as Fitting's embedding extended to nestedness. Included cut-confinement results. Replaced the completeness theorem, which was wrong in the previous version. This does not affect protocol verification as for that soundness is what we need.