不可归因性与历史保存双isimilarity

日益增多的关键基础设施依赖于安全协议满足各种要求的假设。因此，重要性在于使用更擅长检测攻击的方法来认证，例如隐私属性。本文审视了“不可归因性”隐私属性，使用等价行为的关系来衡量攻击者无法区分的行为。从某些合理设计选择可能导致形式化工具漏洞的观察出发，我们引起对经典并发语义（accounting for past events 之间的关系）的关注，指出有些并发感知语义能够发现我们所考虑的所有协议上的攻击。更准确地说，我们关注那些已知使用分支时间等价性会遗漏一些使用分支时间等价性可观察到的攻击的协议。我们考虑三个维度：由程序员指定的不可归因性问题的设计决策（style）、尊重执行中选择的语义（分支时间）以及敏感于并发的语义（非交错）——我们发现，除非赋予攻击者足够的能力观察选择和并发，否则合理的 style 会遗漏攻击。我们的主要贡献是引起对如何应用时，一种流行的并发语义——历史保存双isimilarity（history-preserving bisimilarity）——可以发现我们所考虑的所有协议上的攻击，无论选择的 style 如何。此外，我们可以使用一种新颖的模态逻辑来描述所有此类攻击，因此该逻辑适用于正式认证隐私属性上的攻击。