目前,大量的安全协议已经被设计出来,如何验证这些协议是否满足声称的安全性是协议设计与分析的一个重要研究领域。为了验证和分析协议的安全性,密码学家提出了不同的基于符号的形式化方法,如模态逻辑,模型检测逻辑,定理证明逻辑。然而大多数形式化方法都集中在协议的认证性和机密性的分析上,且这些方面的研究已经很成熟,而其他安全属性,如匿名性的形式化分析还处在起步阶段。为了进一步完善安全协议形式化分析理论和更好地分析协议的匿名属性,本文提出一种基于协议组合逻辑(PCL)的匿名性分析方法。通过将观察等价思想和PCL理论相结合,提出分析协议匿名性的形式化方法,并且将这种新的形式化方法应用到具体的网络协议中,通过实例分析说明了该方法的可行性和正确性。本文首先阐述了协议形式化分析研究的背景及意义,指出匿名性形式化分析的研究现状和目前存在的一些不足,介绍了安全协议、匿名性和形式化方法的基本概念,并归纳总结了三类常见的形式化方法,详细描述和分析了一种主要的形式化分析方法——PCL模型。其次,针对协议组合逻辑(PCL)缺乏匿名性分析能力的问题,提出一种新的匿名性形式化分析方法。考虑到协议交互过程中涉及到的信息,将PCL中的消息重新定义为三类：明文,密文和组合消息；结合观察者的分析能力,针对以上三类消息,定义了五条消息等价定理,并归纳了消息等价的语义；在消息等价的基础上,结合迹的概念,定义了迹等价语义；并在迹等价定义的基础上,定义了发送者匿名性、接收者匿名性和关系匿名性。最后,为了验证新方法在形式化分析协议匿名性方面的可行性和正确性,本文选用直接匿名认证协议(DAA)作为新方法的应用实例。使用新方法分别对DAA的两个子协议的匿名性进行形式化推理证明,分析结果表明,DAA协议满足匿名性,并验证了新方法的可行性和正确性。