Google DeepMind anunció el 10 de noviembre que había verificado formalmente, gracias a agentes de inteligencia artificial, propiedades de seguridad esenciales del protocolo de cifrado de Signal, el mismo que protege WhatsApp y Google Messages. El trabajo, realizado por cinco personas en cuatro semanas con una herramienta llamada AlphaProof Code, habría requerido años a expertos humanos. Pero no garantiza que la aplicación Signal no tenga fallos, y su coste sigue siendo desconocido.
Lo que DeepMind ha demostrado
La verificación formal no consiste en probar un programa con miles de casos: establece, mediante una demostración matemática comprobada por una máquina, que una propiedad es cierta en todas las situaciones previstas por el modelo. Según The Register, el equipo centró su esfuerzo en dos componentes del protocolo: PQXDH, el apretón de manos diseñado para resistir a los futuros ordenadores cuánticos, y el Triple Ratchet, que renueva las claves a medida que se intercambian mensajes.
Las propiedades demostradas afectan al núcleo de la promesa de Signal: la confidencialidad persistente (un mensaje antiguo sigue protegido aunque una clave se filtre más tarde), la autenticación de los interlocutores, la recuperación tras el compromiso temporal de un dispositivo y el secreto del intercambio inicial. Los investigadores reivindican una primicia: una IA habría ayudado a construir una demostración que vincula estas garantías teóricas con una implementación criptográfica realmente utilizada, a nivel de código máquina.
Cómo funciona AlphaProof Code
La herramienta es un sistema multiagente. Expertos en criptografía definen lo que hay que demostrar; varios modelos traducen esos objetivos en una especificación que los expertos revisan, y después agentes basados en Gemini Carbon, el modelo de Google, redactan las demostraciones en Lean, un asistente de demostración cuyo núcleo verifica cada paso. The Register menciona unos 6,5 millones de líneas de Lean generadas, seguidas de una auditoría automática que señala los pasajes que debe revisar un humano. Según el blog de DeepMind, que habla de más de seis millones de líneas, esta revisión humana solo afectó a cerca del 1 % del código.
Para asegurarse de que la herramienta no valida cualquier cosa, el equipo hizo una prueba a la inversa. Según 9to5Mac, versiones antiguas de Signal, portadoras de vulnerabilidades conocidas, fueron efectivamente señaladas como fallidas en la verificación. DeepMind precisa que dos errores reales, corregidos desde entonces, se reintrodujeron en una copia aislada del código: en ambos casos, el sistema produjo una demostración verificada por la máquina de que la versión defectuosa no era segura.
El investigador Swarat Chaudhuri, de DeepMind y de la Universidad de Texas en Austin, insiste en el papel de los humanos. Citado por The Register, considera que la próxima dificultad ya no será la demostración sino la especificación, es decir, la definición exacta de lo que el software debe garantizar. Por parte de Signal, su director técnico Ehren Kret, citado por DeepMind, califica de «major breakthrough» el hecho de que unos agentes traduzcan código en producción a teoremas de Lean válidos, ya que las verificaciones formales anteriores se habían centrado en porciones más reducidas del código.
Lo que este trabajo no demuestra
El titular de 9to5Mac, que habla de un cifrado «demostrado seguro», va más allá del contenido. La demostración se refiere al protocolo y a algunas de sus garantías, no a la aplicación Signal entera, ni a la forma en que WhatsApp o Google Messages lo han integrado. The Register recuerda también que el resultado supone una criptografía perfecta: no dice nada sobre la solidez matemática de los propios algoritmos.
Queda la cuestión de la escala. No se han publicado ni el coste de cálculo ni el volumen exacto de recursos consumidos. El propio Swarat Chaudhuri reconoce, según 9to5Mac, que queda «a long distance to go» antes de aplicar el método al conjunto del software. DeepMind anuncia, en cambio, que publica en acceso abierto sus artefactos de verificación, acompañados de un artículo técnico. Según The Register, este trabajo también acerca un reto lanzado en abril por la Beneficial AI Foundation: verificar formalmente en Lean el protocolo y la aplicación Signal.
Por qué es importante
Proyectos de verificación célebres han movilizado años de trabajo: The Register cita el micronúcleo seL4, que requirió unos veinte años-persona. Si los agentes pueden reducir ese plazo a unas pocas semanas, la verificación formal podría salir de los laboratorios para cubrir componentes críticos como las bibliotecas de cifrado, los protocolos de mensajería o los sistemas embebidos. Para las empresas, la lección inmediata es más modesta: una demostración vale lo que vale su especificación, y la experiencia humana sigue siendo el eslabón decisivo.
Preguntas frecuentes
¿Es Signal ahora imposible de piratear?
No. El trabajo de DeepMind demuestra propiedades precisas del protocolo, bajo la hipótesis de una criptografía perfecta. La aplicación, el teléfono y los errores de uso siguen siendo posibles puntos de ataque.
¿Afecta a WhatsApp?
WhatsApp y Google Messages utilizan el protocolo Signal, por lo que las garantías demostradas sobre el protocolo les afectan. Su propia implementación, en cambio, no se ha verificado en este trabajo.
¿Qué es Lean?
Lean es un asistente de demostración: un programa que verifica mecánicamente cada paso de una demostración. Una demostración aceptada por su núcleo no depende de la confianza depositada en la IA que la redactó.
Fuentes
- Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques — The Register, 2026-11-10
- Google DeepMind analysis proves Signal and WhatsApp encryption is secure — 9to5Mac, 2026-11-10
- Introducing AlphaProof Code — Google DeepMind (blog oficial), 2026-11-10