DeepMind Uses AI Agents to Formally Verify Signal Encryption Protocol
Google DeepMind used autonomous AI agents to formally verify the Signal end-to-end encryption protocol, mathematically proving it meets its security claims while also flagging older implementations with known vulnerabilities. Described as a landmark for both cryptography and AI, the effort took roughly four weeks and heavy compute, limiting near-term scalability.
Related Entities
Full Report
IT之家 November 10 news — For a long time, the Signal encryption protocol has been regarded as the gold standard for end-to-end encrypted messaging. Now, Google DeepMind's team has used artificial intelligence to carry out formal verification of this protocol's security.
According to IT之家, in addition to the Signal app itself, this encryption protocol is also used by WhatsApp and Google Messages, and this research result has been described as "a landmark advance."
"Formal verification" refers to the use of mathematical methods to rigorously prove or disprove whether a given encryption algorithm or protocol satisfies its security promises. Unlike traditional testing, formal verification aims to prove that a protocol meets its security requirements under all conditions consistent with a given model, rather than merely searching for known vulnerabilities through testing. Even if traditional testing finds no problems, it cannot guarantee that no other as-yet-undiscovered vulnerabilities exist.
Using AI agents with autonomous execution capabilities to complete formal verification is significant for both cryptography and artificial intelligence. However, this process requires substantial computational resources. Google told Wired that it is not yet possible to determine the practical feasibility of applying this technology more broadly.
DeepMind researchers also emphasized that this result is only one milestone in the overall research process. DeepMind research scientist Swarat Chaudhuri said: "We are very excited about this result, but there is still a long way to go before we can scale this technology to all software in the world, and that is exactly what we hope to achieve."
It should be noted in particular that this verification targeted the Signal encryption protocol itself, not a comprehensive security review of the entire Signal application. However, one result is worth noting: the researchers also used this method to test older implementations of the Signal protocol that contained known security vulnerabilities, and the AI successfully identified the relevant issues and determined that these versions failed formal verification.
In addition, Google's research this time did not start entirely from scratch. The research team built on some previously completed formal verification results, some of which were not carried out with the help of artificial intelligence.
The entire analysis process took about four weeks, and Google has not disclosed the specific scale of computational resources required to complete this work. Therefore, the outside world cannot yet expect a large number of other encryption protocols to complete similar verification one after another in a short period of time.
Nevertheless, this is still a significant advance: AI can not only help developers write and check code, but may also verify through rigorous mathematical proof whether software security mechanisms are truly reliable.