Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif
Seiten
2016
now publishers Inc (Verlag)
978-1-68083-206-8 (ISBN)
now publishers Inc (Verlag)
978-1-68083-206-8 (ISBN)
- Titel ist leider vergriffen;
keine Neuauflage - Artikel merken
Focuses on the verification of specifications of protocols in the symbolic model. ProVerif is an automatic symbolic protocol verifier. This survey presents an overview of the research on ProVerif and is the most comprehensive text available on the topic.
The verification of security protocols has been an active research area since the 1990s. This topic is interesting for several reasons. Security protocols are ubiquitous: they are used for e-commerce, wireless networks, credit cards, e-voting, among others. The design of security protocols is notoriously error-prone. These errors can also have serious consequences. Hence, the formal verification or proof of protocols is particularly desirable.
This survey focuses on the verification of specifications of protocols in the symbolic model. Even though it is fairly abstract, this level of verification is relevant in practice as it enables the discovery of many attacks. ProVerif is an automatic symbolic protocol verifier. It supports a wide range of cryptographic primitives, defined by rewrite rules or by equations. It can prove various security properties: secrecy, authentication, and process equivalences, for an unbounded message space and an unbounded number of sessions. It takes as input a description of the protocol to verify in a dialect of the applied pi calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol description into Horn clauses and determines whether the desired security properties hold by resolution on these clauses.
This survey presents an overview of the research on ProVerif and is the most comprehensive text available on the topic.
The verification of security protocols has been an active research area since the 1990s. This topic is interesting for several reasons. Security protocols are ubiquitous: they are used for e-commerce, wireless networks, credit cards, e-voting, among others. The design of security protocols is notoriously error-prone. These errors can also have serious consequences. Hence, the formal verification or proof of protocols is particularly desirable.
This survey focuses on the verification of specifications of protocols in the symbolic model. Even though it is fairly abstract, this level of verification is relevant in practice as it enables the discovery of many attacks. ProVerif is an automatic symbolic protocol verifier. It supports a wide range of cryptographic primitives, defined by rewrite rules or by equations. It can prove various security properties: secrecy, authentication, and process equivalences, for an unbounded message space and an unbounded number of sessions. It takes as input a description of the protocol to verify in a dialect of the applied pi calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol description into Horn clauses and determines whether the desired security properties hold by resolution on these clauses.
This survey presents an overview of the research on ProVerif and is the most comprehensive text available on the topic.
1: Introduction
2: The Protocol Specification Language
3: Verifying Security Properties
4: Link with the Applied Pi Calculus
5: Applications
6: Conclusion
Appendices
References
| Erscheinungsdatum | 16.11.2016 |
|---|---|
| Reihe/Serie | Foundations and Trends® in Privacy and Security |
| Verlagsort | Hanover |
| Sprache | englisch |
| Maße | 156 x 234 mm |
| Gewicht | 224 g |
| Themenwelt | Informatik ► Netzwerke ► Sicherheit / Firewall |
| Mathematik / Informatik ► Informatik ► Theorie / Studium | |
| ISBN-10 | 1-68083-206-9 / 1680832069 |
| ISBN-13 | 978-1-68083-206-8 / 9781680832068 |
| Zustand | Neuware |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
Mehr entdecken
aus dem Bereich
aus dem Bereich
Das Lehrbuch für Konzepte, Prinzipien, Mechanismen, Architekturen und …
Buch | Softcover (2022)
Springer Vieweg (Verlag)
CHF 53,15
Lehrbuch für Prüfung und Praxis
Buch | Softcover (2023)
Springer Fachmedien Wiesbaden GmbH (Verlag)
CHF 27,95
Management der Informationssicherheit und Vorbereitung auf die …
Buch (2024)
Carl Hanser (Verlag)
CHF 97,95
