Article · AI translation
IT Home reported on November 10 that the Signal encryption protocol has long been regarded as the gold standard for end-to-end encrypted messaging. Now, Google’s DeepMind team has used artificial intelligence to formally verify the protocol’s security.
According to IT Home, the encryption protocol is used by WhatsApp and Google Messages as well as the Signal app itself. The research has been described as “a milestone achievement.”
“Formal verification” refers to using mathematical methods to rigorously prove or disprove whether an encryption algorithm or protocol meets its security promises. Unlike conventional testing, formal verification aims to prove that a protocol meets security requirements under all conditions covered by a specified model, rather than merely using tests to find known vulnerabilities. Even if conventional testing finds no problems, it cannot guarantee that other, as yet undiscovered vulnerabilities do not exist.
Using AI agents capable of acting autonomously to carry out formal verification is significant for both cryptography and artificial intelligence. However, the process requires substantial computing resources. Google told Wired that it cannot yet determine whether deploying the technology more widely is practical.
DeepMind researchers also stressed that this result is only one milestone in a broader research effort. DeepMind research scientist Swarat Chaudhuri said, “We’re very excited about this result, but there’s still a long way to go before we can scale this technology to all the software in the world, and that’s what we hope to achieve.”
It is important to clarify that the verification concerned the Signal encryption protocol itself; it was not a comprehensive security review of the entire Signal app. One result is worth noting, however: the researchers also used the method to test older implementations of the Signal protocol that contained known security vulnerabilities. The AI successfully identified the relevant problems and determined that those versions failed formal verification.
Google’s research also did not start entirely from scratch. The team drew on earlier formal verification work, some of which had been done without artificial intelligence.
The entire analysis took about 4 weeks, and Google has not disclosed the specific amount of computing resources required. For now, therefore, observers cannot expect many other encryption protocols to undergo similar verification in quick succession.
Even so, this remains a significant advance: AI can help developers write and review code, and it may also be able to verify, through rigorous mathematical proofs, whether software security mechanisms are truly reliable.