GSkit: Un DSL/framework para Pruebas de Groth-Sahai

Tesis de Magíster en Ciencias, mención Computación, y Memoria de Ingeniería Civil en Computación — Universidad de Chile.

Autor: Benjamín Hurtado · Profesores guía: Matías Toro, Federico Olmedo

Resumen

Las pruebas de Groth-Sahai son pruebas de conocimiento cero (Zero-Knowledge Proof) no interactivas (NIZK/NIWI), eficientes y ampliamente usadas en firmas de grupo, credenciales anónimas, votación electrónica y firmas basadas en atributos.

Su construcción manual es laboriosa, de bajo nivel, propensa a errores y está fuertemente acoplada a las primitivas de emparejamientos bilineales (bilinear pairings): cada ecuación se construye una vez para probar y, casi idénticamente, otra vez para verificar. No existe una herramienta de alto nivel que abstraiga esta complejidad.

GSkit es un DSL en Python que permite especificar pruebas de Groth-Sahai de forma declarativa, abstrayendo la complejidad matemática subyacente con una sintaxis cercana a la notación del esquema.

Objetivos

Presentar GSkit, un DSL en Python para especificar pruebas de Groth-Sahai de forma declarativa.
Abstraer la complejidad matemática subyacente con una sintaxis cercana a la notación del esquema.
Detectar errores en tiempo de especificación, no en tiempo de ejecución, mediante una gramática estructurada y verificación de tipos.
Generar automáticamente, a partir de una única especificación, el código de generación y de verificación de la prueba.
Evaluar el enfoque en dos casos de estudio de complejidad creciente (BLS y ABS-UCL), comparándolo contra una implementación manual previa.

Metodología

El desarrollador anota su código de verificación con el decorador @gsfy y declara variables, constantes y ecuaciones del esquema. Un sistema de tipado fuerte y estático valida que la especificación esté bien formada antes de construir la prueba, trasladando una clase de errores desde el tiempo de ejecución al tiempo de especificación.

@gsfy
def verify(self, vk, m, signature):
    g2 = self.g2
    lhs = signature.pair(g2)
    rhs = G1Element.hash_from_string(m).pair(vk)
    GS_STRING = """
    variables: signature : G1
    constants: g2 : G2, rhs : GT
    equations: signature * g2 = rhs
    """
    return lhs == rhs

A partir de la especificación (variables, constantes y ecuaciones), GSkit verifica los tipos y genera automáticamente tanto el código de generación como el de verificación de la prueba.

Resultados

BLS: se extrae una única ecuación de producto de emparejamientos desde la rutina de verificación de firma, con mínimo esfuerzo.

ABS-UCL: esquema compuesto por varios subprotocolos que comparten ecuaciones (política MSP, token de enlace, firmas de atributos aleatorizadas, pseudo-atributo).

Manualmente: 85 líneas en sign() + 84 casi idénticas en verify() = 169 líneas duplicadas, con 60 objetos construidos a mano. Con GSkit: 8 ecuaciones declarativas escritas una sola vez.
El total de líneas no es la métrica relevante (de hecho sube de 420 a 540, pues cada subprotocolo suma su propia especificación); lo que se elimina es el código de ecuaciones duplicado, que es donde ocurren los errores.

Conclusiones

GSkit simplifica la construcción de pruebas de Groth-Sahai para desarrolladores, reduciendo el esfuerzo y la probabilidad de error sin sacrificar la seguridad. Traslada una clase de errores del tiempo de ejecución al tiempo de especificación, eliminando el código duplicado sin comprometer las garantías de seguridad criptográfica, y facilita la adopción de ZKP complejas en aplicaciones criptográficas.

Trabajo futuro: verificación por lotes, más ejemplos, e integración en una aplicación completa (el foro anónimo que motivó este trabajo).