Ok you nerdsniped me
The proof verification equation (from section 3.2 of [Groth2016]) is:
- [A]_1 \cdot [B]_2 = [\alpha]_1 \cdot [\beta]_2 + \sum_{i=0}^{\ell} a_i \left[ \frac{\beta u_i(x) + \alpha v_i(x) + w_i(x)}{\gamma} \right]_1 \cdot [\gamma]_2 + [C]_1 \cdot [\delta]_2
The notation here is additive, i.e. it is in terms of the indices of points in the relevant groups (shown by the subscript, e.g. for a , [A]_1 means the index of A in \mathbb{G}_1).
Call a Groth16 proof proof \pi = (A, B, C) with any of A, B, or C a point at infinity “degenerate”. We can prove that degenerate proofs do not help to break soundness.
Partition the cases of degenerate proofs as follows:
a) [A]_1 = 0 and/or [B]_2 = 0 (so the LHS of the verification equation in additive form is 0).
b) [C]_1 = 0 and [A]_1 \neq 0.
In case a), for the proof to be valid we would need 0 = [\alpha]_1 \cdot [\beta]_2 + \sum_{i=0}^{\ell} a_i \left[ \frac{\beta u_i(x) + \alpha v_i(x) + w_i(x)}{\gamma} \right]_1 \cdot [\gamma]_2 + [C]_1 \cdot [\delta]_2.
It is infeasible to find a satisfying C given that \alpha, \beta, \gamma, and \delta are chosen as random group elements with unknown discrete logarithms.
In case b), we can make use of the rerandomizability property of Groth16 stated in [BKSV2020]. Let p be the group order. For any r_1, r_2 \in \mathbb{Z}^*_p, there is a “rerandomized” proof that is valid whenever the input proof is. Figure 1 of [BKSV2020] gives the rerandomization algorithm. With minor changes in notation, it is:
\mathsf{Rand}(\sigma, \pi = (A, B, C)):
\hspace{1em} r_1, r_2 \leftarrow^{\kern-0.85em\small\$} \mathbb{Z}^*_p
\hspace{1em} a := (1/r_1) A;\; b := r_1 B + r_1 r_2 [\delta]_2;\; c := C + r_2 a
\hspace{1em} \textbf{return } (a, b, c)
Note that r_1 and r_2 need not actually be random. So in case b), where C = \mathcal{O}_1 and A \neq \mathcal{O}_1, choose r_1 = 1 and any r_2 such that B \neq -r_2 [\delta]_2. This gives a nondegenerate proof that is valid when the input proof is. Therefore, if the proof system allowing degenerate proofs is unsound, then so is the proof system disallowing them. This means that the system allowing degenerate proofs is just as secure for soundness as the system that disallows them.
Note that I am not recommending that points at infinity be allowed in proofs. There is still no good reason to allow them. In particular, just because the idealized proof system with correct handling of exceptional cases is still sound, does not mean that any particular implementation will correctly handle those cases.