Understanding the Usability of Cryptographic Verification Tools

• URL: http://arxiv.org/abs/2609.16323v1
• Date: Mon, 14 Sep 2026 20:40:52 GMT
• Title: Understanding the Usability of Cryptographic Verification Tools
• Abstract summary: We present an exploratory human-centered study of experienced users of Tamarin, ProVerif, and related protocol verifiers.<n>Our survey included researchers, graduate students, and practitioners with hands-on experience using Tamarin, ProVerif, or related tools.
• Score: 1.5604334108839177
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Cryptographic protocol verification tools are widely used to analyze the security of complex protocols, yet how users interact with these tools remains comparatively understudied. We present an exploratory human-centered study of experienced users of Tamarin, ProVerif, and related protocol verifiers. Our survey included researchers, graduate students, and practitioners with hands-on experience using Tamarin, ProVerif, or related tools. The findings reveal usability barriers across the verification workflow, including difficulties debugging non-termination and performance issues, and the lack of systematic methods for validating formal models against real protocols. When proofs fail without concrete attacks, users commonly simplify models, add helper lemmas, and revisit modeling abstractions. Participants also called for actionable diagnostics, clearer explanations of results, visualization, and automation for recurring proof tasks. Our findings suggest that persistent usability challenges arise from the gap between protocol-level reasoning and the verifier's formal model, proof procedures, and diagnostic output. We derive concrete design priorities for improving the accessibility, interpretability, and usability of cryptographic protocol verification tools.

Related papers

• AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
  "AI slop" is artifacts, hallucinated vulnerabilities, plausible but incorrect patches, and semantically repackaged bug reports.<n>This paper surveys the empirical evidence, identifies a unifying mechanism, and traces a path toward trustworthy triage.
  arXiv  Detail & Related papers  (2026-08-26T11:48:38Z)
• AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation [0.0]
  We present a novel language-first method for verification of trace properties using a domain-specific language for protocol implementations.<n>We target the Tamarin prover for verification, and we prove that verified universal trace properties translate back to the implementation.<n>We use our tool to implement and generate accurate models for a signed Diffie-Hellman protocol, and for the WireGuard VPN protocol.
  arXiv  Detail & Related papers  (2026-06-18T08:34:17Z)
• IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation [49.796717294455796]
  We present IMMACULATE, a practical auditing framework that detects economically motivated deviations.<n>IMMACULATE selectively audits a small fraction of requests using verifiable computation, achieving strong detection guarantees while amortizing cryptographic overhead.
  arXiv  Detail & Related papers  (2026-02-26T07:21:02Z)
• Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
  We present WebDetective, a benchmark of hint-free multi-hop questions paired with a controlled Wikipedia sandbox.<n>Our evaluation of 25 state-of-the-art models reveals systematic weaknesses across all architectures.<n>We develop an agentic workflow, EvidenceLoop, that explicitly targets the challenges our benchmark identifies.
  arXiv  Detail & Related papers  (2025-10-01T07:59:03Z)
• Scan-do Attitude: Towards Autonomous CT Protocol Management using a Large Language Model Agent [39.72587188702086]
  Large Language Model (LLM)-based agent framework is proposed to assist with the interpretation and execution of protocol configuration requests.<n>The agent combines in-context-learning, instruction-following, and structured toolcalling abilities to identify relevant protocol elements and apply accurate modifications.
  arXiv  Detail & Related papers  (2025-09-24T16:04:11Z)
• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, Large Language Models (LLMs), Kontrol, and Forge.<n>Our approach is designed to reliably detect defects and generate proofs.
  arXiv  Detail & Related papers  (2025-09-16T12:46:11Z)
• Evaluating Language Model Reasoning about Confidential Information [95.64687778185703]
  We study whether language models exhibit contextual robustness, or the capability to adhere to context-dependent safety specifications.<n>We develop a benchmark (PasswordEval) that measures whether language models can correctly determine when a user request is authorized.<n>We find that current open- and closed-source models struggle with this seemingly simple task, and that, perhaps surprisingly, reasoning capabilities do not generally improve performance.
  arXiv  Detail & Related papers  (2025-08-27T15:39:46Z)
• Deep Learning Models for Robust Facial Liveness Detection [56.08694048252482]
  This study introduces a robust solution through novel deep learning models addressing the deficiencies in contemporary anti-spoofing techniques.<n>By innovatively integrating texture analysis and reflective properties associated with genuine human traits, our models distinguish authentic presence from replicas with remarkable precision.
  arXiv  Detail & Related papers  (2025-08-12T17:19:20Z)
• Formal Verification of Permission Voucher [1.4732811715354452]
  The Permission Voucher Protocol is a system designed for secure and authenticated access control in distributed environments.<n>The analysis employs the Tamarin Prover, a state-of-the-art tool for symbolic verification, to evaluate key security properties.<n>Results confirm the protocol's robustness against common attacks such as message tampering, impersonation, and replay.
  arXiv  Detail & Related papers  (2024-12-18T14:11:50Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  Property-based testing is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC) We devise a test that can detect various flaws in a bit-level implementation of an MPC protocol.
  arXiv  Detail & Related papers  (2024-03-08T02:02:24Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  We introduce a novel Unsupervised Continual Anomaly Detection framework called UCAD. The framework equips the UAD with continual learning capability through contrastively-learned prompts. We conduct comprehensive experiments and set the benchmark on unsupervised continual anomaly detection and segmentation.
  arXiv  Detail & Related papers  (2024-01-02T03:37:11Z)
• Deepfake Detection: A Comprehensive Survey from the Reliability Perspective [20.873480187150804]
  The mushroomed Deepfake synthetic materials circulated on the internet have raised a profound social impact on politicians, celebrities, and individuals worldwide. We identify three reliability-oriented research challenges in the current Deepfake detection domain: transferability, interpretability, and robustness.
  arXiv  Detail & Related papers  (2022-11-20T06:31:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.