5 Search Results for "Beckmann, Arnold"

Document
DOI: 10.4230/LIPIcs.CCC.2024.15
Quantum Automating TC⁰-Frege Is LWE-Hard

Authors: Noel Arteche, Gaia Carenini, and Matthew Gray

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC⁰-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC⁰-Frege and AC⁰-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.
Cite as

Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum Automating TC⁰-Frege Is LWE-Hard. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 15:1-15:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.CCC.2024.15,
  author =	{Arteche, Noel and Carenini, Gaia and Gray, Matthew},
  title =	{{Quantum Automating TC⁰-Frege Is LWE-Hard}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{15:1--15:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.15},
  URN =		{urn:nbn:de:0030-drops-204117},
  doi =		{10.4230/LIPIcs.CCC.2024.15},
  annote =	{Keywords: automatability, post-quantum cryptography, feasible interpolation}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.22
Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP

Authors: Theodoros Papamakarios

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
We show that for any integer d > 0, depth-d Frege systems are NP-hard to automate. Namely, given a set S of depth-d formulas, it is NP-hard to find a depth-d Frege refutation of S in time polynomial in the size of the shortest such refutation. This extends the result of Atserias and Müller [JACM, 2020] for the non-automatability of resolution - a depth-1 Frege system - to Frege systems of any depth d > 0.
Cite as

Theodoros Papamakarios. Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{papamakarios:LIPIcs.CCC.2024.22,
  author =	{Papamakarios, Theodoros},
  title =	{{Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.22},
  URN =		{urn:nbn:de:0030-drops-204187},
  doi =		{10.4230/LIPIcs.CCC.2024.22},
  annote =	{Keywords: Proof complexity, Automatability, Bounded-depth Frege}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.24
IMELL Cut Elimination with Linear Overhead

Authors: Beniamino Accattoli and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one. Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.
Cite as

Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24,
  author =	{Accattoli, Beniamino and Sacerdoti Coen, Claudio},
  title =	{{IMELL Cut Elimination with Linear Overhead}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24},
  URN =		{urn:nbn:de:0030-drops-203539},
  doi =		{10.4230/LIPIcs.FSCD.2024.24},
  annote =	{Keywords: Lambda calculus, linear logic, abstract machines}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.12
From Proof Complexity to Circuit Complexity via Interactive Protocols

Authors: Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.
Cite as

Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.ICALP.2024.12,
  author =	{Arteche, Noel and Khaniki, Erfan and Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{From Proof Complexity to Circuit Complexity via Interactive Protocols}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12},
  URN =		{urn:nbn:de:0030-drops-201557},
  doi =		{10.4230/LIPIcs.ICALP.2024.12},
  annote =	{Keywords: proof complexity, circuit complexity, interactive protocols}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2021.1
Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control

Authors: Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
This paper contributes to the verification of programs written in Bitcoin’s smart contract language script in the interactive theorem prover Agda. It focuses on the security property of access control for script programs that govern the distribution of Bitcoins. It advocates that weakest preconditions in the context of Hoare triples are the appropriate notion for verifying access control. It aims at obtaining human-readable descriptions of weakest preconditions in order to close the validation gap between user requirements and formal specification of smart contracts. As examples for the proposed approach, the paper focuses on two standard script programs that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). The paper introduces an operational semantics of the script commands used in P2PKH and P2MS, which is formalised in the Agda proof assistant and reasoned about using Hoare triples. Two methodologies for obtaining human-readable descriptions of weakest preconditions are discussed: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes grouping several instructions together; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of conjunctions of conditions along accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda.
Cite as

Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1:1-1:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{alhabardi_et_al:LIPIcs.TYPES.2021.1,
  author =	{Alhabardi, Fahad F. and Beckmann, Arnold and Lazar, Bogdan and Setzer, Anton},
  title =	{{Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{1:1--1:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.1},
  URN =		{urn:nbn:de:0030-drops-167704},
  doi =		{10.4230/LIPIcs.TYPES.2021.1},
  annote =	{Keywords: Blockchain, Cryptocurrency, Bitcoin, Agda, Verification, Hoare logic, Bitcoin Script, P2PKH, P2MS, Access control, Weakest precondition, Predicate transformer semantics, Provable correctness, Symbolic execution, Smart contracts}
}
  • Refine by Author
  • 2 Arteche, Noel
  • 1 Accattoli, Beniamino
  • 1 Alhabardi, Fahad F.
  • 1 Beckmann, Arnold
  • 1 Carenini, Gaia
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Proof complexity
  • 2 Theory of computation → Operational semantics
  • 1 Applied computing → Digital cash
  • 1 Security and privacy → Access control
  • 1 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 Access control
  • 1 Agda
  • 1 Automatability
  • 1 Bitcoin
  • 1 Bitcoin Script
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 4 2024
  • 1 2022

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact