Verificación automatizada

AAVP se auto-examina con cada cambio. Un sistema de verificación automática comprueba que la especificación es coherente, que las propiedades de seguridad se cumplen y que las implementaciones son correctas.

Consistencia de la especificación Verificación formal del protocolo

Por qué verificamos

Un protocolo de seguridad no puede permitirse ambigüedades ni contradicciones en su documentación. Si la especificación técnica dice una cosa y el white paper dice otra, los implementadores producirán software incompatible. Si un campo del token aparece en un documento pero no en otro, las auditorías de seguridad partirán de premisas incorrectas.

La verificación automatizada garantiza que cada cambio en la especificación — por pequeño que sea — se valida contra el resto de documentos antes de ser aceptado. No es un sustituto de la revisión humana, pero es una primera línea de defensa contra errores silenciosos.

Consistencia de la especificación

Activa
Consistencia de la especificación

Verifica que los documentos de la especificación (README.md, PROTOCOL.md, SECURITY-ANALYSIS.md) son coherentes entre sí: versiones, campos del token, terminología, esquema criptográfico y referencias cruzadas.

Coherencia de versión

  • La versión en VERSION coincide con las cabeceras y pies de README.md y PROTOCOL.md

Tamaño del token

  • No quedan referencias obsoletas a tamaños anteriores del token
  • PROTOCOL.md especifica el tamaño correcto (331 bytes)

Campos canónicos del token

  • Los 6 campos activos están documentados en PROTOCOL.md
  • Los campos eliminados no aparecen como parte activa de la estructura

Franjas de edad

  • Las 4 franjas (UNDER_13, AGE_13_15, AGE_16_17, OVER_18) están definidas

Esquema criptográfico

  • RSAPBSSA-SHA384 y RFC 9474 están referenciados en PROTOCOL.md y SECURITY-ANALYSIS.md

Terminología

  • Device Agent no se equipara con control parental
  • Los roles del protocolo usan sus nombres canónicos

Coherencia cruzada

  • Terminología de firmas ciegas coherente entre documentos
  • Franjas de edad coherentes entre README.md y PROTOCOL.md

Formato binario del token

  • Los offsets de la tabla binaria son secuenciales (cada offset = anterior + tamaño)
  • La suma total de campos coincide con el tamaño declarado (331 bytes)

Semáforo de seguridad

  • El recuento de áreas rojas, amarillas y verdes en el resumen coincide con los iconos de la tabla

Integridad del CHANGELOG

  • Existe la sección [Unreleased] (necesaria para el workflow de release)
  • El link de comparación de [Unreleased] apunta a la versión actual
Ver script Ver ejecuciones

Referencias

  1. Keep a Changelog 1.1.0 — Convención de registro de cambios adoptada por AAVP
  2. Semantic Versioning 2.0.0 — Esquema de versionado seguido por el proyecto

Verificación formal del protocolo

Activa
Verificación formal del protocolo

Modelo formal en Tamarin Prover que demuestra matemáticamente las propiedades de seguridad del protocolo. Dos modelos independientes: uno para propiedades de traza (unforgeability, ejecutabilidad) y otro para equivalencia observacional (unlinkability).

Propiedades de seguridad (aavp.spthy)

  • Ejecutabilidad: el protocolo puede completarse (comprobación de cordura)
  • Unforgeability: un token verificado implica participación del IM con los mismos metadatos
  • Unforgeability con compromiso: un token verificado implica participación del IM o compromiso de clave
  • Unicidad de nonce: cada emisión produce un nonce diferente
  • Vinculación de metadatos: age_bracket y expires_at no pueden alterarse tras la firma

Unlinkability (aavp-unlinkability.spthy)

  • Equivalencia observacional: dos tokens de DA distintos (misma franja) son indistinguibles
  • Anonimato intra-franja: el IM no puede vincular un token finalizado con el DA que lo solicitó

Modelo de adversario

  • Dolev-Yao: adversario con control total de la red (intercepta, modifica, inyecta)
  • Colusión IM + plataforma: el adversario ve tanto mensajes cegados como tokens finales
  • Compromiso de claves: modelado explícito de revelación de clave del IM
Ver script Ver ejecuciones

Referencias

  1. Tamarin Prover — Herramienta de verificación formal de protocolos de seguridad. Basin, Cremers, Dreier, Meier, Sasse, Schmidt.
  2. RFC 9474 — RSA Blind Signatures. Amjad, Celi, Davidson, Wood, Armando. IRTF, 2023.
  3. Partially Blind RSA Signatures — draft-amjad-cfrg-partially-blind-rsa. Amjad, Celi, Davidson, Wood.
  4. Blind Signatures for Untraceable Payments — David Chaum. Advances in Cryptology (CRYPTO), 1983.
  5. Automated Verification of Security Protocols with Tamarin — Meier, Schmidt, Cremers, Basin. CAV, 2013.
  6. Privacy Pass: A Formal Analysis — Davidson, Faz-Hernandez, Sullivan, Wood. ePrint 2025/2022.

Verificaciones en desarrollo

Las siguientes verificaciones están planificadas y se incorporarán progresivamente a la suite de CI. Cuando estén activas, sus badges aparecerán junto al de consistencia de la especificación.

Vectores de test

Planificada

Suite de vectores de prueba con entradas y salidas conocidas para validar que cualquier implementación de AAVP produce resultados correctos. Requiere la implementación de referencia del protocolo.

Generación de tokens

  • Token generado con nonce conocido produce la estructura esperada de 331 bytes
  • Los offsets y tamaños de cada campo son correctos

Validación

  • Tokens expirados se rechazan
  • Tokens con age_bracket manipulado se detectan
  • Tokens con authenticator inválido se rechazan

Interoperabilidad

  • Tokens generados por diferentes implementaciones son mutuamente verificables

Transparencia total

Los scripts de verificación, los workflows de CI y los resultados de cada ejecución son públicos. Cualquiera puede auditarlos, reproducirlos localmente o proponer nuevas comprobaciones.

Ver scripts Ver ejecuciones Especificación Técnica