Little can be achieved in the design of security protocols without trusting at least some participants. This trust should be justified or, at the very least, subject to examination. One way to strengthen trustworthiness is to hold parties accountable for their actions, as this provides a strong incentive to refrain from malicious behavior. This has led to an increased interest in accountability in the design of security protocols. In this work, we combine the accountability definition of K\"unnemann, Esiyok, and Backes, with the notion of case tests to extend its applicability to protocols with unbounded sets of participants. We propose a general construction of verdict functions and a set of verification conditions that achieve soundness and completeness. Expressing the verification conditions in terms of trace properties allows us to extend Tamarin -- a protocol verification tool -- with the ability to analyze and verify accountability properties in a highly automated way. In contrast to prior work, our approach is significantly more flexible and applicable to a wider range of protocols.

翻译：在不至少信任某些参与者的情况下,在设计安全协议方面几乎不可能取得什么成果。这种信任应该是合理的,或者至少要经过审查。加强信任的一个办法是要求各方对其行动负责,因为这提供了避免恶意行为的强烈激励。这导致对安全协议设计问责制的兴趣增加。在这项工作中,我们将K\"unmann, Esiyok, and Backes的问责定义与案例测试概念结合起来,将其适用范围扩大到无限制参与者组成的协议。我们建议对裁决功能进行总体构建,并制订一套核查条件,以实现可靠性和完整性。在追查财产方面表达核查条件,使我们能够扩展Tamarin -- -- 一个协议核查工具 -- -- 能够以高度自动化的方式分析和核查问责属性。与以前的工作相比,我们的方法非常灵活,适用于更广泛的协议。