针对无界参与者集合的可追责性验证

在设计安全协议时，若不信任至少部分参与者，则几乎无法取得任何成果。这种信任应当有正当理由，或至少应可被审查。增强可信性的一种方式是让各方对其行为负责，因为这能有力地抑制恶意行为。这促使安全协议设计中越来越关注可追责性。在本工作中，我们将 K"unnemann、Esiyok 和 Backes 的可追责性定义与案例测试概念相结合，将其适用范围扩展至具有无界参与者集合的协议。我们提出了一种判决函数的一般构造以及一组验证条件，以实现可靠性与完备性。将验证条件表示为迹属性，使我们能够扩展 Tamarin——一个协议验证工具——使其能够以高度自动化的方式分析和验证可追责性属性。与先前工作相比，我们的方法显著更具灵活性，且适用于更广泛的协议。