Skip to the end of the images gallery Nav bascule
Skip to the beginning of the images gallery Nav bascule
Verifpal User Manual
Livres pratiques & développement personnel
Couverture dure
100 pages
ISBN: 9782322161294
Éditeur : Books on Demand
Date de parution : 02.03.2020
Langue: anglais
Impression couleurs: oui
19,99 €
TVA incluse / Envoi en sus
Votre propre livre !
Devenez auteur avec BoD et vendez votre livre et votre ebook en librairie.
En savoir plusThe security of cryptographic protocols remains as relevant as ever, with systems such as TLS and Signal being responsible for much of the Web's security guarantees. One main venue for the analysis and verification of these protocols has been automated analysis with formal verification tools, such as ProVerif, CryptoVerif and Tamarin. Indeed, these tools have led to confirming security guarantees (as well as finding attacks) in secure channel protocols, including TLS and Signal. However, formal verification in general has not managed to significantly attract a wider audience.
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 Verifpal language is meant to illustrate protocols close to how one may describe them in an informal conversation, while still being precise and expressive enough for formal modeling. Verifpal reasons about the protocol model with explicit principals: Alice and Bob exist and have independent states.
Easy to Understand Analysis Output
When a contradiction is found for a query, the result is related in a readable format that ties the attack to a real-world scenario. This is done by using terminology to indicate how the attack could have been possible, such as through a man-in-the-middle on ephemeral keys.
Friendly and Integrated Software
Verifpal comes with a Visual Studio Code extension that offers syntax highlighting and, soon, live query verification within Visual Studio Code, allowing developers to obtain insights on their model as they are writing it.
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 Verifpal language is meant to illustrate protocols close to how one may describe them in an informal conversation, while still being precise and expressive enough for formal modeling. Verifpal reasons about the protocol model with explicit principals: Alice and Bob exist and have independent states.
Easy to Understand Analysis Output
When a contradiction is found for a query, the result is related in a readable format that ties the attack to a real-world scenario. This is done by using terminology to indicate how the attack could have been possible, such as through a man-in-the-middle on ephemeral keys.
Friendly and Integrated Software
Verifpal comes with a Visual Studio Code extension that offers syntax highlighting and, soon, live query verification within Visual Studio Code, allowing developers to obtain insights on their model as they are writing it.
Rédigez votre propre commentaire
Il n'y a pour le moment pas de critique presse.