Understanding the Usability of Cryptographic Verification Tools
Survey of Tamarin and ProVerif users reveals usability barriers: debugging non-termination, model validation, and opaque proof failures hinder cryptographic protocol verification.
The paper presents an exploratory human-centered survey of researchers, graduate students, and practitioners with hands-on experience using Tamarin, ProVerif, and related cryptographic protocol verification tools. Findings reveal usability barriers across the verification workflow, including difficulties debugging non-termination and performance issues plus the lack of systematic methods for validating formal models against real protocols. When proofs fail without concrete attacks, users commonly simplify models, add helper lemmas, and revisit modeling abstractions. Participants called for actionable diagnostics, clearer explanations of results, visualization, and automation for recurring proof tasks.