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 Vectores de test e implementación de referencia

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, PROTOCOL.md y SECURITY-ANALYSIS.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

Credencial de sesión del VG

  • PROTOCOL.md contiene la sección de credencial de sesión
  • El campo session_expires_at está documentado

Endpoints de descubrimiento

  • PROTOCOL.md especifica el endpoint .well-known/aavp-issuer (IM)
  • PROTOCOL.md especifica el endpoint .well-known/aavp (VG) con vg_endpoint
  • El campo accepted_token_types está documentado
  • No quedan referencias a esquemas de algoritmo obsoletos en los ejemplos

Generación segura del nonce

  • PROTOCOL.md especifica APIs de CSPRNG del SO por plataforma

Segmentation Accountability Framework (SAF)

  • Sección SAF presente en PROTOCOL.md
  • Endpoint .well-known/aavp-age-policy.json especificado
  • Taxonomía de contenido con 6 categorías mínimas definida
  • Policy Transparency Log (PTL) especificado
  • Open Verification Protocol (OVP) especificado
  • SECURITY-ANALYSIS.md referencia al SAF
  • Campo age_policy en endpoint .well-known/aavp

Supuestos de seguridad y device attestation

  • PROTOCOL.md contiene la sección de supuestos de seguridad
  • PROTOCOL.md contiene la sección de device attestation / key attestation
  • SECURITY-ANALYSIS.md referencia las nuevas secciones de PROTOCOL.md

Resistencia al análisis de tráfico

  • PROTOCOL.md especifica pre-firma y desacoplamiento temporal
  • PROTOCOL.md especifica padding de mensajes
  • PROTOCOL.md referencia RFC 9458 (OHTTP)
  • PROTOCOL.md referencia RFC 9614 (privacy partitioning)

Metodología de muestreo OVP

  • PROTOCOL.md especifica metodología de muestreo para el OVP
  • PROTOCOL.md especifica ugc_handling en el esquema SPD
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.

Vectores de test e implementación de referencia

Activa
Vectores de test e implementación de referencia

Implementación de referencia en Go del protocolo AAVP con verificación completa contra vectores de test. Cubre codificación binaria del token, lógica de validación del VG y el flujo criptográfico de emisión (RSAPBSSA-SHA384) en sus 6 pasos: preparación, cegamiento, derivación de clave, firma ciega, finalización y verificación.

Codificación binaria del token (4 vectores)

  • Encode produce la estructura esperada de 331 bytes para cada franja de edad
  • Los offsets y tamaños de cada campo son correctos
  • Decode invierte correctamente la codificación (round-trip)

Validación del VG (14 vectores)

  • Tokens válidos con diferentes franjas se aceptan
  • Tokens expirados se rechazan (con y sin tolerancia de clock skew)
  • expires_at excesivamente futuro se rechaza (TTL máximo)
  • age_bracket fuera de rango, token_type inválido y tamaño incorrecto se rechazan
  • Authenticator manipulado se detecta

Flujo de emisión — preparación y cegamiento (4 vectores)

  • Step 1: message_to_sign y public_metadata coinciden con el vector
  • Step 2: Blind con r determinista produce blinded_msg e inv correctos

Flujo de emisión — firma y verificación (4 vectores)

  • Step 3: DeriveKeyPair produce sk’ y pk’ correctos via HKDF-SHA384
  • Step 4: BlindSign produce blind_sig correcto
  • Step 5: Finalize produce authenticator correcto
  • Step 6: Verify confirma firma válida
  • Token completo ensamblado coincide con expected_token
Ver script Ver ejecuciones

Referencias

  1. RFC 9474 — RSA Blind Signatures. Amjad, Celi, Davidson, Wood, Armando. IRTF, 2023.
  2. Partially Blind RSA Signatures — draft-amjad-cfrg-partially-blind-rsa. Amjad, Celi, Davidson, Wood.

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