Encryption in Zoom calls verified by NGI-supported Verifpal

The recent ability for video conferencing platform Zoom to offer end-to-end encryption to its paying customers was made possible with the help of a cutting edge research project from Europe. The new proprietary encryption protocol has been verified using the open source formal verification software Verifpal, which was developed in France with funding from the Next Generation Internet initiative. Until recently, such verification would have taken much longer to complete.

As the COVID-19 pandemic forces people to work and study from home, organizations, businesses and schools everywhere rely heavily on video conferencing and chat solutions to collaborate and connect. Users of the freemium videoconferencing platform Zoom raised issues of privacy and security, among others about whether the end-to-end encryption for audio and video calls actually worked as promised. In response to this, Zoom redesigned its software and protocols so that actual end-to-end encryption could be provided - although for business reasons it reserves this feature for paying users only.

Easily model and test end-to-end encryption

To verify whether the new end to-end encryption protocol in fact guarantees private and secure videoconferencing, Zoom tested their designs using the open source cryptographic protocol verification software Verifpal. Developed with funding from NLnet and the Next Generation Internet initiative, Verifpal introduces an intuitive language for modeling cryptographic protocols that is easier to write and understand than languages employed by existing tools. Users and developers can easily write out or model their encryption protocols and verify whether they are secure, testing their security against all sorts of attacks.

Verifpal aids in eliminating potential Zoom protocol issues at early stage

Nadim Kobeissi, the lead developer for Verifpal, helped Zoom's team test more than 8 Verifpal models which during the development of Zoom's protocols helped identify a non-obvious attack on some of the proposals considered for Zoom's encryption. "It's wonderful to see how Verifpal can make protocol modeling and analysis immediately available to developers right in the protocol design stage," said Dr. Kobeissi. "This helps engineers such as the ones at Zoom to identify weaknesses in protocol design proposals very early on." Other projects and tools that recently started using Verifpal to make their software more secure include the private messaging app Delta Chat and the end-to-end encrypted signalling protocol SaltyRTC.

Integrate protocol modeling and verification in Visual Studio Code

Last year Verifpal was one of the first technology projects funded by the Next Generation Internet initiative, a programme initiated by the European Commission to re-imagine and re-engineer a more trustworthy internet. With a recent grant from NGI Zero to expand its feature set, Verifpal is now able to further prove that its verification of protocols is sound using the Coq theorem prover, automatically generate implementations from verified Verifpal-models for real-world testing and integrate into development environments like Visual Studio Code. "We are eager to see this kind of protocol verification become the new norm, not just in video conferencing solutions but across the board", states Michiel Leenaars, director of Strategy at NLnet Foundation. "The right to confidentiality is of critical importance to our society, and in the online world this is no different. In a situation like the current pandemic, this needs to happen as soon as possible. The low threshold to work with Verifpal is critical to achieve that goal." NLnet coordinates the NGI Zero PET call for privacy and trust enhancing technology that supports Verifpal, as well as the NGI Zero Discovery call for open search and discovery.

Help us make a trustworthy internet

NGI Zero is proud to support open source software and open hardware projects that address online security and privacy on all layers, from improving fundamental components to developing human-centric middleware and trustworthy end user apps. Do you want to help make the Internet more open, trustworthy and reliable? Submit your proposal to the NLnet foundation before the next following deadline and see if we can help you.