Paper 2019/971
Verifpal: Cryptographic Protocol Analysis for the Real World
Nadim Kobeissi, Georgio Nicolas, and Mukesh Tiwari
Abstract
Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for 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 easier to write and understand than the languages employed by existing tools. Its formal verification paradigm is also designed explicitly to provide protocol modeling that avoids user error. 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. Furthermore, Verifpal's semantics have been formalized within the Coq theorem prover, and Verifpal models can be automatically translated into Coq as well as into ProVerif models for further verification. Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3 as well as the first formal model for the DP-3T pandemic-tracing protocol, which we present in this work. Through Verifpal, we show that advanced verification with formalized semantics and sound logic can exist without any expense towards the convenience of real-world practitioners.
Note: Fix formatting of Figure 5.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Major revision. 21st International Conference on Cryptology in India (INDOCRYPT 2020)
- Keywords
- formal verificationcryptographic protocols
- Contact author(s)
- nadim @ symbolic software
- History
- 2020-10-26: last of 20 revisions
- 2019-08-29: received
- See all versions
- Short URL
- https://ia.cr/2019/971
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2019/971,
author = {Nadim Kobeissi and Georgio Nicolas and Mukesh Tiwari},
title = {Verifpal: Cryptographic Protocol Analysis for the Real World},
howpublished = {Cryptology ePrint Archive, Paper 2019/971},
year = {2019},
note = {\url{https://eprint.iacr.org/2019/971}},
url = {https://eprint.iacr.org/2019/971}
}
