Cryptography · Bilinear maps · NIZK

GSkit

A domain-specific language and framework for Groth-Sahai proofs

Benjamín Hurtado Torrealba

Advisors: Matías Toro Ipinza · Federico Olmedo Berón

Departamento de Ciencias de la Computación · Universidad de Chile

Magíster en Ciencias, mención Computación · Ingeniería Civil en Computación

Tuesday 13 October 2026

benjamin.hurta.do/gskit

Agenda

1Zero-knowledge proofs
2Signatures & bilinear maps
3Groth-Sahai proofs
4GSkit: the DSL and framework
5Case study: ABS-UCL
6Evaluation & conclusions
1 · Zero-knowledge proofs

Why prove without revealing?

Every day we have to convince someone of a fact, and usually we do it by handing over the evidence: an ID to prove our age, a password to prove it's us.

But the evidence is often a secret we'd rather not give away. Can we prove the statement is true while keeping the secret to ourselves?

That is the question zero-knowledge proofs answer.

1 · Zero-knowledge proofs

Zero-knowledge, by example

Peggy (the prover) claims she knows the secret word that opens the door inside Ali Baba's cave. Victor (the verifier) wants to be convinced, without learning the word.

  • 1 · CommitPeggy walks in through A or B at random, while Victor waits outside
  • 2 · ChallengeVictor shouts the side she must come out from
  • 3 · ResponsePeggy comes out on that side, through the door if she has to

Illustrations: Dake, Wikimedia Commons (CC BY 2.5)

1 · Zero-knowledge proofs

Three properties

Repeating the cave game makes the three properties of a zero-knowledge proof concrete:

  • CompletenessAn honest prover with a valid witness always convinces the verifierIf Peggy knows the word, she always comes out where Victor asks
  • SoundnessA cheating prover cannot convince the verifier of a false statementWithout the word she gets caught half of the time: after kk rounds she fools Victor with probability 2−k2^{-k}
  • Zero-knowledgeThe verifier learns nothing beyond the truth of the statementVictor only sees her come out where he asked, a scene he could have staged himself
1 · Zero-knowledge proofs

Formally — NIZK

Consider an NP-relation R\mathcal{R} and the language it defines:

L:={ x ∣ ∃ w s.t. (x,w)∈R }\mathcal{L} := \{\ x \ \mid\ \exists\, \wit{w} \text{ s.t. } (x, \wit{w}) \in \mathcal{R}\ \}

where xx is the statement (public) and w\wit{w} the witness (secret). A non-interactive zero-knowledge proof (NIZK) is a single message π\pi, checked against a common reference string:

  • Setup — CRS←Setup(1λ)\mathsf{CRS} \leftarrow \mathsf{Setup}(1^\lambda)
  • Prove — π←Prove(CRS, x, w)\pi \leftarrow \mathsf{Prove}(\mathsf{CRS},\, x,\, \wit{w})
  • Verify — b←Verify(CRS, x, π)b \leftarrow \mathsf{Verify}(\mathsf{CRS},\, x,\, \pi)

secret values: the same color marks them on every slide

2 · Signatures & bilinear maps

Worst Bank in the World

To make this concrete, meet the worst bank in the world. It issues cheques, and everyone around it needs a way to tell a genuine one from a forgery.

Bank

You

WORST BANK IN THE WORLD Pay 1_000_000 σ

KeyGen→ secret key sk, public key vk

Sign(m, sk) → signature σ

Verify(m, σ, vk) → ✓ / ✗

Your worst friend

watching…
2 · Signatures & bilinear maps

Signatures, in one idea

A signature scheme is the bank's anti-forgery tool. The bank keeps a secret key sk\wit{sk} and publishes a verification key vkvk: anyone can check, nobody can forge.

  • KeyGen — produces the key pair (sk,vk)(\wit{sk}, vk). The secret stays with the bank; vkvk goes public.
  • Sign — only the holder of sk\wit{sk} can turn a message mm into a signature σ\sigma.
  • Verify — anyone with vkvk can confirm that σ\sigma really matches mm.

The ingredient that makes a good signature scheme possible is the bilinear map.

2 · Signatures & bilinear maps

Bilinear maps

A bilinear map is a function e:G1×G2→GTe: \mathbb{G}_1 \times \mathbb{G}_2 \to \mathbb{G}_T that lets us move scalars across a pairing:

e(a g1, b g2)=e(g1,g2)abe(a \, g_1,\ b \, g_2) = e(g_1, g_2)^{ab}

  • G1,G2\mathbb{G}_1, \mathbb{G}_2 and GT\mathbb{G}_T are finite groups of prime order pp, defined over elliptic curves
  • g1,g2g_1, g_2 generate G1\mathbb{G}_1 and G2\mathbb{G}_2 respectively, and a,b∈Zpa, b \in \mathbb{Z}_p

This one property, pulling exponents out of a pairing, is the lever behind both BLS signatures and Groth-Sahai proofs.

2 · Signatures & bilinear maps

BLS signature

Boneh–Lynn–Shacham [BLS04] turn that lever into a signature scheme: the secret key hides as an exponent, and the pairing lets anyone check it without ever seeing it. A hash-to-curve H:{0,1}∗→G1\mathcal{H}:\{0,1\}^* \to \mathbb{G}_1 maps messages onto the curve.

  • KeyGen — sk←RZp\wit{sk} \xleftarrow{R} \mathbb{Z}_p   vk←[sk] g2vk \leftarrow [\wit{sk}]\, g_2
  • Sign — h←H(m)h \leftarrow \mathcal{H}(m)   σ←[sk] h\sigma \leftarrow [\wit{sk}]\, h
  • Verify — h←H(m)h \leftarrow \mathcal{H}(m)   e(σ,g2)=?e(h,vk)e(\sigma, g_2) \stackrel{?}{=} e(h, vk)

Verification works because bilinearity makes both sides collapse to the same value:

e([sk]h, g2)=e(h,g2)sk=e(h, [sk]g2)e([\wit{sk}]h,\ g_2) = e(h, g_2)^{\wit{sk}} = e(h,\ [\wit{sk}]g_2)

2 · Signatures & bilinear maps

Worst Bank in the World uses BLS

So the bank adopts BLS: it writes a cheque and signs it with its secret key. Anyone can verify it; only the bank could have produced it.

Pay 1_000_000 σ

The bank signs the cheque using BLS:

σ←[sk] H(“Pay 1_000_000”)\sigma \leftarrow [\wit{sk}]\, \mathcal{H}(\text{``Pay 1\_000\_000''})

Anyone with the verification key vkvk can verify it:

e(σ,g2)=?e ⁣(H(“Pay 1_000_000”), vk)e(\sigma, g_2) \stackrel{?}{=} e\!\left(\mathcal{H}(\text{``Pay 1\_000\_000''}),\, vk\right)

watching…

Your worst friend

Just by seeing σ\sigma, your worst friend can cash the cheque: the bank pays whoever shows a valid signature.

2 · Signatures & bilinear maps

A new problem

The cheque is signed and verifiable. Now you hold a valid cheque and want to prove to a friend that the bank really signed it, without handing over σ\wit{\sigma}, or they could cash it themselves.

You want to prove "a valid σ\wit{\sigma} exists", i.e. that the verification equation has a solution, while keeping σ\wit{\sigma} hidden.

That's exactly a zero-knowledge proof about a bilinear-map equation. Enter Groth-Sahai.

3 · Groth-Sahai proofs

Groth-Sahai proofs

Groth-Sahai proofs [GS08] are efficient non-interactive zero-knowledge proofs for statements written as equations over a bilinear group. The richest kind is the pairing-product equation (PPE):

∏i=1ne(Ai,Yi)⋅∏i=1me(Xi,Bi)⋅∏i=1m∏j=1ne(Xi,Yj)γij=tT\prod_{i=1}^n e(\mathcal{A}_i, \wit{\mathcal{Y}_i}) \cdot \prod_{i=1}^m e(\wit{\mathcal{X}_i}, \mathcal{B}_i) \cdot \prod_{i=1}^m\prod_{j=1}^n e(\wit{\mathcal{X}_i}, \wit{\mathcal{Y}_j})^{\gamma_{ij}} = t_T

  • Constants · public Ai∈G1\mathcal{A}_i \in \mathbb{G}_1, Bi∈G2\mathcal{B}_i \in \mathbb{G}_2, tT∈GTt_T \in \mathbb{G}_T, γij∈Zp\gamma_{ij} \in \mathbb{Z}_p
  • Witness · secret X1,…,Xm∈G1\wit{\mathcal{X}_1, \ldots, \mathcal{X}_m} \in \mathbb{G}_1, Y1,…,Yn∈G2\wit{\mathcal{Y}_1, \ldots, \mathcal{Y}_n} \in \mathbb{G}_2

The prover knows a witness that satisfies the equation; the verifier becomes convinced without ever learning it.

3 · Groth-Sahai proofs

Four equation types

The same quadratic shape, over a different bilinear map, gives four equation types:

  • PPE · pairing product∏ie(Ai,Yi)⋅∏ie(Xi,Bi)⋅∏i,je(Xi,Yj)γij=tT\displaystyle\prod_i e(\mathcal{A}_i,\wit{\mathcal{Y}_i})\cdot\prod_i e(\wit{\mathcal{X}_i},\mathcal{B}_i)\cdot\prod_{i,j} e(\wit{\mathcal{X}_i},\wit{\mathcal{Y}_j})^{\gamma_{ij}}=t_TWitness: Xi∈G1\wit{\mathcal{X}_i}\in\mathbb{G}_1, Yj∈G2\wit{\mathcal{Y}_j}\in\mathbb{G}_2
  • MSME · multi-scalar in G1∑iyiAi+∑ibiXi+∑i,jγij yj Xi=T1\displaystyle\sum_i \wit{y_i}\mathcal{A}_i+\sum_i b_i\wit{\mathcal{X}_i}+\sum_{i,j}\gamma_{ij}\,\wit{y_j}\,\wit{\mathcal{X}_i}=\mathcal{T}_1Witness: Xi∈G1\wit{\mathcal{X}_i}\in\mathbb{G}_1, yj∈Zp\wit{y_j}\in\mathbb{Z}_p
  • MSME · multi-scalar in G2∑iaiYi+∑ixiBi+∑i,jγij xi Yj=T2\displaystyle\sum_i a_i\wit{\mathcal{Y}_i}+\sum_i \wit{x_i}\mathcal{B}_i+\sum_{i,j}\gamma_{ij}\,\wit{x_i}\,\wit{\mathcal{Y}_j}=\mathcal{T}_2Witness: xi∈Zp\wit{x_i}\in\mathbb{Z}_p, Yj∈G2\wit{\mathcal{Y}_j}\in\mathbb{G}_2
  • QE · quadratic in Zp∑iaiyi+∑ixibi+∑i,jγij xi yj≡t(modp)\displaystyle\sum_i a_i \wit{y_i}+\sum_i \wit{x_i} b_i+\sum_{i,j}\gamma_{ij}\,\wit{x_i}\,\wit{y_j}\equiv t\pmod{p}Witness: xi,yj∈Zp\wit{x_i},\wit{y_j}\in\mathbb{Z}_p
3 · Groth-Sahai proofs

Formally — the Groth-Sahai language

L:={ statement ∣ ∃ witness: E1(stmt,wit), …, En(stmt,wit) hold }\mathcal{L} := \Big\{\ \texttt{statement} \ \Big|\ \exists\, \wit{\texttt{witness}} :\ \mathcal{E}_1(\texttt{stmt}, \wit{\texttt{wit}}),\ \ldots,\ \mathcal{E}_n(\texttt{stmt}, \wit{\texttt{wit}})\ \text{hold}\ \Big\}

where each Ei\mathcal{E}_i is one of the four Groth-Sahai equation types over the variables:

Group variables

X1,…,Xm∈G1\wit{\mathcal{X}_1, \ldots, \mathcal{X}_m} \in \mathbb{G}_1

Y1,…,Yn∈G2\wit{\mathcal{Y}_1, \ldots, \mathcal{Y}_n} \in \mathbb{G}_2

Scalar variables

x1,…,xm′∈Zp\wit{x_1, \ldots, x_{m'}} \in \mathbb{Z}_p

y1,…,yn′∈Zp\wit{y_1, \ldots, y_{n'}} \in \mathbb{Z}_p

One proof shows that all the equations hold for one shared witness. GSkit's DSL, coming next, is a surface syntax for exactly this language: declare the witness and the equations, and the framework builds the proof.

4 · GSkit: the DSL and framework

The problem we want to solve

Writing one of these proofs by hand is intricate and error-prone: you commit every variable, build the aa, bb vectors and the γ\gamma matrix, and keep the prover's and verifier's views perfectly in sync.

The pain

Low-level commitments, easy to get wrong, hard to read; prover and verifier can drift apart.

The idea

Describe what the equation is, declaratively, and let a compiler generate the rest.

So we designed a small DSL: you declare the equation once, and the framework compiles both proving and verification.

4 · GSkit: the DSL and framework

Related work — and the gap

Zero-knowledge DSLs

Circom · ZoKrates · Noir · Cairo · Leo

They compile programs to circuits (R1CS, ACIR, AIR) for SNARK and STARK back-ends. None supports bilinear-group equations natively.

Groth-Sahai libraries

groth-sahai-rs · groth-sahai-python · a Java prototype

Programmatic APIs: the developer still classifies witnesses, picks equation types, builds commitments and names variables across sub-proofs.

GSkit fills the gap: Groth-Sahai statements written as declarative equations, not as circuits or API calls.

4 · GSkit: the DSL and framework

This thesis

  1. A DSL for Groth-Sahai statements. Declare variables, constants and equations; a type system infers each equation's type (PPE, MSME, QE) and rejects ill-formed specs before any proof is built.
  2. GSkit, a Python framework on Charm/PBC that compiles one spec into both the prover and the verifier, from the command line or from Python code with @gsfy.
  3. Two case studies, BLS and ABS-UCL, the latter compared against an earlier hand-written implementation.
4 · GSkit: the DSL and framework

A DSL for Groth-Sahai

A specification has just three blocks: which names are hidden (variables), which are public (constants), and the equations:

variables:
    <hidden names> : G1 | G2 | ZP

constants:
    <public names> : G1 | G2 | ZP | GT

equations:
    <term> + <term> + ... = <name>
  • variables — the witness, what stays secret (only G1, G2, ZP)
  • constants — public values, including the right-hand side (GT allowed here)
  • equations — sums of product terms; * is the bilinear operation, + combines terms
4 · GSkit: the DSL and framework

Reading a term

Each term is a product of names. Which groups the names live in decides the equation type, and the compiler infers it for you:

∏i=1ne(Ai,Yi)⋅∏i=1me(Xi,Bi)⋅∏i,je(Xi,Yj)γij=tT\prod_{i=1}^n e(\mathcal{A}_i, \wit{\mathcal{Y}_i}) \cdot \prod_{i=1}^m e(\wit{\mathcal{X}_i}, \mathcal{B}_i) \cdot \prod_{i,j} e(\wit{\mathcal{X}_i}, \wit{\mathcal{Y}_j})^{\gamma_{ij}} = t_T

  • const · var   e(Ai,Yi)e(\mathcal{A}_i, \wit{\mathcal{Y}_i})  →  written A * Y
  • var · const   e(Xi,Bi)e(\wit{\mathcal{X}_i}, \mathcal{B}_i)  →  written X * B
  • var · var, scaled   e(Xi,Yj)γije(\wit{\mathcal{X}_i}, \wit{\mathcal{Y}_j})^{\gamma_{ij}}  →  written gamma * X * Y
4 · GSkit: the DSL and framework

BLS proof to my worst friend

Back to the cheque. You (the prover) know σ\wit{\sigma}; your friend (the verifier) must be convinced without seeing it.

Prover · you

knows the signature σ\wit{\sigma}

e(σ, g2)=tTe(\wit{\sigma},\, g_2) = t_T

sends π σ stays hidden

Verifier · your worst friend

never sees σ\wit{\sigma}

checks e( ? , g2)=tTe(\,?\,,\, g_2) = t_T

Key insight: your friend learns that a valid signature exists, but never sees σ\wit{\sigma} itself.

tT←e ⁣(H(“Pay 1_000_000”), vk)e(σ, g2)=tTt_T \leftarrow e\!\left(\mathcal{H}(\text{``Pay 1\_000\_000''}),\, vk\right) \qquad e(\wit{\sigma},\, g_2) = t_T

4 · GSkit: the DSL and framework

The BLS proof, in the DSL

The whole statement "I know a σ\wit{\sigma} such that e(σ,g2)=tTe(\wit{\sigma}, g_2) = t_T" becomes a few lines. The secret σ\wit{\sigma} is a variable; everything else is a constant:

  • σ\wit{\sigma} is the witness → declared under variables
  • g2g_2 and the target tTt_T are public → constants
  • a single PPE: signature * g2 = rhs

The compiler reads the types and recognises a pairing-product equation, with no manual setup.

variables:
    signature: G1

constants:
    g2:  G2
    rhs: GT

equations:
    signature * g2 = rhs
4 · GSkit: the DSL and framework

One spec, both sides

The same typed spec compiles into two programs, so the prover's and the verifier's view of the equations can never drift apart:

witness spec.gs the only source Parser Type checker PPE · MSME · QE caught at spec time type error Prover proof.py Verifier verify.py proof π commitments + proofs ✓ / ✗

Inside Python, the @gsfy decorator reads the same spec from a GS_STRING in the function and wires its variables automatically.

5 · Case study: ABS-UCL

Where it all began: an anonymous forum

BLS was a warm-up. This thesis started from a concrete goal: an anonymous forum, where members prove they belong without revealing who they are. But anonymity alone has a catch:

Anonymous forum · #park-policy4 posts
anon_4821In my opinion we should kick puppies at the park.
anon_1337Totally agree. Finally someone said it.
anon_0042+1. Those puppies had it coming.
dog_lover_77As a dog lover, I fully support this.
▲ 4 agree · 0 disagree

One clown, four accounts

Sybil attack
one person behind many fake identities:
a consensus out of thin air.

Not just a forum problem: sockpuppet accounts and bot farms manufacture consensus in today's public debate and elections, a real threat to democracy.

5 · Case study: ABS-UCL

The fix: ABS-UCL

Attribute-based signatures with user-controlled linkability [EKCGD14, EG17]. Every post carries one signature proving:

  • "my attributes satisfy the policy" (say, UChile student), revealing neither who signed nor which attributes;
  • a well-formed linking token τ\tau, derived from the author's secret key usk\wit{usk} and the thread.
#park-policysigned with ABS-UCL
τ 9c4e…a1In my opinion we should kick puppies at the park.
τ 9c4e…a1Totally agree. Finally someone said it.
τ 9c4e…a1+1. Those puppies had it coming.
τ 9c4e…a1As a dog lover, I fully support this.
4 posts · 1 author

Same author, same thread, same τ\tau: the four "supporters" count as one voice. Across threads the tokens look unrelated, so authors stay anonymous. Privacy and accountability, in one signature.

5 · Case study: ABS-UCL

One signature, four sub-protocols

A single ABS-UCL signature is a conjunction of zero-knowledge statements, each from an independent sub-protocol: many Groth-Sahai equations proved as one.

  • RPSPSThe attribute keys the user holds were genuinely issued by the authorities.Re-randomizable structure-preserving signatures
  • MSPThose attributes satisfy the access policy.Monotone span program
  • LITThe linking token is well-formed: the key to controlled linkability.Linking token
  • FBB · PSDOA pseudo-attribute provides a distinguished branch, so the policy is always satisfiable.Full Boneh–Boyen signature [BB04]
5 · Case study: ABS-UCL

The payoff: compose, don't duplicate

Each sub-protocol declares its Groth-Sahai logic once with @gsfy; the scheme composes these specs over a shared context, and both prover and verifier come from that single source.

The old way · manual sign() 85 lines ≈ verify() 84 lines every equation is written twice, and the copies can drift apart GSkit · modular RPSPS MSP LIT FBB GSContext shared context Prover one proof, all specs Verifier generated each equation is written once, inside its sub-protocol
5 · Case study: ABS-UCL

The result

The decisive evidence is not fewer total lines, but the elimination of duplicated, hand-maintained equation code:

Equation-construction effortManualGSkit (modular)
Lines in sign()858 declarative equations
Lines in verify()840, generated
Hand-built equation / pairing-map objects600
Times each equation is written21

Total developer-written code is not smaller (420 → 540 lines): each sub-protocol now carries its own spec.

The contribution: moving the equations into a single declarative source is what lowers the error surface, and makes a scheme as complex as ABS-UCL practical to build and maintain.

6 · Evaluation & conclusions

Performance

Proving and verifying a pairing-product statement takes time linear in the number of variables and in the number of equations.

VerifyProve

Growing the number of variables 0 1 2 3 4 s 10 50 100 variables Verify · 10 variables: 774 ms Verify · 20 variables: 1,112 ms Verify · 30 variables: 1,467 ms Verify · 40 variables: 1,764 ms Verify · 50 variables: 2,100 ms Verify · 60 variables: 2,466 ms Verify · 70 variables: 2,795 ms Verify · 80 variables: 3,105 ms Verify · 90 variables: 3,467 ms Verify · 100 variables: 3,778 ms Verify 3.8 s Prove · 10 variables: 231 ms Prove · 20 variables: 303 ms Prove · 30 variables: 344 ms Prove · 40 variables: 411 ms Prove · 50 variables: 442 ms Prove · 60 variables: 501 ms Prove · 70 variables: 563 ms Prove · 80 variables: 627 ms Prove · 90 variables: 684 ms Prove · 100 variables: 737 ms Prove 0.7 s Growing the number of equations 0 4 8 12 s 1 5 10 equations Verify · 1 equations: 1,446 ms Verify · 2 equations: 2,806 ms Verify · 3 equations: 4,049 ms Verify · 4 equations: 5,469 ms Verify · 5 equations: 6,613 ms Verify · 6 equations: 8,066 ms Verify · 7 equations: 9,047 ms Verify · 8 equations: 10,496 ms Verify · 9 equations: 11,382 ms Verify · 10 equations: 12,614 ms Verify 12.6 s Prove · 1 equations: 345 ms Prove · 2 equations: 406 ms Prove · 3 equations: 480 ms Prove · 4 equations: 556 ms Prove · 5 equations: 643 ms Prove · 6 equations: 736 ms Prove · 7 equations: 795 ms Prove · 8 equations: 858 ms Prove · 9 equations: 921 ms Prove · 10 equations: 967 ms Prove 1.0 s

GSkit on Charm/PBC, BN254 curve. Data from the thesis evaluation.

6 · Evaluation & conclusions

Conclusions

What we showed

  • One declarative spec per statement: prover and verifier are generated from it, so they cannot drift apart.
  • Type checking moves a class of errors from run time to specification time.
  • On ABS-UCL, 169 hand-written lines and 60 equation objects become 8 declarative equations, written once.

Future work

  • Batch verification and proof-size optimizations
  • More case studies beyond BLS and ABS-UCL
  • End to end: the anonymous attribute-based forum that motivated this work

Hypothesis confirmed: a domain-specific language lowers the barrier to building Groth-Sahai proofs, reducing effort and error surface without giving up their security guarantees.

Thank you

Questions?

Benjamín Hurtado Torrealba

GSkit: a domain-specific language and framework for Groth-Sahai proofs

More at benjamin.hurta.do/gskit

Backup

Is GSkit sound?

Three separate questions:

  • The proofsGSkit generates standard Groth-Sahai proofs [GS08] over BN254 (SXDH): no new cryptographyWith the soundness CRS the proofs are perfectly sound; with the WI CRS they are sound under SXDH
  • The languageFormal grammar and typing rules: a well-typed spec elaborates into a Groth-Sahai equation of the inferred typeThat property is not formally proven: mechanizing it is future work
  • The implementationThe prover and the verifier come from the same elaboration, so they cannot disagreeBLS end to end: the valid signature verifies and a forged one is rejected, with both CRS types

GSkit proves exactly the equation you write. Whether that equation is the right one for the protocol is still up to whoever writes it.

Backup

WI or zero-knowledge?

In Groth-Sahai [GS08] every equation admits WI proofs, but only MSMEs, QEs and PPEs with tT=1t_T = 1 are ZK.

  • The BLS proof we showed is a PPE with tT=e(H(m),vk)≠1t_T = e(\mathcal{H}(m), vk) \neq 1: it is only WI.
  • And BLS signatures are unique: with a single possible witness, WI does not hide it.

To make it ZK: also commit to Y=H(m)\wit{Y} = \mathcal{H}(m) and prove two equations, a PPE with tT=1t_T = 1 and a linear MSME in G1\mathbb{G}_1, both ZK:

e(σ,g2)⋅e(Y,vk)−1=1TY=H(m)e(\wit{\sigma}, g_2) \cdot e(\wit{Y}, vk)^{-1} = 1_T \qquad\qquad \wit{Y} = \mathcal{H}(m)

In the DSL that is one more witness and one MSME equation; the thesis typing rules cover both.

Backup

What does ABS-UCL assume against Sybil attacks?

The linking token is a weak Boneh–Boyen signature on the thread, made with the author's key:

τ=[1usk+thread]g\tau = \left[\dfrac{1}{\wit{usk} + \text{thread}}\right] g

  • It is deterministic: the same author in the same thread gets the same τ\tau, so each person has one voice per thread.
  • Tokens from different threads cannot be linked: the author stays anonymous.

Assumption: each person holds a single key usk\wit{usk}. The authority that issues the attributes must certify one key per person, e.g. one per national ID. Anyone who gets several keys gets several τ\tau: ABS-UCL does not prevent that, because it is a registration problem, not a cryptographic one.

References

[GS08]J. Groth, A. Sahai. Efficient Non-interactive Proof Systems for Bilinear Groups. EUROCRYPT 2008, LNCS 4965, pp. 415–432.

[BLS04]D. Boneh, B. Lynn, H. Shacham. Short Signatures from the Weil Pairing. Journal of Cryptology 17(4), pp. 297–319, 2004.

[BB04]D. Boneh, X. Boyen. Short Signatures Without Random Oracles. EUROCRYPT 2004, pp. 56–73.

[EKCGD14]A. El Kaafarani, L. Chen, E. Ghadafi, J. Davenport. Attribute-Based Signatures with User-Controlled Linkability. CANS 2014, pp. 256–269.

[EG17]A. El Kaafarani, E. Ghadafi. Attribute-Based Signatures with User-Controlled Linkability Without Random Oracles. IMACC 2017, pp. 161–184.

FiguresAli Baba's cave illustrations by Dake, Wikimedia Commons, CC BY 2.5.

Presentarse y agradecer a la comisión. La tesis presenta GSkit, un lenguaje de dominio específico y un framework para construir pruebas de Groth-Sahai. El hilo de la charla va de pruebas de conocimiento cero, a firmas BLS, a Groth-Sahai, y termina con GSkit aplicado a ABS-UCL.

Las tres primeras secciones son el contexto necesario para entender el problema. La contribución está en las secciones 4 a 6.

Partir con la intuición, sin fórmulas. Ejemplos cotidianos: mostrar el carnet para probar la edad entrega mucha más información que la edad.

La cueva tiene dos caminos, A y B, unidos por una puerta que solo se abre con la palabra secreta. Una ronda tiene tres pasos: Peggy se compromete con un camino, Victor la desafía y Peggy responde. Si Peggy no conoce la palabra, solo puede responder bien si adivinó el lado.

Cada propiedad tiene una lectura directa en la cueva. Para zero-knowledge, la idea clave es el simulador: Victor podría fabricar un video idéntico sin la ayuda de Peggy, así que el video no le enseña nada.

La cueva es interactiva; las pruebas que nos interesan son no interactivas: un solo mensaje π. Notar que Verify nunca recibe el witness w. Desde aquí, el color ámbar marca siempre lo secreto.

La historia que recorre la charla. El banco emite cheques firmados; tú recibes uno; tu "peor amigo" lo está mirando y le encantaría cobrarlo o falsificarlo. La tarjeta resume las tres operaciones de un esquema de firma.

Unforgeability: sin sk nadie puede producir una firma válida para un mensaje nuevo. Con eso, pasamos a la herramienta matemática que hace funcionar BLS.

GSkit usa la curva BN254 a través de Charm/PBC. Si preguntan: el emparejamiento además es no degenerado y eficientemente computable.

Lo importante para lo que viene: la verificación de BLS es una sola ecuación de emparejamientos.

Aquí la firma σ es pública: va escrita en el cheque, y cualquiera con vk puede verificarla. Click: vuelve tu peor amigo. Para verificar el cheque tiene que ver σ, y con solo verla ya puede cobrarlo: el banco le paga a quien presente una firma válida. En la siguiente slide cambia el escenario y σ pasa a ser el secreto.

Desde aquí σ se marca en ámbar: es el witness. El enunciado es "existe una firma válida", no "esta es la firma".

El prover se compromete a cada variable y entrega elementos de prueba; el verificador revisa ecuaciones sobre los compromisos. Ojo con la terminología: en general GS da pruebas NIWI; son zero-knowledge para MSME y QE, y para PPE cuando t_T = 1.

Los cuatro tipos son la misma forma cuadrática instanciada con distintos mapas bilineales: e, multiplicación escalar en G1 o en G2, y producto en Zp. Lo único que cambia es dónde viven las variables, y eso es exactamente lo que el type checker de GSkit infiere.

Este es el lenguaje que GSkit sabe probar: conjunciones de ecuaciones de los cuatro tipos sobre un witness compartido.

Hipótesis de la tesis: un DSL específico para Groth-Sahai reduce la complejidad y los errores de implementar estas pruebas.

Los DSL de ZK conocidos apuntan a circuitos de propósito general; traducir ecuaciones de pairings a circuitos pierde claridad. Las bibliotecas de Groth-Sahai existentes obligan a hacer a mano lo que GSkit automatiza.

Las tres contribuciones; el resto de la charla las recorre en este orden.

La gramática está escrita en Lark. El type checker clasifica cada variable y arma los vectores a, b y la matriz γ de cada ecuación.

Los tres tipos de término de una PPE corresponden a tres formas sintácticas en el DSL. El desarrollador nunca escribe los vectores ni la matriz γ: salen de los tipos.

El prover eres tú, que tienes el cheque; el verificador es el amigo. t_T se calcula con datos públicos: el mensaje y la clave del banco. Posible pregunta: con t_T distinto de 1, GS08 da WI y no ZK. La forma estándar de obtener ZK es comprometer también H(m) con una ecuación lineal y dejar la PPE con lado derecho 1.

Comparar con lo que habría que escribir a mano: compromisos, vectores, matriz γ, y la verificación por separado.

El parser y el type checker son comunes a ambos lados; un error de tipos se detecta antes de construir cualquier prueba. Solo el prover recibe el witness. El verificador recibe π: compromisos y elementos de prueba.

Esta fue la motivación original de la tesis: un foro anónimo donde los miembros prueban que pertenecen (por ejemplo, ser estudiantes de la Universidad de Chile) sin revelar quiénes son. El problema es que con anonimato total nada impide que una misma persona cree muchas identidades. Click: las cuatro cuentas son la misma persona, un solo payaso detrás de todas. Eso es un ataque Sybil: una persona se hace pasar por muchas para fabricar un consenso. Click: no es solo un problema de foros. Las cuentas falsas y las granjas de bots fabrican consenso en el debate público y en elecciones, y eso daña la democracia.

ABS-UCL resuelve justamente eso. Cada post lleva una firma que prueba que los atributos del autor cumplen la política, sin revelar quién firma ni qué atributos usó. Además lleva un linking token τ, calculado con la clave secreta del autor y el hilo (en el paper el hilo es el "recipient"). Mismo autor y mismo hilo dan el mismo τ: las cuatro cuentas cuentan como una sola voz. En hilos distintos los τ no se pueden relacionar, así que el autor sigue siendo anónimo. Ejemplo de la tesis: en un foro médico, un doctor mantiene una identidad consistente dentro de un hilo sin ser vinculable entre discusiones distintas. Si preguntan: esto supone que las autoridades entregan atributos a una sola clave por persona; si alguien pudiera registrar muchas claves, el ataque Sybil volvería.

Cada subprotocolo aporta su propio conjunto de ecuaciones Groth-Sahai al enunciado completo. Esa estructura es justamente lo que motiva un tratamiento modular.

A la izquierda, la implementación manual previa: las mismas ecuaciones armadas en sign() y otra vez en verify(). A la derecha, cada subprotocolo trae su spec con @gsfy; sign() agrega cada spec al contexto con una sola llamada por atributo, y la verificación se genera.

Ser honesto con las líneas totales: el código modular es algo más largo porque cada subprotocolo trae su especificación. Lo que importa es que cada ecuación se escribe una sola vez y la verificación se deriva de ella.

Ambas curvas crecen linealmente, tanto con el número de variables como con el de ecuaciones. Verificar cuesta más que probar porque la verificación evalúa emparejamientos por cada ecuación, y probar usa principalmente operaciones de grupo.

Volver a la hipótesis: un DSL de alto nivel baja la barrera para construir pruebas de Groth-Sahai, y los casos de estudio lo respaldan.

Todo el material queda en benjamin.hurta.do/gskit: la tesis, el póster, el repositorio y estas slides.

Respuesta corta: la soundness criptográfica es la de Groth-Sahai, y GSkit no la modifica. Lo que aporta el lenguaje es que lo que escribes es lo que se prueba: el sistema de tipos asegura que cada ecuación es una ecuación de Groth-Sahai bien formada del tipo correcto, y el prover y el verifier se derivan de esa misma ecuación. Ser honesto: no hay una demostración formal de que la elaboración preserve el significado. Está descrita con reglas de inferencia en la tesis y validada con los casos de estudio. Mecanizarla, por ejemplo conectando con EasyCrypt como dice la tesis, es trabajo futuro. Si preguntan por ABS-UCL: la evaluación fue a nivel de especificación (líneas y ecuaciones). En la implementación actual falta el chequeo de tipos de las ecuaciones MSME, así que la prueba compuesta de ABS-UCL todavía no se ejecuta de punta a punta. BLS sí: verificado con ambos tipos de CRS.

Si preguntan: la PPE de BLS tiene lado derecho distinto de 1, y para esas ecuaciones GS08 solo da WI. Además la firma BLS es única para cada mensaje, así que WI por sí sola no oculta nada: hace falta ZK. La solución estándar de GS08: comprometer también H(m) como una variable Y, probar con una ecuación lineal que Y = H(m), y reescribir la PPE con lado derecho 1. Ambas ecuaciones son ZK. Ojo: en la implementación actual el chequeo de tipos de las ecuaciones MSME no está terminado, así que esta versión no corre hoy en GSkit. No prometer una demostración en vivo.

Si preguntan cómo evita ABS-UCL el ataque Sybil: el token τ es determinista para cada par (autor, hilo), así que las cuatro cuentas del payaso tendrían el mismo τ. Pero eso supone una clave por persona: la protección real contra Sybil está en el registro, cuando la autoridad entrega los atributos. ABS-UCL hace que esa garantía sobreviva al anonimato. En el código de GSkit, τ es la firma WBB del recipient (el hilo) con usk: lit.sign(usk, recip).