安全协议是以密码学为基础的协议,它在因特网和分布式系统中提供各种各样的安全服务。近年来,利用形式化方法分析安全协议正在成为一个新的趋势。本文首先在分布式时序逻辑的基础上,给出了这个逻辑中局部公式的几组等价性定理并进行了证明,并和时序逻辑中的等价性公理进行了比较。然后用分布式时序逻辑描述了IEEE802.11i协议,给出了这个协议的事件结构模型,证明了三个主体之间的相互认证性。其次在分布式时序逻辑的基础上,增加了存在量词和全称量词,提出了分布式计算树时序逻辑。给出了分布式计算树时序逻辑的状态公式和路径公式的定义,以及这个逻辑的语义。同时也给出了分布式计算树时序逻辑中局部状态公式的几组等价性定理,并进行了证明。最后利用本文提出的分布式计算树时序逻辑描述了多方认证电子邮件协议,给出了这个协议的事件结构模型以及一些公平性公理。在有可信第三方参与和没有可信第三方参与的两种情况下,证明了发送者的不可否认性和接收者的不可否认性。