Cryptology ePrint Archive: Report 2019/971

Verifpal: Cryptographic Protocol Analysis for the Real World

Nadim Kobeissi and 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.

Category / Keywords: cryptographic protocols / formal verification, cryptographic protocols

Date: received 27 Aug 2019, last revised 9 Sep 2020

Contact author: nadim at symbolic software

Available format(s): PDF | BibTeX Citation

Note: Minor clarifications regarding the scope of the Coq work.

Version: 20200909:162149 (All versions of this report)

Short URL: ia.cr/2019/971