本文提出了打结不变的命题投影时序逻辑,介绍了基于该逻辑的模型检测方法,并采用该方法验证了无条件安全通信协议。命题投影时序逻辑(PPTL)可表达所有ω-正则式其表达能力强于其他线性命题时序逻辑(如PTLL),此外作为性质描述语言,其中的projection和chop算子使得性质定义更为灵活,因此PPTL适用于有穷状态并发系统的描述和验证。基于PPTL的模型检测方法近年来被提出,然而其作为一种形式化验证方法同样要面临状态爆炸问题。为此,本文定义了PPTL的打结不变子逻辑(记作PPTLst),证明了PPTLst可表达所有PPTL可表达的打结不变性质。由于PPTLst定义的性质对系统中打结等价的行为不做区别,所以在偏序规约验证中,针对打结等价类只需验证其中的一个行为而不必验证等价类中的所有行为。因此支持PPTLst的偏序归约技术可避免遍历整个系统状态空间。基于该思想本文实现了支持基于PPTLst偏序规约的模型检测器。此外,PPTLst还可作为性质描述语言用于组合验证。其包含的projection和chop算子允许将性质定义在系统路径中受关注的状态上,并且由这些状态构成的抽象路径与原路径打结等价。因为PPTLst定义的性质不区分打结等价路径,所以该抽象操作对验证不构成影响。由此在自下而上的组合验证中,每层的模块可根据其性质先进行抽象再向上组合。经过逐层抽象,约减掉了与性质无关的状态,从而可缓解状态爆炸问题。除了以上技术外,性质公式的简化也可减少验证所需遍历的状态个数从而提高验证效率。为了找出影响PPTLst空间复杂度的因素,本文研究了PPTLst的空间复杂度上界。为此,定义了完全正则图(CNG),给出了PPTLst公式向CNG转换的算法。基于CNG证明了PPTLst空间复杂度上界属于非初等,从该证明可知PPTLst的空间复杂度由其‘chop(或projection)的非’嵌套的深度和原子命题个数两个因素决定。因此,验证中应尽可能选择chop(或projection)的非’-嵌套较低和原子命题个数较少的公式来描述性质,从达到简化性质公式的目的。本文将上述PPTLst模型检测技术用于验证Russian Cards协议以分析无条件通信的安全性。为此,首先扩展了原始Russian Cards(?)司题并根据该扩展方法提出了Russian Cards协议,给出了该协议的安全通信条件以及构造安全通信序列的算法。然后,利用PPTLst组合验证方法分析协议模型的安全性,在组合过程中,每个模块的验证又基于PPTLst偏序规约技术。实验表明PPTLst模型检测技术可缓解状态爆炸问题,并且支持大规模并发系统的验证。