ai and ml

Post-quantum handshake and Triple Ratchet get a formal security check

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…