give example of how soundness proof can go wrong

[amiller]

given the focus of this writeup on soundness proofs, motivated in party by https://eprint.iacr.org/2019/119 https://eprint.iacr.org/2015/437 it would be great to illustrate a buggy variation of BabySNARK that is unsound and can be exploited to create false proofs for at least some statements.
partially explored by @sanket1729 and @SilverPoker but needs to be completed

[bl4ck5un]

Maybe this is relevant here. From reading the soundness proof I didn't get why \gamma is needed. I.e., if you remove it from the scheme and the proof, it extraction seems still going through.

Specifically, if you

• remove \gamma and related terms from CRS;
• change the last line of Verify to e(B_w, G)=?e(\beta G, V_w);
• in the soundness proof, remove terms with Z from B_w(.), V_w(.), H(.).

the extraction proof seems still going through. What did I miss?

[bl4ck5un]

oh, I think I see where the problem is. Extracted V(.) will be off by a constant term.

Hmm. this is subtle. Would def. appreciate some intuition around why \gamma is there.

[SilverPoker]

The intuition is still enforcing the prover only to evaluate a polynomial that lies in the linear span of u_i(X). If you don't have \gamma, then \beta is exposed to the prover. So he can use the span of 1 and u_i(X). (A constant shift can be used to make fake proof) @bl4ck5un

[bl4ck5un]

Yeah once you see it, it's clear.

I suppose "without z, the prover can compute in the span of 1 and {u_i(X)}" is a nice and intuitive explanation. thanks.

[sanket1729]

Yes, this is indeed a non-intuitive part of the crs. We originally tried to remove it and prove the soundness but struggled at exactly this step.

However, generically for all circuits, this on its own does not allow the prover to create fake proof.

Maybe, if for a particular circuit 1 lied in the span of statement u_i, then maybe a fake proof can be created. (I am not sure, have not worked this out completely).