The Strand Spaces Theory And Its Application To The Analysis Of Security Protocols

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.