Research On The Formal Analysis Technology To Security Protocols Based On Strand Space Model

Network has penetrated our life with the growth of network techniques. But it brings up some serious security problems as well as great benefit at the same time, and security of communication information of network has been paid much attention by researchers. Protocols are a foundation of communication, bearing the weight of all data and information communicating through network, and have been a communication bridge between principals. How to realize security from the level of protocols is a basic and important research topic. Security protocols are protocols that use cryptography to distribute keys and authenticate principals and data over a network and are a basic guarantee of secure communication through open and hostile network. But proved by practice, analysis of security protocol has been recognized much more difficult than initially thought and needs a rigorous formal approach to provide credible analysis guarantee.Formal methods produce models for security protocols by some formal languages of models and verify their correctness by specific assumptions and rules. Application of formal methods to analyze security protocols is an important research subject in cryptography. Cryptographers have provided many formal methods to verify correctness and detect weakness of security protocols.Among existing formal models of security protocols, strand space model is a popular framework, it embodies the developing trend of research and integrates many thoughts and techniques of different methods and has attracted more attention since its emergence. The model has a solid mathematical base and it is a theorem proving method. Security of protocol is a theorem in the model to be proved. The proof can be achieved by hand and its result is convincing. The theory is simple and concise, and it can provide illustrated diagram to help description and proof. Some flaws of protocols have been found using this formalism, and some automatic tools are developed under this model.Basic strand space model can only analyze security protocols using only concatenation and encryption operation, and the description of attacker is limited too, which restrict the analysis scope of security protocols. Much more operations have been used in protocols since the seventieth of the twentieth century, such as signature, hash etc. We extent and consummate the original model to describe and analyze more data structures and operations, including hash function, signature etc. The main contributions of this dissertation are as follows:· Introduce several typical formal analysis technologies of them, detailedly describe the definition, analysis principles and methods of Strand Spaces theory.· Study further on the semantics of the model. A strand space semantic description for logic is proposed to resolve the problem that BAN logic brings about some semantic confusion, and make some extensions to BAN logic, redefine the process of protocol analyzing.· Introduce two main development of strand space theory: ideals and authentication test.· Make some extensions to strand space theory and authentication test, including term algebra extension and penetrator model extension, introduces the description of more operations, including hash function and signature.The main innovations of this thesis are listed as follows:· Propose a strand space semantic description for BAN logic, and make some extensions to BAN logic.· Extend Strand Space Model, so it has the ability of analyze protocols which contain signature and hash function.