论文标题
验证无限参与者集的问责制
Verifying Accountability for Unbounded Sets of Participants
论文作者
论文摘要
在不信任至少一些参与者的情况下，在设计安全协议的设计中几乎无法实现。该信任应该是合理的，或者至少应进行检查。增强可信赖性的一种方法是使各方对其行为负责，因为这提供了避免恶意行为的强烈动力。这导致对安全协议设计的责任感增加了兴趣。 在这项工作中，我们将Künnemann，Esiyok和Backes的责任定义与案例测试的概念相结合，以将其适用性扩展到具有无限参与者集的协议上。我们提出了判决功能的一般结构以及一组实现健全性和完整性的验证条件。 根据痕量属性表达验证条件使我们能够扩展tamarin（一种协议验证工具），能够以高度自动化的方式分析和验证问责属性。与先前的工作相反，我们的方法明显更灵活，并且适用于更广泛的协议。
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ünnemann, 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.
