· ai-devtools
Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques
Google DeepMind researchers have completed a formal verification of Signal's messaging security, marking what they claim is the first time AI has helped devise a proof that links protocol-level security guarantees to a widely used cryptographic implementation.
They did so using AlphaProof Code, a multi-agent framework for formal software specification and verification. AlphaProof Code relies on a human-guided agent that writes a Lean specification, assesses machine code semantics, and crafts an agent-authored proof that the Lean kernel checks against the specification. In this instance, AlphaProof Code verified Signal’s post-quantum PQXDH handshake and Triple Ratchet, thereby validating the design of libsignal's forward secrecy, authentication, post-compromise security, and handshake secrecy.
In so doing, the Google/DeepMind team – Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli – has taken a step toward a challenge the Beneficial AI Foundation issued in April to formally verify the Signal protocol and Signal app with Lean. The AlphaProof Code process involves working with various models to turn Signal's security goals into a human-reviewed mathematical specification.
