‘Secure internet encryption is paramount to national security’
Encryption is essential to a safe and private internet and ensures no one can intercept the messages you send through Whatsapp, how you login to your bank or what sites you visit. But how can we actually know that the technology designed to protect billions of internet users everyday is actually trustworthy? Verifpal is one of the first technology projects funded by the NGI and will make formal verification of important cryptographic protocols more accessible. Cryptography researcher and open-source developer Nadim Kobeissi explains why it is crucial to thoroughly test the protocols that safeguard us online.
To actually create an open, trustworthy and sustainable Next Generation Internet, we need concrete technological building blocks that advance the state of art and address fundamental insecurities and privacy sinkholes that continue to plague the internet. Cryptography has become crucial to keeping online communication and data sharing private and secure, but that does not mean that every cryptographic protocol used to keep our internet traffic safe is actually secure. Formal verification of these protocols is a surefire way to control for possible attacks, but can be complicated and costly.
Thoroughly testing the protocols that protect our banking information, password logins and instant messaging apps is nothing more than vital to a trustworthy internet. That is why cryptography professor, internet activist and developer Nadim Kobeissi has developed the open-source tools Noise Explorer and ProVerif that make it easier to analyze, verify and generate secure encrypted channels. VerifPal is his latest effort to democratize encryption verification with a new and accessible modeling language that developers can use to describe how their cryptographic protocol works and test whether it holds up against attacks.
VerifPal is one of the first ever projects to receive funding and support from the NGI initiative and was selected by the NGI Zero open call for privacy and trust enhancing technologies.
VerifPal is a new modeling language that can verify and analyze the secure implementation of cryptographic protocols like Noise (used in Whatsapp) and Transport Layer Security (TLS, used for example to protect web traffic through HTTPS). Why did you design VerifPal, what was missing from the current technology?
Recent years have seen an explosion in the number of cryptographic protocols that are being specified and implemented. We’ve got Signal for secure messaging, WireGuard for VPNs, TLS 1.3 for web traffic, and so on. When it comes to formally verifying the security of all these protocols, none of the existing verification tools were accessible or usable with an elegant, intuitive language. Verifpal aims to be formal verification software that has its own language, the Verifpal language, where protocols can be described as interactions between principals (Alice, Bob, etc.) over the internet. Verifpal has its own formal verification logic against passive and active attackers, and allows for advanced features and queries (such as testing for authentication, etc.) This makes it very different from existing tools, such as ProVerif and Tamarin, which focus more on full-featuredness but less on being accessible to people who are not specialized in formal verification. We want Verifpal to be usable for formally verifying any secure channel protocol easily, not just Noise protocols as is the limitation of Noise Explorer.
Furthermore, Verifpal will be integrated into Visual Studio Code and allow for generating prototype implementations based on formal verification models and results, as well as many other features that I don’t want to spoil now.
Both Verifpal and your earlier work on ProVerif and the Noise Protocol Framework focuses on how secure and private the cryptographic protocols are that services like Whatsapp use for encryption. How important are these protocols for secure internet communication and the trustworthiness of apps and tools we use everyday?
I would argue that the security of protocols like TLS and Signal is paramount to global national security. If these protocols were to be broken, billions of people would immediately be at risk for the compromise of their personal information, bank information and more. These are the stakes today. Unfortunately, previous versions of TLS, Signal and other protocols had some significant issues (minor ones in the case of Signal) that weren’t caught until formal verification was more deployed. Verifpal is important because it will encourage protocol designers to include formal verification as part of their workflow.
Formal verification mathematically proves that new protocols only do what they are supposed to do and ensures that new technology derived from a formal proof can leave no loose ends. Unfortunately this is often complex and costly. How does VerifPal make formal verification more accessible?
Verifpal introduces a new language, the Verifpal language, for easily and expressively writing formal verification models. This language is a huge advance from the applied pi-calculus used in ProVerif and the state transition-based language of Tamarin when it comes to intuitiveness and accessibility. It’s less full-featured than those other languages, but that is a feature, not a bug: we intentionally guide the language to prevent user error and maximize expressiveness and intuitiveness.
Verifpal will focus on ease of use and integration. By being easy to integrate into your workflow, you can get relevant formal verification results on a protocol that you are prototyping quickly. We also want Verifpal to be easy to extend by the open source community. Verifpal’s formal verification results will also be easy to read and understand, in a similar vein to Noise Explorer’s compendium of verification results.
Verifpal will focus on being fast! We want to give users formal verification results quickly, and avoid state space explosions which can make ProVerif take hours for complex protocols.
Who do you think should start using VerifPal right now?
Well, you can’t use it right now because it’s not ready yet. But later this year, I hope that Verifpal will offer everyone easy to use, fun and effective formal verification workflows. The goal is for it to be so accessible that the protocol designer would have to find reasons *not* to include it in their process.