You are looking at a specific version 20190909:171018 of this paper. See the latest version.

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

Note: Updated the names of two functions.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Preprint. MINOR revision.
Keywords
formal verification
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
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.