Understanding the Usability of Cryptographic Verification Tools Tarikul Islam Samsung R&D Institute Bangladesh
Yasin Islam Bangladesh University of Engineering and Technology
arXiv:2609.16323v1 [cs.CR] 14 Sep 2026
Khandakar Ashrafi Akbar Towson University
Imtiaz Karim The University of Texas at Dallas
Abstract
post-compromise security, ratcheting, and stateful hardware components, the practical demand for rigorous, tool-assisted verification continues to grow. Yet the effectiveness of a verification tool depends not only on its theoretical expressiveness but on whether its intended users can actually apply it correctly. A protocol verifier that can, in principle, establish strong security guarantees is of limited value if practitioners cannot construct a faithful model of the protocol, cannot understand why a proof fails to terminate, or cannot distinguish a genuine attack from an artifact of an overly coarse abstraction. Usable security research has long shown that this kind of gap between theoretical capability and practical usability is a recurring source of real-world security failure: studies of cryptographic APIs, for instance, have found that developers can produce code they believe is secure while violating basic security requirements, not because the underlying primitives are flawed, but because the tools and interfaces around them are hard to use correctly [3, 35]. Adjacent classes of security tooling, including constant-time analysis tools and fuzzers, exhibit similar patterns: usability shortcomings around installation, documentation, and output interpretation measurably suppress adoption even when the underlying technique is mature and effective [18, 52]. Despite this, the usability of cryptographic protocol verification tools themselves has received comparatively little systematic attention. Prior work on Tamarin and ProVerif overwhelmingly focuses on their formal expressiveness and analytical power, for example comparing which tool can detect which class of attack on a shared benchmark of protocols [26]. This line of work is valuable for understanding what these tools can prove, but it says little about how real users, ranging from graduate students encountering formal methods for the first time to expert researchers modeling novel protocols, actually experience the process of learning the tool, constructing a model they trust, and interpreting the tool’s output. The formal methods community has itself begun to recognize this gap: recent position papers call explicitly for more human-centered study of formal verification tools, arguing that questions of learnability, mental models, and practical
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 nontermination 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
Formal verification has become a cornerstone of modern protocol security engineering. Tools such as ProVerif [9, 10] and the Tamarin Prover [5, 31] allow researchers and practitioners to symbolically model cryptographic protocols, specify adversarial capabilities, and either prove that a protocol satisfies a given security property for an unbounded number of sessions or produce a concrete attack trace that violates it. These tools have moved well beyond academic exercises: Tamarin was used in the design and analysis of Apple’s iMessage PQ3 protocol [4] and helped uncover a security flaw in an early draft of TLS 1.3 [15], while ProVerif has been applied to widely deployed protocols including TLS 1.3 [6] and Signal [8, 29]. As protocols grow more complex, incorporating features such as 1
impact remain underexplored relative to the pace of technical advances in the tools themselves [12, 30]. Industrial user studies of verification engineers echo this concern, finding that the interpretability of verification results, rather than the underlying formal guarantees, is often what determines whether engineers trust and adopt a tool [28]. We address this gap and present a survey-based empirical study of 16 experienced users of cryptographic protocol verification tools. The users had direct, hands-on experience using Tamarin, ProVerif, or related tools in academic or industry settings, recruited through academic publications, opensource contributions, community outreach, and snowball sampling. The survey combined closed- and open-ended questions across five sections, covering participant background, tool learnability, the end-to-end modeling and verification workflow, and tool-specific usability issues unique to Tamarin and ProVerif respectively. Guided by this study, we investigate three research questions:
messages, interactive debugging and visualization support, and automation for common but tedious tasks such as helperlemma generation. This paper makes the following contributions: • We present an exploratory human-centered study focused specifically on the end-to-end experiences of 16 experienced users of Tamarin, ProVerif, and related cryptographic protocol verifiers. • We identify and characterize usability barriers spanning the full verification workflow, from learnability through modeling, proof debugging, and result interpretation, and show that these barriers are shared across tools despite their differing theoretical foundations. • We analyze the extent to which programming and general-purpose model-checking experience transfers to cryptographic protocol verification, providing evidence for where existing user knowledge helps and where it falls short.
• RQ1: What usability barriers do users encounter when applying cryptographic protocol verification tools such as Tamarin and ProVerif?
• We distill participants’ feedback into concrete, prioritized recommendations for improving the usability, diagnostics, and automation support of cryptographic verification tools, informing both future tool design and the development of educational and documentation resources.
• RQ2: How do users perceive the transfer of prior programming and general purpose model-checking experience to learning and using cryptographic protocol verification tools? • RQ3: What improvements do users believe would make these tools more accessible and effective?
2
Background
Cryptographic protocol verification tools analyze formal models of protocols under explicitly defined adversarial capabilities. Many such tools adopt the symbolic, or Dolev– Yao, model [16], in which cryptographic operations such as encryption and signatures are represented as symbolic functions rather than concrete bit-level computations. Cryptographic primitives are assumed to behave ideally: for example, an adversary can decrypt an encrypted message only when it possesses the required key. Verification therefore reasons about which symbolic terms an adversary can derive from its initial knowledge and from messages observed or generated during protocol execution. This abstraction enables automated reasoning about protocols with potentially unbounded executions while separating protocol-level reasoning from computational properties of the underlying cryptographic primitives. ProVerif and Tamarin are among the most widely adopted tools for performing this type of symbolic security protocol analysis. Tamarin [5, 31] models protocol behavior using multiset rewriting rules and expresses security properties using first-order logic. Its symbolic reasoning supports equational theories and protocols involving mutable state and temporal relationships between events. Tamarin provides both automated and interactive verification. Automated proof search
Our findings show that usability barriers are distributed across the entire verification workflow rather than concentrated at any single stage. While learning a tool’s syntax and underlying formal theory poses an initial hurdle, participants consistently identified the most persistent difficulties elsewhere: validating that a formal model faithfully captures the real protocol, debugging proofs that fail to terminate or fail without a concrete counterexample, and interpreting sparse or non-actionable error messages and progress output. We find that programming experience transfers partially, supplying useful problem-solving strategies such as algorithmic thinking and case analysis, but does not substitute for the domain-specific reasoning that symbolic protocol verification demands, and that prior exposure to general-purpose model checkers, while helpful, is not a prerequisite that most users bring with them. Tool-specific findings further show that Tamarin users frequently rely on manually constructed helper lemmas and interactive proof inspection to manage scalability, while ProVerif users report persistent friction modeling stateful protocols, complex algebraic theories, and advanced properties such as post-compromise security. Across both tools, participants converge on a consistent set of desired improvements: mechanisms for validating models against the protocols they represent, more actionable and localized error 2
can either establish a property or produce a counterexample trace, but termination is not guaranteed. In interactive mode, users can inspect intermediate proof states and dependency graphs and manually guide the search, including through auxiliary or helper lemmas. These characteristics make proof guidance, non-termination, trace interpretation, and stateful modeling particularly relevant to Tamarin’s usability. ProVerif [7, 9, 10] is an automated symbolic protocol verifier based on the applied pi calculus [1, 2]. It translates protocol models into an abstraction that enables reasoning about an unbounded number of protocol sessions and an unbounded message space. The tool supports a range of cryptographic operations through equational and functional theories and can analyze properties including secrecy, authentication, and forms of equivalence. ProVerif’s verification engine primarily emphasizes automated analysis. Although it also provides an interactive process simulator, this differs from Tamarin’s workflow for interactively inspecting and guiding proof search. Its abstractions can make verification highly scalable, but the modeling of features such as mutable state, complex algebraic properties, equivalence properties, and state-evolving security guarantees may require additional modeling choices or workarounds. These differences are important for our study. Both tools require users to translate an informal protocol into a symbolic representation and interpret the resulting verification outcome, but they expose different modeling formalisms and proof workflows. We therefore examine both usability challenges shared across cryptographic verifiers and tool-specific issues arising from Tamarin’s interactive proof process and ProVerif’s automated abstraction-based analysis.
3
inadequate explanations, and weak workflow integration as barriers to effective use [14, 27, 36, 43]. Developers also need warnings that explain the cause, security relevance, and possible remediation of a reported problem [46, 47]. Usability evaluations consequently report difficulties with navigation, scalability, alert interpretation, prioritization, and remediation, while warning presentation and specificity can influence developers’ ability to understand and act on results [34,45,48]. Comparable difficulties have been reported for fuzzing, including setup, configuration, workflow integration, progress interpretation, and failure diagnosis [40, 41, 52], and for constant-time analysis tools, where installation, documentation, and output interpretation can hinder routine use [18]. Broader studies of developer security practices likewise emphasize the importance of usable feedback and support for recovering from security-relevant mistakes [23, 50]. These findings suggest that cryptographic protocol verifiers may face related challenges, compounded by the additional demands of formal modeling, proof construction, and result interpretation. Usability and Human Factors in Formal Verification. Usability concerns have also been identified specifically in formal security-protocol verification. Garcia and Modesti [20] observed that specialized specification languages and fragmented workflows make protocol-analysis tools difficult to use and proposed an IDE integrating higher-level protocol modeling with OFMC and ProVerif. Their subsequent evaluation found that integrated tooling and abstractions can assist users with limited formal-methods or cryptography backgrounds, while complexity, training, integration, and interpretation of verification results remain important obstacles [21]. Braghin et al. [11] similarly identify the specialized languages of tools such as Tamarin and ProVerif as an expertise barrier and propose higher-level textual and graphical representations for these verification back ends. Broader formal-methods research reinforces these concerns. Surveys of researchers and practitioners identify ease of use, training, skills, scalability, tool maturity, and workflow integration as persistent adoption challenges [19, 22]. Krishnamurthi and Nelson [30] argue for greater attention to the humans interacting with formal methods, while Carreira et al. [12] call for research into users’ mental models and understanding of formal-verification guarantees. Empirical studies also highlight difficulties interpreting formal notation and verification outcomes, debugging failed proofs, and maintaining proofs over time; explanatory support can improve users’ understanding and acceptance of verification results [28, 33]. Ter Beek and Ferrari [49] further note that empirical evaluations of formal-method tools remain comparatively rare and advocate greater use of usability and human-subject studies. Taken together, prior work establishes that effective security and formal-verification tools depend not only on analytical capability, but also on learnability, appropriate abstractions, actionable feedback, debugging support, and alignment with users’ workflows. Existing work has recog-
Related Work
Usability in Cryptographic Software and APIs. Prior work has shown that API design, abstraction, documentation, defaults, examples, and required security knowledge affect developers’ ability to use cryptographic software securely [3, 32, 35, 38]. Controlled studies further show that interface design can materially affect security and functional correctness, while programming experience alone does not prevent security-relevant API blind spots [3, 37]. Accordingly, researchers have advocated developer-centered APIs, safer defaults, higher-level abstractions, and contextual guidance that reduce the amount of cryptographic reasoning required from users [17,23–25]. Similar abstraction and usability problems have been observed in Ethereum cryptographic APIs and in the design and use of cryptographic libraries more broadly [39, 44, 51]. Systematization work, however, suggests that many proposed security-API usability recommendations still lack extensive empirical validation [38]. Usability of Security Analysis Tools. Adjacent securityanalysis tools exhibit similar problems. Studies of static analysis identify false positives, poor warning prioritization, 3
4.2
nized usability barriers in security-protocol verification and proposed interfaces intended to reduce them, but systematic empirical evidence about how experienced users interact with cryptographic protocol verifiers such as Tamarin and ProVerif remains limited. In particular, little is known about how users learn these tools, how prior programming and model-checking knowledge transfers to them, how they assess model fidelity, and how they diagnose and recover from unsuccessful or non-terminating verification attempts. Our study addresses these gaps by examining users’ experiences across the end-to-end verification workflow.
4
We used purposive recruitment to reach participants with hands-on experience using cryptographic protocol verification tools in academic or professional settings. Because these tools serve a relatively small and specialized community, we recruited through four complementary channels: academic publications involving protocol verification, public technical contributions such as protocol models and tool-related repositories, relevant online research communities, and professional referrals and snowball sampling. Authors and contributors were identified as potential participants based on evidence of relevant tool use rather than assumed expertise. Recruitment was conducted from May to July 2026. We sent approximately 100 recruitment invitations by email to potential participants identified through the recruitment channels described above. The invitations included a link to the Qualtrics survey, and follow-up reminder emails were sent during the recruitment period. In total, 24 individuals started the survey. Of these, 16 completed the survey and were retained for analysis, while eight incomplete responses were excluded. Thus, our final sample consisted of 16 participants. Eligibility was based on self-reported prior experience with cryptographic protocol verification tools. On the consent page, prospective participants were informed that the study was intended for individuals with experience using such tools and were asked to confirm that they met this requirement before proceeding. Participants also reported the specific tools they had used and their level of experience in the demographic portion of the survey.
Methodology
In this section, we provide an overview of the methodology used in our questionnaire-based survey study. We also discuss recruitment and screening procedures, participant eligibility criteria, and data analysis. To examine the usability of cryptographic verification tools, we conducted an online survey with participants who had practical experience using these tools in academic or professional contexts. Our goal was to understand how users interact with cryptographic verification tools, the challenges they face during modeling and verification tasks, and the improvements they believe would make these tools more usable. For reference, the survey questionnaire is included in the Appendix A.
4.1
Recruitment and Eligibility Criteria
4.3
Study Design
Study Structure
We conducted the study using an online survey implemented in Qualtrics [42]. The survey was organized into five sections: consent, participant background and tool experience, learnability, modeling and verification, and tool-specific usability questions. Conditional display logic was used so that participants were shown Tamarin and ProVerif specific questions only when they reported prior experience with the corresponding tool. Appendix Figure 3 shows the complete survey flow. Consent. The participants were first presented with a consent page describing the purpose of the study, the procedure, the potential risks and benefits, and the participation requirements. Only participants who selected “I agree” were allowed to continue. Participant background. Participants reported their current role, experience with cryptographic verification tools, selfrated expertise, and the specific tools they had used. Their tool selections determined which tool-specific sections were subsequently displayed. Learnability. This section examined how participants learned cryptographic verification tools and the difficulties they encountered. Questions covered learning resources, prior knowledge, the steepest parts of the learning curve,
We designed the study as an online questionnaire-based survey focused on user experiences with cryptographic verification tools. Because these tools are highly specialized and require substantial technical knowledge, we targeted participants with direct hands-on experience rather than general familiarity with formal methods or security protocols. The survey was intended to capture both closed-ended and open-ended responses. Closed-ended questions were used to collect information about the background of the participants, tool usage and common usability challenges. Open-ended questions allowed participants to describe their experiences in more detail, including difficulties they encountered, strategies they used to overcome those difficulties, and suggestions for improving cryptographic verification tools. The study focused on practical usability rather than theoretical robustness of the tools. In particular, we were interested in users’ experiences with learning the tools, writing protocol models, understanding tool syntax and semantics, interpreting error messages or verification results, debugging failed proofs or models, and integrating these tools into broader research or development workflows. 4
Table 1: Summary of the survey instrument. See Appendix A for the complete questionnaire.
transferable programming concepts, and previous experience with general-purpose model checkers. Modeling and verification. Participants were asked about their confidence in model fidelity, factors limiting that confidence, strategies for handling unsuccessful proofs, communication during slow or non-terminating verification, and shortcomings in error messages. Tool-specific usability. Participants with Tamarin experience received questions concerning counterexample analysis, scalability, helper lemmas, dependency-graph visualization, modeling difficulty, and desired improvements. Participants with ProVerif experience received questions concerning observational equivalence, algebraic properties, state-dependent protocols, forward secrecy, post-compromise security, and desired improvements. The survey included both closed- and open-ended questions, allowing participants to report specific difficulties, describe strategies or workarounds, and suggest improvements. Table 1 summarizes the survey structure, while Appendix A provides the complete questionnaire.
4.4
Section (# Questions)
Sample Questions
Demographic (4)
Which of the following verification tools have you used?
Learnability (4)
What resources did you rely on when learning the tool? (select all that apply)
Modeling & Verification (5)
How confident are you that your formal model accurately reflects the real-world protocol you intend to verify?
Tamarin (6)
What is the most important usability improvement you would like to see in Tamarin Prover?
ProVerif (6)
How adequate is ProVerif’s current support for reasoning about complex algebraic properties (e.g., Diffie–Hellman, XOR, group equations)? Please explain your reasoning for your choice.
or formalism-level gap rather than a modeling inconvenience), and Not Sure (no opinion expressed). This shared scale allowed us to aggregate and compare adequacy ratings across properties with different underlying codes, and underlies the response distributions reported in Appendix Tables 2–6. Finally, we conducted a lightweight axial coding pass across the justifications for all five questions to identify crosscutting themes that recurred across multiple properties rather than being specific to any single one, such as the manual effort required by workarounds, recurring termination concerns, and comparisons participants drew to Tamarin’s support for algebraic reasoning. These cross-cutting themes inform the synthesis presented alongside individual question results in Section Results and the discussion in Section RQ3. Coding limitations. Open-ended responses were coded by a single researcher; we did not compute inter-rater reliability, and a second coder did not independently verify the coding. Given the relatively small number of free-text responses per question (n = 13 per property) and the exploratory goals of the study, we treat the resulting codes and themes as a structured, transparent summary of participants’ stated reasoning rather than as a statistically validated coding scheme. The full codebook, including per-question code definitions, severityband mappings, and cross-cutting themes, is included in our open-science artifacts (see Open Science).
Data Analysis
We analyzed closed-ended and open-ended survey responses using complementary quantitative and qualitative approaches. Quantitative analysis. For closed-ended and multiple-choice items, we report descriptive statistics (counts and percentages) across respondents. Because Qualtrics’ conditional display logic showed tool-specific question blocks only to participants who reported experience with the corresponding tool, and because not all participants answered every item, we report the applicable n for each question alongside its results. Qualitative coding of open-ended justifications. Several survey items (e.g., Q20–Q24 in the ProVerif block) asked participants to rate the adequacy of ProVerif’s support for a specific security property or protocol feature and to justify that rating in free text. To analyze these justifications systematically, we developed a codebook through an inductive, datadriven process. One researcher read all open-ended responses for a given question and derived a set of codes capturing the distinct concerns, caveats, or justifications participants raised, iteratively refining code definitions and splitting or merging codes as needed until they stably captured the range of responses. Each code was documented with a definition and one or more representative (de-identified) response excerpts, and annotated with the number of respondents assigned to it. To enable comparison of perceived adequacy across the five properties (Q20–Q24), each per-question code was additionally mapped onto a shared five-level ordinal severity scale, ranging from Fully Adequate (no significant caveats reported), through Adequate with Minor Limitations and Adequate but Requires Significant Improvement (verifiable in principle, but only via substantial manual effort, workarounds, or careful nonstandard modeling), to Insufficient (a structural
5 5.1
Results Participants
Our sample (see Appendix Table 8 for details) was predominantly experienced: 12 of 16 participants were academic researchers or faculty, two were graduate students, and two were 5
Combinations of learning resources used by participants
5.2
Intersection size
industry professionals. Thirteen participants rated themselves as having Advanced or Deep Expertise, and nine reported more than six years of experience with security-protocol verification tools. Thirteen participants had used ProVerif, while twelve had used Tamarin, with several reporting experience across multiple verification tools. These characteristics indicate that our findings primarily reflect the experiences of established users rather than novice users. This is important when interpreting the results: difficulties reported in later sections, particularly around model validation, proof debugging, and non-termination, persist even among participants with substantial prior experience.
4
Before users can effectively apply cryptographic verifiers, they must learn both the tool-specific modeling language and the formal reasoning style that underlies the verification process. In this section, we examine how participants learned cryptographic verification tools, what resources they relied on, which parts of the learning process they found most difficult, and what prior programming knowledge helped them become more effective users. Similar to other specialized security tools, cryptographic verifiers require users to move beyond ordinary programming or testing workflows and adopt a more abstract way of representing protocols, adversarial behavior, and security properties. Learning Resources. Participants reported relying on a combination of official documentation, research papers, publicly available models, recorded lectures, and guidance from peers or supervisors when learning cryptographic verification tools. Figure 1 shows that all 16 participants (100%) used official documentation or tool manuals, making this the most common learning resource. Research papers applying the tools to real protocols were used by 12 participants (75.0%), while 10 participants (62.5%) relied on publicly available models, such as GitHub repositories. Peer or supervisor guidance was reported by 9 participants (56.3%), and 4 participants (25%) used video lectures or summer-school recordings.
10
3 2
2
2 1
1
1
1
Video lectures Peer guidance Public models Research papers Documentation
9 10 12 16
Learnability of Cryptographic Verifiers
3.0 3 2.5 2.0 1.5 1.0 0.5 0.0
0 N = 16; participants could select multiple resources.
Figure 1: Combinations of learning resources used by participants. Filled circles identify the resources included in each combination, while the vertical bars show the number of participants reporting that combination.
resources. Addressing these problems often requires users to inspect proof states, modify models, introduce helper lemmas, and experiment with proof strategies. Understanding the underlying formal theory, such as applied pi-calculus or multiset rewriting, was identified by 4 participants (25.0%). Two participants (12.5%) reported that translating informal protocol descriptions into the tool’s modeling language was the steepest challenge, while only one participant (6.3%) selected interpreting verification output and attack traces. · Takeaway: Although learning challenges occurred across modeling, theory, and result interpretation, non-termination and performance debugging emerged as the most frequently reported steepest part of the learning curve. Becoming proficient with a verifier requires learning not only its language and formal foundations, but also how to diagnose and manage the behavior of its proof search.
· Takeaway: Participants relied on multiple complementary resources rather than a single learning source (see Figure 1), combining official documentation with research papers, public models, and interpersonal guidance. It indicates that respondents commonly supplemented official documentation with papers, public models, and interpersonal guidance.
Programming concepts that helped. Participants reported that several programming concepts helped them use cryptographic verification tools more effectively. Step-by-step algorithmic thinking was the most commonly selected concept, reported by 11 of 16 participants (68.8%). Pattern matching and case analysis were selected by seven participants (43.8%), while six participants (37.5%) identified recursion and reasoning through repeated structures as helpful.
Steepest part of the learning curve. When asked about the steepest part of the learning curve, 9 participants (56.3%) selected debugging non-termination and performance issues. This indicates that the most significant difficulty is not limited to learning the tool’s syntax or modeling language, but also involves understanding why proof search becomes slow, fails to terminate, or consumes excessive computational
Control flow, higher-order functions, and debugging skills were each selected by four participants (25.0%). Three participants (18.8%) reported that immutability was 6
useful, while one participant (6.3%) selected error handling. Two participants (12.5%) also mentioned other relevant experience, including knowledge of multiple programming languages and logic programming.
reasonable degree, a meaningful minority (18.8%) remain only slightly confident, indicating that confidence in model fidelity is far from uniform across users of these tools. This pattern is consistent with participants’ explanations of what most limits their confidence. The two most frequently cited factors were the lack of a systematic methodology to validate the model against the real protocol (8, 50%) and difficulty modeling stateful or complex protocol behavior (8, 50%), followed by having no way to cross-check the model against the actual implementation (7, 43.8%) and concern that the symbolic model’s assumption of perfect cryptography may not reflect real-world implementation weaknesses (6, 37.5%). Fewer participants (3, 18.75%) cited uncertainty about the realism of the Dolev-Yao attacker model, and one participant additionally identified limitations inherent to symbolic formal verification.
· Takeaway: Existing programming knowledge can provide useful cognitive scaffolding, but cryptographic verifiers cannot assume a single programming background or rely on conventional programming concepts alone. Learning resources can therefore connect verifier concepts to familiar reasoning patterns while explicitly introducing domain-specific abstractions that do not transfer directly from prior programming experience.
Previous use of general-purpose model checkers: Participants were also asked whether they had previously used general-purpose model checkers that helped them understand verification concepts. Half of the participants (8, 50.0%) reported no prior experience with such tools. SPIN was the most commonly used model checker, selected by 4(25.0%), followed by Maude with 3(18.8%) and UPPAAL with two participants (12.5%). NuSMV and PRISM were each reported by one participant (6.3%). Two participants (12.5%) mentioned other formal reasoning tools, including SMT solvers such as Z3 and Vampire, and the Isabelle theorem prover. Since participants could report multiple tools, the percentages do not sum to 100%.
· Takeaway: The moderate confidence levels reported in Q9 are driven primarily by structural gaps in the verification workflow, namely the absence of validation methodology and cross-checking mechanisms against real implementations, rather than by fundamental doubts about the symbolic modeling paradigm or the underlying attacker model.
Handling proof failures without a concrete attack trace. When a proof failed without producing a concrete attack trace, participants’ most used strategies were simplifying the model to isolate the source of failure, adding helper or auxiliary lemmas to guide the proof, and re-examining modeling decisions and abstractions for potential unsoundness. These three approaches were selected at identical rates (11, 68.8%), suggesting that experienced users treat proof failures as a debugging problem to be decomposed methodically rather than a signal to abandon or restart the model. Increasing computational resources or adjusting tool parameters was also fairly common (6, 37.5%), while consulting published models or peers (3, 18.75%) and switching tools to crossvalidate results (2, 12.5%) were used less frequently, possibly reflecting the relative isolation in which many users work or the limited availability of comparable published models. Only one participant reported assuming the model was flawed and rewriting it from scratch, and one participant stated:
· Takeaway: Interfaces, documentation, and tutorials cannot assume that new users already understand concepts such as state exploration, formal properties, or counterexample-based reasoning. Cryptographic verification tools must therefore remain learnable for users entering from security or programming backgrounds without previous model-checking experience.
5.3
Modeling and Verification
After learning the tools’ basic syntax and workflow, participants still face difficult modeling decisions. Verification depends on whether the formal model accurately captures the protocol, its assumptions, and intended security properties. We therefore examine participants’ confidence in model fidelity, factors limiting that confidence, and strategies used when verification does not proceed as expected. Confidence in model accuracy. When asked how confident they were that their formal model accurately reflects the realworld protocol or implementation, participants leaned toward moderate-to-high confidence, though with notable spread. The most common response (7, 43.75%) was "Confident", while the remaining responses were split evenly (3, 18.75%) across "Slightly confident", "Moderately confident", and "Very confident". This distribution yields a mean confidence rating of approximately 3.6/5 across the 16 respondents, suggesting that while a majority of participants trust their models to a
“Tweak model to consider a less complex case and see what happens”. – P7 · Takeaway: Participants addressed proof failures through iterative, model-focused debugging, such as simplifying models, adding auxiliary lemmas, and revisiting assumptions. This places substantial diagnostic burden on users, suggesting a need for better support in identifying problematic model components and explaining unsuccessful proof search.
7
Communication during slow or non-terminating verification. Participants’ experiences with tool communication during slow or non-terminating verification runs were predominantly negative. The most frequently selected response (8, 50%) was that the tool hangs silently with no output or progress indication, followed by the tool producing verbose low-level output that is hard to map back to the participant’s model (6, 37.5%) and the tool showing generic progress output but nothing specific to the model (5, 31.25%). Fewer participants (3, 18.75%) reported that the tool at least indicates which rule or lemma is causing the bottleneck, though without offering guidance, and only two participants(12.5%) described the tool as clearly communicating the source of the problem and how to address it. Overall, most of the selections described feedback as absent, generic, or difficult to map back to the model, whereas only two selections described the tool as clearly communicating both the source of the problem and how to address it. Shortcomings in error messaging. When asked about the most common shortcomings in the tool’s error messaging, participants most often pointed to the absence of actionable guidance, with no suggestion or hint on how to fix the issue being the top-selected shortcoming (9, 56.25%). This was followed by error messages that do not pinpoint the exact location of the problem in the model (8, 50%) and semantic errors that are silently ignored rather than explicitly reported (7, 43.75%). A smaller number of participants (5, 31.25%) noted that error messages assume too much prior knowledge of the underlying formal theory or that errors are too lowlevel and tied to internal tool mechanics rather than the model itself (3, 18.75%), while only two participants reported no shortcoming in the tool’s error messaging at all.
situations, participants with Tamarin experience were asked whether they had encountered false positive counterexamples and how they typically resolved them. The responses show that the most common strategy was manually analyzing the counterexample to confirm that it was not a real attack, reported by 10 participants (83.3%). Eight participants (66.7%) refined or corrected the protocol model or specification, indicating that false positives often result from mismatches between the intended protocol behavior and its formal representation. Two participants adjusted assumptions about the adversary or environment, while one sought help from peers, supervisors, or online communities. One participant reported another recovery approach. · Takeaway: The recovery mainly depends on careful trace interpretation and iterative model refinement. This process can require considerable expertise, suggesting a need for clearer counterexample explanations and better diagnostic support in Tamarin.
5.4.2
To examine the practical usability of Tamarin beyond small examples, participants were asked about the most common limiting factors they encountered when running larger or more realistic case studies. The response options included memory usage, long or non-terminating execution, manual effort required for interactive tracing, tool crashes or instability, not running large models, and other factors. The responses to this question help capture the scalabilityrelated challenges of using Tamarin in practice. While small protocol models may be easier to construct and verify, larger case studies often introduce additional complexity due to a larger state space, more protocol rules, richer adversary behavior, and more complex security properties. As a result, users may face limitations not only from computational resources, but also from the amount of manual effort required to guide, inspect, or debug the verification process. Manual effort was the most frequently (8, 66.7%) reported limitation. This indicates that larger models often require substantial interactive tracing, inspection, and debugging. Memory usage and long or non-terminating execution were each reported by 7 participants (58.3%), showing that computational resource requirements and verification time are also major scalability concerns. Tool crashes or instability were reported by 2 participants (16.7%).
· Takeaway: Taken together with the findings on Q12, these results indicate that error and progress messaging represent a substantial usability gap in current cryptographic verification tools: participants are frequently left to diagnose both the location and the cause of a problem largely on their own, whether that problem manifests as a stalled verification run or an unclear error message, with silent failures, either through non-termination or unreported semantic errors, emerging as a recurring theme across both questions.
5.4
Tamarin specific usability
5.4.1
Recovery from false positive counter-example
Scalability and Practical Limitations
Tamarin users may sometimes encounter counterexamples that initially appear to represent valid attacks but are later determined to be false positives. In this study, we use the term false positive to refer to a counterexample that does not correspond to a realistic attack on the intended protocol, but rather arises from modeling errors, under-specified assumptions, abstraction choices, or misunderstandings of the verification output. To examine how users recover from such
· Takeaway: Tamarin’s scalability is limited by both computational demands and the human effort required to guide and interpret complex verification tasks. Improved automation, resource management, and support for interactive analysis could therefore make larger case studies more practical.
8
5.4.3
Difficulty of modeling selected features in Tamarin
Reliance on Helper Lemmas.
Stateful protocols
Helper lemmas are intermediate properties used to guide Tamarin’s proof search, reduce the search space, and support termination when automated reasoning is insufficient. Among the 12 participants, five (41.7%) reported that they often needed to write helper lemmas, while three (25.0%) needed them almost always. Another three participants (25.0%) required them sometimes, and only one (8.3%) rarely relied on them. Overall, eight participants (66.7%) often or almost always needed helper lemmas, while 11 (91.7%) required them at least sometimes.
8%
8%
17%
25%
Forward secrecy
9%
36%
Complex equational theories (e.g., Diffie-Hellman, XOR)
33%
17%
Observational equivalence properties 100
27%
75
27%
50
25%
8%
33%
17%
55%
42%
8%
45%
25
0
25
50
Percentage of responses
Very difficult Difficult
Neutral Easy
75
100
Very easy
Figure 2: Participants’ ratings of the difficulty of modeling selected features in Tamarin. Ratings ranged from 1 (Very difficult) to 5 (Very easy). Numbers inside the bars indicate response percentage.
task as easy. Similarly, (7, 58%) of the ratings for stateful protocols indicated difficulty, compared with (4, 33%) indicating easy. 11 participants responded to observational equivalence properties. By contrast, forward secrecy received the most favorable ratings: (6, 55%) of participants rated it as easy, (4, 36%) were neutral, and only 9% rated it as difficult. Multi-session scenarios also received comparatively positive ratings, with 50% selecting either Easy or Very easy, 25% selecting Neutral, and 25% reporting difficulty. For complex equational theories, including Diffie–Hellman and XOR, half of the responses indicated ease, while 33% indicated difficulty and 17% were neutral.
Usefulness of dependency graph
In Tamarin’s interactive mode, the dependency graph visualizes the current proof state by showing rule instances and the dependencies between their premises and conclusions. It helps users examine protocol traces, identify unresolved constraints, and navigate the proof process. Among the 12 participants, four (33.3%) rated the dependency graph as intuitive, while one (8.3%) considered it very intuitive. Four participants (33.3%) found it moderately intuitive, indicating that the graph was readable but required effort. Two participants (16.7%) rated it as unintuitive, and one (8.3%) considered it very unintuitive. In general, five participants (41.7%) viewed the visualization positively, while three (25.0%) found it unintuitive or very unintuitive.
· Takeaway: Participants reported the greatest difficulty with observational equivalence and stateful protocols. Forward secrecy was viewed as the most approachable feature, while ratings for multi-session scenarios and complex equational theories were comparatively favorable but more varied.
· Takeaway: Participants’ ratings suggest that Tamarin’s dependency graph is usable for many users but is not uniformly intuitive. The graph is intended to help users understand and navigate complex proof states; if interpreting the visualization itself requires substantial experience, some of its diagnostic value is lost precisely for users who need additional guidance. Clearer visual organization, navigation, and explanations of proof-state elements could make interactive analysis more accessible.
5.4.5
50%
Multi-session scenarios
· Takeaway: These findings indicate that successful verification frequently depends on manually constructed intermediate lemmas, requiring users to understand both the protocol model and Tamarin’s proof-search behavior. Better automated guidance for generating or recommending helper lemmas could therefore reduce manual effort and improve usability.
5.4.4
8%
5.5
ProVerif specific usability
Ratings and representative concerns for Q20–Q24 were derived using the coding procedure described in Section 4.4: each open-ended justification was assigned an inductivelyderived, question-specific code, which was in turn mapped onto a shared five-level adequacy scale (Fully Adequate, Adequate with Minor Limitations, Adequate but Requires Significant Improvement, Insufficient, Not Sure) to allow comparison across properties. This shared scale underlies the response distributions reported details in Appendix Tables 2–6.
Difficulty of modeling protocol features.
Participants rated the difficulty of modeling five protocol features on a five-point scale ranging from Very difficult to Very easy. As shown in Figure 2, observational equivalence properties and stateful protocols received the highest proportions of difficult ratings. For observational equivalence, (6, 54%) of responses were either Very difficult or Difficult, while the remaining (5, 45%) were neutral; no participants rated this
5.5.1
Adequacy of Observational Equivalence Support (ProVerif)
Participants expressed mixed views on ProVerif’s support for observational equivalence (i.e., whether an intruder can distinguish between two protocols or scenarios). Appendix Ta9
ble 6 provides the full response distribution and representative concerns from participants’ free-text justifications. When asked how adequate ProVerif’s current support for observational equivalence is, responses were fairly evenly distributed across the scale, with a slight lean toward perceiving limitations: four participants rated it insufficient for modern protocols, three rated it adequate but requiring significant improvements, two rated it adequate with only minor limitations, two rated it fully adequate, and two were not sure. Notably, 7 of the 13 respondents (54%) selected one of the two Insufficient or Requires Significant Improvement bands, suggesting that a majority of participants who ventured an opinion see room for growth in this area. The qualitative comments accompanying these ratings point to a few recurring themes rather than a single shared complaint. Several participants raised concerns about the granularity and precision of diff-equivalence, describing it as an over-approximation that is often too coarse or too strong to capture properties like anonymity, unlinkability, or processes that differ in more than simple terms. Others pointed to practical limitations, including termination difficulties and a desire for more specific diagnostic explanations when equivalence checks fail, echoing the broader error-messaging concerns raised in Q13. A smaller number of participants noted domainspecific gaps, such as applicability to IoT and post-quantum computing contexts, or the desire to reason about more than two executions for properties like robust declassification. Interestingly, even among participants who rated the feature as adequate, one noted that usability depends heavily on deep prior knowledge of the tool, reinforcing a theme that surfaces throughout the survey: ProVerif’s core theoretical machinery may be sound, but its accessibility and diagnostic transparency remain significant barriers for users. 5.5.2
sidered ProVerif’s algebraic support adequate, responses emphasized that this adequacy is conditional: users must carefully construct equational theories and explicitly account for properties such as associativity and commutativity, and one participant noted that termination behavior in the presence of such theories is not always predictable. · Takeaway: Together, these results suggest that algebraic reasoning, particularly involving DH-type and AC equations, remains one of the more technically demanding aspects of modeling in ProVerif, requiring either specialized expertise or acceptance of reduced expressiveness.
5.5.3
Support for State-Dependent Protocols
Responses tended to identify limitations in ProVerif’s support for state-dependent protocols, particularly for complex stateful designs. Appendix Table 4 reports the full distribution and representative concerns. Responses to Q22 skewed toward viewing ProVerif’s support for state-dependent protocols as inadequate: four participants rated it insufficient for complex stateful designs, three rated it adequate but requiring significant improvements, and only two rated it fully adequate. Combined, 7 of 13 respondents (54%) selected one of the two lowest-rated bands. A recurring theme across responses was the reliance on tables as a workaround for modeling state, which multiple participants described as usable but unsatisfactory, requiring substantial manual effort, and of uncertain scalability to larger protocols. Several participants pointed to concrete domains where this limitation is especially acute, such as protocols involving TPMs or IoT devices, and one noted having to significantly deviate from the original protocol specification simply to achieve termination. Extensions such as GSVerif were mentioned as a partial mitigation, and debugging stateful models was separately flagged as a source of difficulty even when a workable encoding was found. Several participants also expressed hope that native support for mutable state would appear in future tool versions.
Support for Complex Algebraic Properties
Participants generally viewed ProVerif’s support for complex algebraic properties as limited or dependent on careful modeling. Appendix Table 5 provides the detailed responses distribution and representative comments. Participant ratings of ProVerif’s support for complex algebraic properties were mixed but leaned toward identifying limitations: four participants found support limited for algebra-heavy designs, three were not sure, three considered it adequate with careful modeling, and one each rated it fully adequate, prone to false positives, or insufficient and requiring redesign. The most consistent theme across responses, appearing in both the Limited and Requires Redesign codes, was ProVerif’s lack of native support for AC (associativecommutative) operators and Diffie–Hellman-type equations, which participants noted are common in real-world protocol designs and are better supported in tools like Tamarin; several participants explicitly benchmarked ProVerif against Tamarin on this point. Even among participants who con-
· Takeaway: Respondents reported burdens when encoding richer state evolution using ProVerif’s available mechanisms.
5.5.4
Adequacy of Support for Perfect Forward Secrecy
Appendix Table 3 summarizes participant ratings of ProVerif’s support for verifying Perfect Forward Secrecy (PFS). For Perfect Forward Secrecy, the dominant response was uncertainty: seven of 13 participants (54%) selected Not Sure, considerably more than for any other adequacy question in the survey. Among participants who did express an opinion, responses were generally positive, with three rating ProVerif’s support fully adequate and two rating it adequate with only minor limitations. The concerns raised by these participants were relatively narrow in scope, centering on the need to 10
carefully model the notion of a compromised “past” state and a suggestion that testing a greater number of sessions could strengthen confidence in verification results. Only one participant rated support as requiring significant improvement, noting that modeling PFS still requires ad hoc tricks. The high proportion of Not Sure responses suggests that, relative to other properties surveyed, participants have comparatively less direct experience modeling Perfect Forward Secrecy in ProVerif, which limits how strongly conclusions about its adequacy can be drawn from this sample. 5.5.5
earlier in Q11. Termination behavior surfaced as an independent source of uncertainty across observational equivalence, algebraic properties, and stateful modeling (Q20–Q22), reinforcing the non-termination concerns raised throughout the broader modeling and verification workflow (Q12). Participants also explicitly benchmarked ProVerif against Tamarin, particularly regarding native support for Diffie–Hellman-type and AC-operator reasoning (Q21), and raised domain-specific applicability concerns for IoT, TPM, and post-quantum settings (Q20, Q22). Several participants expressed hope for native support of currently unsupported features, such as mutable global state, in future tool versions (Q22, Q24), while others pointed to existing published models (e.g., for Signal) as evidence that even demanding properties can be verified given sufficient effort (Q24).
Support for Post-Compromise Security
Participant ratings of ProVerif’s support for post-compromise security, which requires reasoning about state evolution are shown in Appendix Table 2. As with Perfect Forward Secrecy, uncertainty dominated responses regarding post-compromise security, with seven of 13 participants (54%) selecting Not Sure. Among the remaining participants, opinions were split evenly between viewing ProVerif’s support as workable and viewing it as insufficient: two participants rated it adequate with careful modeling, citing existing models for protocols such as Signal as evidence of feasibility while explicitly noting that such models require substantial manual effort to construct, and two rated it insufficient for modern ratcheting protocols, with one hoping that related overfitting issues would be addressed in future updates despite acknowledging this as a hard problem. Only one participant rated support as fully adequate, and one rated it adequate but limited specifically for dynamic recovery scenarios, noting that this remains difficult to model in a straightforward way. The high rate of uncertainty for Q24 suggests that many participants had limited direct experience modeling post-compromise security in ProVerif. Participants who did express an opinion frequently emphasized the modeling effort required. These responses should therefore be interpreted as usability judgments rather than bounds on ProVerif’s technical capabilities. Recent work [13] has demonstrated a highly automated ProVerif-based analysis of Signal’s Double Ratchet that reasons about key compromise and proves post-compromise security in the analyzed model, showing that sophisticated PCS verification is possible while potentially requiring specialized modeling expertise. 5.5.6
· Takeaway: Participants’ concerns about ProVerif extend beyond any single security property to shared structural limitations, namely termination predictability, native algebraic and state support, and the manual effort required to work around their absence.
5.5.7
Desired Features and Improvements for ProVerif
When asked which features or improvements would most increase their productivity with ProVerif, participants most frequently selected a model validation mechanism to check whether the formal model matches the intended protocol (n = 10), followed by an interactive debugging mode allowing stepby-step inspection of the proof state (n = 8) and a graphical interface for model visualization and attack trace exploration (n = 6). Improved documentation with realistic, well-annotated protocol examples was also fairly commonly selected (n = 5), while integration with standard development tools such as IDE plugins or CI/CD pipelines (n = 3) and automated suggestions for fixing common modeling mistakes (n = 3) were selected less frequently. Two participants used the openended option to specifically request automated generation of helper lemmas. This ranking of desired improvements aligns closely with limitations identified elsewhere in the survey. The top-ranked request, a model validation mechanism, directly mirrors the leading concerns raised in Q10, where the lack of a systematic methodology to validate the model against the real protocol and the inability to cross-check the model against the actual implementation were among the most commonly cited limits on confidence. Similarly, the demand for an interactive debugging mode and a graphical interface for trace exploration reflects the debugging-heavy troubleshooting strategies reported in Q11 and the recurring complaints in Q12 and Q13 about silent failures and unhelpful error messages. The relatively lower demand for IDE or CI/CD integration and automated mistake-fixing suggests that participants’ priorities center less on tooling convenience and more on fundamental
Cross-Cutting Themes in ProVerif Adequacy
Beyond the property-specific concerns above, our axial coding pass across Q20–Q24 identified several themes that recurred across multiple properties rather than being specific to any single one. Manual effort was repeatedly cited as the qualifier that separates a nominally adequate feature from a practically usable one, appearing in participants’ justifications for complex algebraic properties (Q21), state-dependent protocols (Q22), and post-compromise security (Q24), and echoing the workaround-heavy debugging strategies reported 11
gaps in validation, transparency, and debuggability.
guiding proofs, diagnosing non-termination, and interpreting results remain largely the user’s responsibility, so effective use depends on substantial formal-methods expertise, which may limit accessibility and wider adoption.
· Takeaway: Users are less concerned with ProVerif fitting into modern development workflows than with being able to trust and understand the models and proofs it produces.
7 6
RQ1: Usability Barriers in Cryptographic Protocol Verification Tools
RQ2: Perceived Transfer of Programming and Model-Checking Knowledge
Transferable programming strategies. Prior programming experience transfers mainly through general problem-solving strategies. Participants drew on step-by-step algorithmic reasoning, pattern matching, case analysis, recursion, and debugging when constructing and analyzing models, supporting decomposition, reasoning about alternative execution paths, and diagnosis. However, no single concept was universally essential, and programming experience does not fully prepare users for symbolic reasoning, unbounded sessions, attacker knowledge, equational theories, or interpreting formal security guarantees, so users must adapt familiar reasoning to a substantially different setting. Model checking as a conceptual bridge. Prior experience with general-purpose model checkers may provide a more direct bridge: familiarity with state exploration, property specification, and counterexamples helps users understand the broader purpose and behavior of cryptographic verifiers. However, half of participants had no such experience, so this background is helpful but not a prerequisite, and verifiers cannot assume new users already understand these concepts. Limits of knowledge transfer. Cryptographic verification introduces domain-specific concepts not typically found in conventional programming or model checking, including symbolic adversary models, cryptographic term algebras, protocolspecific security properties, and formalisms such as multiset rewriting and the applied pi calculus. Prior knowledge may clarify the shape of the verification task, but does not eliminate the need to learn these specialized theories and conventions. Implications for onboarding. Programming and modelchecking knowledge together provide a helpful but incomplete foundation: programming contributes transferable reasoning and debugging strategies, while model checking provides familiarity with verification concepts and workflows. Neither fully addresses the specialized abstractions and proof-management demands of cryptographic protocol analysis, so onboarding materials should explicitly connect familiar concepts to their verification counterparts while supporting users without prior formal-methods experience.
Barriers across the verification workflow. Usability barriers occur throughout the verification workflow rather than at a single stage. Learning specialized syntax and formal theory is challenging, but the more persistent difficulties arise during model construction, proof management, and interpreting outcomes: translating informal protocols into suitable symbolic abstractions, judging whether those abstractions are accurate, and managing proof searches that may stall or fail to terminate. Model fidelity and validation. A central barrier is confidence in model fidelity. Even confident participants reported limited support for systematically validating a formal model against the original protocol or implementation, a gap between verifying a representation and establishing that it faithfully captures the real system. Difficulty representing stateful and complex behavior widens this uncertainty, particularly when the verifier requires workarounds that diverge from the original specification. Proof debugging and diagnostic feedback. Proof failures impose a substantial manual debugging burden. Users typically respond by simplifying models, revisiting assumptions, and introducing helper lemmas, work that requires understanding both the protocol and the verifier’s proof-search behavior. Limited progress information and non-actionable error messages compound this: silent hangs, low-level internal output, or unlocalized errors leave users to diagnose problems largely through experimentation and prior expertise. Tool-specific modeling and proof challenges. Tool-specific findings reinforce these broader barriers. Tamarin users frequently depend on helper lemmas, interactive proof guidance, and manual counterexample analysis; its dependency graph can support expert analysis but may require substantial experience to interpret, and modeling stateful protocols or observational equivalence remains especially demanding. ProVerif participants identified similar difficulties with state-dependent protocols, complex algebraic properties, and observational equivalence, properties that workarounds can represent only at the cost of significant manual effort and reduced fidelity to the original protocol. Gap between protocol reasoning and verifier behavior. The main usability challenge is therefore not learning to operate a verifier, but managing the gap between the user’s protocol-level reasoning and the tool’s formal representation, proof procedures, and diagnostic output. Validating models,
8
RQ3: Usability, Design, and Functional Improvements
Improving these tools requires more than simplifying syntax or modernizing interfaces. Participants prioritized reducing uncertainty during model construction, making proof behavior 12
transparent, and strengthening support for diagnosing unsuccessful verification. Across both tools, the most important needs concerned model validation, actionable diagnostics, counterexample explanation, interactive debugging, and assistance with complex proof tasks. An overview appears in Appendix Table 7. Model construction and validation support. A modelvalidation mechanism was the most requested ProVerif improvement, helping users compare formal models with protocol descriptions, identify omitted assumptions, and link model elements to implementation behavior. It would not guarantee correctness but could reduce mismatches between the verified model and the intended protocol. Error feedback and counterexample explanation. For Tamarin, error feedback and counterexample explanation were the top requests (eight responses each). Participants wanted diagnostics that identify the relevant rule, lemma, query, or construct and explain possible causes and fixes, with counterexamples summarized at the protocol level so genuine attacks can be distinguished from modeling errors or abstraction artifacts. Interactive debugging and visualization. Interactive debugging and visualization could reduce the manual effort needed to understand verification behavior. Eight ProVerif participants wanted step-by-step proof-state inspection, and six wanted a graphical interface for model and trace exploration. Such interfaces should connect internal proof operations to the user’s original protocol representation, letting users trace attacker knowledge, identify unresolved branches, and locate where search becomes unmanageable. For Tamarin, this means clearer dependency-graph layouts, better navigation, and stronger interactive/proof-oracle support for case distinctions; for ProVerif, an interactive mode for examining failed queries and diagnosing non-termination that is currently hard to infer from static output. Automation and proof guidance. Tamarin users frequently depend on manually written helper lemmas and case distinctions, and two ProVerif respondents requested automated lemma generation. Future tools could analyze recurring proof patterns to recommend intermediate lemmas, case distinctions, model simplifications, or alternative strategies, and detect modeling mistakes or abstractions that produce false counterexamples or non-termination. AI-assisted functionality could also synthesize counterexamples, summarize proof states, and explain unresolved branches, but such recommendations should remain transparent and reviewable, supporting rather than obscuring the formal basis of the result. Documentation and tooling support. Documentation and tooling support were each selected by five Tamarin participants, and five ProVerif respondents wanted improved, realistic, well-annotated examples. Traditional reference manuals appear insufficient alone; documentation should explain modeling choices, rejected alternatives, common mistakes, and debugging steps, ideally with comparative
examples across tools for non-termination, false counterexamples, helper lemmas, and stateful or equivalence properties. Tooling support could include syntax-aware editors, inline diagnostics, navigation between models and counterexample traces, and state-transition visualization. IDE and CI/CD integration was a lower priority (three respondents), suggesting adoption is currently constrained more by validation, interpretability, and debuggability than by workflow convenience; integration is likely to matter more once users can trust the verification process. Functional support for complex protocols and properties. Some barriers require changes beyond interfaces or documentation. For Tamarin, participants wanted stronger support for stateful protocols, observational equivalence, proof scalability, and interactive analysis; for ProVerif, improvements to mutable state, ordered transitions, complex algebraic theories, observational equivalence, and properties involving state evolution such as post-compromise security. Addressing these may require changes to the underlying frameworks, reducing reliance on workarounds that increase manual effort and distance the model from the original protocol.
9
Acknowledgments
We thank all survey participants for generously contributing their time and sharing their experiences and perspectives. We are particularly grateful to Qifan Zhang of Palo Alto Networks and Zilin Shen of Purdue University for participating in the pilot survey and providing valuable feedback that informed the refinement and finalization of the questionnaire. Their input helped improve the clarity, relevance, and overall quality of the survey instrument.
10
Conclusion
We presented an exploratory survey of 16 experienced users of cryptographic protocol verification tools, including Tamarin and ProVerif. Participants reported challenges in validating whether formal models faithfully represent intended protocols, diagnosing slow or non-terminating verification, and interpreting unsuccessful proofs and tool feedback. Prior programming and model-checking experience provided useful reasoning strategies but did not replace the domain-specific knowledge required for symbolic protocol verification. Across tools, participants emphasized the need for better model-validation support, actionable diagnostics, clearer explanations of verification outcomes, interactive debugging, and greater automation of recurring proof tasks. Our findings should be interpreted in light of the study’s small, self-selected, and predominantly experienced sample and its reliance on self-reported rather than observed tool use. Overall, improving cryptographic verifiers requires reducing the gap between users’ protocol-level reasoning and the tools’ 13
formal representations and proof procedures. Future work should evaluate these needs through observational studies and concrete mechanisms for model validation, proof guidance, and explanation.
considered re-identification and associated professional or reputational harm to be the primary risks and therefore limited the disclosure and linkage of participant-specific information; (2) Tool developers and maintainers: are also affected because our findings identify perceived limitations and recommend changes to existing tools. We therefore distinguish participants’ reported experiences from objective technical deficiencies and avoid attributing usability problems or design trade-offs to individual developers; (3) Current and prospective users: may benefit from improved diagnostics, model-validation support, documentation, visualization, and proof guidance, while inaccurate or overly broad interpretations of our findings could give users misleading expectations about the capabilities or limitations of particular tools; (4) The broader security and formal-methods research community: may use these findings to inform future tool design and human-centered research. Because our evidence is based on a small, specialized, self-selected sample, we avoid claiming that the reported experiences are representative of all users of cryptographic verification tools. Responsible Characterization of Tools and Findings. Our study examines users’ experiences with cryptographic verification tools rather than evaluating the competence or intentions of their developers. Some challenges reported by participants, including non-termination, limitations in modeling particular protocol features, or difficulties associated with specific abstractions, may arise from fundamental properties or design trade-offs of the underlying verification approaches rather than straightforward software defects. We therefore distinguish between participants’ reported experiences, our interpretation of those experiences, and objective claims about a tool’s technical capabilities. Similarly, difficulty using a verification tool should not be interpreted as evidence of insufficient expertise on the part of an individual participant. Our goal is to identify opportunities for improving usability and supporting users rather than assigning responsibility for the difficulties reported. Respect for Law and Public Interest. The study consisted of a questionnaire about participants’ experiences with cryptographic protocol verification tools and did not involve probing deployed systems, exploiting vulnerabilities, or interacting with third-party systems without authorization. The survey focused on participants’ learning experiences, modeling and verification workflows, difficulties encountered during proof construction and debugging, and desired improvements to existing tools. We avoid reporting identifying project details or other information that could create unnecessary risks to participants or third parties. The expected public benefit of this research is a better understanding of the usability barriers surrounding cryptographic protocol verification and the identification of design priorities that may help researchers and practitioners construct, debug, interpret, and validate formal protocol models more effectively. Responsible Interpretation and Generalization. Partici-
Ethical Considerations Human Subjects and Informed Consent. This study involved an online questionnaire with researchers, graduate students, and industry practitioners who had hands-on experience with cryptographic protocol verification tools. The study was reviewed and approved by the relevant Institutional Review Board (IRB). Before beginning the survey, participants were presented with a consent form describing the purpose and scope of the study, the survey procedure, potential risks and benefits, and other information relevant to participation. Participants could proceed with the survey only after explicitly providing consent by selecting the “I agree” option; participants who selected “I disagree” were not permitted to continue. Participant Privacy and Confidentiality. Because cryptographic protocol verification is a relatively small and specialized research community, combinations of professional role, experience, tool usage, research activities, or qualitative responses could potentially make individual participants identifiable even after direct identifiers are removed. This creates potential professional or reputational risks, particularly when participants describe difficulties they encountered, limitations of particular tools, or their own verification practices. To mitigate these risks, we refer to participants using anonymous identifiers, remove potentially identifying details from quoted responses, and avoid reporting project-specific information that could reveal participant identities. We also avoid unnecessarily linking qualitative responses with detailed participant characteristics when such combinations could increase re-identification risk. Data Protection and Reporting. Survey responses were collected through Qualtrics and stored securely for research purposes. We report quantitative results primarily in aggregate and use de-identified excerpts when presenting qualitative responses. Because the participant population is specialized and some combinations of demographic characteristics and tool experience may be distinctive, we take particular care when reporting participant-level information. Any materials released alongside the paper will be reviewed to ensure that they do not expose direct identifiers or combinations of information that could reasonably facilitate re-identification. Affected Stakeholders. We identify the following primary stakeholder groups that may be affected by our work: (1) Study participants: are the primary stakeholders because they provided potentially sensitive descriptions of their expertise, workflows, difficulties, and opinions about particular verification tools. Given the relatively small and specialized cryptographic-verification community, we 14
pants were recruited from a specialized community through academic publications, open-source contributions, community outreach, professional contacts, referrals, and snowball sampling. Participation was voluntary, and the recruitment strategy may introduce self-selection bias. The study also relies on participants’ self-reported experiences rather than direct observation of their verification activities. We therefore interpret the findings as evidence about the experiences and practices reported by our participants and do not claim that the results are statistically representative of all Tamarin, ProVerif, or cryptographic-verification users.
[3] Yasemin Acar, Michael Backes, Sascha Fahl, Simson Garfinkel, Doowon Kim, Michelle L. Mazurek, and Christian Stransky. Comparing the usability of cryptographic apis. In 2017 IEEE Symposium on Security and Privacy (SP), pages 154–171, 2017. doi: 10.1109/SP.2017.52. [4] Apple Security Engineering and Architecture (SEAR). iMessage with PQ3: The new state of the art in quantumsecure messaging at scale, February 2024. Accessed: 2026-07-03. URL: https://security.apple.com/ blog/imessage-pq3/. [5] David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, and Benedikt Schmidt. Tamarin prover, 2026. Accessed April 2026. URL: https:// tamarin-prover.github.io/.
Open Science To support transparency, reproducibility, and evaluation of our study, we make the study materials and analysis artifacts publicly available. During the anonymous review period, these materials are available through an anonymized repository at https://anonymous.4open.science/r/ protocol-verifier-usability-artifact-6625/. The research artifacts associated with this study are:
[6] Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified models and reference implementations for the tls 1.3 standard candidate. In 2017 IEEE Symposium on Security and Privacy (SP), pages 483– 502, 2017. doi:10.1109/SP.2017.26. [7] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pages 82–96, 2001. doi:10.1109/CSFW.2001.930138.
• Survey questionnaire • Consent form • Codebook
[8] Bruno Blanchet. Automatic verification of security protocols in the symbolic model: The verifier proverif. In International School on Foundations of Security Analysis and Design, pages 54–87. Springer, 2012.
Materials Shared: We include the complete questionnaire used in the study, including the consent information. We also share the lightweight codebook used to analyze the explanatory free-text responses, with codes, definitions, and example quotes that we coded for each code. Materials Not Shared: We do not publicly release the raw Qualtrics response data. Although the survey did not intentionally collect direct personally identifiable information, the cryptographic-verification community is relatively small and specialized, and combinations of response content and survey metadata could increase the risk of participant reidentification. To minimize this risk and preserve participant anonymity, we share only de-identified, processed, and aggregated data necessary to support the analyses reported in this paper, rather than the original Qualtrics export.
[9] Bruno Blanchet. ProVerif: Cryptographic Protocol Verifier in the Formal Model, 2023. Accessed April 2026. URL: https://bblanche.gitlabpages.inria.fr/ proverif/. [10] Bruno Blanchet, Ben Smyth, and Vincent Cheval. Proverif 2.05: Automatic cryptographic protocol verifier, user manual and tutorial, 2026. Accessed April 2026. URL: https://bblanche.gitlabpages.inria.fr/ proverif/manual.pdf. [11] Chiara Braghin, Mario Lilli, and Elvinia Riccobene. Aprover front-end modelling language for designing security protocols. SN Computer Science, 6(8):992, 2025.
References
[12] Carolina Carreira, Joao F Ferreira, Alexandra Mendes, and Nicolas Christin. Exploring usable security to improve the impact of formal verification: a research agenda. arXiv preprint arXiv:2111.08209, 2021.
[1] Martín Abadi, Bruno Blanchet, and Cédric Fournet. The applied pi calculus: Mobile values, new names, and secure communication. J. ACM, 65(1), 2017. doi: 10.1145/3127586.
[13] Vincent Cheval, Charlie Jacomme, and Jessica Richards. Automated formal analysis of signal’s double ratchet: Attacks, fixes and security proofs. In 2026 IEEE Symposium on Security and Privacy (SP), pages 1522–1538, 2026. doi:10.1109/SP63933.2026.00120.
[2] Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. ACM Sigplan Notices, 36(3):104–115, 2001. 15
[14] Maria Christakis and Christian Bird. What developers want and need from program analysis: an empirical study. In Proceedings of the 31st IEEE/ACM international conference on automated software engineering, pages 332–343, 2016.
[24] Peter Leo Gorski, Luigi Lo Iacono, Dominik Wermke, Christian Stransky, Sebastian Möller, Yasemin Acar, and Sascha Fahl. Developers deserve security warnings, too: On the effect of integrated security advice on cryptographic API misuse. In Fourteenth Symposium on Usable Privacy and Security (SOUPS 2018), pages 265– 281, Baltimore, MD, August 2018. USENIX Association. URL: https://www.usenix.org/conference/ soups2018/presentation/gorski.
[15] Cas Cremers, Marko Horvat, Sam Scott, and Thyla Van Der Merwe. Automated analysis and verification of tls 1.3: 0-rtt, resumption and delayed authentication. In 2016 IEEE Symposium on Security and Privacy (SP), pages 470–485. IEEE, 2016.
[25] Matthew Green and Matthew Smith. Developers are not the enemy!: The need for usable security apis. IEEE Security & Privacy, 14(5):40–46, 2016. doi:10.1109/ MSP.2016.111.
[16] Danny Dolev and Andrew Yao. On the security of public key protocols. IEEE Transactions on information theory, 29(2):198–208, 1983.
[26] A Hassan, I Ishaq, J Munilla, AU Ardelia, CF Fangasadha, R Widuri, and V Polepally. Evaluating formal methods for verifying security protocols: a case study of tamarin, avispa, and proverif. Journal of Theoretical and Applied Information Technology, 103(5):1597– 1614, 2025.
[17] Ehsan Firouzi, Ammar Mansuri, Mohammad Ghafari, and Maziar Kaveh. From struggle to simplicity with a usable and secure api for encryption in java. In Proceedings of the 18th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement, pages 556–565, 2024.
[27] Brittany Johnson, Yoonki Song, Emerson Murphy-Hill, and Robert Bowdidge. Why don’t software developers use static analysis tools to find bugs? In 2013 35th International Conference on Software Engineering (ICSE), pages 672–681, 2013. doi:10.1109/ICSE. 2013.6606613.
[18] Marcel Fourné, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, PierreAlain Fouque, and Yasemin Acar. " these results must be false": A usability evaluation of constant-time analysis tools. In 33rd USENIX Security Symposium (USENIX Security 24), pages 6705–6722, 2024. [19] Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. The 2020 expert survey on formal methods. In International Conference on Formal Methods for Industrial Critical Systems, pages 3–69. Springer, 2020.
[28] Arut Prakash Kaleeswaran, Arne Nordmann, Thomas Vogel, and Lars Grunske. A user study for evaluation of formal verification results and their explanation at bosch. Empirical Software Engineering, 28(5):125, 2023.
[20] Rémi Garcia and Paolo Modesti. An ide for the design, verification and implementation of security protocols. In 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pages 157– 163. IEEE, 2017.
[29] Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pages 435–450, 2017. doi:10.1109/EuroSP.2017.38.
[21] Rémi Garcia and Paolo Modesti. A practical approach to formal methods: An eclipse integrated development environment (ide) for security protocols. Electronics, 13(23):4660, 2024.
[30] Shriram Krishnamurthi and Tim Nelson. The human in formal methods. In International Symposium on Formal Methods, pages 3–10. Springer, 2019.
[22] Mario Gleirscher and Diego Marmsoler. Formal methods in dependable systems engineering: a survey of professionals from europe and north america. Empirical Software Engineering, 25(6):4473–4546, 2020.
[31] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The tamarin prover for the symbolic analysis of security protocols. In International conference on computer aided verification, pages 696–701. Springer, 2013.
[23] Peter Leo Gorski, Yasemin Acar, Luigi Lo Iacono, and Sascha Fahl. Listen to developers! a participatory design study on security warnings for cryptographic apis. In Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems, pages 1–13, 2020.
[32] Kai Mindermann, Philipp Keck, and Stefan Wagner. How usable are rust cryptography apis? In 2018 IEEE International Conference on Software Quality, Reliability and Security (QRS), pages 143–154. IEEE, 2018. 16
[33] Eric Mugnier, Yuanyuan Zhou, Ranjit Jhala, and Michael Coblenz. On the impact of formal verification on software development. Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3642–3668, 2025.
[41] Stephan Plöger, Mischa Meier, and Matthew Smith. A usability evaluation of afl and libfuzzer with cs students. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems, pages 1–18, 2023.
[34] Marcus Nachtigall, Michael Schlichtig, and Eric Bodden. A large-scale study of usability criteria addressed by static analysis tools. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 532–543, 2022.
[42] Qualtrics. Accessed: 2026-07-29. URL: https://www. qualtrics.com/. [43] Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, and Ciera Jaspan. Lessons from building static analysis tools at google. Communications of the ACM, 61(4):58–66, 2018.
[35] Sarah Nadi, Stefan Krüger, Mira Mezini, and Eric Bodden. Jumping through hoops: why do java developers struggle with cryptography apis? In Proceedings of the 38th International Conference on Software Engineering, ICSE ’16, page 935–946, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/2884781.2884790.
[44] Juliane Schmüser, Philip Klostermeyer, Kay Friedrich, and Sascha Fahl. “i’m pretty expert and i still screw it up”: Qualitative insights into experiences and challenges of designing and implementing cryptographic library apis. In 2025 IEEE Symposium on Security and Privacy (SP), pages 2322–2340. IEEE, 2025. [45] Justin Smith, Lisa Nguyen Quang Do, and Emerson Murphy-Hill. Why can’t johnny fix vulnerabilities: A usability evaluation of static analysis tools for security. In Sixteenth Symposium on Usable Privacy and Security (SOUPS 2020), pages 221–238. USENIX Association, August 2020. URL: https://www.usenix.org/ conference/soups2020/presentation/smith.
[36] Lisa Nguyen Quang Do, James Wright, and Karim Ali. Why do software developers use static analysis tools? a user-centered study of developer needs and motivations. IEEE Transactions on Software Engineering, 48:835– 847, 03 2022. doi:10.1109/TSE.2020.3004525. [37] Daniela Seabra Oliveira, Tian Lin, Muhammad Sajidur Rahman, Rad Akefirad, Donovan Ellis, Eliany Perez, Rahul Bobhate, Lois A. DeLong, Justin Cappos, and Yuriy Brun. API blindspots: Why experienced developers write vulnerable code. In Fourteenth Symposium on Usable Privacy and Security (SOUPS 2018), pages 315– 328, Baltimore, MD, August 2018. USENIX Association. URL: https://www.usenix.org/conference/ soups2018/presentation/oliveira.
[46] Justin Smith, Brittany Johnson, Emerson Murphy-Hill, Bill Chu, and Heather Richter Lipford. Questions developers ask while diagnosing potential security vulnerabilities with static analysis. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, page 248–259, New York, NY, USA, 2015. Association for Computing Machinery. doi:10.1145/2786805.2786812.
[38] Nikhil Patnaik, Andrew C Dwyer, Joseph Hallett, and Awais Rashid. Don’t forget your classics: Systematizing 45 years of ancestry for security api usability recommendations. arXiv preprint arXiv:2105.02031, 2021.
[47] Justin Smith, Brittany Johnson, Emerson Murphy-Hill, Bill Chu, and Heather Richter Lipford. How developers diagnose potential security vulnerabilities with a static analysis tool. IEEE Transactions on Software Engineering, 45(9):877–897, 2019. doi:10.1109/TSE.2018. 2810116.
[39] Nikhil Patnaik, Joseph Hallett, and Awais Rashid. Usability smells: An analysis of Developers’ struggle with crypto libraries. In Fifteenth Symposium on Usable Privacy and Security (SOUPS 2019), pages 245– 257, Santa Clara, CA, August 2019. USENIX Association. URL: https://www.usenix.org/conference/ soups2019/presentation/patnaik.
[48] Mohammad Tahaei, Kami Vaniea, Konstantin Beznosov, and Maria K Wolters. Security notifications in static analysis tools: Developers’ attitudes, comprehension, and ability to act on them. In Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems, pages 1–17, 2021.
[40] Stephan Plöger, Mischa Meier, and Matthew Smith. A qualitative usability evaluation of the clang static analyzer and libFuzzer with CS students and CTF players. In Seventeenth Symposium on Usable Privacy and Security (SOUPS 2021), pages 553–572. USENIX Association, August 2021. URL: https://www.usenix.org/ conference/soups2021/presentation/ploger.
[49] Maurice H ter Beek and Alessio Ferrari. Empirical formal methods: guidelines for performing empirical studies on formal methods. Software, 1(4), 2022. [50] Daniel Votipka, Kelsey R Fulton, James Parker, Matthew Hou, Michelle L Mazurek, and Michael Hicks. Understanding security mistakes developers make: Qualitative 17
A.2
analysis from build it, break it, fix it. In 29th USENIX Security Symposium (USENIX Security 20), pages 109– 126, 2020.
Block: Learnability
Q5. What resources did you rely on when learning the tool? (select all that apply) □ Official documentation and tool manual
[51] Jiashuo Zhang, Jiachi Chen, Zhiyuan Wan, Ting Chen, Jianbo Gao, and Zhong Chen. When contracts meets crypto: Exploring developers’ struggles with ethereum cryptographic apis. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, pages 1–13, 2024.
□ Research papers applying the tool to real protocols □ Video lectures or summer school recordings □ Publicly available models from other researchers (e.g., GitHub) □ Peer or supervisor guidance □ Other (please specify)
[52] Yunze Zhao, Wentao Guo, Harrison Goldstein, Daniel Votipka, Kelsey R Fulton, and Michelle L Mazurek. A qualitative analysis of fuzzer usability and challenges. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, pages 2504– 2518, 2025.
Q6. What was the steepest part of the learning curve? (select one) 1. Translating informal protocol descriptions into the tool’s modeling language 2. Understanding the underlying formal theory (e.g., applied picalculus, multiset rewriting) 3. Interpreting verification output and attack traces 4. Debugging non-termination and performance issues
A
Survey Instruments
5. Knowing what the proof actually guarantees in practice 6. Other (please specify)
This appendix presents the full text of the survey administered to participants with experience using cryptographic protocol verification tools (Tamarin Prover, ProVerif, and other). The survey was organized into five blocks: Demographic, Learnability, Modeling & Verification, Tamarin, and ProVerif. Unless otherwise noted, single-select items are marked (select one) and multi-select items are marked (select all that apply) or checkbox.
Q7. Which programming concepts from your prior experience helped you be more effective when learning or using this cryptographic verification tool? (select all that apply) □ Step-by-step algorithmic thinking □ Control flow (if/else, loops)
A.1
Block: Demographic
□ Debugging skills (tracing execution, logging, breakpoints) □ Error handling (exceptions, return codes, defensive checks)
Q1. Which of the following verification tools have you used? (select all that apply)
□ Higher-order functions
□ Tamarin
□ Immutability (avoiding unintended state changes)
□ ProVerif
□ Pattern matching / case analysis
□ DeepSec
□ Recursion (reasoning via repeated structure)
□ Other (please specify)
□ Other (please specify)
Q2. How long have you been using formal verification tools for security protocols?
Q8. Have you previously used any general-purpose model checker that helped you learn or use this cryptographic verification tool?
1. Less than 1 year 2. 1–3 years
□ SPIN
3. 4–6 years
□ NuSMV
4. More than 6 years
□ UPPAAL
Q3. What is your current role or background?
□ TLA+ (TLC)
1. Undergraduate student (studying relevant field)
□ PRISM
2. Graduate student (Master’s or PhD)
□ Maude
3. Academic researcher or faculty
□ Other (please specify)
4. Industry professional (practitioner using formal methods)
□ None
5. Other (please specify) Q4. How would you rate your expertise in formal methods / cryptographic protocol verification?
A.3
Block: Modeling & Verification
Q9. How confident are you that your formal model accurately reflects the real-world protocol you intend to verify?
1. Novice: new to formal verification (just learning or only basic knowledge) 2. Intermediate: comfortable with core concepts and have used verification tools on some projects
1. 1 – Not confident at all
3. Advanced: very proficient with formal verification; extensive experience using these tools
3. 3 – Moderately confident
2. 2 – Slightly confident 4. 4 – Confident
4. Deep expertise (e.g., you contribute to tool development or advanced research in this area)
5. 5 – Very confident
18
A.4
Q10. What most limits your confidence in the accuracy of your model? (select all that apply)
Block: Tamarin
Q14. Have you ever encountered a counterexample in Tamarin that you later determined to be a false positive? If so, how did you typically recover from or resolve it?
□ The symbolic model assumes perfect cryptography, which may not reflect actual weaknesses in real-world implementations
□ Refined or corrected the protocol model/specification
□ Difficulty modeling stateful or complex protocol behavior
□ Manually analyzed the counterexample to confirm it was not a real attack
□ Uncertainty about whether the Dolev–Yao attacker model is realistic enough
□ Consulted documentation, examples, or academic papers
□ Lack of a systematic methodology to validate the model against the real protocol
□ Asked for help from peers, supervisors, or online communities □ Adjusted assumptions about the adversary or environment
□ No way to cross-check the model against the actual implementation
□ Other (please specify)
□ Other (please specify)
Q15. When running larger/realistic case studies in Tamarin, what is your most common limiting factor(s)?
Q11. When a proof fails without a concrete attack trace, what is your typical approach? (select all that apply)
□ Memory (RAM) □ Time (runs too long / non-terminating)
□ Simplify the model to isolate which part is causing the failure
□ Manual effort (requires deep interactive tracing)
□ Add helper lemmas or auxiliary lemmas to guide the proof (e.g., in Tamarin)
□ Tool crashes / instability □ I don’t run large models
□ Re-examine modeling decisions and abstractions for potential unsoundness
□ Other (please specify)
□ Consult related published models or ask peers for guidance
Q16. How often do you need to write helper lemmas to guide Tamarin’s proof search toward termination?
□ Switch to a different tool to cross-validate the result
1. Never
□ Assume the model is flawed and rewrite it from scratch
2. Rarely
□ Increase computational resources or adjust tool parameters and re-run
3. Sometimes 4. Often
□ Other (please specify)
5. Almost always Q12. Which best describes the tool’s communication when verification is slow or non-terminating? (select all that apply)
Q17. How intuitive is the visualization of the dependency graph in Tamarin’s interactive mode?
□ The tool hangs silently with no output or progress indication
1. 1 – Very unintuitive: the graph is difficult to read and interpret
□ The tool shows generic progress output but nothing specific to my model
2. 2 – Unintuitive: requires significant experience to navigate 3. 3 – Moderate: readable with effort but could be clearer
□ The tool produces verbose low-level output that is hard to map back to my model
4. 4 – Intuitive: the graph is generally easy to read and navigate 5. 5 – Very intuitive: the graph clearly communicates the proof state
□ The tool indicates which rule or lemma is causing the bottleneck but offers no guidance
Q18. How difficult is it to model the following in Tamarin? Rate each on a scale from 1 (Very Difficult) to 5 (Very Easy).
□ The tool clearly communicates the source of the problem and how to address it
□ Stateful protocols
Q13. What best describes the most common shortcoming in the tool’s error messaging? (select all that apply)
□ Multi-session scenarios □ Forward secrecy
□ Error messages do not pinpoint the exact location of the problem in the model
□ Complex equational theories (e.g., Diffie–Hellman, XOR) □ Observational equivalence properties
□ Errors are too low-level and tied to internal tool mechanics rather than the model itself
Q19. What is the important usability improvement you would like to see in Tamarin Prover?
□ Semantic errors are silently ignored rather than explicitly reported
□ Modeling support
□ No suggestion or hint is provided on how to fix the issue
□ Error feedback
□ Error messages assume too much prior knowledge of the underlying formal theory
□ Counterexample explanation
□ No shortcoming in the tool’s error messaging
□ Tooling support
□ Other (please specify)
□ Other (please specify)
□ Documentation
19
A.5
Block: ProVerif
□ A graphical interface for model visualization and attack trace exploration
Q20. How adequate is ProVerif’s current support for observational equivalence (two protocol executions are indistinguishable to any attacker) in analyzing modern privacy-preserving protocols? Please explain your reasoning for your choice.
□ Automated suggestions for fixing common modeling mistakes □ Improved documentation with realistic, well-annotated protocol examples □ Integration with standard development tools (e.g., IDE plugins, CI/CD pipelines)
1. Fully adequate 2. Adequate with minor limitations
□ A model validation mechanism to check whether the formal model matches the intended protocol
3. Adequate but requires significant improvements 4. Insufficient for modern protocols
□ Other (please specify)
5. Not sure Q21. How adequate is ProVerif’s current support for reasoning about complex algebraic properties (e.g., Diffie–Hellman, XOR, group equations)? Please explain your reasoning for your choice.
B
1. Fully adequate for modern protocols 2. Adequate with careful modeling 3. Adequate but prone to false positives 4. Limited for algebra-heavy designs 5. Insufficient and requires redesign 6. Not sure Q22. Considering that ProVerif does not natively support mutable global state or ordered transitions, do you believe its current framework is fundamentally adequate for verifying stateful protocols (e.g., TPMs, IoT devices, e-passports)? Please explain your reasoning for your choice. 1. Fully adequate 2. Adequate with minor limitations 3. Adequate but requires significant improvements 4. Insufficient for complex stateful designs 5. Not sure Q23. In your opinion, how adequate is ProVerif’s support for verifying Perfect Forward Secrecy (compromise of long-term keys does not break past sessions)? Please explain your reasoning for your choice. 1. Fully adequate 2. Adequate with minor limitations 3. Adequate but requires significant improvements 4. Insufficient for modern protocols 5. Not sure Q24. Considering that post-compromise security requires reasoning about state evolution, key updates, and temporal ordering (e.g., compromise occurs, then secure recovery), do you believe ProVerif’s current Hornclause-based over-approximation is fundamentally adequate for this? Please explain your reasoning for your choice. 1. Fully adequate 2. Adequate with careful modeling 3. Adequate but limited for dynamic recovery 4. Insufficient for modern ratcheting protocols 5. Not sure Q25. Which features or improvements would most increase your productivity with ProVerif? □ An interactive debugging mode allowing step-by-step inspection of the proof state
20
Figures
Table 2: Participant ratings of ProVerif’s support for post-compromise security. Response
Representative concerns raised
Not sure (7)
—
Adequate with careful modeling (2)
• Models exist for protocols such as Signal, but require substantial manual effort • Reference to a recent Signal ProVerif model (S&P ’26)
Insufficient for modern ratcheting protocols (2)
• Current support described as inadequate • Hope that issues related to overfitting will be addressed in future updates, despite this being a challenging problem
Fully adequate (1)
—
Adequate but limited for dynamic recovery (1)
• Not straightforward to model
Table 3: Participant ratings of ProVerif’s support for verifying Perfect Forward Secrecy. Response
Representative concerns raised
Not sure (7)
—
Fully adequate (3)
—
Adequate with minor limitations (2)
• Care is needed in how “past” states are modeled • Increasing the number of sessions tested may improve confidence in results
Adequate but requires significant improvements (1)
• Requires tricks to model correctly
Table 4: Participant ratings of ProVerif’s support for state-dependent protocols. Response
Representative concerns raised
Insufficient for complex stateful designs (4)
• Modeling attempts required deviating significantly from the protocol specification just to get ProVerif to terminate • Particularly limiting for stateful devices such as TPMs and IoT devices • Tables can be used to emulate a notion of state, but this is unsatisfactory and likely does not scale to large protocols • Hope for future updates to natively support mutable global state and ordered transitions
Adequate but requires significant improvements (3)
• Workarounds can often be made to work, but require substantial manual effort • Reasoning about mutable state is inherently difficult • Extensions such as GSVerif can help address this gap
Adequate with minor limitations (2)
• Tables can handle state, though not always easily • Debugging stateful models is difficult
Fully adequate (2)
—
Not sure (2)
—
21
Table 5: Participant ratings of ProVerif’s support for reasoning about complex algebraic properties. Response
Representative concerns raised
Limited for algebra-heavy designs (4)
• Almost no support for Diffie–Hellman (DH)-type equations or theories using AC operators, which are common in practice • Does not support full DH reasoning the way Tamarin does
Not sure (3)
—
Adequate with careful modeling (3)
• Can handle Diffie–Hellman, but one must be careful about the equations written and account for properties like associativity and commutativity • Expected to be of comparable quality to Tamarin
Fully adequate for modern protocols (1)
—
Adequate but prone to false positives (1)
• Termination is not obvious
Insufficient and requires redesign (1)
• No support for AC symbols in ProVerif
Table 6: Participant ratings of ProVerif’s support for observational equivalence, with representative open-ended concerns for each category. Response
Representative concerns raised
Insufficient for modern protocols (4)
• Diff-equivalence is too coarse or too strong, limiting precision for properties like anonymity or unlinkability • Limited to reasoning about processes that differ only by certain terms • Gaps in applicability to IoT and post-quantum computing settings
Adequate but requires significant improvements (3)
• Diff-equivalence is an over-approximation that is sometimes hard to overcome • Termination issues • Need for more specific explanations of failure causes
Adequate with minor limitations (2)
• Desire to examine more than two executions (e.g., for robust declassification) • Sufficient, but usability requires deep prior knowledge of the tool
Fully adequate (2)
—
Not sure (2)
—
22
Table 7: Summary of requested usability, design, and functional improvements. Improvement Area
Tamarin Evidence
ProVerif Evidence
Main Implication
Error feedback and diagnostics
Error feedback: 8(67%) responses in Q19
Automated suggestions for modeling mistakes (3 responses); interactive debugging (8 responses)
Errors should identify the relevant model element, explain the cause, and recommend possible corrective actions.
Counterexample and result explanation
Counterexample explanation: 8(67%) responses; high-level AI synthesis requested in open-ended responses
Graphical attack-trace exploration (6 responses)
Verification outcomes should be explained at the protocol level and connected to assumptions and modeling decisions.
Modeling and validation support
Modeling support: 6(50%) responses
Model-validation mechanism (10 responses)
Tools should assist model construction and help users assess whether the formal model matches the intended protocol.
Interactive verification and debugging
Better interactive verification and proof-oracle support requested in open-ended responses
Interactive debugging mode (8 responses)
Users need step-by-step access to proof states, bottlenecks, unresolved branches, and attacker behavior.
Visualization
Improved interactive and counterexample support implied by responses
Graphical model and attack-trace interface (6 responses)
Visualizations should map internal proof structures to protocol roles, messages, states, and properties.
Documentation and examples
Documentation: 5(42%) responses
Improved documentation(5 responses)
Documentation should include realistic annotated models, modeling rationale, failure cases, and debugging workflows.
Proof automation and guidance
Better proof oracles and case-distinction support; AI synthesis requested by 2 respondents
Helper-lemma generation requested by 2 respondents
Tools could recommend helper lemmas, case distinctions, model simplifications, and proof strategies.
Tooling and workflow support
Tooling support: 5(42%) responses
IDE or CI/CD integration (3 responses)
Editor and workflow integration is useful, but currently less important than interpretability and validation.
Functional and expressive support
Greater support needed for stateful protocols and observational equivalence
Greater support needed for state, algebraic theories, observational equivalence, and state-evolving properties
Some usability barriers require improvements to the tools’ underlying verification and modeling capabilities.
23
ID P1 P2 P3
Role Academic Researcher or Faculty Graduate Academic Researcher or Faculty
Experience 1–3 yrs 1–3 yrs 4–6 yrs
Expertise Intermediate Deep Expertise Deep Expertise
P4
Academic Researcher or Faculty
> 6 yrs
Deep Expertise
P5
Academic Researcher or Faculty
4–6 yrs
Advanced
P6
Industry Professional
> 6 yrs
Advanced
P7
Academic Researcher or Faculty
> 6 yrs
Deep Expertise
P8
Academic Researcher or Faculty
> 6 yrs
Advanced
P9
Academic Researcher or Faculty
> 6 yrs
Advanced
P10
Graduate student
1–3 yrs
Intermediate
P11 P12 P13
Academic Researcher or Faculty Academic Researcher or Faculty Industry professional
1–3 yrs > 6 yrs > 6 yrs
Intermediate Deep Expertise Advanced
P14
Academic Researcher or Faculty
4–6 yrs
Advanced
P15 P16
Academic Researcher or Faculty Academic Researcher or Faculty
> 6 yrs > 6 yrs
Advanced Deep Expertise
Table 8: Demographic details of survey participants.
24
Tool(s) ProVerif ProVerif, Squirrel Tamarin Tamarin, ProVerif, CryptoVerif Tamarin, EasyCrypt, ProofFrog Isabelle/PSPSP, OFMC Tamarin, ProVerif, OFMC, AVISPA, AVANTSSAR, SPaCIoS Tamarin, ProVerif Tamarin, ProVerif, DeepSec Tamarin, ProVerif, AVISPA ProVerif Tamarin, ProVerif Tamarin, ProVerif Tamarin, ProVerif, DeepSec Tamarin, ProVerif Tamarin, ProVerif
Intro & Consent Description of the study and informed consent. Demographics Demographic & users' research background questions
Learnability Questions regarding how participants learned cryptographic verification and the challenges they faced during the process.
Modeling & verification workflow Questions about the usability of cryptographic verification tools during protocol modeling and verification.
Tamarin related usability Usability questions based on Tamarin verifier. Has proVerif experience
ProVerif related usability Usability questions based on ProVerif verifier. End of Survey Confirmation
No experience on Tamarin/ProVerif
Has tamarin experience
Figure 3: Overview of the survey flow and conditional toolspecific branches.
25