# Appendix B: Mathematical Considerations by Issue

## 1. Non-Standard Cryptographic Assumption (§7, Line 186)

**Restated claim.** The protocol assumes “Power-Target Hardness” in asymmetric bilinear groups of prime order r: given bases {U_j} ⊂ 𝔾₂, {V_k} ⊂ 𝔾₁, their r-powers with unknown r, and an independent T ∈ 𝔾_T, it is infeasible to output T^r.
**Sources.** Preliminary analysis: Analysis_report-preliminary-2025-10-07.md (Critical Issue #1). Updated analysis: report-update-2025-10-07/PVUGC-001-gt-xpdh-assumption.md (status 🔓 Open, mitigated by Multi-CRS AND-ing).

**Key concerns.**
- No known reduction to CDH, DDH, SXDH, XDH, DLIN, or q-type assumptions; hardness landscape is uncharted.
- CRS sampling for Groth16 and Groth-Sahai may induce linear dependencies between exponent vectors defining {U_j}, {V_k} and the Groth16 verification product G_G16(vk,x). Algebraic relations in the joint exponent lattice could allow deriving G_G16^ρ from published masks D_{1,j}, D_{2,k} without discrete log solves.
- Availability of {U_j^ρ}, {V_k^ρ} reveals the linear span of exponent vectors; if G_G16’s exponent vector lies in this span, Power-Target Hardness collapses.

**Proof obligations / counterexample targets.**
- Provide a formal reduction from Power-Target Hardness to a standard pairing assumption or prove random self-reducibility of the assumption.
- Perform rank and dependency analysis of CRS-derived exponent matrices; prove that G_G16’s exponent vector falls outside the span with overwhelming probability.
- Attempt Gröbner-basis or lattice attacks on concrete CRS distributions to exhibit algebraic correlations; any success breaks the assumption.

**Suggested formalizations.** Define Power-Target Hardness precisely (including distributions for {U_j}, {V_k}, T). Prove independence lemmas for CRS generation, and model knowledge extraction under the Algebraic Group Model (AGM) to argue that access to exponentiated bases does not reveal G_G16^ρ. Supply bounds on adversarial advantage when CRS randomness is partially controlled.

## 2. GS Attestation Layer: Commitment Malleability (§6, Lines 118-131)

**Restated claim.** Groth-Sahai commitments with a binding CRS ensure that any tuple of commitments satisfying the PPE corresponds to a valid Groth16 proof under the same statement.

**Key concerns.**
- The PPE may admit extraneous solutions if commitments are only computationally binding; re-randomization factors must cancel exactly.
- Without a formal cancellation lemma, adversarial commitments could satisfy the product equation yet decrypt to invalid proof elements.
- CRS generation requirements (SXDH/DLIN binding mode) lack explicit structural tests; malicious CRS may switch to witness-indistinguishable mode.

**Proof obligations / counterexample targets.**
- Prove simulation-sound extractability for the exact PPE layout: from any accepting commitment tuple derive the Groth16 witness, or contradict SXDH/DLIN.
- Construct toy CRS examples where binding fails (e.g., in small groups) to show necessity of specified structural checks.
- Verify algebraically that re-randomization parameters vanish in the final PPE; missing cancellation implies malleability.

**Suggested formalizations.** Provide explicit CRS matrices, formalize binding via matrix rank arguments, and supply an extractor in AGM. Define and prove the tag/check that enforces binding CRS structure using pairings. Offer mechanized proofs or symbolic derivations validating PPE cancellation.

## 3. Independence Claim: Potential Violation (§6, Lines 131-132)

**Restated claim.** Bases {U_j(x), V_k(x)} and target G_G16(vk,x) are fixed independently of armer randomness; armers cannot correlate their randomness with the basis structure.
**Sources.** Analysis_report-preliminary-2025-10-07.md (Critical Issue #3). report-update-2025-10-07/PVUGC-003-independence-property.md (status 🔧 Improved; MUST clause added, proof pending).

**Key concerns.**
- Shared randomness between Groth16 and GS CRS may create algebraic dependencies; independence must be proven over the joint CRS distribution.
- Adaptive selection of (vk, x) after CRS publication could correlate G_G16 with {U_j, V_k} without explicit countermeasures.
- Multi-party CRS ceremonies lacking bias-resistant proofs may allow malicious participants to skew bases.

**Proof obligations / counterexample targets.**
- Demonstrate via information-theoretic bounds that mutual information between spans generated by {U_j, V_k} and G_G16’s exponent vector is negligible.
- Model an adaptive adversary choosing (vk, x) after observing CRS and prove G_G16 remains independent with overwhelming probability.
- Attempt to construct attacking CRS that make G_G16 a product of published bases; success indicates failure of independence.

**Suggested formalizations.** Specify the CRS ceremony protocol, introduce commitments or verifiable randomness extraction to guarantee uniformity, and prove independence using hybrid games or Jacobian rank arguments. Include formal restrictions preventing armers from influencing CRS parameters post-setup.

## 4. PoCE-A Soundness: Malicious Armer Detection Gaps (§5, §8)

**Restated claim.** PoCE-A proves knowledge of (ρᵢ, sᵢ) tied to published masks and adaptor share, ensuring correctness of armer contributions.
**Sources.** Analysis_report-preliminary-2025-10-07.md (High Severity Issue #4). report-update-2025-10-07/PVUGC-004-poce-soundness.md (status 🔓 Open; publication SHOULD clause added).

**Key concerns.**
- Ciphertext ctᵢ is not bound to (ρᵢ, sᵢ); PoCE-A allows semantically invalid encryptions that pass algebraic checks.
- Constraint ρᵢ ≠ 0 via auxiliary equation permits special values (ρᵢ = 1, small subgroups) that leak Mᵢ or collapse α.
- Aggregated checks (Σ sᵢ ≠ 0) occur late, enabling publication of degenerate per-share values.

**Proof obligations / counterexample targets.**
- Extend PoCE-A with relations binding ctᵢ to the same randomness (e.g., ciphertext commitments) and prove knowledge soundness.
- Exhibit explicit ρᵢ = 1 / sᵢ = 0 counterexamples showing current constraints insufficient.
- Analyze probability of small-subgroup leakage and show that without additional checks adversaries succeed with probability 1.

**Suggested formalizations.** Formalize PoCE-A in AGM, proving extraction of (ρᵢ, sᵢ, plaintext). Define acceptable scalar ranges and show validation rules enforce primesubgroup membership. Introduce early aggregation lemmas verifying Tᵢ ≠ 𝒪 and Σ sᵢ ≠ 0 before pre-signing.

## 5. Context Binding: Incomplete Binding and Replay Risks (§3)

**Restated claim.** Layered hashes (ctx_core, arming_pkg_hash, presig_pkg_hash) bind all artifacts to a unique execution context.
**Sources.** Analysis_report-preliminary-2025-10-07.md (High Severity Issue #5). report-update-2025-10-07/PVUGC-005-context-binding.md (status 🔧 Improved; layered hash tags defined, testing outstanding).

**Key concerns.**
- ctx_core omits GS CRS hash; contexts differing only in CRS collide, enabling reinterpretation of masks under malicious CRS.
- arming_pkg_hash excludes ctx_core, allowing reuse of {D₁}, {D₂} across distinct transactions sharing header_meta.
- Lack of nonce/epoch introduces potential ctx_hash collisions when templates repeat.

**Proof obligations / counterexample targets.**
- Construct contexts A and B with differing transactions but identical arming_pkg_hash, demonstrating replay risk.
- Prove (under collision resistance) that updated hash definitions bind all parameters uniquely.
- Formalize serialization to show injectivity; any ambiguity undermines binding arguments.

**Suggested formalizations.** Treat hashes as random oracles; conduct sequence-of-games proof that any successful replay implies hash collision. Introduce a unique execution nonce and prove uniqueness of ctx_hash. Provide canonical encoding specifications with injectivity proofs.

## 6. Degenerate Values: Insufficient Edge Case Coverage (§6, Lines 146-148)

**Restated claim.** Validation rules eliminate algebraic degeneracy in scalars and group elements used for masks and adaptor shares.
**Sources.** Analysis_report-preliminary-2025-10-07.md (High Severity Issue #6). report-update-2025-10-07/PVUGC-006-degenerate-values.md (status ✅ Resolved; degenerate guards codified).

**Key concerns.**
- Scalars ρᵢ = 1 reveal Mᵢ = G_G16; sᵢ = 0 nullifies α; small-order scalars circumvent prime-order guarantees.
- Per-share tests for Tᵢ = 𝒪 or subgroup membership are absent; only aggregate checks exist.
- No normative serialization for 𝔾_T; different encodings lead to distinct HKDF inputs.

**Proof obligations / counterexample targets.**
- Provide explicit adversarial choices (ρᵢ = 1, sᵢ = 0) illustrating leakage or liveness failure.
- Prove that range constraints (e.g., ρᵢ ∈ [2^λ, r-2^λ]) prevent exposures while remaining efficiently checkable.
- Show bijectivity of the chosen serialization function; any ambiguity directly affects KEM correctness.

**Suggested formalizations.** Define admissible scalar set and prove enforcement via modular inequalities. Supply canonical encoding algorithms with proofs of involution (decode(encode(P)) = P). Develop a formal edge-case test suite verifying rejection of degenerate inputs.

## 7. Timing Attacks: Race Conditions and Side-Channels (§9)

**Restated claim.** Timing and race behavior should not leak witness information or confer probabilistic advantages to adversaries.

**Key concerns.**
- Pairing counts depend on GS commitment sizes; timing differences may reveal witness structure despite zero-knowledge claims.
- Lack of phase deadlines enables adversaries to game completion probability (e.g., mempool front-running).
- DEM decryption success/failure timing forms a distinguishing oracle unless constant-time behavior is ensured.

**Proof obligations / counterexample targets.**
- Bound mutual information between timing traces and secret data; any non-zero leakage violates zero-knowledge guarantees.
- Provide empirical counterexamples showing measurable timing differences for varying witness structures.
- Model race conditions as stochastic games and prove adversarial advantage is negligible with enforced deadlines.

**Suggested formalizations.** Adopt leakage-resilient models, proving constant-time implementations within tolerance ε. Formalize phase transitions with timeouts, using probabilistic analysis (martingale/concentration inequalities) to bound adversarial success. Include DEM operations in leakage model and prove indistinguishability of success/failure timing.

## 8. MuSig2 Integration: Adaptor Compartmentalization Enforcement (§4, §10)

**Restated claim.** Unique adaptor nonce R and adaptor point T per context prevent Schnorr key exposure and cross-context interference.

**Key concerns.**
- Reusing R yields classical Schnorr key recovery (s₁ - s₂) / (e₁ - e₂) = x.
- Without deterministic derivation or blacklisting, implementations may accidentally reuse R or T across contexts.
- Miscomputed MuSig coefficients alter aggregate key P, producing unverifiable signatures with no detection mechanism.

**Proof obligations / counterexample targets.**
- Provide formal derivation proving deterministic HKDF(ctx_hash, label) yields unique (R, T) with overwhelming probability.
- Construct transcripts showing key recovery when R is reused; ensures enforceable uniqueness is mandatory.
- Prove algebraically that verifying coefficients prevents malformed P; supply consistency checks.

**Suggested formalizations.** Define deterministic nonce derivation and prove collision resistance under PRF assumptions. Model MuSig2 per BIP-327 and prove state-machine compliance; any deviation yields abort or contradicts discrete log hardness. Encode adaptor uniqueness in the overall security proof, reducing violations to Schnorr forgeries.

## 9. Key-Committing DEM: Multiple Schemes Allowed (§8, Lines 217-220)

**Restated claim.** The DEM must be key-committing so that ciphertexts uniquely determine the encryption key and thus bind to the KEM output.

**Key concerns.**
- Allowing both hash-only and AEAD variants complicates security proofs; the hash-only scheme requires ROM assumptions, AEAD needs deterministic nonce safety.
- Deterministic nonce reuse in non-SIV AEADs (e.g., GCM) breaks key commitment; two keys could decrypt the same ciphertext.
- Differences in AD serialization may destroy injectivity required for commitment.

**Proof obligations / counterexample targets.**
- Formalize key-commitment for the chosen DEM and prove the property; if using hash-only, provide ROM proofs.
- Demonstrate nonce reuse counterexamples for non-SIV AEADs, proving catastrophic failure.
- Verify that the mapping (K, AD, plaintext) → ciphertext is injective; absence of injectivity violates key commitment.

**Suggested formalizations.** Standardize on a single DEM (e.g., AES-SIV) and supply composable security proof (KEM+DEM → IND-CCA). Prove τᵢ = H(Kᵢ, AD_core, ctᵢ) adds collision resistance. Provide formal test vectors and, if possible, machine-checked proofs in cryptographic proof assistants.

## 10. CRS Validation: Underspecified Tag Mechanism (§7, Line 190)

**Restated claim.** A tag embedded in GS_instance_digest lets verifiers distinguish binding CRS from witness-indistinguishable CRS.

**Key concerns.**
- Absence of explicit tag construction; adversaries can craft WI CRS with forged tags.
- No set of algebraic equations is provided to characterize binding CRS; verification cannot be implemented.
- Serialization ambiguities undermine tag checking if not canonically defined.

**Proof obligations / counterexample targets.**
- Provide necessary and sufficient algebraic conditions (pairing equations) that characterize binding CRS; prove completeness and soundness.
- Construct WI CRS examples; show acceptance without a proper tag to highlight risk.
- Prove collision resistance of the tag function under canonical serialization.

**Suggested formalizations.** Describe CRS generation algorithm, define tag computation (e.g., H("PVUGC/GS-BINDING" || ser(CRS) || label)), and prove verification algorithm accepts only binding CRS under SXDH/DLIN. Supply mechanized proofs (Coq/Lean) for small instances validating CRS characterization.

---

## Cross-Cutting Dependencies

Issues 1–3 rely on rigorous independence proofs between CRS components and Groth16 verification targets; any shared randomness undermines Power-Target Hardness and GS soundness simultaneously. Issues 4–6 require precise scalar-domain enforcement and canonical encodings to ensure algebraic reductions compose without leaks. Issues 7–9 demand integrating timing- and key-commitment proofs into the global security argument so that KEM, DEM, and Schnorr adaptor properties align. Issue 10 underpins all prior assumptions because CRS authenticity is prerequisite for every algebraic guarantee. A unified formal model encompassing CRS generation, scalar admissibility, hash binding, and side-channel leakage is necessary to deliver an end-to-end security proof.