Verifpal
Prove soundness of verification in Verifpal
Verifpal is new software for verifying the security of cryptographic protocols. Building upon contemporary research in symbolic formal verification, Verifpal’s main aim is to appeal more to real-world practitioners, students and engineers without sacrificing comprehensive formal verification features.
In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is much easier to write and understand than the languages employed by existing tools. At the same time, Verifpal is able to model protocols under an active attacker with unbounded sessions and fresh values, and supports queries for advanced security properties such as forward secrecy or key compromise impersonation.
Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3, Telegram and other protocols. It is a community-focused project, and available under a GPLv3 license.
- The project's own website: https://verifpal.com
Why does this actually matter to end users?
Secure communication over the internet is critical. Humans however are not infallible, and the same holds for the humans that design the protocols that should make our internet traffic safe. Internet engineers and software developers need to handle a lot of complexity, and even a small oversight or a very improbable scenario or combination of factors can mean breaking part or whole of the protection required The secure technologies we depend on to keep internet communications secure are frequently found to suffer from fundamental design vulnerabilities as well as implementation errors. Truth is, while trust is a fundamental human trait, we should not just trust human intuition to get everything right.
This is where computers can come to help us out, to see if we can underpin that trust in a systematic way. Computers have no problem to exhaustively try out all options, even if it takes them millions and millions of tries. When instructed in the right way, that means their endless combinatorial capabilities can be used to simulate even the most unlikely of events. Again and again, if necessary. A lot of awesome computer science brain power has gone into so called formal proofs. Formal proofs use very strict mathematical modelling to take everything that could possibly happen into account, and prove that the software or protocol at hand does what it is assumed to do. However, as you may imagine, this modelling can get pretty complex and as such is an art in itself - restricting the usage to a very limited set of experts. However, once you have the models right you can actually go a lot further than just prove the protocol: from the model you can automatically generate secure software libraries that you can be sure implement the protocols involved exactly right. This is a guarantee that no human programmer can give.
VerifPal is new software that makes formal verification of cryptographic protocols more accessible and intuitive. It is a breakthrough that regular users and software engineers can easily write out (or model) protocols to verify whether they are secure, and then immediately them against all sorts of possible attacks.
VerifPal is one of the first technology projects funded by the NGI and has already been used to verify the security of widely used protocols that for example protect Whatsapp and Signal-messages. Through this new project VerifPal will further prove that its verification of these protocols is sound, create extra implementations of the modeling language for a larger user base and integrate other protocol verification software to add additional layers of security checks. This way software developers, engineers and students around the world can benefit from formal verification software that is both secure and accessible, which can ultimately help make the internet a safer and more trustworthy place.
Run by Symbolic Software
This project was funded through the NGI0 PET Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 825310.
