Design And Analysis Of Security Protocols Based On SPALL Logic

Network has penetrated our life with the growth of network techniques. But it brings up some serious security as well as great benefit at the same time. Security protocols are communication protocols that use cryptographic transformations and whose primary purpose is to achieve security related goals. These goals typically include the authentication of the communicating parties and the establishment of a secret session key. Security protocol is one absolutely necessary components of the communication of networks and its applications, and it is the basis of composing information security systems. But proved by practice, the security protocol design has been recognized as much more difficult as initially thought and needs a formal approach to provide credible analysis guarantee.The purpose of this dissertation is to explore and research into standardized analysis and design methods of security protocols based on component. This research presents a modular-based method of security protocol design through composition. Firstly, it defines the concepts of the base case and the component in the protocol. Secondly, it analyzes the security attributes on the components, and designs the single-step protocols which can implement the special security goals based on the components. Finally, it defines composition rules allow the combination of several single-step protocols part into a complicated protocol without destroying the security properties established by each independent part. Then it can design security protocol by the context of specific applications based on the choice of the single-step protocols. In other words, the composition framework permits the specification of a complex protocol to be decomposed into the specifications of simpler single-step protocols which based on the components, and thus makes the design and verification of the protocol easier to handle. The main research work of this dissertation can be summarized as follows:(1) According to the components which in symmetric and asymmetric environment, we use Security Protocol Analysis Latent Logic (SPALL) to analyze the security attributes on those components, and design the single-step protocols which based on the components. We also define the composition rules to guarantee the single-step protocols can be combined. The rules can be proved logically. Then it can design security protocol by the choice and composition of the single-step protocols which in specific application environment. At last, we illustrate the two-party authentication and key establishment protocols which in symmetric and asymmetric environment to show how one uses this approach to design secure protocols.(2) This paper illustrates the secure payment protocol to show how one uses this approach to design complex protocols and expands the scope of application of the method. At the same time, this paper presents an identity-based authenticated key exchange protocol in the standard model. The protocol is good forward security and session key non-hosting. Through the explicit authentication, it improves the efficiency of the implementation of the protocol. Compared with the protocol in the random oracle model, the protocol has the same computational and communication efficiencies. We use the modal logic approach and the provable secure approach to analyze the security of the protocol, and then we compare the different ideas and processes of the two methods.(3) The modal logic approach and the provable secure approach are two different approaches in security protocols'formal analysis. Each approach has flaws and virtues. How to bridge the gap by drawing virtues from both approach and discarding their flaw is the new challenge. An idea is brought forward that is engaged in drawing virtues from both approaches and discarding their flaws to build a mature approach to analyze security protocols, through analyzing the two approaches. An eclectic analytic approach reconciling the two approaches is constructed following this idea. This new approach can provide a more complete formal analysis of security protocols.The research on the formal design methods of security protocols can improve security protocol design automation to meet the increasing application demand for security protocols. It nor only has important research value, but also has significant application potential to solve the difficult design problem of security protocols. The applicability and practicality of the proposed methodology are validated through many design examples of protocols found in many different environments and with various initial assumptions. The method is not aimed to cover all existent design issues, but a new method of protocol design is addressed.