Understanding the Usability of Cryptographic Verification Tools

arXiv:2609.16323 · cs.CR · Submitted 2026-09-14 · Read on arXiv

cs.CR

Submitted: 2026-09-14

Updated: 2026-09-14

Project page: https://tamarin-prover.github.io

License: http://creativecommons.org/licenses/by/4.0/

The gist: Cryptographic protocol verification tools are widely used to analyze the security of complex protocols, yet how users interact with these tools remains comparatively understudied.

Terminology

Verification — 141× in this paper · explained in 2 episodes
Verifier — 30× in this paper · explained in 2 episodes
Abstraction — 22× in this paper · explained in 1 episode
Trace — 18× in this paper · explained in 2 episodes
Formal Methods — 13× in this paper · explained in 3 episodes
Formal Verification — 9× in this paper · explained in 2 episodes
Fidelity — 7× in this paper · explained in 2 episodes
Perfect Forward Secrecy — 7× in this paper
Interpretability — 5× in this paper · explained in 15 episodes
IEEE Symposium on Security and Privacy — 4× in this paper
International Conference on Software Engineering — 3× in this paper
Accuracy — 2× in this paper · explained in 1 episode
Core — 2× in this paper · explained in 2 episodes
Alignment — 1× in this paper · explained in 1 episode
Analyzer — 1× in this paper · explained in 1 episode
Benchmark — 1× in this paper · explained in 2 episodes
Cognitive Scaffolding — 1× in this paper · explained in 3 episodes
Generalization — 1× in this paper · explained in 13 episodes
Robustness — 1× in this paper · explained in 5 episodes
SMT solver — 1× in this paper · explained in 2 episodes
Scaffolding — 1× in this paper · explained in 3 episodes
Selection Bias — 1× in this paper · explained in 4 episodes

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.

Understanding the Usability of Cryptographic Verification Tools

Terminology

Abstract

Sources

Related papers