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 Original Publication (with major differences): 21st International Conference on Cryptology in India (INDOCRYPT 2020) Date: received 27 Aug 2019, last revised 26 Oct 2020 Contact author: nadim at symbolic software Available format(s): PDF | BibTeX Citation Note: Fix formatting of Figure 5. Version: 20201026:150128 (All versions of this report) Short URL: ia.cr/2019/971