Google DeepMind realizó un análisis de verificación formal del protocolo criptográfico de Signal, utilizado también por WhatsApp y Google Messages, y confirmó que cumple sus propiedades de seguridad bajo las condiciones evaluadas. El trabajo, publicado el 10 de noviembre de 2026, importa porque aplica inteligencia artificial a una comprobación matemática más rigurosa que las pruebas de vulnerabilidades habituales, aunque no certifica por completo las aplicaciones.
Qué verificó Google DeepMind del protocolo Signal
La verificación formal busca demostrar matemáticamente que un sistema satisface determinadas propiedades de seguridad, en lugar de limitarse a buscar fallos mediante pruebas. En este caso, el análisis se centró en el protocolo de cifrado de extremo a extremo asociado a Signal, considerado una referencia en mensajería segura y utilizado también por WhatsApp y Google Messages.
El resultado respalda las garantías de seguridad del protocolo dentro del modelo y las condiciones analizadas. Esto representa un avance frente a los métodos tradicionales de evaluación, que pueden encontrar errores concretos, pero no demostrar por sí solos que no existan otros. Aun así, una prueba formal depende de las propiedades definidas, las hipótesis del modelo y el alcance del código examinado: no equivale a una garantía universal sobre cualquier situación real.
La verificación con IA identificó fallos en versiones antiguas
Como parte del trabajo, los investigadores probaron versiones antiguas de Signal que contenían vulnerabilidades conocidas. El sistema identificó esos problemas y determinó que las versiones afectadas no superaban la verificación formal. Esa comprobación sirve como indicio de que el método puede distinguir entre implementaciones que cumplen las propiedades examinadas y otras que presentan fallos conocidos.
El análisis combinó herramientas de inteligencia artificial con trabajos previos de verificación formal realizados sin IA. Por eso, el resultado no debe interpretarse como una revisión automática e independiente de todo el software de Signal, WhatsApp o Google Messages. La validación se refiere al protocolo, no a cada componente de las aplicaciones, sus dispositivos, sus sistemas operativos ni la forma en que cada servicio gestiona las cuentas y los respaldos.
El análisis tomó cuatro semanas y su escalado sigue pendiente
Según la información publicada por 9to5Mac y las declaraciones de un investigador de DeepMind a WIRED, el análisis tomó cuatro semanas. Google no detalló los recursos computacionales empleados, y el equipo advirtió que todavía queda un largo camino para aplicar el método a una parte amplia del software existente.
El coste y la complejidad son importantes: verificar formalmente un protocolo requiere definir con precisión qué debe garantizar, representar sus posibles interacciones y comprobar el resultado. El uso de agentes de IA puede ayudar a automatizar partes de ese proceso, pero la investigación no demuestra que cualquier sistema criptográfico pueda revisarse rápidamente ni sin supervisión especializada.
Qué significa el resultado para quienes usan mensajería cifrada
Para los usuarios, el hallazgo aporta evidencia adicional sobre las bases criptográficas de servicios de mensajería populares, pero no elimina la necesidad de mantener las aplicaciones actualizadas y proteger los dispositivos. El cifrado de extremo a extremo protege el contenido durante la comunicación según el funcionamiento del protocolo; no impide, por sí solo, que alguien acceda a mensajes desde un dispositivo desbloqueado o comprometido.
La principal relevancia está en el método: combinar inteligencia artificial y verificación matemática podría ayudar a detectar errores en sistemas críticos antes de que se exploten. Por ahora, DeepMind presenta el resultado como un hito inicial, no como una certificación definitiva de todas las versiones y funciones de Signal o WhatsApp.
En resumen
- Google DeepMind verificó formalmente propiedades de seguridad del protocolo de Signal.
- WhatsApp y Google Messages también utilizan ese protocolo.
- El análisis tomó cuatro semanas y se apoyó en trabajos previos de verificación formal.
- La prueba se refiere al protocolo, no a las aplicaciones completas.
- El equipo considera que escalar el método a más software todavía supone un reto.
