【作者】 龙士工；

【导师】 李祥；

【作者基本信息】 贵州大学 ， 计算机软件与理论， 2007， 博士

【摘要】 论文以串空间理论为基本架构，因为串空间理论结合了多种形式化方法的思想和技术，本身体现了协议形式化分析领域的发展方向，而且可以用定理证明的手动方法完成证明，得到可信的结果。该理论简洁易用，基于图论对协议进行描述，在协议证明中，可以使用图形提供辅助说明。在串空间理论中，攻击者具有的原子行为用定义的攻击者迹描述，它总结了攻击者丢弃消息、生成消息、连接消息，以及攻击者的密码运算能力。显然，随着攻击者攻击手段的不断翻新和密码学本身的发展，串空间理论需要扩展和完善。在论文中我们增加了攻击者的原子描述，增加了散列函数、签名验证和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)将协议变量引入到串空间模型中，形成了有变量参与运算并以协议串为基础的新的协议模型，我们称它为带变量的串空间模型。由于将变量的匹配操作、替换操作以及串的合成操作引入到模型中，从而丰富了模型的语义信息。将模态逻辑和串空间语义结合起来，给出了模态逻辑的串空间语义，并运用串空间模型的良好语义，证明了模态逻辑的推理规则是正确的。更多还原

【Abstract】 Strand space theory is regarded as as the basic framework in this paper, because strand spaces combines with a variety of methods and technologies, and it reflects developments of formal analysis of protocols in the field of direction. The complete manual methods can be used to prove the theorem proving to get credible results. The theory is user-friendly and graph-based description, and graphics can be used to provide background information. In the strand spaces, atomic behavior of the attackers is the definition of the attackers trace description. It summed up the attackers discarding information, generating information, linking information and cryptographical computational capabilities. Clearly, as a means of attack constantly renovation and development of cryptography, the strand spaces need to be expanded and improved. In the paper, we increase the atomic attack, including hash function, the signature certification and atomic behavior DH operation. We give an atomic attack on a password. And according to the different types of password guessing, a composed strand is constituted by the combination of atomic trace. Thus, the theory is extended in the scope of application of analysis of protocols.The transport protocol(TLS),Based on the Diffie-Hellman key exchange mechanism for the safety, provides data integrity and confidentiality for application procedures for the communication. Protocols is related to encryption, signature, verification, cryptographic operations of DH types, etc., the original strand space theory did not distinguish between signatures and encryption algorithm. It also lacks other original definition of the term. So in the original strand spaces the analysis of the TLS protocol is very inconvenient. In the extended strand spaces model, the definition of a signature, DH calculation and one-way operation type are added. Based on the extended theory, the TLS protocol is analyzed. The theorem is given, in which TLS Key secret and its Authentication is proved.Security protocols based passwords are classified by guessing attacks, including a simple guess, layered guess, internal guessing attacks and replayed guessing attacks. For each type of attack, the analytical framework is given in strand spaces. Four new password guessing attacks is added, and using the concept of combination, in which various traces are unified, models guessing attacks. GLNS protocol is analyzed using the extended theory, and the proved result is that the protocol can withstand guessing attack.During Expanding and improving the strand space theory, we found that in a distributed open networks many of the protocol items are unknown before. For example, the protocol initiators and recipients should be regarded as unknown before they are identified. Another example is when the participant receives the encrypted items, but no decrypted, the content should be regarded as unknown etc. We introduced variables into a protocol to form a new model As the model is still based on the protocol strand, we call it strand space model with variables. The traditional strand space adopts algebra method, and introduces the concept of two kinds of directed edges. so protocol process performs for a directed acyclic fig. Semantic is rich and clear, making accurate description of the protocol, so as to lay a good foundation for analysis of the protocol. But the traditional strand space cannot depict characterization of "P said just X" and "X is fresh,", and temporal logic is suitable for such an assertion. Therefore, we use the definition of the timing and modal logic language to prove and reason protocol properties. As the timing logic uses some judgment predication, expressing content of the protocol will be direct much. And the modal words of 0 and ? can express of one moment operator.The modal logic is combined with strand spaces, the strand spaces semantics for the modal logic is given, and the inference rules of modal logic are proved correct by use of the semantic. Helsinki protocol is analyzed as the case, The results show that the model can effectively express the security needs of the protocol. To avoid state space explosion, the multi-model of a security protocol is provided for a complex security needs, a complex protocol will be sub-divided into several protocols, which are proved about their correctness. Then, the cross-application rules can prove that the nature of the merger protocol is still hold if the environment is not changed. The authenticate Diffie-Hellman key exchange protocol is analyzed using the combining inference rules. A series of ideal and testing theories in strand space are expanded. The concept of ideal is the further deepening and expansion of the strand space model. The concept of ideal can restrain the attack ability, in which the binding is independent analysis of protocol. So, ideal can demonstrate ability of the attack universal conclusions. The original definition of the ideal concept only includes integrated computing and encryption on a closure, As the actual cryptographic operations goes far beyond this. For example, One-way hash operations, trapdoor one-way hash operations and guessing attacks are increased. Besides, signature operation and encryption operation are separated, signature and certification are increased in the model. Thus, the model semantic information is enriched. Since a new type of cryptographic operations is added, the original concept of the ideal is adjusted in this paper. Based on the extended model, a new theorem about honest ideal is proved. Strand space aims mainly analysis of identification, confidentiality and exclusivity. Analysis of e-commerce undeniable, fair and accountable using proof testing theory is a new research direction. Application about design and analysis of e-commerce protocol is researched in the paper. The general design method from the perspective of e-commerce security certification is provided.Using ideal model in strand spaces, a few representative security protocols is focused on being analyzed including the well-known Otway-Rees authentication protocol, the Kerberos authentication protocol widely used in the distributed network based on symmetric key cryptography. Ideal model is used for analysis of Otway-Rees authentication protocol, pointing out that the design flaws can be found supplementary by formal analysis of protocol. The Kerberos protocol is analyzed, and there is guessing attack defects. DH key exchange algorithm and public-key cryptosystem are introduced to Kerberos authentication protocol. The result is that the security of Kerberos is improved, and the risk of being guessing attack is avoided.A comprehensive series of analysis methods and advantages are explored by combining strand space and model checking. Major advantage is that the state can be automatically searched. But the state explosions can arise. Therefore, the state reduction techniques need to be researched. The original detection algorithm is further improved in this paper by increasing the binding rules of the state spaces, thereby the scale of the state automated search process can be effectively controlled. Meanwhile, we also made use of the finite state machine inference algorithm. Each step in a state of transformation, the honest agent can choose inference rules as a match in the main library; In addition to matching any one of inference rules, the attacker can also choose any action rules. According to the different paths, the final protocol security needs are verified. Overall, about research on strand space theory, the work is mainly in the following aspects:(1)The basic strand space theory is expanded and improved by adding one-way hash operations, trapdoor one-way hash operations, an increase of signatures and certification in the model. Thus, the model semantic information is enriched. The security protocol based passwords has conducted in-depth studies, and a password guessing atomic attack is presented. Also password guessing attacks in strand space model are classified. The combination of atomic constitute trace about password guessing is given. Thus, the scope of application of strand space is extended.(2)The ideal model is expanded, and the theorem of the honest ideal is proven.For the original concept of the ideal did not contain more cryptographic operations, the original concept of the ideal is redefined. E-commerce is different from the general protocol due to the special nature of the security protocol. Formal analysis of the e-commerce protocol using certification and test theory is a new study direction in this paper. Based on the idea of certification and test, and from the perspective of e-commerce security certification the general design and analysis methods is proposed.(3) we also proposed he new inference algorithm using finite state machine. The comprehensive analysis methods and advantages are explored in theory. The unreachable theory and backwards generated technique are used in the algorithm, state explosion is avoided in the process of a search for states’, the strand backwards generated requires fairly lower space resources. The analysis example shows the effect of the arithemetic is good.(4)Variables are introduced into strand space model forming a series of variables involved in operation, and a new model, which is called strand space with variables, is formed for foundation. As a series of operations, such as matching, replacement and synthetic operation, are introduced into the model, the model is rich semantic information. A modal logic is combined with strand spaces, the semantics for the modal logic is given. The inference rules of modal logic are proved correct by use of the good semantics of strand spaces.更多还原