该论文针对密码学协议形式化验证工具的实际使用体验开展了一项以人为中心的探索性研究。作者指出，Tamarin、ProVerif 等协议验证工具已被广泛用于分析复杂协议的安全性，但用户如何与这些工具交互、在哪里受阻，长期以来缺乏系统性研究。为此，研究团队面向具备实操经验的用户群体（包括科研人员、研究生与工业界实践者）开展问卷调查，覆盖 Tamarin、ProVerif 及相关协议验证器的使用者。研究结果显示，可用性障碍贯穿整个验证工作流：首先是调试困难，尤其是证明过程不终止（non-termination）与性能退化问题时，用户难以定位原因；其次是缺乏系统化方法，用于验证形式化模型是否忠实反映真实协议，即模型与现实协议之间可能存在的语义偏差难以被发现。在证明失败且未给出具体攻击路径的情况下，用户普遍采取三类应对策略：简化模型、添加辅助引理（helper lemmas）、回溯并重新审视建模抽象层次。参与者还明确提出了若干改进诉求，包括可操作的诊断信息、对验证结果更清晰的解释、可视化支持，以及针对重复性证明任务的自动化能力。作者进一步归纳出一个核心洞察：持续的可用性挑战源自“协议层推理”与“验证器的形式化模型、证明过程、诊断输出”之间的鸿沟，即用户以协议语义思考，而工具以形式化演算和求解器状态回应。基于这些发现，论文提出了面向设计者的具体优先级，旨在提升密码学协议验证工具的可访问性、可解释性与易用性。该工作属于人机交互与形式化方法交叉方向的实证研究，适合协议设计者、形式化验证工具开发者、以及将验证工具引入安全工程流程的团队阅读。