Questions tagged [interactive-proof-systems]

Filter by
Sorted by
Tagged with
1
vote
0answers
16 views

Proving (relativized) upper bounds against SZK

Does anyone know of any instances where we've been able to show that some complexity class is strictly harder than SZK relative to some oracle? In general, it seems that SZK is really hard (for ...
1
vote
0answers
10 views

Practical applications of multi-prover interactive proof protocols

A multi-prover interactive proof protocol, as described here, consists of computationally unbound provers $P_1,P_2,\ldots$ which together convince a polynomial-time verifier $V$ of some proposition, ...
1
vote
0answers
98 views

Perfect Completeness of AM protocols?

I understand the idea behind making a MA protocol perfectly complete. In a MA protocol, Merlin sends a proof $\pi$ which Arthur checks with his machine $V$ by plugging in some random bits $r$ such ...
1
vote
1answer
24 views

Changing probabilities to 0/1 in definition of class IP

A language $L$ belongs to $\mathbf{IP}$ if there exists $V,P$ such that for all $Q$, $w$, $$w\in L\Rightarrow Pr[V\leftrightarrow P\text{ accepts }w]\geq2/3$$ $$w\notin L\Rightarrow Pr[V\...
0
votes
1answer
52 views

How to remove a universal quantifier in Lean theorem prover

I am working with two binary relations: g_o and pw_o, and I've defined pw_o below: constants {A : Type} (g_o : A → A → Prop) ...
4
votes
4answers
240 views

Are there deterministic and/or non-interactive zero-knowledge proofs?

The Wikipedia page on zero-knowledge proof says Zero-knowledge proofs are not proofs in the mathematical sense of the term because there is some small probability, the soundness error, that a ...
0
votes
0answers
78 views

If P=BPP, then Is it correct that IP=NP?

I'm now studying Interactive Proof System in Goldreich's textbook and here. I have the following question: Suppose P=BPP, then this show that randomness doesn't give us power over deterministic ...
5
votes
1answer
61 views

Symmetry of IP complexity class

Wikipedia defines the IP complexity class as follows: A language $L$ belongs to IP if there exists $V,P$ such that for all $Q$, $w$, $$w\in L\Rightarrow Pr[V\leftrightarrow P\text{ accepts }w]\...
1
vote
0answers
78 views

Interactive protocols for showing knots are “hard” to untie

Given two graphs $G_1$ and $G_2$, a zero-knowledge interactive protocol for a prover to convince a verifier that $G_1\not\cong G_2$ entails: The verifier choosing a random $i\in\{1,2\}$ The verifier ...
6
votes
1answer
331 views

How similar is the Goldwasser-Sipser Set Lower Bound Protocol to the Hashcash/Bitcoin Proof-of-Work?

Given a hash function $H:\{0,1\}^*\rightarrow\{0,1\}^n$, a difficulty $d\in\mathbb{N}$, and data $D\in\{0,1\}^*$, the framework of the Hashcash/Bitcoin Proof-of-Work entails finding a nonce $c$ such ...
2
votes
1answer
225 views

proving $IP^\star = NP$

Consider the following complexity class $IP^\star$, a variant of $IP$. A language $L$ is in $IP^\star$ if there's a proof system $(P,V)$ s.t. $V$ is a verifier runs for a polynomial time and: ...
1
vote
0answers
26 views

Prove you computed hash^r(input) for some cryptographic hash function [closed]

What is the most efficient way to prove that a person computed r rounds of some cryptographic hash function (ex. sha256) on an input?. The trivial solution seems to be to show all r hashes, where <...
2
votes
2answers
86 views

Does proofs are programs apply to any functional program?

Does Curry howard correspondence, apply to all Functional Program, e.g. in Haskell. i.e. Is it possible to write Equivalent Haskell programs, to COQ proofs?
1
vote
0answers
59 views

Why does the proof that #SAT is in IP stop after m rounds?

I've been struggling to understand why the interactive proof for #SAT stops after only $m$ rounds, where $m$ is the number of variables in the formula $\phi$. I understand that two polynomials of ...
3
votes
1answer
60 views

Prove count without revealing data

Suppose I maintain a proprietary database and claim that it has N records. Before subscribing to my database a client wants a proof that the database is indeed this large. What theoretical protocol ...
1
vote
0answers
51 views

Use of Mizar for algorithm specification and automatic analysis and discovery of algorithms?

Is it possible to use Mizar Mathematical Library for the specification of algorithms at the same detalization level as the implementation of the algorithm in industrial programming language? Mizar ...
5
votes
1answer
202 views

Why is the complement of SAT in IP?

It is mentioned in Sipser's text that the complement of SAT is in $IP$, before $IP$ is formally introduced. After looking at the definition and some of the results, I still don't see why this is the ...
1
vote
1answer
61 views

Tool for generating all the consequences of the logical theory (general logic programming framework)?

I am reading article https://arxiv.org/pdf/cs/0511055v1.pdf (about defeasible deontic logic) and it mentions on page 10 the operator T that constructs extension (set of immediate consequences) from ...
3
votes
1answer
361 views

What is the difference between AM and IP

Intro I am trying to understand how those two models of interactive proof are different. I understand that $\text{AM}$ relies on public coins (the prover knows the random bits used by the verifier) $...
4
votes
0answers
106 views

Interactive proofs for coNP languages proof clarification

I was reading a paper by Lance Fortnow and Michael Sipser. "Are there interactive protocols for co-NP languages?" Information Processing Letters 28 v5 (1988), pp. 249-251. An online version of the ...
4
votes
1answer
72 views

Why there is no constraint on “Prover” in definition of $IP$?

According to the definition of $IP$ given in Sanjeev Arora and Barak there is no constraint on the running time of the "Prover" ( when "verifier" sends a message to the "Prover" and expects a message ...
1
vote
0answers
47 views

Reasoning approaches for implementing a Knowledge-based System?

What are the major approaches in implementing a Knowledge-based System (KBS)? Approaches used to take decisions in a KBS that I have come across so far are the case-based and rule-based reasoning ...
12
votes
1answer
143 views

Are there any known AM-complete problems/is AM-complete well defined?

I'm curious about whether there are any complete problems in the Arthur-Merlin complexity class. Graph Non-Isomorphism (GNI) seems to be the canonical example of a problem in AM, but it's probably not ...
1
vote
1answer
58 views

Why is there only a polynomial number of provers in multi-prover interactive protocols?

The paper On The Power of Multi-prover Interactive Protocols by Fortnow, Rompel, Sipser states the following: There are provers $P_1, P_2, \dots, P_k$ in a multi-prover interactive proof system such ...
0
votes
1answer
221 views

Implementation of datatypes in Haskell?

In Haskell, are datatypes converted to the "Church encoding" i.e. folding the data type. For example, given data N = Z | S N in Haskell, it can be converted to ...
4
votes
1answer
120 views

Number of rounds in interactive proofs - Arora & Barak

In the web draft of Arora and Barak, "Computational Complexity: A Modern Approach", the way I understand their definition of a round of interaction is that it consists of either the verifier or the ...
9
votes
2answers
345 views

Interactive Proofs for coNP

I am trying to understand interactive proof systems and tried the following problem as an exercise. We know that $PH \subseteq PSPACE$ and $IP=PSPACE$, so come up with (easy to understand) interactive ...
4
votes
1answer
233 views

Sketch an IP proof for minSAT

I have to sketch an IP proof for the minSAT problem. The minSAT problem is define in this way: For a given formulae find a satisfying assignment with a min subset of variables assigned to True; My ...
4
votes
1answer
992 views

Relation between interactive proof systems (IP), NP, coNP, PSPACE

I would like to ask you some clarification on the following question: know that ${\sf NP}$ is a subset of ${\sf IP}$ and also ${\sf coNP}$ it is a subset of ${\sf IP}$. So ${\sf IP}$ is a biggest ...
10
votes
0answers
196 views

“Essential” problem for MA

I am trying to understand different interactive proof systems, in particular AM and MA. Is there a typical problem for the complexity class MA as Graph-NonIsomorphism problem is for AM? Is there ...