PaperlayerView exact revision on arXiv

Source-linked AI summary

Understanding the Usability of Cryptographic Verification Tools

Tarikul Islam, Yasin Islam, Khandakar Ashrafi Akbar, Imtiaz Karim

arXiv:2609.16323v1cs.CR

TL;DR

Practical use of cryptographic protocol verifiers remains comparatively understudied despite their use in security analysis. This paper surveys experienced users and finds workflow-wide usability barriers, alongside requests for model validation, clearer diagnostics, debugging, and automation.

  • Problem

    How users interact with cryptographic protocol verifiers is comparatively understudied, despite the importance of being able to apply these tools correctly.

    Source: §1 · p. 1

  • Method

    The authors conducted an exploratory survey of 16 experienced users of Tamarin, ProVerif, and related protocol-verification tools.

    Source: §1 · p. 2, §10 · p. 13

  • Results

    Users report difficulties validating model fidelity, diagnosing slow or non-terminating verification, interpreting failed proofs and feedback, and handling tool-specific modeling challenges.

    Source: §1 · p. 2, §6 · p. 12, §10 · p. 13

  • Takeaways & Limitations

    Participants call for model-validation support, actionable diagnostics, clearer explanations, interactive debugging, visualization, and automation of recurring proof tasks.

    Source: §1 · p. 2, §10 · p. 13

    Larger Tamarin case studies can add state-space, rule, adversary, and property complexity, increasing computational and manual proof-guidance demands.

    Source: §5.4.2 · p. 8

Abstract

from arXiv · show

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.

1 Introduction

Although protocol verifiers are technically powerful and used in practice, systematic evidence about how people use them remains limited. This study surveys experienced users and identifies workflow-wide barriers and priorities for improvement.

1 Introduction

  • Verification tools have been applied to protocols including iMessage PQ3, TLS 1.3, and Signal as protocol complexity and practical demand grow.The introduction notes features such as post-compromise security, ratcheting, and stateful hardware components.Source: §1 · p. 1
  • Prior comparisons of protocol verifiers emphasize formal expressiveness and attack detection, leaving users’ experiences of learning, modeling, and interpreting outputs comparatively understudied.The study addresses a recognized call for human-centered formal-verification research.Source: §1 · pp. 1–2
  • The study surveys 16 experienced users of Tamarin, ProVerif, and related verifiers about learnability, end-to-end workflows, and tool-specific usability issues.Participants were recruited through academic publications, open-source contributions, community outreach, and referrals.Source: §1 · p. 2
  • Participants report persistent difficulties validating model fidelity, debugging non-termination or failed proofs without concrete attacks, and interpreting sparse feedback across the verification workflow.Programming experience helps with problem-solving but does not replace domain-specific reasoning; Tamarin users also rely on helper lemmas, while ProVerif users report friction with stateful protocols and advanced properties.Source: §1 · p. 2
  • Users call for model-validation mechanisms, actionable localized diagnostics, interactive debugging and visualization, and automation for recurring tasks such as helper-lemma generation.The improvement requests converge across both tools.Source: §1 · p. 2

2 Background

Protocol verifiers reason over symbolic models with explicitly defined adversarial capabilities, enabling analysis of unbounded executions. Tamarin and ProVerif use different formalisms and expose different proof workflows.

2 Background

  • Symbolic analysis represents cryptographic operations as idealized symbolic functions and reasons about adversary knowledge, separating protocol reasoning from bit-level primitive properties.This abstraction supports automated reasoning about potentially unbounded protocol executions.Source: §2 · p. 2
  • Tamarin models behavior with multiset rewriting rules and first-order security properties, supporting equational theories, mutable state, and temporal event relations.It offers automated and interactive verification; users can inspect proof states and dependency graphs and guide search with helper lemmas.Source: §2 · pp. 2–3
  • ProVerif translates applied-pi-calculus models into an abstraction for unbounded sessions and message spaces, emphasizing automated analysis of properties including secrecy and authentication.Its abstractions can scale, but state, complex algebraic or equivalence properties, and state-evolving guarantees may require modeling choices or workarounds.Source: §2 · p. 3
  • Both tools require translating informal protocols into symbolic representations, but their formalisms and proof workflows differ, motivating study of shared and tool-specific usability challenges.Tamarin offers interactive proof guidance, whereas ProVerif emphasizes automated abstraction-based analysis.Source: §2 · p. 3

3 Related Work

Prior research identifies usability concerns across cryptographic software, security-analysis tools, and formal verification, while empirical evidence about experienced users of protocol verifiers remains limited.

3 Related Work

  • Studies of cryptographic APIs and security-analysis tools identify usability barriers involving abstractions, documentation, defaults, feedback, warning interpretation, prioritization, and workflow integration [38].Related work also reports usability concerns in fuzzing and constant-time analysis.Source: §3 · p. 3
  • Earlier protocol-verification work proposed higher-level interfaces and representations, but complexity, training, integration, and interpretation remained concerns [21].These studies recognize usability barriers but do not supply systematic evidence about experienced users’ end-to-end interactions with Tamarin and ProVerif.Source: §3 · pp. 3–4
  • Formal-verification research reports challenges with learnability, training, scalability, workflow integration, result interpretation, and debugging failed proofs [28].Researchers have called for more attention to users’ mental models and empirical evaluation [12] [49].Source: §3 · p. 3
  • The study addresses limited evidence about how users learn verifiers, transfer prior knowledge, assess model fidelity, and recover from unsuccessful or non-terminating verification attempts.Prior work emphasizes analytical capability and proposed interfaces, while systematic empirical evidence remains limited.Source: §3 · pp. 3–4

4 Methodology

The study uses an online questionnaire to examine practical usability among experienced cryptographic-verification-tool users. Closed-ended responses are summarized descriptively, while open-ended justifications are coded to identify recurring concerns and themes.

4.1 Study Design

  • The questionnaire targets users with direct hands-on experience because cryptographic verification tools require substantial technical knowledge.The online study sought participants’ experiences in academic or professional contexts.Source: §4.1 · p. 4, §4 · p. 4

4 Methodology

  • The survey examines practical usability across learning, protocol modeling, tool semantics, result interpretation, debugging, and integration into broader workflows.It combines closed-ended questions about backgrounds and challenges with open-ended accounts of difficulties, workarounds, and suggested improvements.Source: §4.1 · p. 4, §4 · p. 4

4.2 Recruitment and Eligibility Criteria

  • Purposive recruitment used publications, public technical contributions, research communities, and referrals; 16 of 24 survey starters completed the survey and were analyzed.Recruitment ran from May to July 2026, and eligibility was based on self-reported prior experience.Source: §4.2 · p. 4

4.3 Study Structure

  • The five survey sections covered consent, participant background, learnability, modeling and verification, and tool-specific usability questions shown according to participants’ reported experience.Tamarin questions addressed counterexamples, scalability, helper lemmas, and visualization; ProVerif questions addressed equivalence, algebraic properties, state dependence, and security properties.Source: §4.3 · pp. 4–5, Table 1 · p. 5

4.4 Data Analysis

  • Closed-ended responses were summarized with counts and percentages, while open-ended justifications were inductively coded and mapped to a shared five-level adequacy scale.A lightweight axial-coding pass identified cross-property themes; one researcher coded the open-ended responses without inter-rater reliability or independent second-coder verification.Source: §4.4 · p. 5

5 Results

The results describe participants’ experiences using protocol-verification tools, including challenges with learning, model validation, proof debugging, and tool feedback. They also cover uncertainty about ProVerif property adequacy and participants’ priorities for validation, transparency, and debuggability.

5.2 Learnability of Cryptographic Verifiers

  • Findings primarily reflect established users; 9 participants (56.3%) selected debugging non-termination and performance issues as the steepest learning-curve challenge, and all 16 (100%) used official documentation or tool manuals.Half (8, 50.0%) reported no prior experience with general-purpose model checkers.Source: §5.1 · p. 6, §5.2 · pp. 6–7

5.3 Modeling and Verification

  • Model confidence averaged approximately 3.6/5, while 8 (50%) cited absent validation methods and 8 (50%) complex stateful behavior; without attack traces, 11 (68.8%) used each of three model-focused debugging strategies.The strategies were simplifying the model, adding helper or auxiliary lemmas, and revisiting modeling decisions and abstractions.Source: §5.3 · p. 7

“Tweak model to consider a less complex case and see

  • During slow runs, 8 (50%) reported silent hangs; actionable guidance was the most common error-message shortcoming (9, 56.25%), alongside errors that failed to locate the problem (8, 50%).Only two participants (12.5%) said tools clearly communicated both the source of a slow-run problem and how to address it.Source: “Tweak model to consider a less… · p. 8

5.4.1 Recovery from false positive counter-example

  • Among Tamarin users, 10 (83.3%) manually analyzed false-positive counterexamples and 8 (66.7%) refined or corrected the model or specification.Recovery relied on trace interpretation and iterative model refinement, pointing to a need for clearer counterexample explanations and diagnostic support.Source: §5.4.1 · p. 8

5.4.2 Scalability and Practical Limitations

  • In larger Tamarin case studies, manual effort was the most reported limitation (8/12, 66.7%); memory use and long or non-terminating execution each affected 7/12 (58.3%), and 8/12 often or almost always needed helper lemmas.Overall, 11 of 12 participants (91.7%) required helper lemmas at least sometimes.Source: §5.4.2 · p. 8, §5.4.3 · p. 9

5.4.4 Usefulness of dependency graph

  • Five of 12 participants (41.7%) viewed Tamarin’s dependency graph positively, while 3 (25.0%) found it unintuitive; observational equivalence and stateful protocols drew difficult ratings from 54% and 58%, respectively.Forward secrecy was rated easy by 6 participants (55%).Source: §5.4.4 · p. 9, §5.4.5 · p. 9

5.5.1 Adequacy of Observational Equivalence Support (ProVerif)

  • For ProVerif observational equivalence, 7 of 13 respondents (54%) rated support insufficient or in need of significant improvement; comments cited coarse diff-equivalence and termination or diagnostic difficulties.Participants also described complex algebraic support as limited or conditional on careful modeling, especially for AC operators and Diffie–Hellman-type equations.Source: §5.5.1 · p. 10, §5.5.2 · p. 10

5.5.3 Support for State-Dependent Protocols

  • For ProVerif state-dependent protocols, 7 of 13 respondents (54%) gave one of the two lowest adequacy ratings, while 7 of 13 (54%) were unsure about Perfect Forward Secrecy support.State modeling often relied on labor-intensive tables, with concerns about scalability and debugging; among those expressing an opinion on Perfect Forward Secrecy, responses were generally positive.Source: §5.5.3 · p. 10, §5.5.4 · p. 10

5.5.4 Adequacy of Support for Perfect Forward Secrecy

  • Participants’ limited direct experience with ProVerif’s Perfect Forward Secrecy support, alongside reports of ad hoc modeling tricks, leaves adequacy conclusions uncertain.One participant rated support as requiring significant improvement; suggestions included modeling compromised past states carefully and testing more sessions to strengthen confidence.Source: §5.5.4 · p. 11

5.5.5 Support for Post-Compromise Security

  • Seven of 13 participants (54%) selected Not Sure about ProVerif’s post-compromise security support, while other opinions ranged from workable to insufficient.Participants often emphasized substantial manual modeling effort; these responses are usability judgments, not bounds on technical capability. Recent work demonstrated automated ProVerif-based analysis of Signal’s Double Ratchet proving post-compromise security in the analyzed model.Source: §5.5.5 · p. 11

5.5.6 Cross-Cutting Themes in ProVerif Adequacy

  • Across properties, participants cited manual effort, unpredictable termination, and gaps in native algebraic and state support as shared structural limitations.They also raised applicability concerns for IoT, TPM, and post-quantum settings, and hoped for native support for features such as mutable global state.Source: §5.5.6 · p. 11

5.5.7 Desired Features and Improvements for ProVerif

  • Model validation was the most requested ProVerif improvement (n = 10), followed by interactive debugging (n = 8) and graphical visualization and attack-trace exploration (n = 6).Documentation with realistic examples was selected by five participants; IDE or CI/CD integration and automated mistake-fixing by three each, while two requested automatic helper-lemma generation. The priorities center on trusting and understanding models and proofs rather than workflow integration.Source: §5.5.7 · pp. 11–12

6 RQ1: Usability Barriers in Cryptographic Protocol Verification Tools

Usability barriers span the verification workflow, with persistent difficulties in model fidelity, proof debugging, and interpreting verifier output. These challenges reflect a gap between protocol-level reasoning and the verifier’s formal representation and behavior.

Barriers across the verification workflow

  • Barriers arise across learning, model construction, proof management, and outcome interpretation, not at a single workflow stage.Users must translate informal protocols into symbolic abstractions and manage searches that stall or fail to terminate.Source: §6 · p. 12

Model fidelity and validation

  • Users lack systematic support for validating whether formal models faithfully represent the original protocol or implementation.Stateful and complex behaviors, and workarounds that diverge from specifications, widen this uncertainty.Source: §6 · p. 12

Proof debugging and diagnostic feedback

  • Proof failures create substantial manual debugging work, often involving model simplification, revisiting assumptions, and adding helper lemmas.Limited progress information and non-actionable errors leave users diagnosing problems through experimentation and prior expertise.Source: §6 · p. 12

Tool-specific modeling and proof challenges

  • Tamarin and ProVerif users report difficulties with stateful protocols and observational equivalence, often requiring workarounds and substantial manual effort.Tamarin users also rely on helper lemmas, interactive guidance, and manual counterexample analysis; its dependency graph can be hard to interpret.Source: §6 · p. 12

Gap between protocol reasoning and verifier behavior

  • Validating models, guiding proofs, diagnosing non-termination, and interpreting results remain largely users’ responsibility, demanding substantial formal-methods expertise.The central challenge is managing the gap between protocol-level reasoning and formal representations, proof procedures, and diagnostic output.Source: §6 · p. 12

7 RQ2: Perceived Transfer of Programming and Model-Checking Knowledge

Programming and model-checking experience offer useful but incomplete foundations for learning cryptographic verification. Users must adapt familiar reasoning strategies to specialized abstractions and proof-management demands.

Transferable programming strategies

  • Programming contributes algorithmic reasoning, pattern matching, case analysis, recursion, and debugging, but does not fully prepare users for symbolic protocol reasoning.Users still need to learn attacker knowledge, equational theories, unbounded sessions, and formal security guarantees.Source: §7 · p. 12

Model checking as a conceptual bridge

  • Model-checking experience can help users understand state exploration, property specification, and counterexamples, but is not a prerequisite.Half of participants had no model-checking experience, so onboarding cannot assume this background.Source: §7 · p. 12

Limits of knowledge transfer

  • Cryptographic verification introduces specialized concepts—including symbolic adversaries, term algebras, multiset rewriting, and applied pi calculus—that prior knowledge does not eliminate.Programming and model-checking experience provide a helpful but incomplete foundation for these conventions and abstractions.Source: §7 · p. 12

Implications for onboarding

  • Onboarding should connect familiar programming and model-checking concepts to verification while supporting users without formal-methods experience.Neither background fully addresses specialized abstractions and proof-management demands.Source: §7 · p. 12

8 RQ3: Usability, Design, and Functional Improvements

Participants prioritized improvements that reduce uncertainty in model construction, make proof behavior transparent, and support diagnosis of unsuccessful verification. Their requests span validation, diagnostics, interactive analysis, automation, documentation, and underlying support for complex protocols and properties.

Cross-tool priorities

  • Participants prioritized model validation, actionable diagnostics, counterexample explanations, interactive debugging, and help with complex proof tasks.Improving usability requires more than simplifying syntax or modernizing interfaces.Source: §8 · pp. 12–13

Model construction and validation support; Error feedback and counterexample explanation

  • ProVerif users requested model-validation support, while Tamarin users most often requested better error feedback and counterexample explanation.Users want diagnostics to identify relevant rules, lemmas, queries, or constructs and explain possible causes and fixes.Source: §8 · p. 13

Interactive debugging and visualization

  • Interactive proof-state inspection and visualization could help users explore traces, attacker knowledge, unresolved branches, and unmanageable searches.Eight ProVerif participants wanted step-by-step inspection, and six wanted a graphical interface for model and trace exploration.Source: §8 · p. 13

Automation and proof guidance; Documentation and tooling support

  • Participants proposed automating recurring proof guidance and improving examples, documentation, editors, diagnostics, and trace navigation.Suggested automation includes recommending lemmas or case distinctions and detecting modeling mistakes; recommendations should remain transparent and reviewable.Source: §8 · p. 13

Functional support for complex protocols and properties

  • Some barriers require framework-level support for stateful protocols, observational equivalence, proof scalability, and complex properties.Participants noted that workarounds can increase manual effort and distance models from the original protocol.Source: §8 · p. 13

10 Conclusion

The survey of 16 experienced users found usability challenges in model fidelity, unsuccessful verification, and interpreting tool feedback. Participants identified design priorities, while the authors caution that the findings are limited by the sample and self-reported data.

10 Conclusion

  • Participants reported difficulties validating model fidelity, diagnosing slow or non-terminating verification, and interpreting unsuccessful proofs and tool feedback.Programming and model-checking experience helped with reasoning but did not replace domain-specific knowledge of symbolic protocol verification.Source: §10 · p. 13
  • Participants prioritized model-validation support, actionable diagnostics, clearer explanations of outcomes, interactive debugging, and automation of recurring proof tasks.Source: §10 · p. 13
  • The study’s small, self-selected, predominantly experienced sample and reliance on self-reports constrain interpretation; future work should use observational studies and evaluate concrete support mechanisms.Source: §10 · pp. 13–14

Ethical Considerations

The study obtained consent before participants could proceed and took steps to protect a small, specialized community from re-identification. The authors distinguish reported user experiences from claims about tools or their developers.

Ethical Considerations

  • Participants reviewed study information and had to explicitly consent before beginning the online questionnaire.Source: Ethical Considerations · p. 14
  • To reduce re-identification and professional or reputational risks, the authors used anonymous identifiers, removed identifying details, and limited disclosure and linkage of participant-specific information.Source: Ethical Considerations · p. 14
  • The study describes reported experiences rather than objective tool deficiencies, and its small, specialized, self-selected sample is not claimed to represent all users.Source: Ethical Considerations · pp. 14–15

Open Science

The authors make study materials and analysis artifacts available while withholding raw survey responses to protect participant anonymity.

Open Science

  • The shared materials include the complete questionnaire and a lightweight codebook with codes, definitions, and example quotes.Source: Open Science · p. 15
  • Raw Qualtrics responses are not released; the authors share de-identified, processed, and aggregated data instead to reduce re-identification risk.Source: Open Science · p. 15

A Survey Instruments

The survey was organized into five blocks covering demographics, learnability, modeling and verification, and tool-specific usability. Its questions examined user backgrounds, learning experiences, modeling confidence, verification difficulties, and Tamarin use.

A Survey Instruments

  • The instrument comprised five blocks: Demographic, Learnability, Modeling & Verification, Tamarin, and ProVerif; it marked single- and multi-select questions.Source: A Survey Instruments · p. 18

A.1 Block: Demographic

  • The demographic block asked about tools used, experience length, role, and formal-methods expertise.Source: §A.1 · p. 18

A.2 Block: Learnability

  • The learnability block covered learning resources, steepest learning challenges, transferable programming concepts, and prior use of general-purpose model checkers.Source: §A.2 · p. 18

A.3 Block: Modeling & Verification

  • The modeling and verification block asked about model confidence, its limits, responses to proofs without attacks, and communication during slow or non-terminating runs.Source: §A.3 · pp. 18–19

A.4 Block: Tamarin

  • The Tamarin block covered counterexamples, scalability, helper lemmas, dependency-graph intuitiveness, modeling difficulty, and desired improvements.Source: §A.4 · p. 19

A.5 Block: ProVerif

The ProVerif block asks participants to assess support for several protocol features and identify usability improvements. Its accompanying appendix tables cover ratings across those features, participant demographics, and requested improvements.

A.5 Block: ProVerif

  • Other questions ask about ProVerif support for observational equivalence, Perfect Forward Secrecy, and complex algebraic properties.Source: §A.5 · p. 20
  • The stateful-protocol question notes ProVerif lacks native mutable global state or ordered transitions and asks whether its framework remains adequate.The response choices include insufficient support for complex stateful designs and adequacy requiring significant improvements.Source: §A.5 · p. 20
  • A separate question frames post-compromise security around state evolution, key updates, and temporal ordering, including recovery after compromise.Source: §A.5 · p. 20
  • Improvement options include interactive proof-state inspection and graphical model visualization with attack-trace display.Source: §A.5 · p. 20
  • Other proposed options include modeling-mistake suggestions, annotated documentation, development-tool integration, and formal-model validation.Source: §A.5 · p. 20

B Figures

Loading 2609.16323v1…