论文以串空间理论为基本架构，因为串空间理论结合了多种形式化方法的思想和技术，本身体现了协议形式化分析领域的发展方向，而且可以用定理证明的手动方法完成证明，得到可信的结果。该理论简洁易用，基于图论对协议进行描述，在协议证明中，可以使用图形提供辅助说明。在串空间理论中，攻击者具有的原子行为用定义的攻击者迹描述，它总结了攻击者丢弃消息、生成消息、连接消息，以及攻击者的密码运算能力。显然，随着攻击者攻击手段的不断翻新和密码学本身的发展，串空间理论需要扩展和完善。在论文中我们增加了攻击者的原子描述，增加了散列函数、签名验证和DH操作的原子行为，给出了基于口令猜测的原子攻击。以及针对不同类型的口令猜测，给出了由原子行为构成的组合迹。这样就扩展了串空间理论分析安全协议的适用范围。基于Diffie-Hellman密钥交换机制的安全传输层协议(TLS)，为通信应用程序提供保密性和数据完整性。协议中涉及到加密、签名、验证以及DH运算等密码运算类型，原始的串空间理论没有把加密运算和签名运算区分开，同时还缺乏其它的密码原语的定义。因此用原始的串空间理论分析TLS协议很不方便。在扩展定义的串空间模型中，增加了签名、DH运算和单向计算的原语类型，并基于扩展的串空间理论对TLS协议进行了分析，给出的定理证明了TLS协议的密钥协商的秘密性和通信主体双方的可鉴别性。将安全协议的口令猜测攻击进行了分类，包括：简单的猜测攻击、分层猜测攻击、内部猜测攻击以及带重放的猜测攻击。针对每类猜测攻击给出了一个串空间理论分析框架。为串空间理论新增加了四种口令猜测的攻击原语，并利用组合迹概念对各类猜测攻击进行了统一建模。用扩展的串空间理论对GLNS协议进行了分析，证明了该协议能抵御猜测攻击。在扩展和完善串空间理论的研究中，我们发现在一个分布式的开放网络中，很多信息项在协议运行前都是未知的。例如协议发起者和接收者在鉴别确认之前，主体身份应该视为未知。又如当主体在接收到一个加密消息而在没有解密之前，加密内容应该视为未知等等。这样我们把协议变量引入到模型中形成了一个新的协议模型，由于这个模型仍然以协议串为基础，我们称它为带变量的串空间模型。传统的串空间采用代数方法，并引进了两种有向边的概念，从而使协议进程表示为一个无环的有向图。语义丰富而且清晰。使得协议描述精确，从而给分析协议打下了良好的基础。但是传统的串空间不能刻画“P刚刚说过X”，“X是新鲜的”这样的断言，而时序逻辑则适合刻画这样的断言。所以我们使用了时序和模态逻辑语言证明和推理协议性质。由于逻辑语言直接使用一些判断谓词，因而用于表达协议内容和目标时，则要直观得多。而上一时刻算子(?)和曾经算子◆可以表示出刚刚发生过这样的断言等。将模态逻辑和串空间模型结合起来，给出模态逻辑的串空间语义，并运用该语义证明了模态逻辑的推理规则是正确的。给出了Helsinki协议的分析案例，结果表明给出的分析模型可有效地表达协议的安全需求。为了避免出现状态空间爆炸问题，提出了安全协议的多层分析模型，在证明一个复杂的安全协议的安全需求时，将一个复杂协议分割成几个子协议，分别证明子协议的正确性。然后，应用交叉组合规则证明如果环境不变时，在子协议中成立的性质，在子协议合并后仍然存立。用统一的时序逻辑框架对认证Diffie-Hellman密钥交换协议进行了分析。论文针对理想理论和认证测试理论对串空间模型进行了扩展。理想的概念是对串空间模型的进一步深化和扩展，串空间使用理想的概念来约束攻击者的能力，该约束独立于所分析的协议，可以证明出关于攻击者能力的普适性结论。原来的理想概念只定义了关于联结运算和加密运算的一个闭包，由于实际的密码运算远不止这些，例如论文增加了单向散列运算和陷门单向散列运算和猜测攻击原语。另外，将加密运算和签名运算区分开来，增加了签名和验证类型，从而丰富了模型的语义信息。由于在模型中增加了新的密码运算的类型，因此论文对原来的理想概念进行了调整。基于论文的扩展模型，得到了新的关于理想的诚实性定理。串空间理论主要分析安全协议的可鉴别性、保密性以及唯一性。用认证测试理论分析电子商务协议的不可否认性、公平性、以及可追究性，是该理论的一个新的研究方向。利用串空间理想模型，重点分析了几个有代表性的安全协议，包括著名的具有双向认证功能的Otway-Rees认证协议，在分布式网络中广泛使用的基于对称密钥密码技术的Kerberos认证协议。利用理想模型对Otway-Rees认证协议分析指出，形式分析可以辅助发现协议的设计缺陷。对Kerberos协议分析指出，协议存在猜测攻击的缺陷，提出将DH密钥交换算法和公钥密码体制引入到Kerberos认证协议中。协议改进的结果提高了Kerberos论证协议的安全性，可以避免遭受口令攻击的危险。从理论上探讨了将模型检测与串空间结合在一起的综合分析方法和优势。主要优势是可以发挥模型检测的自动状态搜索的优势，但会出现状态空间爆炸问题，因此，需要研究状态约简技术。论文进一步完善了原来的模型检测算法，通过增加删减规则对状态空间进行约束，从而有效地控制自动搜索过程中的状态规模。同时，我们还提出了利用有限状态机进行推理的算法。在每一步状态转换中，诚实主体可选择执行规则库中任一匹配的规则；攻击者除了可选择执行任一匹配的推理规则外，还可选择执行任一攻击规则。最后根据产生的不同路径验证协议是否满足安全需求。总的来说，本文围绕串空间理论的研究，其工作主要有以下几个方面：1)对基本串空间理论进行了扩展和完善，加入了单向散列运算和陷门单向散列运算，增加了签名和验证类型，从而丰富了模型的语义信息。对基于口令的一类的安全协议进行了深入研究，给出了基于口令猜测的原子攻击。并对口令猜测攻击的各种类型在串空间模型中作了分类，给出了由口令猜测原子行为构成的组合迹。这样就扩展了串空间理论分析安全协议的适用范围。2)扩展了串空间的理想模型，并得到了新的关于理想的诚实性定理。针对原来的理想概念没有包含更多的密码原语，论文重新定义了原来的理想概念。电子商务协议因其特殊性而区别于一般的安全协议。用串空间的认证测试理论形式化分析电子商务协议的性质是本文研究的一个新的方向。基于认证测试的思想，本文从认证安全性的角度提出了电子商务协议的一般设计方法和分析方法。3)提出了一个新的有限状态自动验证算法，从理论上探讨了将模型检测与串空间结合在一起的综合分析方法和优势。算法利用不可达理论和逆向生成技术，避免了状态搜索过程中出现状态爆炸的可能；逆向生成的可达串，使得对空间资源的要求大大降低，用实例证明算法的实际效果良好。4)将协议变量引入到串空间模型中，形成了有变量参与运算并以协议串为基础的新的协议模型，我们称它为带变量的串空间模型。由于将变量的匹配操作、替换操作以及串的合成操作引入到模型中，从而丰富了模型的语义信息。将模态逻辑和串空间语义结合起来，给出了模态逻辑的串空间语义，并运用串空间模型的良好语义，证明了模态逻辑的推理规则是正确的。