建立密码协议中基于等价性质的符号方法综述

密码协议旨在保护互联网等不安全网络上的通信安全，在这些网络中，不诚实的用户可能会窃听并干扰通信。安全通信的含义因底层应用而异，其范围从数据机密性到例如电子投票系统中的可验证性。隐私是安全概念的另一个例子。形式化符号模型已经证明了其在分析协议安全性方面的有效性。直到最近，大多数结果都集中在机密性或认证性等迹性质上。然而，存在若干种无法（或无法自然地）定义为迹性质的安全属性，它们需要行为等价的概念。典型的例子是匿名性和隐私相关属性。在过去十年中，已经发展出多种结果和验证工具来分析基于等价的安全属性。我们在此提出关于基于等价的安全属性的可判定性与不可判定性结果的综合论述。此外，我们概述了可用于验证基于等价安全属性的现有验证工具。