Cryptology ePrint Archive: Report 2019/971

Verifpal: Cryptographic Protocol Analysis for Students and Engineers

Nadim Kobeissi

Abstract: Contemporary research in symbolic formal verification has led to confirming security guarantees (as well as finding attacks) in secure channel protocols such as TLS and Signal. However, formal verification in general has not managed to significantly exit the academic bubble. Verifpal is new software for verifying the security of cryptographic protocols that aims is 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. By modeling principals explicitly and with discrete states, Verifpal models are able to be written in a way that reflects how protocols are described in the real world. At the same time, 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. Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3 and other protocols. It is a community-focused project, and available under a GPLv3 license.

Category / Keywords: cryptographic protocols / formal verification

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

Contact author: nadim at symbolic software

Available format(s): PDF | BibTeX Citation

Note: Updated the names of two functions.

Version: 20190909:171018 (All versions of this report)

Short URL: ia.cr/2019/971