Research On Logic-based Method For Formal Analysis Of Composed Security Protocols

In recent years, a number of successful formal methods and corresponding tools have been developed to analyze security protocols. These methods are generally limited to the verification of protocols that run in isolation, without considering the verification of composed protocols. However, many protocols that are in use today are composed of several sub-protocosls. The traditional formal methods can not satisfy the requirements for these protocols. So it is very necessary and important to propose a formal method for composed protocols.This dissertation studies the compositionality of security protocols. Aiming at the problems in composing protocols, a logic-based model for formal analysis of composed protocols is proposed, and the automatic verification of secrecy and authentication properties of composed protocols is realized. The main contributions of this dissertation are summarized as follows:1. The existing methods for formal analysis of composed protocols are studied, and the advantages and disadvantages of these methods are compared. Based on the characteristics of protocol interaction in multi-protocol environment, the compositional problems needed to be resolved in composing protocols are studied.2. The compositionality of security protocols is studied. Aiming at resolving the additive composition and nondestructive composition, a logic model for formal analysis of composed protocols is presented with its protocol specification, logic syntax, logic semantics and corresponding proof system. Based on the logic model, the formal definitions of secrecy and authentication properties for protocols that run in isolation are presented. On the basis of the order of protocol runs, the protocol composition is classified in two sorts, including parallel composition and sequential composition, and the corresponding composition theorems are proposed. Based on the composition theorems, the verification of composed protocols is translated into the verifications of sub-protocols, which reduces the complexity of the verification for composed protocols. This is the keystone and difficulty of the paper.3. After the research on the IKEv2, the protocol is manually analyzed under the proposed logic model. Firstly, the sub-protocols are analyzed respectively. Then, based on the composition theorems and the result of the verification for sub-protocols, the secrecy and authentication properties of protocols composed of any two of the three sub-protocols are verified. It is found that the protocol sequential composed by the IKEv2DS sub-protocol and CREATE_CHDLD_SA sub-protocol can satisfy the authentication property, which the IKEv2DS sub-protocol can not satisfy when runs in isolation. This part is also one of the difficulties of the paper.4. Based on the proposed logic model, the verification arithmetics for secrecy and authentication properties are designed, realized, and experimented on with the IKEv2 protocol. The result is consistent with the manual deduction.