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).