【摘要】目前,大量的安全协议已经被设计出来,如何验证这些协议是否满足声称的安全性是协议设计与分析的一个重要研究领域。为了验证和分析协议的安全性,密码学家提出了不同的基于符号的形式化方法,如模态逻辑,模型检测逻辑,定理证明逻辑。然而大多数形式化方法都集中在协议的认证性和机密性的分析上,且这些方面的研究已经很成熟,而其他安全属性,如匿名性的形式化分析还处在起步阶段。为了进一步完善安全协议形式化分析理论 […]