Users face challenges with cryptographic protocol verification tools
Understanding the Usability of Cryptographic Verification Tools
Cryptography and Security
Summary
Many tools exist to check if cryptographic protocols are secure, but how people actually use these tools has not been studied much. The authors surveyed experienced users of verification tools like Tamarin and ProVerif and found that users struggle with problems such as unclear error messages, performance issues, and difficulty linking the tool’s models to real-world protocols. When proofs fail, users simplify models and add extra steps to try to fix problems. The authors suggest ways these tools could be improved to make them easier and clearer to use.
What this means in practice
- •For security engineers: Enhance existing protocol verification workflows by adopting improved diagnostics and visualization features to reduce time spent debugging failed proofs.
- •For software verification teams: Develop extensions for cryptographic verification tools that automate recurring proof tasks and provide clearer feedback to assist users during model validation.
A survey. It maps existing work.
Authors
Tarikul Islam, Yasin Islam, Khandakar Ashrafi Akbar, Imtiaz Karim
Abstract
Cryptographic protocol verification tools are widely used to analyze the security of complex protocols, yet how users interact with these tools remains comparatively understudied. We present an exploratory human-centered study of experienced users of Tamarin, ProVerif, and related protocol verifiers. Our survey included researchers, graduate students, and practitioners with hands-on experience using Tamarin, ProVerif, or related tools. The findings reveal usability barriers across the verification workflow, including difficulties debugging non-termination and performance issues, and 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 also called for actionable diagnostics, clearer explanations of results, visualization, and automation for recurring proof tasks. Our findings suggest that persistent usability challenges arise from the gap between protocol-level reasoning and the verifier's formal model, proof procedures, and diagnostic output. We derive concrete design priorities for improving the accessibility, interpretability, and usability of cryptographic protocol verification tools.