密码学验证工具可用性理解

中文摘要 AI 辅助

密码学协议验证工具被广泛用于分析复杂协议的安全性，然而用户如何与这些工具交互的研究相对不足。我们针对Tamarin、ProVerif及相关协议验证器的经验用户开展了一项探索性的人本中心研究。我们的调查涵盖了具有Tamarin、ProVerif或相关工具实际操作经验的研究人员、研究生和从业者。研究结果揭示了验证工作流程中的可用性障碍，包括调试非终止和性能问题的困难，以及缺乏系统方法来验证形式化模型与真实协议的一致性。当证明在没有具体攻击的情况下失败时，用户通常会简化模型、添加辅助引理并重新审视建模抽象。参与者还呼吁提供可操作的诊断信息、更清晰的结果解释、可视化以及针对重复性证明任务的自动化。我们的研究结果表明，持续存在的可用性挑战源于协议级推理与验证器的形式化模型、证明过程和诊断输出之间的差距。我们据此得出了具体的设计优先级，以提升密码学协议验证工具的可访问性、可解释性和可用性。

英文摘要

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.

发表机构

• Samsung R&D Institute Bangladesh（三星孟加拉研发中心）
• Bangladesh University of Engineering and Technology（孟加拉国工程与技术大学）
• Towson University（陶森大学）
• The University of Texas at Dallas（德克萨斯大学达拉斯分校）

机构由 AI 辅助整理，请以论文原文为准。