### 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.

Available format(s)
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)
History
2020-10-26: last of 20 revisions
See all versions
Short URL
https://ia.cr/2019/971

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}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.