Google DeepMind’s use of AlphaProof Code to mathematically prove parts of the Signal protocol is considered a milestone in the fields of cryptography and AI. It validates the cryptography that is used to protect the troves of messages and other communications exchanged across the world through major platforms such as Signal, WhatsApp, Facebook Messenger, and Google Messages – all of which have integrated the Signal encryption protocol.
It also underscores how AI tools could speed up independent security assessments, helping researchers analyse and formally verify the integrity of cryptographic protocols more efficiently. This comes at a time when AI-driven cyber attacks are on the rise, with entire code bases and software supply chains facing threats.
“We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that,” Swarat Chaudhuri, a DeepMind research scientist, was quoted as saying by Wired.
“While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach enables significant expansion. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees,” Ehren Kret, Signal’s chief technology officer, said in a statement.
Story continues below this ad
What is the Signal encryption protocol?
Secure communications today usually rely on a pair of cryptographic keys: a private key and public key used in combination with it to create a message that disallows interception.
Signal is a pioneer of encrypted communications. It is widely considered to be a leading easy-to-use, encrypted messaging service among cybersecurity experts, since there are no public reports of hackers intercepting users’ messages in-transit by cracking the platform’s end-to-end encryption protocol.
The app is also a favourite of privacy and digital rights activists as it collects minimal user data and offers robust privacy features such as the option to hide your phone number and display a username instead.
Unlike Telegram, end-to-end encryption is enabled by default for all messages and voice calls on Signal. The underlying protocol is open-source, meaning that anyone can take a look under the hood and verify its security. In addition, the encryption protocol forms the basis of the security offered by other messaging apps like WhatsApp.
Story continues below this ad
Since 2023, Signal has been upgrading its encryption technology so that it remains secure against the future, hypothetical threat of quantum computers.
When DeepMind researchers used AlphaProof Code to analyse older versions of Signal, it identified security flaws and showed that the encryption protocol could not be formally verified. However, these security flaws were already known and have long been patched.
DeepMind researchers further said that they are releasing the specification and proof they developed for the Signal protocol analysis to aid other formal verification work. The lab’s analysis of the Signal protocol was done as a research project without incurring any costs for Signal.
It is unclear whether Google DeepMind has plans to release a commercial formal verification product or service in the future.
Story continues below this ad
Benefits and limitations of AI-led verification
Manual verification is reportedly time-consuming for researchers as it involves describing the characteristics of software they want to prove, turning these summaries into formulas, and then developing the proof. AI agent tools like AlphaProof Code could help significantly cut down the timeline of such projects.
“If you can now verify the correctness of these implementations, then you can rest easy. You can imagine banks, imagine all those other companies who rely on assurances and who worry about bugs who could now say, ‘I can prove these properties,’” Pushmeet Kohli, chief scientist at Google Cloud and DeepMind’s vice president of research, was quoted as saying.
While there are many advantages to AI-aided formal verification, it comes with certain limitations too. For instance, Google DeepMind said its analysis of the Signal protocol was limited in scope and does not cover the entire Signal mobile app.
The researchers also pointed out that their findings were also based on some past formal verification work carried out by the Signal Foundation, the non-profit organisation behind the app. There are also questions about whether it is possible to automate formal verification at scale using AI, and if it can be done at a reasonable cost.
Story continues below this ad
In the future, it is more likely that formal verification will be a human-AI collaboration process where AI agents can contribute and self-correct, while still seeking human input and review at key points of the process. “We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written. There’s a middle ground,” Chaudhuri said.
