On Computational Indistinguishability and Logical Relations
- URL: http://arxiv.org/abs/2408.17340v2
- Date: Tue, 22 Oct 2024 21:28:16 GMT
- Title: On Computational Indistinguishability and Logical Relations
- Authors: Ugo Dal Lago, Zeinab Galal, Giulia Giusti,
- Abstract summary: The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.
- Score: 1.024113475677323
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: A $\lambda$-calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptographic constructions and adversaries for them, even when the latter are oracle-based. A notion of observational equivalence capturing computational indistinguishability and a class of approximate logical relations are then presented, showing that the latter represent a sound proof technique for the former. The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.
Related papers
- Tokenization Constraints in LLMs: A Study of Symbolic and Arithmetic Reasoning Limits [15.941209553757274]
Tokenization is the first - and often underappreciated - layer of computation in language models.<n>We show that the success of such reasoning is fundamentally bounded by the structure of tokenized inputs.
arXiv Detail & Related papers (2025-05-20T10:32:30Z) - Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification [5.806034991979994]
Bisimulation is crucial for verifying process equivalence in probabilistic systems.<n>This paper presents a novel framework for analyzing bisimulation in infinite families of finite-state probabilistic systems.<n>We show that essential properties like anonymity and uniformity can be encoded and verified within this framework.
arXiv Detail & Related papers (2025-05-15T04:56:53Z) - Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups [0.0]
We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic.
We outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
arXiv Detail & Related papers (2025-02-26T10:10:10Z) - TabVer: Tabular Fact Verification with Natural Logic [11.002475880349452]
We propose a set-theoretic interpretation of numerals and arithmetic functions in the context of natural logic.
We leverage large language models to generate arithmetic expressions by generating questions about salient parts of a claim which are answered by executing functions on tables.
In a few-shot setting on FEVEROUS, we achieve an accuracy of 71.4, outperforming both fully neural and symbolic reasoning models by 3.4 points.
arXiv Detail & Related papers (2024-11-02T00:36:34Z) - (Quantum) Indifferentiability and Pre-Computation [50.06591179629447]
Indifferentiability is a cryptographic paradigm for analyzing the security of ideal objects.
Despite its strength, indifferentiability is not known to offer security against pre-processing attacks.
We propose a strengthening of indifferentiability which is not only composable but also takes arbitrary pre-computation into account.
arXiv Detail & Related papers (2024-10-22T00:41:47Z) - Generalized one-way function and its application [0.76146285961466]
We develop an unconditionally secure key distribution protocol based solely on classical data processing.
We demonstrate that probability theory and randomness are effective tools for countering adversaries with unlimited computational capabilities.
arXiv Detail & Related papers (2024-08-24T15:56:30Z) - The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
Tokenization is a critical step in the NLP pipeline.
Despite its recognized importance as a standard representation method in NLP, the theoretical underpinnings of tokenization are not yet fully understood.
The present paper contributes to addressing this theoretical gap by proposing a unified formal framework for representing and analyzing tokenizer models.
arXiv Detail & Related papers (2024-07-16T11:12:28Z) - Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models.
A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters.
We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
arXiv Detail & Related papers (2023-10-05T07:10:40Z) - Oracle Computability and Turing Reducibility in the Calculus of
Inductive Constructions [0.0]
We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions.
As usual in synthetic approaches, we employ a definition of oracle computations based on meta-level functions.
We show that Turing reducibility forms an upper semilattice, transports decidability, and is strictly more expressive than truth-table reducibility.
arXiv Detail & Related papers (2023-07-28T13:16:46Z) - From Probabilistic Programming to Complexity-based Programming [0.5874142059884521]
The paper presents the main characteristics and a preliminary implementation of a novel computational framework named CompLog.
Inspired by probabilistic programming systems like ProbLog, CompLog builds upon the inferential mechanisms proposed by Simplicity Theory.
The proposed system enables users to compute ex-post and ex-ante measures of unexpectedness of a certain situation.
arXiv Detail & Related papers (2023-07-28T10:11:01Z) - A Hybrid System for Systematic Generalization in Simple Arithmetic
Problems [70.91780996370326]
We propose a hybrid system capable of solving arithmetic problems that require compositional and systematic reasoning over sequences of symbols.
We show that the proposed system can accurately solve nested arithmetical expressions even when trained only on a subset including the simplest cases.
arXiv Detail & Related papers (2023-06-29T18:35:41Z) - Multivariate Systemic Risk Measures and Computation by Deep Learning
Algorithms [63.03966552670014]
We discuss the key related theoretical aspects, with a particular focus on the fairness properties of primal optima and associated risk allocations.
The algorithms we provide allow for learning primals, optima for the dual representation and corresponding fair risk allocations.
arXiv Detail & Related papers (2023-02-02T22:16:49Z) - Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
We show that we can learn arbitrary logic in a single layer using an activation function of matching or greater arity.
We represent belief tables using a basis that directly associates the number of nonzero parameters to the effective arity of the belief function.
This opens optimization approaches to reduce logical complexity by inducing parameter sparsity.
arXiv Detail & Related papers (2022-03-16T22:47:53Z) - Logical Credal Networks [87.25387518070411]
This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability.
We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
arXiv Detail & Related papers (2021-09-25T00:00:47Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.